@@ -714,8 +714,9 @@ elab ist info emode opts fn tm
714 g <- goal
714 g <- goal
715 hs <- get_holes
715 hs <- get_holes
716 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
716 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
717+ then handleError (tcRecoverable emode)
717− then try (resolveTC' True False 10 g fn ist)
718+ (resolveTC' True False 10 g fn ist)
718− (movelast n)
719+ (movelast n)
719 else movelast n)
720 else movelast n)
720 (ivs' \\ ivs)
721 (ivs' \\ ivs)
721 -- HACK: If the name leaks into its type, it may leak out of
722 -- HACK: If the name leaks into its type, it may leak out of
@@ -886,7 +887,8 @@ elab ist info emode opts fn tm
886 env <- get_env
887 env <- get_env
887 hs <- get_holes
888 hs <- get_holes
888 if all (\n -> not (n `elem` hs)) (freeNames g)
889 if all (\n -> not (n `elem` hs)) (freeNames g)
890+ then handleError (tcRecoverable emode)
889− then try (resolveTC' False False 10 g fn ist)
891+ (resolveTC' False False 10 g fn ist)
890 (movelast n)
892 (movelast n)
891 else movelast n)
893 else movelast n)
892 (ivs' \\ ivs)
894 (ivs' \\ ivs)
@@ -1672,6 +1674,15 @@ solveAutos ist fn ambigok
1672 = do autos <- get_autos
1674 = do autos <- get_autos
1673 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
1675 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)
1677+-- Return true if the given error suggests a type class failure is
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
1675trivial' ist
1686trivial' ist
1676 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1687 = trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
1677trivialHoles' psn h ist
1688trivialHoles' psn h ist