@@ -608,7 +608,9 @@ recoverable f (Bind _ (Pi _) sc)
608recoverable (Bind _ (Pi _) sc) f
608recoverable (Bind _ (Pi _) sc) f
609 | (P (DCon _ _) _ _, _) <- unApply f = False
609 | (P (DCon _ _) _ _, _) <- unApply f = False
610 | (P (TCon _ _) _ _, _) <- unApply f = False
610 | (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
613errEnv = map (\(x, b) -> (x, binderTy b))
615errEnv = map (\(x, b) -> (x, binderTy b))