Check for consistency before improving.

We may want to do this more often, but it may have a performance penalty.

Anyway, we need this check here, because previously the code was assuming
that the goals are known to be consistent, and we are just wanting to
default them, which should never make them inconsistent, just more instantiated.

The current solution is a bit of a stop-gap, until we redo the defaulting
story, and separate it form improvement.

src/Cryptol/TypeCheck/Infer.hs

@@ -27,7 +27,7 @@ import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
                                           checkNewtype)
 import           Cryptol.TypeCheck.Instantiate
 import           Cryptol.TypeCheck.Depends
-import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@))
+import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),emptySubst)
 import           Cryptol.TypeCheck.Solver.InfNat(genLog)
 import           Cryptol.Utils.Ident
 import           Cryptol.Utils.Panic(panic)
@@ -687,7 +687,14 @@ generalize bs0 gs0 =
 
 
      solver <- getSolver
-     (as0,here1,defSu,ws) <- io $ improveByDefaultingWith solver maybeAmbig here0
+     (as0,here1,mb_defSu,ws) <- io $ improveByDefaultingWith solver maybeAmbig here0
+     defSu <- case mb_defSu of
+               Nothing -> do recordError $ UnsolvedGoals True here0
+                             return emptySubst
+               Just s  -> return s
+
+
+
      mapM_ recordWarning ws
      let here = map goal here1
 
@@ -791,7 +798,12 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
                                 $ AmbiguousType [ thing (P.bName b) ]
 
         solver <- getSolver
-        (_,_,defSu2,ws) <- io $ improveByDefaultingWith solver maybeAmbig later
+        (_,_,mb_defSu2,ws) <-
+            io $ improveByDefaultingWith solver maybeAmbig later
+        defSu2 <- case mb_defSu2 of
+                   Nothing -> do recordError $ UnsolvedGoals True later
+                                 return emptySubst
+                   Just s -> return s
         mapM_ recordWarning ws
         extendSubst defSu2
 

src/Cryptol/TypeCheck/Solve.hs

@@ -30,7 +30,7 @@ import           Cryptol.TypeCheck.Solver.Selector(tryHasGoal)
 import           Cryptol.TypeCheck.SimpType(tMax)
 
 
-import           Cryptol.TypeCheck.Solver.SMT(proveImp)
+import           Cryptol.TypeCheck.Solver.SMT(proveImp,checkUnsolvable)
 import           Cryptol.TypeCheck.Solver.Improve(improveProp,improveProps)
 import           Cryptol.TypeCheck.Solver.Numeric.Interval
 import qualified Cryptol.TypeCheck.Solver.Numeric.AST as Num
@@ -453,28 +453,41 @@ improveByDefaultingWith ::
   [Goal] ->   -- constraints
     IO  ( [TVar]    -- non-defaulted
         , [Goal]    -- new constraints
-        , Subst     -- improvements from defaulting
+        , Maybe Subst   -- Nothing: improve to False
+                        -- Just:    improvements from defaulting
         , [Warning] -- warnings about defaulting
         )
 -- XXX: Remove this
 -- improveByDefaultingWith s as gs = return (as,gs,emptySubst,[])
 improveByDefaultingWith s as gs =
-  case improveByDefaultingWithPure as gs of
-    (xs,gs',su,ws) ->
-      do (res,su1) <- simpGoals' s Map.empty gs'
-         case res of
-           Left err ->
-             panic "improveByDefaultingWith"
-                    [ "Defaulting resulted in unsolvable constraints."
-                    , show err ]
-           Right gs'' ->
-             do let su2 = su1 @@ su
-                    isDef x = x `Set.member` substBinds su2
-                return ( filter (not . isDef) xs
-                       , gs''
-                       , su2
-                       , ws
-                       )
+  do bad <- checkUnsolvable s gs
+     if bad
+       then return (as, gs, Nothing, [])
+       else tryImp
+
+  where
+  tryImp =
+    case improveByDefaultingWithPure as gs of
+      (xs,gs',su,ws) ->
+        do (res,su1) <- simpGoals' s Map.empty gs'
+           case res of
+             Left err ->
+               panic "improveByDefaultingWith"
+                    $ [ "Defaulting resulted in unsolvable constraints."
+                      , "Before:"
+                      ] ++ [ "  " ++ show (pp (goal g)) | g <- gs ] ++
+                      [ "After:"
+                      ] ++ [ "  " ++ show (pp (goal g)) | g <- gs' ] ++
+                      [ "Contradiction:" ] ++
+                      [ "  " ++ show (pp (goal g)) | g <- err ]
+             Right gs'' ->
+               do let su2 = su1 @@ su
+                      isDef x = x `Set.member` substBinds su2
+                  return ( filter (not . isDef) xs
+                         , gs''
+                         , Just su2
+                         , ws
+                         )
 
 
 improveByDefaultingWithPure :: [TVar] -> [Goal] ->