@@ -610,6 +610,10 @@ instance TermSize (TT Name) where
610 | n' == n = 1000000 -- recursive => really big
610 | n' == n = 1000000 -- recursive => really big
611 | otherwise = 1
611 | otherwise = 1
612 termsize n (V _) = 1
612 termsize n (V _) = 1
613+ -- for `Bind` terms, we can erroneously declare a term
614+ -- "recursive => really big" if the name of the bound
615+ -- variable is the same as the name we're using
616+ -- So generate a different name in that case.
613 termsize n (Bind n' (Let t v) sc)
617 termsize n (Bind n' (Let t v) sc)
614 = let rn = if n == n' then MN 0 "noname" else n in
618 = let rn = if n == n' then MN 0 "noname" else n in
615 termsize rn v + termsize rn sc
619 termsize rn v + termsize rn sc