Show some context on errors arising from unification failures.

CHANGES.md

@@ -6,6 +6,17 @@
   a merge sort instead of an insertion sort. This improves the both
   asymptotic and observed performance on sorting tasks.
 
+## UI Improvements
+
+* "Type mismatch" errors now show a context giving more information
+  about the location of the error.   The context is shown when the
+  part of the types match, but then some nested types do not.
+  For example, when mathching `{ a : [8], b : [8] }` with
+  `{ a : [8], b : [16] }` the error will be `8` does not match `16`
+  and the context will be `{ b : [ERROR] _ }` indicating that the
+  error is in the length of the sequence of field `b`.
+
+
 # 2.12.0
 
 ## Language changes

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -1075,6 +1075,7 @@ \subsection{Manipulating sequences}
     Type mismatch:
       Expected type: 10
       Inferred type: 12
+      Context: [ERROR] _
       When checking type of function argument
 \end{replPrompt}
 Cryptol is telling us that we have requested 10 elements in the final

src/Cryptol/TypeCheck/Error.hs

@@ -16,6 +16,7 @@ import Cryptol.TypeCheck.PP
 import Cryptol.TypeCheck.Type
 import Cryptol.TypeCheck.InferTypes
 import Cryptol.TypeCheck.Subst
+import Cryptol.TypeCheck.Unify(Path,isRootPath)
 import Cryptol.ModuleSystem.Name(Name)
 import Cryptol.Utils.Ident(Ident)
 import Cryptol.Utils.RecordMap
@@ -52,7 +53,7 @@ cleanupErrors = dropErrorsFromSameLoc
 
 -- | Should the first error suppress the next one.
 subsumes :: (Range,Error) -> (Range,Error) -> Bool
-subsumes (_,NotForAll _ x _) (_,NotForAll _ y _) = x == y
+subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y
 subsumes (r1,KindMismatch {}) (r2,err) =
   case err of
     KindMismatch {} -> r1 == r2
@@ -84,10 +85,10 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
               | RecursiveTypeDecls [Name]
                 -- ^ The type synonym declarations are recursive
 
-              | TypeMismatch TypeSource Type Type
+              | TypeMismatch TypeSource Path Type Type
                 -- ^ Expected type, inferred type
 
-              | RecursiveType TypeSource Type Type
+              | RecursiveType TypeSource Path Type Type
                 -- ^ Unification results in a recursive type
 
               | UnsolvedGoals [Goal]
@@ -105,11 +106,11 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
                 -- ^ Type wild cards are not allowed in this context
                 -- (e.g., definitions of type synonyms).
 
-              | TypeVariableEscaped TypeSource Type [TParam]
+              | TypeVariableEscaped TypeSource Path Type [TParam]
                 -- ^ Unification variable depends on quantified variables
                 -- that are not in scope.
 
-              | NotForAll TypeSource TVar Type
+              | NotForAll TypeSource Path TVar Type
                 -- ^ Quantified type variables (of kind *) need to
                 -- match the given type, so it does not work for all types.
 
@@ -222,15 +223,15 @@ instance TVars Error where
       TooManyTySynParams {}     -> err
       TooFewTyParams {}         -> err
       RecursiveTypeDecls {}     -> err
-      TypeMismatch src t1 t2    -> TypeMismatch src !$ (apSubst su t1) !$ (apSubst su t2)
-      RecursiveType src t1 t2   -> RecursiveType src !$ (apSubst su t1) !$ (apSubst su t2)
+      TypeMismatch src pa t1 t2 -> TypeMismatch src pa !$ (apSubst su t1) !$ (apSubst su t2)
+      RecursiveType src pa t1 t2   -> RecursiveType src pa !$ (apSubst su t1) !$ (apSubst su t2)
       UnsolvedGoals gs          -> UnsolvedGoals !$ apSubst su gs
       UnsolvableGoals gs        -> UnsolvableGoals !$ apSubst su gs
       UnsolvedDelayedCt g       -> UnsolvedDelayedCt !$ (apSubst su g)
       UnexpectedTypeWildCard    -> err
-      TypeVariableEscaped src t xs ->
-                                 TypeVariableEscaped src !$ (apSubst su t) .$ xs
-      NotForAll src x t         -> NotForAll src x !$ (apSubst su t)
+      TypeVariableEscaped src pa t xs ->
+                                 TypeVariableEscaped src pa !$ (apSubst su t) .$ xs
+      NotForAll src pa x t        -> NotForAll src pa x !$ (apSubst su t)
       TooManyPositionalTypeParams -> err
       CannotMixPositionalAndNamedTypeParams -> err
 
