@@ -714,8 +714,9 @@ elab ist info emode opts fn tm
714714 g <- goal
715715 hs <- get_holes
716716 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
717− then try (resolveTC' True False 10 g fn ist)
718− (movelast n)
717+ then handleError (tcRecoverable emode)
718+ (resolveTC' True False 10 g fn ist)
719+ (movelast n)
719720 else movelast n)
720721 (ivs' \\ ivs)
721722 -- HACK: If the name leaks into its type, it may leak out of
@@ -886,7 +887,8 @@ elab ist info emode opts fn tm
886887 env <- get_env
887888 hs <- get_holes
888889 if all (\n -> not (n `elem` hs)) (freeNames g)
889− then try (resolveTC' False False 10 g fn ist)
890+ then handleError (tcRecoverable emode)
891+ (resolveTC' False False 10 g fn ist)
890892 (movelast n)
891893 else movelast n)
892894 (ivs' \\ ivs)
@@ -1672,6 +1674,15 @@ solveAutos ist fn ambigok
16721674 = do autos <- get_autos
16731675 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
16741676
1677+-- Return true if the given error suggests a type class failure is
1678+-- recoverable
1679+tcRecoverable :: ElabMode -> Err -> Bool
1680+tcRecoverable ERHS (CantResolve f g) = f
1681+tcRecoverable ETyDecl (CantResolve f g) = f
1682+tcRecoverable e (ElaboratingArg _ _ _ err) = tcRecoverable e err
1683+tcRecoverable e (At _ err) = tcRecoverable e err
1684+tcRecoverable _ _ = True
1685+
16751686trivial' ist
16761687 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
16771688trivialHoles' psn h ist