@@ -610,6 +610,10 @@ instance TermSize (TT Name) where
610610 | n' == n = 1000000 -- recursive => really big
611611 | otherwise = 1
612612 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.
613617 termsize n (Bind n' (Let t v) sc)
614618 = let rn = if n == n' then MN 0 "noname" else n in
615619 termsize rn v + termsize rn sc