From 5a885e9f5af6c6e53c59b3c8a9bb5cacdbf8c19f Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Mon, 10 Jul 2017 10:59:40 -0700
Subject: [PATCH] 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 | 18 ++++++++++---
 src/Cryptol/TypeCheck/Solve.hs | 49 +++++++++++++++++++++-------------
 2 files changed, 46 insertions(+), 21 deletions(-)

diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs
index ca029808..4db6ee81 100644
--- a/src/Cryptol/TypeCheck/Infer.hs
+++ b/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
 
diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs
index 78a89476..becc295f 100644
--- a/src/Cryptol/TypeCheck/Solve.hs
+++ b/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] ->