@@ -258,15 +259,15 @@ instance FVS Error where
       TooManyTySynParams {}     -> Set.empty
       TooFewTyParams {}         -> Set.empty
       RecursiveTypeDecls {}     -> Set.empty
-      TypeMismatch _ t1 t2      -> fvs (t1,t2)
-      RecursiveType _ t1 t2     -> fvs (t1,t2)
+      TypeMismatch _ _ t1 t2    -> fvs (t1,t2)
+      RecursiveType _ _ t1 t2   -> fvs (t1,t2)
       UnsolvedGoals gs          -> fvs gs
       UnsolvableGoals gs        -> fvs gs
       UnsolvedDelayedCt g       -> fvs g
       UnexpectedTypeWildCard    -> Set.empty
-      TypeVariableEscaped _ t xs-> fvs t `Set.union`
+      TypeVariableEscaped _ _ t xs-> fvs t `Set.union`
                                             Set.fromList (map TVBound xs)
-      NotForAll _ x t             -> Set.insert x (fvs t)
+      NotForAll _ _ x t             -> Set.insert x (fvs t)
       TooManyPositionalTypeParams -> Set.empty
       CannotMixPositionalAndNamedTypeParams -> Set.empty
       UndefinedTypeParameter {}             -> Set.empty
@@ -308,13 +309,13 @@ instance PP (WithNames Error) where
   ppPrec _ (WithNames err names) =
     case err of
 
-      RecursiveType src t1 t2 ->
+      RecursiveType src pa t1 t2 ->
         addTVarsDescsAfter names err $
         nested "Matching would result in an infinite type." $
-          vcat [ "The type: " <+> ppWithNames names t1
-               , "occurs in:" <+> ppWithNames names t2
-               , "When checking" <+> pp src
-               ]
+          vcat ( [ "The type: " <+> ppWithNames names t1
+                 , "occurs in:" <+> ppWithNames names t2
+                 ] ++ ppCtxt pa ++
+                 [ "When checking" <+> pp src ] )
 
       UnexpectedTypeWildCard ->
         addTVarsDescsAfter names err $
@@ -357,13 +358,14 @@ instance PP (WithNames Error) where
         nested "Recursive type declarations:"
                (commaSep $ map nm ts)
 
-      TypeMismatch src t1 t2 ->
+      TypeMismatch src pa t1 t2 ->
         addTVarsDescsAfter names err $
         nested "Type mismatch:" $
         vcat $
           [ "Expected type:" <+> ppWithNames names t1
           , "Inferred type:" <+> ppWithNames names t2
           ] ++ mismatchHint t1 t2
+            ++ ppCtxt pa
             ++ ["When checking" <+> pp src]
 
       UnsolvableGoals gs -> explainUnsolvable names gs
@@ -389,22 +391,24 @@ instance PP (WithNames Error) where
           nested "while validating user-specified signature" $
           ppWithNames names g
 
-      TypeVariableEscaped src t xs ->
+      TypeVariableEscaped src pa t xs ->
         addTVarsDescsAfter names err $
         nested ("The type" <+> ppWithNames names t <+>
                                         "is not sufficiently polymorphic.") $
-          vcat [ "It cannot depend on quantified variables:" <+>
-                     (commaSep (map (ppWithNames names) xs))
-               , "When checking" <+> pp src
-               ]
+          vcat ( [ "It cannot depend on quantified variables:" <+>
+                       (commaSep (map (ppWithNames names) xs))
+                 ] ++ ppCtxt pa
+                   ++ [ "When checking" <+> pp src ]
+               )
 
-      NotForAll src x t ->
+      NotForAll src pa x t ->
         addTVarsDescsAfter names err $
         nested "Inferred type is not sufficiently polymorphic." $
-          vcat [ "Quantified variable:" <+> ppWithNames names x
-               , "cannot match type:"   <+> ppWithNames names t
-               , "When checking" <+> pp src
-               ]
+          vcat ( [ "Quantified variable:" <+> ppWithNames names x
+                 , "cannot match type:"   <+> ppWithNames names t
+                 ] ++ ppCtxt pa
+                   ++ [ "When checking" <+> pp src ]
+               )
 
       BadParameterKind tp k ->
         addTVarsDescsAfter names err $
@@ -479,6 +483,9 @@ instance PP (WithNames Error) where
 
     noUni = Set.null (Set.filter isFreeTV (fvs err))
 
+    ppCtxt pa = if isRootPath pa then [] else [ "Context:" <+> pp pa ]
+
+
 
 
 explainUnsolvable :: NameMap -> [Goal] -> Doc

src/Cryptol/TypeCheck/Infer.hs

