@@ -608,7 +608,9 @@ recoverable f (Bind _ (Pi _) sc)
608608recoverable (Bind _ (Pi _) sc) f
609609 | (P (DCon _ _) _ _, _) <- unApply f = False
610610 | (P (TCon _ _) _ _, _) <- unApply f = False
611−recoverable _ _ = True
611+recoverable (Bind _ (Lam _) sc) f = recoverable sc f
612+recoverable f (Bind _ (Lam _) sc) = recoverable f sc
613+recoverable x y = True
612614
613615errEnv = map (\(x, b) -> (x, binderTy b))
614616