From bf4ebf9cbb5cd1072a8d26bf5735f3305f03142d Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 23 Feb 2022 10:35:01 -0800 Subject: [PATCH 1/3] Show some context on errors arising from unification failures. --- src/Cryptol/TypeCheck/Error.hs | 67 ++++++------ src/Cryptol/TypeCheck/Infer.hs | 9 +- src/Cryptol/TypeCheck/Kind.hs | 3 +- src/Cryptol/TypeCheck/Monad.hs | 19 ++-- src/Cryptol/TypeCheck/Unify.hs | 166 ++++++++++++++++++++++------- tests/issues/issue084.icry.stdout | 1 + tests/issues/issue1324.cry | 8 ++ tests/issues/issue1324.icry | 1 + tests/issues/issue1324.icry.stdout | 10 ++ tests/issues/issue382.icry.stdout | 1 + 10 files changed, 202 insertions(+), 83 deletions(-) create mode 100644 tests/issues/issue1324.cry create mode 100644 tests/issues/issue1324.icry create mode 100644 tests/issues/issue1324.icry.stdout diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 14d6f3f7f..2a270f117 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/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 diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index f672a7a3c..04ad2a441 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/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 = diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index aac88e3e6..dffa147ad 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/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) $ diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 16d7e4a04..fda532216 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/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 diff --git a/src/Cryptol/TypeCheck/Unify.hs b/src/Cryptol/TypeCheck/Unify.hs index 915561b90..6ba446710 100644 --- a/src/Cryptol/TypeCheck/Unify.hs +++ b/src/Cryptol/TypeCheck/Unify.hs @@ -8,13 +8,20 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE PatternGuards, ViewPatterns #-} -{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveFunctor, DeriveGeneric, DeriveAnyClass #-} +{-# LANGUAGE BlockArguments, OverloadedStrings #-} module Cryptol.TypeCheck.Unify where +import Control.DeepSeq(NFData) +import GHC.Generics(Generic) + import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst import Cryptol.Utils.RecordMap +import Cryptol.Utils.Ident(Ident) +import Cryptol.ModuleSystem.Name(nameIdent) +import Cryptol.TypeCheck.PP import Control.Monad.Writer (Writer, writer, runWriter) import qualified Data.Set as Set @@ -25,9 +32,9 @@ import Prelude.Compat -- on bound variables. type MGU = (Subst,[Prop]) -type Result a = Writer [UnificationError] a +type Result a = Writer [(Path,UnificationError)] a -runResult :: Result a -> (a, [UnificationError]) +runResult :: Result a -> (a, [(Path,UnificationError)]) runResult = runWriter data UnificationError @@ -38,31 +45,56 @@ data UnificationError | UniNonPolyDepends TVar [TParam] | UniNonPoly TVar Type -uniError :: UnificationError -> Result MGU -uniError e = writer (emptyMGU, [e]) +uniError :: Path -> UnificationError -> Result MGU +uniError p e = writer (emptyMGU, [(p,e)]) + + +newtype Path = Path [PathElement] + deriving (Show,Generic,NFData) + +data PathElement = + TConArg TC Int + | TNewtypeArg Newtype Int + | TRecArg Ident + deriving (Show,Generic,NFData) + +rootPath :: Path +rootPath = Path [] + +isRootPath :: Path -> Bool +isRootPath (Path xs) = null xs + +extPath :: Path -> PathElement -> Path +extPath (Path xs) x = Path (x : xs) emptyMGU :: MGU emptyMGU = (emptySubst, []) -mgu :: Type -> Type -> Result MGU +doMGU :: Type -> Type -> Result MGU +doMGU t1 t2 = mgu rootPath t1 t2 + +mgu :: Path -> Type -> Type -> Result MGU -mgu (TUser c1 ts1 _) (TUser c2 ts2 _) +mgu _ (TUser c1 ts1 _) (TUser c2 ts2 _) | c1 == c2 && ts1 == ts2 = return emptyMGU -mgu (TVar x) t = bindVar x t -mgu t (TVar x) = bindVar x t +mgu p (TVar x) t = bindVar p x t +mgu p t (TVar x) = bindVar p x t -mgu (TUser _ _ t1) t2 = mgu t1 t2 -mgu t1 (TUser _ _ t2) = mgu t1 t2 +mgu p (TUser _ _ t1) t2 = mgu p t1 t2 +mgu p t1 (TUser _ _ t2) = mgu p t1 t2 -mgu (TCon (TC tc1) ts1) (TCon (TC tc2) ts2) - | tc1 == tc2 = mguMany ts1 ts2 +mgu p (TCon (TC tc1) ts1) (TCon (TC tc2) ts2) + | tc1 == tc2 = + let paths = [ extPath p (TConArg tc1 i) | i <- [ 0 .. ] ] + in mguMany p paths ts1 ts2 -mgu (TCon (TF f1) ts1) (TCon (TF f2) ts2) +mgu _ (TCon (TF f1) ts1) (TCon (TF f2) ts2) | f1 == f2 && ts1 == ts2 = return emptyMGU -mgu t1 t2 +-- XXX: here we loose the information about where the constarint came from +mgu _ t1 t2 | TCon (TF _) _ <- t1, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2]) | TCon (TF _) _ <- t2, isNum, k1 == k2 = return (emptySubst, [t1 =#= t2]) where @@ -71,58 +103,114 @@ mgu t1 t2 isNum = k1 == KNum -mgu (TRec fs1) (TRec fs2) - | fieldSet fs1 == fieldSet fs2 = mguMany (recordElements fs1) (recordElements fs2) +mgu p (TRec fs1) (TRec fs2) + | fieldSet fs1 == fieldSet fs2 = + let paths = [ extPath p (TRecArg i) | (i,_) <- canonicalFields fs1 ] + in mguMany p paths (recordElements fs1) (recordElements fs2) -mgu (TNewtype ntx xs) (TNewtype nty ys) - | ntx == nty = mguMany xs ys +mgu p (TNewtype ntx xs) (TNewtype nty ys) + | ntx == nty = + let paths = [ extPath p (TNewtypeArg ntx i) | i <- [ 0 .. ] ] + in mguMany p paths xs ys -mgu t1 t2 - | not (k1 == k2) = uniError $ UniKindMismatch k1 k2 - | otherwise = uniError $ UniTypeMismatch t1 t2 +mgu p t1 t2 + | not (k1 == k2) = uniError p $ UniKindMismatch k1 k2 + | otherwise = uniError p $ UniTypeMismatch t1 t2 where k1 = kindOf t1 k2 = kindOf t2 -mguMany :: [Type] -> [Type] -> Result MGU -mguMany [] [] = return emptyMGU -mguMany (t1 : ts1) (t2 : ts2) = - do (su1,ps1) <- mgu t1 t2 - (su2,ps2) <- mguMany (apSubst su1 ts1) (apSubst su1 ts2) +-- XXX: could pass the path to the lists themselvs +mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU +mguMany _ _ [] [] = return emptyMGU +mguMany p (p1:ps) (t1 : ts1) (t2 : ts2) = + do (su1,ps1) <- mgu p1 t1 t2 + (su2,ps2) <- mguMany p ps (apSubst su1 ts1) (apSubst su1 ts2) return (su2 @@ su1, ps1 ++ ps2) -mguMany t1 t2 = uniError $ UniTypeLenMismatch (length t1) (length t2) +mguMany p _ t1 t2 = uniError p $ UniTypeLenMismatch (length t1) (length t2) +-- XXX: I think by this point the types should have been kind checked, +-- so there should be no mismatches with the lengths... -bindVar :: TVar -> Type -> Result MGU +bindVar :: Path -> TVar -> Type -> Result MGU -bindVar x (tNoUser -> TVar y) +bindVar _ x (tNoUser -> TVar y) | x == y = return emptyMGU -bindVar v@(TVBound {}) (tNoUser -> TVar v1@(TVFree {})) = bindVar v1 (TVar v) +bindVar p v@(TVBound {}) + (tNoUser -> TVar v1@(TVFree {})) = bindVar p v1 (TVar v) -bindVar v@(TVBound {}) t +bindVar p v@(TVBound {}) t | k == kindOf t = if k == KNum then return (emptySubst, [TVar v =#= t]) - else uniError $ UniNonPoly v t - | otherwise = uniError $ UniKindMismatch k (kindOf t) + else uniError p $ UniNonPoly v t + | otherwise = uniError p $ UniKindMismatch k (kindOf t) where k = kindOf v -bindVar x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _)) +bindVar _ x@(TVFree _ xk xscope _) (tNoUser -> TVar y@(TVFree _ yk yscope _)) | xscope `Set.isProperSubsetOf` yscope, xk == yk = return (uncheckedSingleSubst y (TVar x), []) -- In this case, we can add the reverse binding y ~> x to the -- substitution, but the instantiation x ~> y would be forbidden -- because it would allow y to escape from its scope. -bindVar x t = +bindVar p x t = case singleSubst x t of Left SubstRecursive - | kindOf x == KType -> uniError $ UniRecursive x t + | kindOf x == KType -> uniError p $ UniRecursive x t | otherwise -> return (emptySubst, [TVar x =#= t]) Left (SubstEscaped tps) -> - uniError $ UniNonPolyDepends x tps + uniError p $ UniNonPolyDepends x tps Left (SubstKindMismatch k1 k2) -> - uniError $ UniKindMismatch k1 k2 + uniError p $ UniKindMismatch k1 k2 Right su -> return (su, []) + + +-------------------------------------------------------------------------------- + +ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc +ppPathEl el prec k = + case el of + TRecArg l -> braces (pp l <+> ":" <+> k 0 <.> comma <+> "…") + + TConArg tc n -> + case tc of + + TCSeq -> optParens (prec > 4) + if n == 0 then brackets (k 0) <+> "_" + else brackets "_" <+> (k 4) + + TCFun -> optParens (prec > 1) + if n == 0 then k 2 <+> "->" <+> "_" + else "_" <+> "->" <+> k 1 + + TCTuple i -> parens (commaSep (before ++ [k 0] ++ after)) + where before = replicate n "_" + after = replicate (i - n - 1) "_" + + _ -> justPrefix (kindArity (kindOf tc)) (pp tc) n + + TNewtypeArg nt n -> + justPrefix (length (ntParams nt)) (pp (nameIdent (ntName nt))) n + + where + justPrefix arity fun n = + optParens (prec > 3) (fun <+> hsep (before ++ [k 5] ++ after)) + where before = replicate n "_" + after = replicate (arity - n - 1) "_" + + kindArity ki = + case ki of + _ :-> k1 -> 1 + kindArity k1 + _ -> 0 + +instance PP Path where + ppPrec prec0 (Path ps0) = go (reverse ps0) prec0 + where + go ps prec = + case ps of + [] -> "ERROR" + p : more -> ppPathEl p prec (go more) + diff --git a/tests/issues/issue084.icry.stdout b/tests/issues/issue084.icry.stdout index 5cfd7eeae..a5d721baa 100644 --- a/tests/issues/issue084.icry.stdout +++ b/tests/issues/issue084.icry.stdout @@ -7,4 +7,5 @@ Showing a specific instance of polymorphic result: Type mismatch: Expected type: Integer Inferred type: [5] + Context: _ -> ERROR When checking function call diff --git a/tests/issues/issue1324.cry b/tests/issues/issue1324.cry new file mode 100644 index 000000000..93c17dd2f --- /dev/null +++ b/tests/issues/issue1324.cry @@ -0,0 +1,8 @@ +type T = { a: [8] } +type S = { a: [16] } + +f : T -> () +f _ = () + +g : S -> () +g = f diff --git a/tests/issues/issue1324.icry b/tests/issues/issue1324.icry new file mode 100644 index 000000000..de1be53fd --- /dev/null +++ b/tests/issues/issue1324.icry @@ -0,0 +1 @@ +:load issue1324.cry diff --git a/tests/issues/issue1324.icry.stdout b/tests/issues/issue1324.icry.stdout new file mode 100644 index 000000000..a80deb48e --- /dev/null +++ b/tests/issues/issue1324.icry.stdout @@ -0,0 +1,10 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main + +[error] at issue1324.cry:8:1--8:6: + Type mismatch: + Expected type: 16 + Inferred type: 8 + Context: {a : [ERROR] _, …} -> _ + When checking the type of 'Main::g' diff --git a/tests/issues/issue382.icry.stdout b/tests/issues/issue382.icry.stdout index a9497e3dd..3c962bc19 100644 --- a/tests/issues/issue382.icry.stdout +++ b/tests/issues/issue382.icry.stdout @@ -16,6 +16,7 @@ Loading module Cryptol Type mismatch: Expected type: 4 Inferred type: 5 + Context: [ERROR] _ When checking user annotation [error] at issue382.icry:4:1--4:14: From fcd5578ee64684121d098b66affb6c5751e864c1 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 23 Feb 2022 14:39:20 -0800 Subject: [PATCH 2/3] Fix documentation --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 7f17718bd..a85a3b7bc 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/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 From 03527f24641225b88e0de5c35a26312ba13ccc10 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 23 Feb 2022 14:39:28 -0800 Subject: [PATCH 3/3] Update CHANGES --- CHANGES.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index d27ab0ff4..2deae4528 100644 --- a/CHANGES.md +++ b/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