@@ -44,6 +44,7 @@ import           Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
                                         checkParameterConstraints)
 import           Cryptol.TypeCheck.Instantiate
 import           Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
+import           Cryptol.TypeCheck.Unify(rootPath)
 import           Cryptol.Utils.Ident
 import           Cryptol.Utils.Panic(panic)
 import           Cryptol.Utils.RecordMap
@@ -525,7 +526,7 @@ expectSeq tGoal@(WithSource ty src rng) =
 
     _ ->
       do tys@(a,b) <- genTys
-         recordErrorLoc rng (TypeMismatch src ty (tSeq a b))
+         recordErrorLoc rng (TypeMismatch src rootPath ty (tSeq a b))
          return tys
   where
   genTys =
@@ -551,7 +552,7 @@ expectTuple n tGoal@(WithSource ty src rng) =
 
     _ ->
       do tys <- genTys
-         recordErrorLoc rng (TypeMismatch src ty (tTuple tys))
+         recordErrorLoc rng (TypeMismatch src rootPath ty (tTuple tys))
          return tys
 
   where
@@ -581,7 +582,7 @@ expectRec fs tGoal@(WithSource ty src rng) =
          case ty of
            TVar TVFree{} -> do ps <- unify tGoal (TRec tys)
                                newGoals CtExactType ps
-           _ -> recordErrorLoc rng (TypeMismatch src ty (TRec tys))
+           _ -> recordErrorLoc rng (TypeMismatch src rootPath ty (TRec tys))
          return res
 
 
@@ -619,7 +620,7 @@ expectFun mbN n (WithSource ty0 src rng)  = go [] n ty0
                   do ps <- unify (WithSource ty src rng) (foldr tFun res args)
                      newGoals CtExactType  ps
                _ -> recordErrorLoc rng
-                        (TypeMismatch src ty (foldr tFun res args))
+                        (TypeMismatch src rootPath ty (foldr tFun res args))
              return (reverse tys ++ args, res)
 
     | otherwise =

src/Cryptol/TypeCheck/Kind.hs

@@ -302,7 +302,8 @@ checkTUser x ts k =
     do let ty = tpVar (mtpParam a)
        (ts1,k1) <- appTy ts (kindOf ty)
        case k of
-         Just ks | ks /= k1 -> kRecordError $ KindMismatch Nothing ks k1
+         Just ks
+           | ks /= k1 -> kRecordError (KindMismatch Nothing ks k1)
          _ -> return ()
 
        unless (null ts1) $

src/Cryptol/TypeCheck/Monad.hs

@@ -45,7 +45,8 @@ import qualified Cryptol.Parser.AST as P
 import           Cryptol.TypeCheck.AST
 import           Cryptol.TypeCheck.Subst
 import           Cryptol.TypeCheck.Interface(genIface)
-import           Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..))
+import           Cryptol.TypeCheck.Unify(doMGU, runResult, UnificationError(..)
+                                        , Path, rootPath)
 import           Cryptol.TypeCheck.InferTypes
 import           Cryptol.TypeCheck.Error( Warning(..),Error(..)
                                         , cleanupErrors, computeFreeVarNames
@@ -561,17 +562,17 @@ unify :: TypeWithSource -> Type -> InferM [Prop]
 unify (WithSource t1 src rng) t2 =
   do t1' <- applySubst t1
      t2' <- applySubst t2
-     let ((su1, ps), errs) = runResult (mgu t1' t2')
+     let ((su1, ps), errs) = runResult (doMGU t1' t2')
      extendSubst su1
-     let toError :: UnificationError -> Error
-         toError err =
+     let toError :: (Path,UnificationError) -> Error
+         toError (pa,err) =
            case err of
-             UniTypeLenMismatch _ _ -> TypeMismatch src t1' t2'
-             UniTypeMismatch s1 s2  -> TypeMismatch src s1 s2
+             UniTypeLenMismatch _ _ -> TypeMismatch src rootPath t1' t2'
+             UniTypeMismatch s1 s2  -> TypeMismatch src pa s1 s2
              UniKindMismatch k1 k2  -> KindMismatch (Just src) k1 k2
-             UniRecursive x t       -> RecursiveType src (TVar x) t
-             UniNonPolyDepends x vs -> TypeVariableEscaped src (TVar x) vs
-             UniNonPoly x t         -> NotForAll src x t
+             UniRecursive x t       -> RecursiveType src pa (TVar x) t
+             UniNonPolyDepends x vs -> TypeVariableEscaped src pa (TVar x) vs
+             UniNonPoly x t         -> NotForAll src pa x t
      case errs of
        [] -> return ps
        _  -> do mapM_ (recordErrorLoc rng . toError) errs