Unifier now returns a substitution even on unification failure.

For example, when type checking `[1..10]:[6][8]`, `mgu` would be called
on [10]?a and [6][8], and `mgu` would return the substitution `?a = [8]`
and the mismatch error `10 != 6`.

Fixes #525.

src/Cryptol/TypeCheck/Monad.hs

@@ -22,7 +22,7 @@ import           Cryptol.Parser.Position
 import qualified Cryptol.Parser.AST as P
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Subst
-import           Cryptol.TypeCheck.Unify(mgu, Result(..), UnificationError(..))
+import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
 import           Cryptol.TypeCheck.InferTypes
 import           Cryptol.TypeCheck.Error(Warning(..),Error(..),cleanupErrors)
 import           Cryptol.TypeCheck.PP (brackets, commaSep)
@@ -483,21 +483,21 @@ unify :: Type -> Type -> InferM [Prop]
 unify t1 t2 =
   do t1' <- applySubst t1
      t2' <- applySubst t2
-     case mgu t1' t2' of
-       OK (su1,ps) -> extendSubst su1 >> return ps
-       Error err   ->
-         do case err of
-              UniTypeLenMismatch _ _ -> recordError (TypeMismatch t1' t2')
-              UniTypeMismatch s1 s2 -> recordError (TypeMismatch s1 s2)
-              UniKindMismatch k1 k2 -> recordError (KindMismatch k1 k2)
-              UniRecursive x t -> recordError (RecursiveType (TVar x) t)
-              UniNonPolyDepends x vs -> recordError
-                                          (TypeVariableEscaped (TVar x) vs)
-              UniNonPoly x t -> recordError (NotForAll x t)
-            return []
-
-
-
+     let ((su1, ps), errs) = runResult (mgu t1' t2')
+     extendSubst su1
+     let toError :: UnificationError -> Error
+         toError err =
+           case err of
+             UniTypeLenMismatch _ _ -> TypeMismatch t1' t2'
+             UniTypeMismatch s1 s2  -> TypeMismatch s1 s2
+             UniKindMismatch k1 k2  -> KindMismatch k1 k2
+             UniRecursive x t       -> RecursiveType (TVar x) t
+             UniNonPolyDepends x vs -> TypeVariableEscaped (TVar x) vs
+             UniNonPoly x t         -> NotForAll x t
+     case errs of
+       [] -> return ps
+       _  -> do mapM_ (recordError . toError) errs
+                return []
 
 -- | Apply the accumulated substitution to something with free type variables.
 applySubst :: TVars t => t -> InferM t

src/Cryptol/TypeCheck/Unify.hs

@@ -13,8 +13,8 @@ module Cryptol.TypeCheck.Unify where
 
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Subst
-import Cryptol.Utils.Panic (panic)
 
+import Control.Monad.Writer (Writer, writer, runWriter)
 import Data.Ord(comparing)
 import Data.List(sortBy)
 import qualified Data.Set as Set
@@ -26,8 +26,10 @@ import Prelude.Compat
 -- on bound variables.
 type MGU = (Subst,[Prop])
 
-data Result a = OK a | Error UnificationError
-                deriving (Functor)
+type Result a = Writer [UnificationError] a
+
+runResult :: Result a -> (a, [UnificationError])
+runResult = runWriter
 
 data UnificationError
   = UniTypeMismatch Type Type
@@ -37,23 +39,8 @@ data UnificationError
   | UniNonPolyDepends TVar [TParam]
   | UniNonPoly TVar Type
 
-instance Applicative Result where
-  pure = OK
-
-  OK f     <*> OK x    = OK (f x)
-  OK _     <*> Error e = Error e
-  Error e  <*> _       = Error e
-
-instance Monad Result where
-  return a      = OK a
-
-  OK a >>= k    = k a
-  Error x >>= _ = Error x
-
-  fail x        = panic "Cryptol.TypeCheck.Unify.fail" [x]
-
-uniError :: UnificationError -> Result a
-uniError e = Error e
+uniError :: UnificationError -> Result MGU
+uniError e = writer (emptyMGU, [e])
 
 
 emptyMGU :: MGU