From 111904d453750ae2847b3e488dc0cc533df73123 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 12 Nov 2020 15:40:54 -0800 Subject: [PATCH 1/6] Eliminate `TCErrorMessage` as it was not contributing much. Tests are broken at this commit --- src/Cryptol/Eval/Type.hs | 4 +- src/Cryptol/TypeCheck/AST.hs | 1 - src/Cryptol/TypeCheck/Error.hs | 37 +++-- src/Cryptol/TypeCheck/Infer.hs | 2 +- src/Cryptol/TypeCheck/Monad.hs | 6 +- src/Cryptol/TypeCheck/SimpType.hs | 29 ++-- src/Cryptol/TypeCheck/SimpleSolver.hs | 6 +- src/Cryptol/TypeCheck/Solve.hs | 7 +- src/Cryptol/TypeCheck/Solver/Class.hs | 168 +++++++------------- src/Cryptol/TypeCheck/Solver/Numeric.hs | 53 +++--- src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs | 3 +- src/Cryptol/TypeCheck/Solver/SMT.hs | 3 - src/Cryptol/TypeCheck/Solver/Types.hs | 7 +- src/Cryptol/TypeCheck/TCon.hs | 15 +- src/Cryptol/TypeCheck/Type.hs | 31 ++-- src/Cryptol/TypeCheck/TypePat.hs | 6 +- 16 files changed, 151 insertions(+), 227 deletions(-) diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index 934bc7980..ec5b51e35 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -132,8 +132,8 @@ evalType env ty = _ -> evalPanic "evalType" ["not a value type", show ty] TCon (TF f) ts -> Left $ evalTF f (map num ts) TCon (PC p) _ -> evalPanic "evalType" ["invalid predicate symbol", show p] - TCon (TError _ x) _ -> evalPanic "evalType" - ["Lingering typer error", show (pp x)] + TCon (TError _) ts -> evalPanic "evalType" + $ "Lingering invalid type" : map (show . pp) ts where val = evalValType env num = evalNumType env diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index b197ae593..d6b016862 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -25,7 +25,6 @@ module Cryptol.TypeCheck.AST , Pragma(..) , Fixity(..) , PrimMap(..) - , TCErrorMessage(..) , module Cryptol.TypeCheck.Type ) where diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 094b24852..a86f8ba46 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -1,5 +1,6 @@ {-# Language FlexibleInstances, DeriveGeneric, DeriveAnyClass #-} {-# Language OverloadedStrings #-} +{-# Language Safe #-} module Cryptol.TypeCheck.Error where import qualified Data.IntMap as IntMap @@ -92,10 +93,13 @@ data Error = ErrorMsg Doc | RecursiveType TypeSource Type Type -- ^ Unification results in a recursive type - | UnsolvedGoals (Maybe TCErrorMessage) [Goal] - -- ^ A constraint that we could not solve - -- If we have `TCErrorMess` than the goal is impossible - -- for the given reason + | UnsolvedGoals [Goal] + -- ^ A constraint that we could not solve, usually because + -- there are some left-over variables that we could not infer. + + | UnsolvableGoals [Goal] + -- ^ A constraint that we could not solve and we know + -- it is impossible to do it. | UnsolvedDelayedCt DelayedCt -- ^ A constraint (with context) that we could not solve @@ -153,7 +157,11 @@ errorImportance err = RecursiveTypeDecls {} -> 9 - UnsolvedGoals _ g + UnsolvableGoals g + | any tHasErrors (map goal g) -> 0 + | otherwise -> 4 + + UnsolvedGoals g | any tHasErrors (map goal g) -> 0 | otherwise -> 4 @@ -193,7 +201,8 @@ instance TVars Error where 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) - UnsolvedGoals x gs -> UnsolvedGoals x !$ (apSubst su gs) + UnsolvedGoals gs -> UnsolvedGoals !$ apSubst su gs + UnsolvableGoals gs -> UnsolvableGoals !$ apSubst su gs UnsolvedDelayedCt g -> UnsolvedDelayedCt !$ (apSubst su g) UnexpectedTypeWildCard -> err TypeVariableEscaped src t xs -> @@ -219,7 +228,8 @@ instance FVS Error where RecursiveTypeDecls {} -> Set.empty TypeMismatch _ t1 t2 -> fvs (t1,t2) RecursiveType _ t1 t2 -> fvs (t1,t2) - UnsolvedGoals _ gs -> fvs gs + UnsolvedGoals gs -> fvs gs + UnsolvableGoals gs -> fvs gs UnsolvedDelayedCt g -> fvs g UnexpectedTypeWildCard -> Set.empty TypeVariableEscaped _ t xs-> fvs t `Set.union` @@ -318,17 +328,16 @@ instance PP (WithNames Error) where , "When checking" <+> pp src ] - UnsolvedGoals imp gs - | Just msg <- imp -> + UnsolvableGoals gs -> addTVarsDescsAfter names err $ nested "Unsolvable constraints:" $ - let reason = ["Reason:" <+> text (tcErrorMessage msg)] - unErr g = case tIsError (goal g) of - Just (_,p) -> g { goal = p } - Nothing -> g + let unErr g = case tIsError (goal g) of + Just p -> g { goal = p } + Nothing -> g in - bullets (map (ppWithNames names) (map unErr gs) ++ reason) + bullets (map (ppWithNames names) (map unErr gs)) + UnsolvedGoals gs | noUni -> addTVarsDescsAfter names err $ nested "Unsolved constraints:" $ diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 80475e07a..5f8b5416e 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -589,7 +589,7 @@ checkP p tGoal@(WithSource _ src) = do (x, t) <- inferP p ps <- unify tGoal (thing t) let rng = fromMaybe emptyRange (getLoc p) - let mkErr = recordError . UnsolvedGoals Nothing . (:[]) + let mkErr = recordError . UnsolvedGoals . (:[]) . Goal (CtPattern src) rng mapM_ mkErr ps return (Located (srcRange t) x) diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index e0530b285..395c82ca7 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -150,7 +150,7 @@ runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver -> (cts,has) -> return $ InferFailed warns $ cleanupErrors [ ( goalRange g - , UnsolvedGoals Nothing [apSubst theSu g] + , UnsolvedGoals [apSubst theSu g] ) | g <- fromGoals cts ++ map hasGoal has ] errs -> return $ InferFailed warns @@ -390,8 +390,8 @@ collectGoals m = simpGoal :: Goal -> InferM [Goal] simpGoal g = case Simple.simplify mempty (goal g) of - p | Just (e,t) <- tIsError p -> - do recordError $ UnsolvedGoals (Just e) [g { goal = t }] + p | Just t <- tIsError p -> + do recordError $ UnsolvableGoals [g { goal = t }] return [] | ps <- pSplitAnd p -> return [ g { goal = pr } | pr <- ps ] diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs index b4fa970bd..dc5531d21 100644 --- a/src/Cryptol/TypeCheck/SimpType.hs +++ b/src/Cryptol/TypeCheck/SimpType.hs @@ -108,7 +108,7 @@ tAdd x y tSub :: Type -> Type -> Type tSub x y | Just t <- tOp TCSub (op2 nSub) [x,y] = t - | tIsInf y = tError (tf2 TCSub x y) "cannot subtract `inf`." + | tIsInf y = tError (tf2 TCSub x y) | Just 0 <- yNum = x | Just k <- yNum , TCon (TF TCAdd) [a,b] <- tNoUser x @@ -165,34 +165,34 @@ tMul x y tDiv :: Type -> Type -> Type tDiv x y | Just t <- tOp TCDiv (op2 nDiv) [x,y] = t - | tIsInf x = bad "Cannot divide `inf`" - | Just 0 <- tIsNum y = bad "Cannot divide by 0" + | tIsInf x = bad + | Just 0 <- tIsNum y = bad | otherwise = tf2 TCDiv x y where bad = tError (tf2 TCDiv x y) tMod :: Type -> Type -> Type tMod x y | Just t <- tOp TCMod (op2 nMod) [x,y] = t - | tIsInf x = bad "Cannot compute remainder of `inf`" - | Just 0 <- tIsNum y = bad "Cannot divide modulo 0" + | tIsInf x = bad + | Just 0 <- tIsNum y = bad | otherwise = tf2 TCMod x y where bad = tError (tf2 TCMod x y) tCeilDiv :: Type -> Type -> Type tCeilDiv x y | Just t <- tOp TCCeilDiv (op2 nCeilDiv) [x,y] = t - | tIsInf x = bad "CeilDiv of `inf`" - | tIsInf y = bad "CeilDiv by `inf`" - | Just 0 <- tIsNum y = bad "CeilDiv by 0" + | tIsInf x = bad + | tIsInf y = bad + | Just 0 <- tIsNum y = bad | otherwise = tf2 TCCeilDiv x y where bad = tError (tf2 TCCeilDiv x y) tCeilMod :: Type -> Type -> Type tCeilMod x y | Just t <- tOp TCCeilMod (op2 nCeilMod) [x,y] = t - | tIsInf x = bad "CeilMod of `inf`" - | tIsInf y = bad "CeilMod by `inf`" - | Just 0 <- tIsNum x = bad "CeilMod to size 0" + | tIsInf x = bad + | tIsInf y = bad + | Just 0 <- tIsNum x = bad | otherwise = tf2 TCCeilMod x y where bad = tError (tf2 TCCeilMod x y) @@ -304,12 +304,15 @@ op3 :: (a -> a -> a -> b) -> [a] -> b op3 f ~[x,y,z] = f x y z -- | Common checks: check for error, or simple full evaluation. +-- We assume that input kinds and the result kind are the same (i.e., Nat) tOp :: TFun -> ([Nat'] -> Maybe Nat') -> [Type] -> Maybe Type tOp tf f ts - | Just (TCErrorMessage e,t) <- msum (map tIsError ts) = Just (tError t e) + | Just t <- msum (map tIsError ts) = Just (tError t) + -- assumes result kind the same as input kind + | Just xs <- mapM tIsNat' ts = Just $ case f xs of - Nothing -> tError (TCon (TF tf) (map tNat' xs)) "invalid type" + Nothing -> tError (TCon (TF tf) (map tNat' xs)) Just n -> tNat' n | otherwise = Nothing diff --git a/src/Cryptol/TypeCheck/SimpleSolver.hs b/src/Cryptol/TypeCheck/SimpleSolver.hs index 2023da3cf..5c7cba1e4 100644 --- a/src/Cryptol/TypeCheck/SimpleSolver.hs +++ b/src/Cryptol/TypeCheck/SimpleSolver.hs @@ -21,8 +21,10 @@ import Cryptol.TypeCheck.PP simplify :: Ctxt -> Prop -> Prop simplify ctxt p = case simplifyStep ctxt p of - Unsolvable (TCErrorMessage e) -> tError p e - Unsolved -> dbg msg p + Unsolvable -> case tIsError p of + Nothing -> tError p + _ -> p + Unsolved -> dbg msg p where msg = text "unsolved:" <+> pp p SolvedIf ps -> dbg msg $ pAnd (map (simplify ctxt) ps) where msg = case ps of diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index 176d86b31..b0bc432dc 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -94,7 +94,7 @@ quickSolver ctxt gs0 = go emptySubst [] gs0 go su unsolved (g : gs) = case Simplify.simplifyStep ctxt (goal g) of - Unsolvable e -> Left (UnsolvedGoals (Just e) [g]) + Unsolvable -> Left (UnsolvableGoals [g]) Unsolved -> go su (g : unsolved) gs SolvedIf subs -> let cvt x = g { goal = x } @@ -104,10 +104,7 @@ quickSolver ctxt gs0 = go emptySubst [] gs0 findImprovement inc [] = do let bad = Map.intersectionWith (,) (integralTVars inc) (fracTVars inc) case Map.minView bad of - Just ((g1,g2),_) -> - pure $ Left $ - UnsolvedGoals (Just (TCErrorMessage "Mutually exclusive goals")) - [g1,g2] + Just ((g1,g2),_) -> pure $ Left $ UnsolvableGoals [g1,g2] Nothing -> mzero findImprovement inc (g : gs) = diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs index e359afc30..87bd879eb 100644 --- a/src/Cryptol/TypeCheck/Solver/Class.hs +++ b/src/Cryptol/TypeCheck/Solver/Class.hs @@ -8,7 +8,7 @@ -- -- Solving class constraints. -{-# LANGUAGE PatternGuards, OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} module Cryptol.TypeCheck.Solver.Class ( solveZeroInst , solveLogicInst @@ -29,7 +29,6 @@ import qualified LibBF as FP import Cryptol.TypeCheck.Type import Cryptol.TypeCheck.SimpType (tAdd,tWidth) import Cryptol.TypeCheck.Solver.Types -import Cryptol.TypeCheck.PP import Cryptol.Utils.RecordMap {- | This places constraints on the floating point numbers that @@ -69,7 +68,7 @@ solveZeroInst :: Type -> Solved solveZeroInst ty = case tNoUser ty of -- Zero Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Zero Bit TCon (TC TCBit) [] -> SolvedIf [] @@ -107,30 +106,22 @@ solveLogicInst :: Type -> Solved solveLogicInst ty = case tNoUser ty of -- Logic Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Logic Bit TCon (TC TCBit) [] -> SolvedIf [] -- Logic Integer fails - TCon (TC TCInteger) [] -> - Unsolvable $ - TCErrorMessage "Type 'Integer' does not support logical operations." + TCon (TC TCInteger) [] -> Unsolvable -- Logic (Z n) fails - TCon (TC TCIntMod) [_] -> - Unsolvable $ - TCErrorMessage "Type 'Z' does not support logical operations." + TCon (TC TCIntMod) [_] -> Unsolvable -- Logic Rational fails - TCon (TC TCRational) [] -> - Unsolvable $ - TCErrorMessage "Type 'Rational' does not support logical operations." + TCon (TC TCRational) [] -> Unsolvable -- Logic (Float e p) fails - TCon (TC TCFloat) [_, _] -> - Unsolvable $ - TCErrorMessage "Type 'Float' does not support logical operations." + TCon (TC TCFloat) [_, _] -> Unsolvable -- Logic a => Logic [n]a TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ] @@ -146,12 +137,13 @@ solveLogicInst ty = case tNoUser ty of _ -> Unsolved + -- | Solve a Ring constraint by instance, if possible. solveRingInst :: Type -> Solved solveRingInst ty = case tNoUser ty of -- Ring Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Ring [n]e TCon (TC TCSeq) [n, e] -> solveRingSeq n e @@ -163,8 +155,7 @@ solveRingInst ty = case tNoUser ty of TCon (TC (TCTuple _)) es -> SolvedIf [ pRing e | e <- es ] -- Ring Bit fails - TCon (TC TCBit) [] -> - Unsolvable $ TCErrorMessage "Type 'Bit' does not support ring operations." + TCon (TC TCBit) [] -> Unsolvable -- Ring Integer TCon (TC TCInteger) [] -> SolvedIf [] @@ -209,11 +200,10 @@ solveIntegralInst :: Type -> Solved solveIntegralInst ty = case tNoUser ty of -- Integral Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Integral Bit fails - TCon (TC TCBit) [] -> - Unsolvable $ TCErrorMessage "Type 'Bit' is not an integral type." + TCon (TC TCBit) [] -> Unsolvable -- Integral Integer TCon (TC TCInteger) [] -> SolvedIf [] @@ -223,13 +213,11 @@ solveIntegralInst ty = case tNoUser ty of case tNoUser elTy of TCon (TC TCBit) [] -> SolvedIf [ pFin n ] TVar _ -> Unsolved - _ -> Unsolvable $ TCErrorMessage $ show - $ "Type" <+> quotes (pp ty) <+> "is not an integral type." + _ -> Unsolvable TVar _ -> Unsolved - _ -> Unsolvable $ TCErrorMessage $ show - $ "Type" <+> quotes (pp ty) <+> "is not an integral type." + _ -> Unsolvable -- | Solve a Field constraint by instance, if possible. @@ -237,17 +225,13 @@ solveFieldInst :: Type -> Solved solveFieldInst ty = case tNoUser ty of -- Field Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Field Bit fails - TCon (TC TCBit) [] -> - Unsolvable $ - TCErrorMessage "Type 'Bit' does not support field operations." + TCon (TC TCBit) [] -> Unsolvable -- Field Integer fails - TCon (TC TCInteger) [] -> - Unsolvable $ - TCErrorMessage "Type 'Integer' does not support field operations." + TCon (TC TCInteger) [] -> Unsolvable -- Field Rational TCon (TC TCRational) [] -> SolvedIf [] @@ -261,24 +245,16 @@ solveFieldInst ty = case tNoUser ty of TCon (TC TCIntMod) [n] -> SolvedIf [ pPrime n ] -- Field ([n]a) fails - TCon (TC TCSeq) [_, _] -> - Unsolvable $ - TCErrorMessage "Sequence types do not support field operations." + TCon (TC TCSeq) [_, _] -> Unsolvable -- Field (a -> b) fails - TCon (TC TCFun) [_, _] -> - Unsolvable $ - TCErrorMessage "Function types do not support field operations." + TCon (TC TCFun) [_, _] -> Unsolvable -- Field (a, b, ...) fails - TCon (TC (TCTuple _)) _ -> - Unsolvable $ - TCErrorMessage "Tuple types do not support field operations." + TCon (TC (TCTuple _)) _ -> Unsolvable -- Field {x : a, y : b, ...} fails - TRec _ -> - Unsolvable $ - TCErrorMessage "Record types do not support field operations." + TRec _ -> Unsolvable _ -> Unsolved @@ -288,22 +264,16 @@ solveRoundInst :: Type -> Solved solveRoundInst ty = case tNoUser ty of -- Round Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Round Bit fails - TCon (TC TCBit) [] -> - Unsolvable $ - TCErrorMessage "Type 'Bit' does not support rounding operations." + TCon (TC TCBit) [] -> Unsolvable -- Round Integer fails - TCon (TC TCInteger) [] -> - Unsolvable $ - TCErrorMessage "Type 'Integer' does not support rounding operations." + TCon (TC TCInteger) [] -> Unsolvable -- Round (Z n) fails - TCon (TC TCIntMod) [_] -> - Unsolvable $ - TCErrorMessage "Type 'Z' does not support rounding operations." + TCon (TC TCIntMod) [_] -> Unsolvable -- Round Rational TCon (TC TCRational) [] -> SolvedIf [] @@ -314,24 +284,16 @@ solveRoundInst ty = case tNoUser ty of -- Round Real -- Round ([n]a) fails - TCon (TC TCSeq) [_, _] -> - Unsolvable $ - TCErrorMessage "Sequence types do not support rounding operations." + TCon (TC TCSeq) [_, _] -> Unsolvable -- Round (a -> b) fails - TCon (TC TCFun) [_, _] -> - Unsolvable $ - TCErrorMessage "Function types do not support rounding operations." + TCon (TC TCFun) [_, _] -> Unsolvable -- Round (a, b, ...) fails - TCon (TC (TCTuple _)) _ -> - Unsolvable $ - TCErrorMessage "Tuple types do not support rounding operations." + TCon (TC (TCTuple _)) _ -> Unsolvable -- Round {x : a, y : b, ...} fails - TRec _ -> - Unsolvable $ - TCErrorMessage "Record types do not support rounding operations." + TRec _ -> Unsolvable _ -> Unsolved @@ -342,7 +304,7 @@ solveEqInst :: Type -> Solved solveEqInst ty = case tNoUser ty of -- Eq Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- eq Bit TCon (TC TCBit) [] -> SolvedIf [] @@ -366,8 +328,7 @@ solveEqInst ty = case tNoUser ty of TCon (TC (TCTuple _)) es -> SolvedIf (map pEq es) -- Eq (a -> b) fails - TCon (TC TCFun) [_,_] -> - Unsolvable $ TCErrorMessage "Function types do not support comparisons." + TCon (TC TCFun) [_,_] -> Unsolvable -- (Eq a, Eq b) => Eq { x:a, y:b } TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ] @@ -380,7 +341,7 @@ solveCmpInst :: Type -> Solved solveCmpInst ty = case tNoUser ty of -- Cmp Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- Cmp Bit TCon (TC TCBit) [] -> SolvedIf [] @@ -392,8 +353,7 @@ solveCmpInst ty = case tNoUser ty of TCon (TC TCRational) [] -> SolvedIf [] -- Cmp (Z n) fails - TCon (TC TCIntMod) [_] -> - Unsolvable $ TCErrorMessage "Type 'Z' does not support order comparisons." + TCon (TC TCIntMod) [_] -> Unsolvable -- ValidFloat e p => Cmp (Float e p) TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] @@ -405,8 +365,7 @@ solveCmpInst ty = case tNoUser ty of TCon (TC (TCTuple _)) es -> SolvedIf (map pCmp es) -- Cmp (a -> b) fails - TCon (TC TCFun) [_,_] -> - Unsolvable $ TCErrorMessage "Function types do not support order comparisons." + TCon (TC TCFun) [_,_] -> Unsolvable -- (Cmp a, Cmp b) => Cmp { x:a, y:b } TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ] @@ -434,32 +393,22 @@ solveSignedCmpInst :: Type -> Solved solveSignedCmpInst ty = case tNoUser ty of -- SignedCmp Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- SignedCmp Bit fails - TCon (TC TCBit) [] -> - Unsolvable $ - TCErrorMessage "Type 'Bit' does not support signed comparisons." + TCon (TC TCBit) [] -> Unsolvable -- SignedCmp Integer fails - TCon (TC TCInteger) [] -> - Unsolvable $ - TCErrorMessage "Type 'Integer' does not support signed comparisons." + TCon (TC TCInteger) [] -> Unsolvable -- SignedCmp (Z n) fails - TCon (TC TCIntMod) [_] -> - Unsolvable $ - TCErrorMessage "Type 'Z' does not support signed comparisons." + TCon (TC TCIntMod) [_] -> Unsolvable -- SignedCmp Rational fails - TCon (TC TCRational) [] -> - Unsolvable $ - TCErrorMessage "Type 'Rational' does not support signed comparisons." + TCon (TC TCRational) [] -> Unsolvable -- SignedCmp (Float e p) fails - TCon (TC TCFloat) [_, _] -> - Unsolvable $ - TCErrorMessage "Type 'Float' does not support signed comparisons." + TCon (TC TCFloat) [_, _] -> Unsolvable -- SignedCmp for sequences TCon (TC TCSeq) [n,a] -> solveSignedCmpSeq n a @@ -468,9 +417,7 @@ solveSignedCmpInst ty = case tNoUser ty of TCon (TC (TCTuple _)) es -> SolvedIf (map pSignedCmp es) -- SignedCmp (a -> b) fails - TCon (TC TCFun) [_,_] -> - Unsolvable $ - TCErrorMessage "Function types do not support signed comparisons." + TCon (TC TCFun) [_,_] -> Unsolvable -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b } TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ] @@ -481,19 +428,16 @@ solveSignedCmpInst ty = case tNoUser ty of -- | Solving fractional literal constraints. solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved solveFLiteralInst numT denT rndT ty - | TCon (TError _ e) _ <- tNoUser numT = Unsolvable e - | TCon (TError _ e) _ <- tNoUser denT = Unsolvable e - | tIsInf numT || tIsInf denT || tIsInf rndT = - Unsolvable $ TCErrorMessage $ "Fractions may not use `inf`" - | Just 0 <- tIsNum denT = - Unsolvable $ TCErrorMessage - $ "Fractions may not have 0 as the denominator." + | TCon (TError {}) _ <- tNoUser numT = Unsolvable + | TCon (TError {}) _ <- tNoUser denT = Unsolvable + | tIsInf numT || tIsInf denT || tIsInf rndT = Unsolvable + | Just 0 <- tIsNum denT = Unsolvable | otherwise = case tNoUser ty of TVar {} -> Unsolved - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable TCon (TC TCRational) [] -> SolvedIf [ pFin numT, pFin denT, denT >== tOne ] @@ -509,24 +453,21 @@ solveFLiteralInst numT denT rndT ty , Just d <- tIsNum denT -> case FP.bfDiv opts (FP.bfFromInteger n) (FP.bfFromInteger d) of (_, FP.Ok) -> SolvedIf [] - _ -> Unsolvable $ TCErrorMessage - $ show n ++ "/" ++ show d ++ " cannot be " ++ - "represented in " ++ show (pp ty) + _ -> Unsolvable | otherwise -> Unsolved - _ -> Unsolvable $ TCErrorMessage $ show - $ "Type" <+> quotes (pp ty) <+> "does not support fractional literals." + _ -> Unsolvable -- | Solve Literal constraints. solveLiteralInst :: Type -> Type -> Solved solveLiteralInst val ty - | TCon (TError _ e) _ <- tNoUser val = Unsolvable e + | TCon (TError {}) _ <- tNoUser val = Unsolvable | otherwise = case tNoUser ty of -- Literal n Error -> fails - TCon (TError _ e) _ -> Unsolvable e + TCon (TError {}) _ -> Unsolvable -- (1 >= val) => Literal val Bit TCon (TC TCBit) [] -> SolvedIf [ tOne >== val ] @@ -544,9 +485,7 @@ solveLiteralInst val ty let bf = FP.bfFromInteger n in case FP.bfRoundFloat opts bf of (bf1,FP.Ok) | bf == bf1 -> SolvedIf [] - _ -> Unsolvable $ TCErrorMessage - $ show n ++ " cannot be " ++ - "represented in " ++ show (pp ty) + _ -> Unsolvable | otherwise -> Unsolved @@ -565,5 +504,6 @@ solveLiteralInst val ty TVar _ -> Unsolved - _ -> Unsolvable $ TCErrorMessage $ show - $ "Type" <+> quotes (pp ty) <+> "does not support integer literals." + _ -> Unsolvable + + diff --git a/src/Cryptol/TypeCheck/Solver/Numeric.hs b/src/Cryptol/TypeCheck/Solver/Numeric.hs index 59253e7c7..e41cba9e8 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric.hs @@ -13,7 +13,6 @@ import qualified GHC.Integer.GMP.Internals as Integer import Cryptol.Utils.Patterns -import Cryptol.TypeCheck.PP import Cryptol.TypeCheck.Type hiding (tMul) import Cryptol.TypeCheck.TypePat import Cryptol.TypeCheck.Solver.Types @@ -34,7 +33,7 @@ import Cryptol.TypeCheck.SimpType as Simp cryIsEqual :: Ctxt -> Type -> Type -> Solved cryIsEqual ctxt t1 t2 = matchDefault Unsolved $ - (pBin PEqual (==) t1 t2) + (pBin (==) t1 t2) <|> (aNat' t1 >>= tryEqK ctxt t2) <|> (aNat' t2 >>= tryEqK ctxt t1) <|> (aTVar t1 >>= tryEqVar t2) @@ -53,13 +52,13 @@ cryIsEqual ctxt t1 t2 = -- | Try to solve @t1 /= t2@ cryIsNotEqual :: Ctxt -> Type -> Type -> Solved -cryIsNotEqual _i t1 t2 = matchDefault Unsolved (pBin PNeq (/=) t1 t2) +cryIsNotEqual _i t1 t2 = matchDefault Unsolved (pBin (/=) t1 t2) -- | Try to solve @t1 >= t2@ cryIsGeq :: Ctxt -> Type -> Type -> Solved cryIsGeq i t1 t2 = matchDefault Unsolved $ - (pBin PGeq (>=) t1 t2) + (pBin (>=) t1 t2) <|> (aNat' t1 >>= tryGeqKThan i t2) <|> (aNat' t2 >>= tryGeqThanK i t1) <|> (aTVar t2 >>= tryGeqThanVar i t1) @@ -94,26 +93,23 @@ cryIsPrime _varInfo ty = if untrie primeTable n then SolvedIf [] else - Unsolvable $ TCErrorMessage (show n ++ " is not a prime number") + Unsolvable - | TCInf <- tc -> - Unsolvable $ TCErrorMessage "`inf` is not a prime number" + | TCInf <- tc -> Unsolvable _ -> Unsolved -- | Try to solve something by evaluation. -pBin :: PC -> (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved -pBin tf p t1 t2 = - Unsolvable <$> anError KNum t1 - <|> Unsolvable <$> anError KNum t2 - <|> (do x <- aNat' t1 - y <- aNat' t2 - return $ if p x y - then SolvedIf [] - else Unsolvable $ TCErrorMessage - $ "It is not the case that " ++ - show (pp (TCon (PC tf) [ tNat' x, tNat' y ]))) +pBin :: (Nat' -> Nat' -> Bool) -> Type -> Type -> Match Solved +pBin p t1 t2 + | Just _ <- tIsError t1 = pure Unsolvable + | Just _ <- tIsError t2 = pure Unsolvable + | otherwise = do x <- aNat' t1 + y <- aNat' t2 + return $ if p x y + then SolvedIf [] + else Unsolvable -------------------------------------------------------------------------------- @@ -181,8 +177,7 @@ tryMinIsGeq t1 t2 = k2 <- aNat t2 return $ if k1 >= k2 then SolvedIf [ b >== t2 ] - else Unsolvable $ TCErrorMessage $ - show k1 ++ " can't be greater than " ++ show k2 + else Unsolvable -------------------------------------------------------------------------------- @@ -327,9 +322,6 @@ tryEqK ctxt ty lk = case nSub lk rk of -- NOTE: (Inf - Inf) shouldn't be possible Nothing -> Unsolvable - $ TCErrorMessage - $ "Adding " ++ showNat' rk ++ " will always exceed " - ++ showNat' lk Just r -> SolvedIf [ b =#= tNat' r ] <|> @@ -352,9 +344,7 @@ tryEqK ctxt ty lk = (Nat 0, Inf) -> SolvedIf [ b =#= tZero ] -- Inf * t = K ~~~> ERR (K /= 0) - (Nat k, Inf) -> Unsolvable - $ TCErrorMessage - $ show k ++ " != inf * anything" + (Nat _k, Inf) -> Unsolvable (Nat lk', Nat rk') -- 0 * t = K2 ~~> K2 = 0 @@ -363,10 +353,7 @@ tryEqK ctxt ty lk = -- K1 * t = K2 ~~> t = K2/K1 | (q,0) <- divMod lk' rk' -> SolvedIf [ b =#= tNum q ] - | otherwise -> - Unsolvable - $ TCErrorMessage - $ showNat' lk ++ " != " ++ showNat' rk ++ " * anything" + | otherwise -> Unsolvable <|> -- K1 == K2 ^^ t ~~> t = logBase K2 K1 @@ -374,8 +361,7 @@ tryEqK ctxt ty lk = return $ case lk of Inf | rk > 1 -> SolvedIf [ b =#= tInf ] Nat n | Just (a,True) <- genLog n rk -> SolvedIf [ b =#= tNum a] - _ -> Unsolvable $ TCErrorMessage - $ show rk ++ " ^^ anything != " ++ showNat' lk + _ -> Unsolvable -- XXX: Min, Max, etx -- 2 = min (10,y) --> y = 2 @@ -501,6 +487,3 @@ matchLinear = go (0, []) -showNat' :: Nat' -> String -showNat' Inf = "inf" -showNat' (Nat n) = show n diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs index b3e83f1f9..4826bdcb0 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs @@ -35,8 +35,7 @@ cryIsFinType ctxt ty = TCon (TC tc) [] | TCNum _ <- tc -> SolvedIf [] - | TCInf <- tc -> - Unsolvable $ TCErrorMessage "Expected a finite type, but found `inf`." + | TCInf <- tc -> Unsolvable TCon (TF f) ts -> case (f,ts) of diff --git a/src/Cryptol/TypeCheck/Solver/SMT.hs b/src/Cryptol/TypeCheck/Solver/SMT.hs index 113e8f043..7d47d1a73 100644 --- a/src/Cryptol/TypeCheck/Solver/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/SMT.hs @@ -381,9 +381,6 @@ instance Mk TVar where instance Mk Type where mk tvs f x = SMT.fun f [toSMT tvs x] -instance Mk TCErrorMessage where - mk _ f _ = SMT.fun f [] - instance Mk (Type,Type) where mk tvs f (x,y) = SMT.fun f [ toSMT tvs x, toSMT tvs y] diff --git a/src/Cryptol/TypeCheck/Solver/Types.hs b/src/Cryptol/TypeCheck/Solver/Types.hs index 9c3015406..235488253 100644 --- a/src/Cryptol/TypeCheck/Solver/Types.hs +++ b/src/Cryptol/TypeCheck/Solver/Types.hs @@ -1,3 +1,4 @@ +{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass #-} module Cryptol.TypeCheck.Solver.Types where import Data.Map(Map) @@ -22,10 +23,11 @@ instance Monoid Ctxt where data Solved = SolvedIf [Prop] -- ^ Solved, assuming the sub-goals. | Unsolved -- ^ We could not solve the goal. - | Unsolvable TCErrorMessage -- ^ The goal can never be solved. + | Unsolvable -- ^ The goal can never be solved. deriving (Show) + elseTry :: Solved -> Solved -> Solved Unsolved `elseTry` x = x x `elseTry` _ = x @@ -48,4 +50,5 @@ instance PP Solved where case res of SolvedIf ps -> text "solved" $$ nest 2 (vcat (map pp ps)) Unsolved -> text "unsolved" - Unsolvable e -> text "unsolvable" <.> colon <+> text (tcErrorMessage e) + Unsolvable -> text "unsolvable" + diff --git a/src/Cryptol/TypeCheck/TCon.hs b/src/Cryptol/TypeCheck/TCon.hs index 0a84142a1..654286036 100644 --- a/src/Cryptol/TypeCheck/TCon.hs +++ b/src/Cryptol/TypeCheck/TCon.hs @@ -1,4 +1,4 @@ -{-# Language DeriveGeneric, DeriveAnyClass #-} +{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass, Safe #-} module Cryptol.TypeCheck.TCon where import qualified Data.Map as Map @@ -123,7 +123,7 @@ instance HasKind TCon where kindOf (TC tc) = kindOf tc kindOf (PC pc) = kindOf pc kindOf (TF tf) = kindOf tf - kindOf (TError k _) = k + kindOf (TError k) = k instance HasKind UserTC where kindOf (UserTC _ k) = k @@ -190,7 +190,7 @@ instance HasKind TFun where -- | Type constants. -data TCon = TC TC | PC PC | TF TFun | TError Kind TCErrorMessage +data TCon = TC TC | PC PC | TF TFun | TError Kind deriving (Show, Eq, Ord, Generic, NFData) @@ -253,10 +253,6 @@ instance Ord UserTC where -data TCErrorMessage = TCErrorMessage - { tcErrorMessage :: !String - -- XXX: Add location? - } deriving (Show, Eq, Ord, Generic, NFData) -- | Built-in type functions. @@ -298,12 +294,9 @@ instance PP TCon where ppPrec _ (TC tc) = pp tc ppPrec _ (PC tc) = pp tc ppPrec _ (TF tc) = pp tc - ppPrec _ (TError _ msg) = pp msg + ppPrec _ (TError _) = "Error" -instance PP TCErrorMessage where - ppPrec _ tc = parens (text "error:" <+> text (tcErrorMessage tc)) - instance PP PC where ppPrec _ x = case x of diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index a4d3b5920..a3bc8b727 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -375,16 +375,16 @@ isBoundTV (TVBound {}) = True isBoundTV _ = False -tIsError :: Type -> Maybe (TCErrorMessage,Type) +tIsError :: Type -> Maybe Type tIsError ty = case tNoUser ty of - TCon (TError _ x) [t] -> Just (x,t) - TCon (TError _ _) _ -> panic "tIsError" ["Malformed error"] - _ -> Nothing + TCon (TError _) [t] -> Just t + TCon (TError _) _ -> panic "tIsError" ["Malformed error"] + _ -> Nothing tHasErrors :: Type -> Bool tHasErrors ty = case tNoUser ty of - TCon (TError _ _) _ -> True + TCon (TError _) _ -> True TCon _ ts -> any tHasErrors ts TRec mp -> any tHasErrors mp _ -> False @@ -640,10 +640,9 @@ tNoUser t = case t of -- | Make an error value of the given type to replace -- the given malformed type (the argument to the error function) -tError :: Type -> String -> Type -tError t s = TCon (TError (k :-> k) msg) [t] +tError :: Type -> Type +tError t = TCon (TError (k :-> k)) [t] where k = kindOf t - msg = TCErrorMessage s tf1 :: TFun -> Type -> Type tf1 f x = TCon (TF f) [x] @@ -762,9 +761,10 @@ pFin :: Type -> Prop pFin ty = case tNoUser ty of TCon (TC (TCNum _)) _ -> pTrue - TCon (TC TCInf) _ -> tError (TCon (PC PFin) [ty]) "`inf` is not finite" - -- XXX: should we be doing this here?? - _ -> TCon (PC PFin) [ty] + TCon (TC TCInf) _ -> tError prop -- XXX: should we be doing this here?? + _ -> prop + where + prop = TCon (PC PFin) [ty] pValidFloat :: Type -> Type -> Type pValidFloat e p = TCon (PC PValidFloat) [e,p] @@ -772,12 +772,11 @@ pValidFloat e p = TCon (PC PValidFloat) [e,p] pPrime :: Type -> Prop pPrime ty = case tNoUser ty of - TCon (TC TCInf) _ -> pError (TCErrorMessage "`inf` is not prime.") - _ -> TCon (PC PPrime) [ty] + TCon (TC TCInf) _ -> tError prop + _ -> prop + where + prop = TCon (PC PPrime) [ty] --- | Make a malformed property. -pError :: TCErrorMessage -> Prop -pError msg = TCon (TError KProp msg) [] -------------------------------------------------------------------------------- diff --git a/src/Cryptol/TypeCheck/TypePat.hs b/src/Cryptol/TypeCheck/TypePat.hs index c6048781f..fd08bd519 100644 --- a/src/Cryptol/TypeCheck/TypePat.hs +++ b/src/Cryptol/TypeCheck/TypePat.hs @@ -182,10 +182,10 @@ aLogic :: Pat Prop Type aLogic = tp PLogic ar1 -------------------------------------------------------------------------------- -anError :: Kind -> Pat Type TCErrorMessage +anError :: Kind -> Pat Type () anError k = \a -> case tNoUser a of - TCon (TError k1 err) _ | k == k1 -> return err - _ -> mzero + TCon (TError (_ :-> k1) ) _ | k == k1 -> return () + _ -> mzero From 6f23c7b08d17982b6ccd219b9bbed3a480b9aba2 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 12 Nov 2020 15:48:43 -0800 Subject: [PATCH 2/6] Checkpoint --- src/Cryptol/ModuleSystem/Monad.hs | 4 ++-- src/Cryptol/TypeCheck.hs | 10 ++++++++-- utils/CryTC.hs | 2 +- 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 77bdde691..a3327c633 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -176,7 +176,7 @@ instance PP ModuleError where NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs) - TypeCheckingFailed _src errs -> vcat (map T.ppError errs) + TypeCheckingFailed _src errs -> T.ppErrors errs ModuleNameMismatch expected found -> hang (text "[error]" <+> pp (P.srcRange found) <.> char ':') @@ -279,7 +279,7 @@ data ModuleWarning instance PP ModuleWarning where ppPrec _ w = case w of - TypeCheckWarnings ws -> vcat (map T.ppWarning ws) + TypeCheckWarnings ws -> T.ppWarnings ws RenamerWarnings ws -> vcat (map pp ws) warn :: [ModuleWarning] -> ModuleM () diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs index 5c2799972..577e1ec51 100644 --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -19,8 +19,10 @@ module Cryptol.TypeCheck , nameSeeds , Error(..) , Warning(..) - , ppWarning - , ppError + -- , ppWarning + -- , ppError + , ppWarnings + , ppErrors ) where import Cryptol.ModuleSystem.Name @@ -121,4 +123,8 @@ ppWarning (r,w) = text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp w) ppError :: (Range,Error) -> Doc ppError (r,w) = text "[error] at" <+> pp r <.> colon $$ nest 2 (pp w) +ppWarnings :: [(Range,Warning)] -> Doc +ppWarnings = vcat . map ppWarning +ppErrors :: [(Range,Error)] -> Doc +ppErrors = vcat . map ppError diff --git a/utils/CryTC.hs b/utils/CryTC.hs index 588052386..1acd2746a 100755 --- a/utils/CryTC.hs +++ b/utils/CryTC.hs @@ -36,7 +36,7 @@ main = print (pp prog) InferFailed ws errs -> do mapM_ (print . TC.ppWarning IMap.empty) ws - mapM_ (print . TC.ppError IMap.empty) errs + print (TC.ppErrors errs) (_,errs) -> hPrint stderr $ vcat $ map pp errs where From 7b4c43353100fdcee91afd81d3a2c0669943f9fb Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Fri, 13 Nov 2020 11:41:26 -0800 Subject: [PATCH 3/6] Nicer pretty printing of unification variables. This should go some way toward solving #782, although there are still funny numbers from quantified variables. Note the tests do not yet work, as the error messages are all different and I'll change them only when I finalize the new error messages --- src/Cryptol/ModuleSystem/Base.hs | 10 +-- src/Cryptol/ModuleSystem/Monad.hs | 22 +++--- src/Cryptol/REPL/Command.hs | 4 +- src/Cryptol/TypeCheck.hs | 24 ++++--- src/Cryptol/TypeCheck/CheckModuleInstance.hs | 18 ++--- src/Cryptol/TypeCheck/Error.hs | 74 ++++++++++++++++---- src/Cryptol/TypeCheck/Monad.hs | 38 +++++----- src/Cryptol/TypeCheck/Type.hs | 28 +++++--- 8 files changed, 143 insertions(+), 75 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index f09dba07e..28e5d8a5e 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -505,10 +505,10 @@ typecheck act i params env = do case out of - T.InferOK warns seeds supply' o -> + T.InferOK nameMap warns seeds supply' o -> do setNameSeeds seeds setSupply supply' - typeCheckWarnings warns + typeCheckWarnings nameMap warns menv <- getModuleEnv case meCoreLint menv of NoCoreLint -> return () @@ -519,9 +519,9 @@ typecheck act i params env = do Left err -> panic "Core lint failed:" [show err] return o - T.InferFailed warns errs -> - do typeCheckWarnings warns - typeCheckingFailed errs + T.InferFailed nameMap warns errs -> + do typeCheckWarnings nameMap warns + typeCheckingFailed nameMap errs -- | Generate input for the typechecker. genInferInput :: Range -> PrimMap -> diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index a3327c633..d40680c8f 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -96,7 +96,7 @@ data ModuleError -- ^ Problems during the NoPat phase | NoIncludeErrors ImportSource [NoInc.IncludeError] -- ^ Problems during the NoInclude phase - | TypeCheckingFailed ImportSource [(Range,T.Error)] + | TypeCheckingFailed ImportSource T.NameMap [(Range,T.Error)] -- ^ Problems during type checking | OtherFailure String -- ^ Problems after type checking, eg. specialization @@ -128,7 +128,7 @@ instance NFData ModuleError where RenamerErrors src errs -> src `deepseq` errs `deepseq` () NoPatErrors src errs -> src `deepseq` errs `deepseq` () NoIncludeErrors src errs -> src `deepseq` errs `deepseq` () - TypeCheckingFailed src errs -> src `deepseq` errs `deepseq` () + TypeCheckingFailed nm src errs -> nm `deepseq` src `deepseq` errs `deepseq` () ModuleNameMismatch expected found -> expected `deepseq` found `deepseq` () DuplicateModuleName name path1 path2 -> @@ -176,7 +176,7 @@ instance PP ModuleError where NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs) - TypeCheckingFailed _src errs -> T.ppErrors errs + TypeCheckingFailed _src nm errs -> vcat (map (T.ppNamedError nm) errs) ModuleNameMismatch expected found -> hang (text "[error]" <+> pp (P.srcRange found) <.> char ':') @@ -239,10 +239,10 @@ noIncludeErrors errs = do src <- getImportSource ModuleT (raise (NoIncludeErrors src errs)) -typeCheckingFailed :: [(Range,T.Error)] -> ModuleM a -typeCheckingFailed errs = do +typeCheckingFailed :: T.NameMap -> [(Range,T.Error)] -> ModuleM a +typeCheckingFailed nameMap errs = do src <- getImportSource - ModuleT (raise (TypeCheckingFailed src errs)) + ModuleT (raise (TypeCheckingFailed src nameMap errs)) moduleNameMismatch :: P.ModName -> Located P.ModName -> ModuleM a moduleNameMismatch expected found = @@ -273,22 +273,22 @@ errorInFile file (ModuleT m) = ModuleT (m `handle` h) -- Warnings -------------------------------------------------------------------- data ModuleWarning - = TypeCheckWarnings [(Range,T.Warning)] + = TypeCheckWarnings T.NameMap [(Range,T.Warning)] | RenamerWarnings [RenamerWarning] deriving (Show, Generic, NFData) instance PP ModuleWarning where ppPrec _ w = case w of - TypeCheckWarnings ws -> T.ppWarnings ws + TypeCheckWarnings nm ws -> vcat (map (T.ppNamedWarning nm) ws) RenamerWarnings ws -> vcat (map pp ws) warn :: [ModuleWarning] -> ModuleM () warn = ModuleT . put -typeCheckWarnings :: [(Range,T.Warning)] -> ModuleM () -typeCheckWarnings ws +typeCheckWarnings :: T.NameMap -> [(Range,T.Warning)] -> ModuleM () +typeCheckWarnings nameMap ws | null ws = return () - | otherwise = warn [TypeCheckWarnings ws] + | otherwise = warn [TypeCheckWarnings nameMap ws] renamerWarnings :: [RenamerWarning] -> ModuleM () renamerWarnings ws diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index c5b685b2c..5cba3d1de 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1554,10 +1554,10 @@ moduleCmdResult (res,ws0) = do isDefaultWarn _ = False filterDefaults w | warnDefaulting = Just w - filterDefaults (M.TypeCheckWarnings xs) = + filterDefaults (M.TypeCheckWarnings nameMap xs) = case filter (not . isDefaultWarn . snd) xs of [] -> Nothing - ys -> Just (M.TypeCheckWarnings ys) + ys -> Just (M.TypeCheckWarnings nameMap ys) filterDefaults w = Just w isShadowWarn (M.SymbolShadowed {}) = True diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs index 577e1ec51..25d4ee9b6 100644 --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -19,10 +19,12 @@ module Cryptol.TypeCheck , nameSeeds , Error(..) , Warning(..) - -- , ppWarning - -- , ppError - , ppWarnings - , ppErrors + , ppWarning + , ppError + , WithNames(..) + , NameMap + , ppNamedWarning + , ppNamedError ) where import Cryptol.ModuleSystem.Name @@ -45,6 +47,7 @@ import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..)) import Cryptol.TypeCheck.Solve(proveModuleTopLevel) import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance) import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints) +import Cryptol.TypeCheck.PP(WithNames(..),NameMap) import Cryptol.Utils.Ident (exprModName,packIdent) import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) @@ -123,8 +126,13 @@ ppWarning (r,w) = text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp w) ppError :: (Range,Error) -> Doc ppError (r,w) = text "[error] at" <+> pp r <.> colon $$ nest 2 (pp w) -ppWarnings :: [(Range,Warning)] -> Doc -ppWarnings = vcat . map ppWarning -ppErrors :: [(Range,Error)] -> Doc -ppErrors = vcat . map ppError +ppNamedWarning :: NameMap -> (Range,Warning) -> Doc +ppNamedWarning nm (r,w) = + text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp (WithNames w nm)) + +ppNamedError :: NameMap -> (Range,Error) -> Doc +ppNamedError nm (r,e) = + text "[error] at" <+> pp r <.> colon $$ nest 2 (pp (WithNames e nm)) + + diff --git a/src/Cryptol/TypeCheck/CheckModuleInstance.hs b/src/Cryptol/TypeCheck/CheckModuleInstance.hs index 23e75fcd5..5bfddcf29 100644 --- a/src/Cryptol/TypeCheck/CheckModuleInstance.hs +++ b/src/Cryptol/TypeCheck/CheckModuleInstance.hs @@ -13,7 +13,6 @@ import Cryptol.TypeCheck.Monad import Cryptol.TypeCheck.Infer import Cryptol.TypeCheck.Subst import Cryptol.TypeCheck.Error -import Cryptol.Utils.PP import Cryptol.Utils.Panic @@ -61,10 +60,12 @@ checkTyParams func inst = tParams = Map.fromList [ (tpId x, x) | x0 <- Map.elems (mParamTypes inst) , let x = mtpParam x0 ] - tpId x = case tpName x of - Just n -> nameIdent n + tpName' x = case tpName x of + Just n -> n Nothing -> panic "inferModuleInstance.tpId" ["Missing name"] + tpId = nameIdent . tpName' + -- Find a definition for a given type parameter checkTParamDefined tp0 = let tp = mtpParam tp0 @@ -78,8 +79,9 @@ checkTyParams func inst = case Map.lookup x tParams of Just tp1 -> checkTP tp tp1 Nothing -> - do recordError $ ErrorMsg $ - text "Missing definition for type parameter:" <+> pp x + do let x' = Located { thing = x, + srcRange = nameLoc (tpName' tp) } + recordError (MissingModTParam x') return (tp, TVar (TVBound tp)) -- hm, maybe just stop! -- Check that a type parameter defined as a type synonym is OK @@ -148,9 +150,9 @@ checkValParams func tMap inst = case Map.lookup (nameIdent x) valMap of Just (n,sD) -> do e <- makeValParamDef n sD (apSubst su sP) return (x,e) - Nothing -> do recordError $ ErrorMsg - $ text "Mising definition for value parameter" - <+> pp x + Nothing -> do recordError (MissingModVParam + Located { thing = nameIdent x + , srcRange = nameLoc x }) return (x, panic "checkValParams" ["Should not use this"]) diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index a86f8ba46..bacc86d92 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -7,7 +7,7 @@ import qualified Data.IntMap as IntMap import qualified Data.Set as Set import Control.DeepSeq(NFData) import GHC.Generics(Generic) -import Data.List((\\),sortBy,groupBy) +import Data.List((\\),sortBy,groupBy,partition) import Data.Function(on) import qualified Cryptol.Parser.AST as P @@ -65,10 +65,7 @@ data Warning = DefaultingKind (P.TParam Name) P.Kind deriving (Show, Generic, NFData) -- | Various errors that might happen during type checking/inference -data Error = ErrorMsg Doc - -- ^ Just say this - - | KindMismatch (Maybe TypeSource) Kind Kind +data Error = KindMismatch (Maybe TypeSource) Kind Kind -- ^ Expected kind, inferred kind | TooManyTypeParams Int Kind @@ -130,6 +127,11 @@ data Error = ErrorMsg Doc -- ^ Could not determine the value of a numeric type variable, -- but we know it must be at least as large as the given type -- (or unconstrained, if Nothing). + + | UndefinedExistVar Name + | TypeShadowing String Name String + | MissingModTParam (Located Ident) + | MissingModVParam (Located Ident) deriving (Show, Generic, NFData) -- | When we have multiple errors on the same location, we show only the @@ -144,6 +146,11 @@ errorImportance err = NotForAll {} -> 6 TypeVariableEscaped {} -> 5 + UndefinedExistVar {} -> 10 + TypeShadowing {} -> 2 + MissingModTParam {} -> 10 + MissingModVParam {} -> 10 + CannotMixPositionalAndNamedTypeParams {} -> 8 TooManyTypeParams {} -> 8 @@ -171,8 +178,6 @@ errorImportance err = AmbiguousSize {} -> 2 - ErrorMsg {} -> 1 - instance TVars Warning where @@ -192,7 +197,6 @@ instance FVS Warning where instance TVars Error where apSubst su err = case err of - ErrorMsg _ -> err KindMismatch {} -> err TooManyTypeParams {} -> err TyVarWithParams -> err @@ -216,10 +220,15 @@ instance TVars Error where AmbiguousSize x t -> AmbiguousSize x !$ (apSubst su t) + UndefinedExistVar {} -> err + TypeShadowing {} -> err + MissingModTParam {} -> err + MissingModVParam {} -> err + + instance FVS Error where fvs err = case err of - ErrorMsg {} -> Set.empty KindMismatch {} -> Set.empty TooManyTypeParams {} -> Set.empty TyVarWithParams -> Set.empty @@ -241,6 +250,10 @@ instance FVS Error where RepeatedTypeParameter {} -> Set.empty AmbiguousSize _ t -> fvs t + UndefinedExistVar {} -> Set.empty + TypeShadowing {} -> Set.empty + MissingModTParam {} -> Set.empty + MissingModVParam {} -> Set.empty instance PP Warning where ppPrec = ppWithNamesPrec IntMap.empty @@ -266,9 +279,6 @@ instance PP (WithNames Warning) where instance PP (WithNames Error) where ppPrec _ (WithNames err names) = case err of - ErrorMsg msg -> - addTVarsDescsAfter names err - msg RecursiveType src t1 t2 -> addTVarsDescsAfter names err $ @@ -400,6 +410,18 @@ instance PP (WithNames Error) where Nothing -> empty in addTVarsDescsAfter names err ("Ambiguous numeric type:" <+> pp (tvarDesc x) $$ sizeMsg) + UndefinedExistVar x -> "Undefined type" <+> quotes (pp x) + TypeShadowing this new that -> + "Type" <+> text this <+> quotes (pp new) <+> + "shadowing an existing" <+> text that <+> "with the same name." + MissingModTParam x -> + "Missing definition for type parameter" <+> quotes (pp (thing x)) + MissingModVParam x -> + "Missing definition for value parameter" <+> quotes (pp (thing x)) + + + + where bullets xs = vcat [ "•" <+> d | d <- xs ] @@ -426,3 +448,31 @@ instance PP (WithNames Error) where mismatchHint _ _ = mempty noUni = Set.null (Set.filter isFreeTV (fvs err)) + + + +computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap +computeFreeVarNames warns errs = + mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars + where + mkName x v = (tvUnique x, v) + mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots)) + + (numVaras,otherVars) = partition ((== KNum) . kindOf) + $ Set.toList + $ Set.filter isFreeTV + $ fvs (map snd warns, map snd errs) + + otherRoots = [ "a", "b", "c", "d" ] + numRoots = [ "m", "n", "u", "v" ] + + useUnicode = True + + suff n + | n < 10 && useUnicode = [toEnum (0x2080 + n)] + | otherwise = show n + + variant n x = if n == 0 then x else x ++ suff n + + variants roots = [ variant n r | n <- [ 0 .. ], r <- roots ] + diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 395c82ca7..aa5348ce0 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -27,11 +27,13 @@ import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst import Cryptol.TypeCheck.Unify(mgu, runResult, UnificationError(..)) import Cryptol.TypeCheck.InferTypes -import Cryptol.TypeCheck.Error(Warning(..),Error(..),cleanupErrors) -import Cryptol.TypeCheck.PP (brackets, commaSep) +import Cryptol.TypeCheck.Error( Warning(..),Error(..) + , cleanupErrors, computeFreeVarNames + ) import qualified Cryptol.TypeCheck.SimpleSolver as Simple import qualified Cryptol.TypeCheck.Solver.SMT as SMT -import Cryptol.Utils.PP(pp, (<+>), text, quotes) +import Cryptol.TypeCheck.PP(NameMap) +import Cryptol.Utils.PP(pp, (<+>), text,commaSep,brackets) import Cryptol.Utils.Ident(Ident) import Cryptol.Utils.Panic(panic) @@ -98,10 +100,10 @@ nameSeeds = NameSeeds { seedTVar = 10, seedGoal = 0 } -- | The results of type inference. data InferOutput a - = InferFailed [(Range,Warning)] [(Range,Error)] + = InferFailed NameMap [(Range,Warning)] [(Range,Error)] -- ^ We found some errors - | InferOK [(Range,Warning)] NameSeeds Supply a + | InferOK NameMap [(Range,Warning)] NameSeeds Supply a -- ^ Type inference was successful. @@ -142,21 +144,26 @@ runInferM info (IM m) = SMT.withSolver (inpSolverConfig info) $ \solver -> [] -> case (iCts finalRW, iHasCts finalRW) of (cts,[]) - | nullGoals cts - -> return $ InferOK warns + | nullGoals cts -> inferOk warns (iNameSeeds finalRW) (iSupply finalRW) (apSubst defSu result) - (cts,has) -> return $ InferFailed warns - $ cleanupErrors + (cts,has) -> + inferFailed warns [ ( goalRange g , UnsolvedGoals [apSubst theSu g] ) | g <- fromGoals cts ++ map hasGoal has ] - errs -> return $ InferFailed warns - $ cleanupErrors [(r,apSubst theSu e) | (r,e) <- errs] + + errs -> inferFailed warns [(r,apSubst theSu e) | (r,e) <- errs] where + inferOk ws a b c = pure (InferOK (computeFreeVarNames ws []) ws a b c) + inferFailed ws es = + let es1 = cleanupErrors es + in pure (InferFailed (computeFreeVarNames ws es1) ws es1) + + mkExternal x = (IsExternal, x) rw = RW { iErrors = [] , iWarnings = [] @@ -636,9 +643,7 @@ existVar x k = Nothing -> case scopes of [] -> - do recordError $ ErrorMsg - $ text "Undefined type" <+> quotes (pp x) - <+> text (show x) + do recordError (UndefinedExistVar x) newType TypeErrorPlaceHolder k sc : more -> @@ -709,10 +714,7 @@ checkTShadowing this new = case shadowed of Nothing -> return () Just that -> - recordError $ ErrorMsg $ - text "Type" <+> text this <+> quotes (pp new) <+> - text "shadows an existing" <+> - text that <+> text "with the same name." + recordError (TypeShadowing this new that) diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index a3bc8b727..95253faf4 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -999,17 +999,23 @@ instance PP (WithNames Type) where instance PP (WithNames TVar) where - ppPrec _ (WithNames (TVBound x) mp) = - case IntMap.lookup (tpUnique x) mp of - Just a -> text a - Nothing -> - case tpFlav x of - TPModParam n -> ppPrefixName n - TPOther (Just n) -> pp n <.> "`" <.> int (tpUnique x) - _ -> pickTVarName (tpKind x) (tvarDesc (tpInfo x)) (tpUnique x) - - ppPrec _ (WithNames (TVFree x k _ d) _) = - char '?' <.> pickTVarName k (tvarDesc d) x + ppPrec _ (WithNames tv mp) = + case tv of + TVBound {} -> nmTxt + TVFree {} -> "?" <.> nmTxt + where + nmTxt + | Just a <- IntMap.lookup (tvUnique tv) mp = text a + | otherwise = + case tv of + TVBound x -> + case tpFlav x of + TPModParam n -> ppPrefixName n + TPOther (Just n) -> pp n <.> "`" <.> int (tpUnique x) + _ -> pickTVarName (tpKind x) (tvarDesc (tpInfo x)) (tpUnique x) + + TVFree x k _ d -> pickTVarName k (tvarDesc d) x + pickTVarName :: Kind -> TypeSource -> Int -> Doc pickTVarName k src uni = From 51910d7e8b7f7552d2ec23c4aace9dd63ce3af83 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Nov 2020 10:32:50 -0800 Subject: [PATCH 4/6] Just a comment --- src/Cryptol/TypeCheck/Error.hs | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index bacc86d92..abe79178e 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -451,9 +451,18 @@ instance PP (WithNames Error) where +-- | This picks the names to use when showing errors and warnings. computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap computeFreeVarNames warns errs = mkMap numRoots numVaras `IntMap.union` mkMap otherRoots otherVars + + {- XXX: Currently we pick the names based on the unique of the variable: + smaller uniques get an earlier name (e.g., 100 might get `a` and 200 `b`) + This may still lead to changes in the names if the uniques got reordred + for some reason. A more stable approach might be to order the variables + on their location in the error/warning, but that's quite a bit more code + so for now we just go with the simple approximation. -} + where mkName x v = (tvUnique x, v) mkMap roots vs = IntMap.fromList (zipWith mkName vs (variants roots)) From bfad11ba8676d36817f2f97aabb7d423ca578c38 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Mon, 16 Nov 2020 13:29:57 -0800 Subject: [PATCH 5/6] Improvements to error messages --- src/Cryptol/TypeCheck/Error.hs | 102 ++++- tests/issues/T146.icry.stdout | 8 +- tests/issues/T820.icry.stdout | 20 +- tests/issues/issue101.icry.stdout | 5 +- tests/issues/issue582.icry.stdout | 30 +- tests/issues/issue835.icry.stdout | 10 +- tests/issues/issue845.icry.stdout | 50 +-- tests/issues/issue910.icry.stdout | 40 +- tests/issues/issue913.icry.stdout | 5 +- tests/mono-binds/test04.icry.stdout | 10 +- tests/regression/float.icry.stdout | 20 +- tests/regression/instance.icry.stdout | 551 +++++++++++-------------- tests/regression/primes.icry.stdout | 10 +- tests/regression/tc-errors.icry.stdout | 21 +- 14 files changed, 421 insertions(+), 461 deletions(-) diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index abe79178e..3ce356135 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -338,14 +338,7 @@ instance PP (WithNames Error) where , "When checking" <+> pp src ] - UnsolvableGoals gs -> - addTVarsDescsAfter names err $ - nested "Unsolvable constraints:" $ - let unErr g = case tIsError (goal g) of - Just p -> g { goal = p } - Nothing -> g - in - bullets (map (ppWithNames names) (map unErr gs)) + UnsolvableGoals gs -> explainUnsolvable names gs UnsolvedGoals gs | noUni -> @@ -451,6 +444,99 @@ instance PP (WithNames Error) where +explainUnsolvable :: NameMap -> [Goal] -> Doc +explainUnsolvable names gs = + addTVarsDescsAfter names gs (bullets (map explain gs)) + + where + bullets xs = vcat [ "•" <+> d | d <- xs ] + + + + explain g = + let useCtr = "Unsolvable constraint:" $$ + nest 2 (ppWithNames names g) + + in + case tNoUser (goal g) of + TCon (PC pc) ts -> + let tys = [ backticks (ppWithNames names t) | t <- ts ] + doc1 : _ = tys + custom msg = msg $$ + nest 2 (text "arising from" $$ + pp (goalSource g) $$ + text "at" <+> pp (goalRange g)) + in + case pc of + PEqual -> useCtr + PNeq -> useCtr + PGeq -> useCtr + PFin -> useCtr + PPrime -> useCtr + + PHas sel -> + custom ("Type" <+> doc1 <+> "does not have field" <+> f + <+> "of type" <+> (tys !! 1)) + where f = case sel of + P.TupleSel n _ -> int n + P.RecordSel fl _ -> backticks (pp fl) + P.ListSel n _ -> int n + + PZero -> + custom ("Type" <+> doc1 <+> "does not have `zero`") + + PLogic -> + custom ("Type" <+> doc1 <+> "does not support logical operations.") + + PRing -> + custom ("Type" <+> doc1 <+> "does not support ring operations.") + + PIntegral -> + custom (doc1 <+> "is not an integral type.") + + PField -> + custom ("Type" <+> doc1 <+> "does not support field operations.") + + PRound -> + custom ("Type" <+> doc1 <+> "does not support rounding operations.") + + PEq -> + custom ("Type" <+> doc1 <+> "does not support equality.") + + PCmp -> + custom ("Type" <+> doc1 <+> "does not support comparisons.") + + PSignedCmp -> + custom ("Type" <+> doc1 <+> "does not support signed comparisons.") + + PLiteral -> + let doc2 = tys !! 1 + in custom (doc1 <+> "is not a valid literal of type" <+> doc2) + + PFLiteral -> + case ts of + ~[m,n,_r,_a] -> + let frac = backticks (ppWithNamesPrec names 4 m <> "/" <> + ppWithNamesPrec names 4 n) + ty = tys !! 3 + in custom (frac <+> "is not a valid literal of type" <+> ty) + + PValidFloat -> + case ts of + ~[e,p] -> + custom ("Unsupported floating point parameters:" $$ + nest 2 ("exponent =" <+> ppWithNames names e $$ + "precision =" <+> ppWithNames names p)) + + + PAnd -> useCtr + PTrue -> useCtr + + _ -> useCtr + + + + -- | This picks the names to use when showing errors and warnings. computeFreeVarNames :: [(Range,Warning)] -> [(Range,Error)] -> NameMap computeFreeVarNames warns errs = diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 99be75750..7e58a3521 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,16 +3,16 @@ Loading module Cryptol Loading module Main [error] at T146.cry:1:18--6:10: - The type ?fv`786 is not sufficiently polymorphic. + The type ?a is not sufficiently polymorphic. It cannot depend on quantified variables: fv`770 When checking type of field 'v0' where - ?fv`786 is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 + ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 fv`770 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: - The type ?fv`788 is not sufficiently polymorphic. + The type ?b is not sufficiently polymorphic. It cannot depend on quantified variables: fv`770 When checking signature variable 'fv' where - ?fv`788 is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 + ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 fv`770 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/T820.icry.stdout b/tests/issues/T820.icry.stdout index 54e3594a6..b63b6350c 100644 --- a/tests/issues/T820.icry.stdout +++ b/tests/issues/T820.icry.stdout @@ -4,15 +4,13 @@ Showing a specific instance of polymorphic result: (ratio 1 2) [error] at :1:1--1:8: - Unsolvable constraints: - • Integral ?a`776 - arising from - use of expression (/) - at :1:1--1:8 - • FLiteral 1 1 0 ?a`776 - arising from - use of fractional literal - at :1:1--1:8 - • Reason: Mutually exclusive goals + • `?a` is not an integral type. + arising from + use of expression (/) + at :1:1--1:8 + • `1/1` is not a valid literal of type `?a` + arising from + use of fractional literal + at :1:1--1:8 where - ?a`776 is type argument 'a' of 'fraction' at :1:1--1:8 + ?a is type argument 'a' of 'fraction' at :1:1--1:8 diff --git a/tests/issues/issue101.icry.stdout b/tests/issues/issue101.icry.stdout index 42f87d8fa..f6c0dd270 100644 --- a/tests/issues/issue101.icry.stdout +++ b/tests/issues/issue101.icry.stdout @@ -1,9 +1,8 @@ Loading module Cryptol [error] at :1:1--1:11: - Unsolvable constraints: - • 0 >= 1 + • Unsolvable constraint: + 0 >= 1 arising from use of partial type function (-) at :1:1--1:11 - • Reason: It is not the case that 0 >= 1 diff --git a/tests/issues/issue582.icry.stdout b/tests/issues/issue582.icry.stdout index 1bb4e3e2b..cf51aa924 100644 --- a/tests/issues/issue582.icry.stdout +++ b/tests/issues/issue582.icry.stdout @@ -1,52 +1,46 @@ Loading module Cryptol [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (/^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (/^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:16: - Unsolvable constraints: - • 0 >= 1 + • Unsolvable constraint: + 0 >= 1 arising from use of partial type function (/^) at :1:1--1:16 - • Reason: It is not the case that 0 >= 1 [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (%^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:18: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of partial type function (%^) at :1:1--1:18 - • Reason: Expected a finite type, but found `inf`. [error] at :1:1--1:16: - Unsolvable constraints: - • 0 >= 1 + • Unsolvable constraint: + 0 >= 1 arising from use of partial type function (%^) at :1:1--1:16 - • Reason: It is not the case that 0 >= 1 Loading module Cryptol Loading module Main diff --git a/tests/issues/issue835.icry.stdout b/tests/issues/issue835.icry.stdout index 6e6137910..13187f61b 100644 --- a/tests/issues/issue835.icry.stdout +++ b/tests/issues/issue835.icry.stdout @@ -3,9 +3,7 @@ Loading module Cryptol Loading module Float [error] at :1:1--1:28: - Unsolvable constraints: - • SignedCmp (Float 5 11) - arising from - use of expression (<$) - at :1:1--1:28 - • Reason: Type 'Float' does not support signed comparisons. + • Type `Float 5 11` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:28 diff --git a/tests/issues/issue845.icry.stdout b/tests/issues/issue845.icry.stdout index 35e922401..1a48ca0db 100644 --- a/tests/issues/issue845.icry.stdout +++ b/tests/issues/issue845.icry.stdout @@ -27,45 +27,35 @@ Loading module Main (ratio 1 2) [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral 1 0 0 Rational - arising from - use of fractional literal - at :1:1--1:9 - • Reason: Fractions may not have 0 as the denominator. + • `1/0` is not a valid literal of type `Rational` + arising from + use of fractional literal + at :1:1--1:9 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral inf 2 0 Rational - arising from - use of fractional literal - at :1:1--1:9 - • Reason: Fractions may not use `inf` + • `inf/2` is not a valid literal of type `Rational` + arising from + use of fractional literal + at :1:1--1:9 Loading module Cryptol Loading module Float 0x0.8 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral 1 0 0 Float64 - arising from - use of fractional literal - at :1:1--1:9 - • Reason: Fractions may not have 0 as the denominator. + • `1/0` is not a valid literal of type `Float64` + arising from + use of fractional literal + at :1:1--1:9 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral inf 2 0 Float64 - arising from - use of fractional literal - at :1:1--1:9 - • Reason: Fractions may not use `inf` + • `inf/2` is not a valid literal of type `Float64` + arising from + use of fractional literal + at :1:1--1:9 0x0.2 [error] at :1:1--1:9: - Unsolvable constraints: - • FLiteral 1 10 1 (Float 3 2) - arising from - use of fractional literal - at :1:1--1:9 - • Reason: 1/10 cannot be represented in Float 3 2 + • `1/10` is not a valid literal of type `Float 3 2` + arising from + use of fractional literal + at :1:1--1:9 diff --git a/tests/issues/issue910.icry.stdout b/tests/issues/issue910.icry.stdout index 231673c25..6341a306c 100644 --- a/tests/issues/issue910.icry.stdout +++ b/tests/issues/issue910.icry.stdout @@ -1,29 +1,25 @@ Loading module Cryptol [error] at :1:1--1:21: - Unsolvable constraints: - • Integral ?a`778 - arising from - use of expression (@) - at :1:8--1:21 - • Field ?a`778 - arising from - use of expression (/.) - at :1:14--1:20 - • Reason: Mutually exclusive goals + • `?a` is not an integral type. + arising from + use of expression (@) + at :1:8--1:21 + • Type `?a` does not support field operations. + arising from + use of expression (/.) + at :1:14--1:20 where - ?a`778 is type argument 'a' of '(/.)' at :1:14--1:20 + ?a is type argument 'a' of '(/.)' at :1:14--1:20 [error] at :1:1--1:16: - Unsolvable constraints: - • Integral ?a`776 - arising from - use of expression (@) - at :1:8--1:16 - • FLiteral 6 5 0 ?a`776 - arising from - use of fractional literal - at :1:13--1:16 - • Reason: Mutually exclusive goals + • `?a` is not an integral type. + arising from + use of expression (@) + at :1:8--1:16 + • `6/5` is not a valid literal of type `?a` + arising from + use of fractional literal + at :1:13--1:16 where - ?a`776 is type argument 'a' of 'fraction' at :1:13--1:16 + ?a is type argument 'a' of 'fraction' at :1:13--1:16 diff --git a/tests/issues/issue913.icry.stdout b/tests/issues/issue913.icry.stdout index 7472047c0..a3ab7aca3 100644 --- a/tests/issues/issue913.icry.stdout +++ b/tests/issues/issue913.icry.stdout @@ -5,9 +5,8 @@ False number`{rep = Bit} : {n} (1 >= n) => Bit [error] at :1:1--1:2: - Unsolvable constraints: - • 1 >= 2 + • Unsolvable constraint: + 1 >= 2 arising from use of literal or demoted expression at :1:1--1:2 - • Reason: It is not the case that 1 >= 2 diff --git a/tests/mono-binds/test04.icry.stdout b/tests/mono-binds/test04.icry.stdout index 377b32b69..f7b58b6d4 100644 --- a/tests/mono-binds/test04.icry.stdout +++ b/tests/mono-binds/test04.icry.stdout @@ -18,9 +18,7 @@ Loading module Cryptol Loading module test04 [error] at test04.cry:1:1--5:14: - Unsolvable constraints: - • Literal 10 () - arising from - use of literal or demoted expression - at test04.cry:3:19--3:21 - • Reason: Type '()' does not support integer literals. + • `10` is not a valid literal of type `()` + arising from + use of literal or demoted expression + at test04.cry:3:19--3:21 diff --git a/tests/regression/float.icry.stdout b/tests/regression/float.icry.stdout index 7524004a0..de525a4e8 100644 --- a/tests/regression/float.icry.stdout +++ b/tests/regression/float.icry.stdout @@ -71,24 +71,20 @@ IEEE-754 floating point numbers. 0x4.0p0 [error] at :1:1--1:20: - Unsolvable constraints: - • FLiteral 5 1 1 Small - arising from - use of fractional literal - at :1:1--1:6 - • Reason: 5/1 cannot be represented in Float 3 2 + • `5/1` is not a valid literal of type `Small` + arising from + use of fractional literal + at :1:1--1:6 0x1.3p0 0x2.0p-4 0x2.0p-4 0x8.0p0 [error] at :1:1--1:2: - Unsolvable constraints: - • Literal 7 Small - arising from - use of literal or demoted expression - at :1:1--1:2 - • Reason: 7 cannot be represented in Float 3 2 + • `7` is not a valid literal of type `Small` + arising from + use of literal or demoted expression + at :1:1--1:2 "-- NaN------------------------------------------------------------------------" fpNaN : {e, p} (ValidFloat e p) => Float e p diff --git a/tests/regression/instance.icry.stdout b/tests/regression/instance.icry.stdout index bce056f4c..2818b2a18 100644 --- a/tests/regression/instance.icry.stdout +++ b/tests/regression/instance.icry.stdout @@ -16,30 +16,24 @@ zero`{Float _ _} : {n, m} (ValidFloat n m) => Float n m complement`{Bit} : Bit -> Bit [error] at :1:1--1:11: - Unsolvable constraints: - • Logic Integer - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Integer' does not support logical operations. + • Type `Integer` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 [error] at :1:1--1:11: - Unsolvable constraints: - • Logic Rational - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Rational' does not support logical operations. + • Type `Rational` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 [error] at :1:1--1:11: - Unsolvable constraints: - • Logic (Z ?n`1011) - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Z' does not support logical operations. + • Type `Z ?m` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 where - ?n`1011 is type wildcard (_) at :1:15--1:16 + ?m is type wildcard (_) at :1:15--1:16 complement`{[_]_} : {n, a} (Logic a) => [n]a -> [n]a complement`{(_ -> _)} : {a, b} (Logic b) => (a -> b) -> a -> b complement`{()} : () -> () @@ -49,23 +43,19 @@ complement`{{x : _, y : _}} : {a, b} (Logic b, Logic a) => {x : a, y : b} -> {x : a, y : b} [error] at :1:1--1:11: - Unsolvable constraints: - • Logic (Float ?n`1025 ?n`1026) - arising from - use of expression complement - at :1:1--1:11 - • Reason: Type 'Float' does not support logical operations. + • Type `Float ?m ?n` does not support logical operations. + arising from + use of expression complement + at :1:1--1:11 where - ?n`1025 is type wildcard (_) at :1:19--1:20 - ?n`1026 is type wildcard (_) at :1:21--1:22 + ?m is type wildcard (_) at :1:19--1:20 + ?n is type wildcard (_) at :1:21--1:22 [error] at :1:1--1:7: - Unsolvable constraints: - • Ring Bit - arising from - use of expression negate - at :1:1--1:7 - • Reason: Type 'Bit' does not support ring operations. + • Type `Bit` does not support ring operations. + arising from + use of expression negate + at :1:1--1:7 negate`{Integer} : Integer -> Integer negate`{Rational} : Rational -> Rational negate`{Z _} : {n} (n >= 1, fin n) => Z n -> Z n @@ -81,259 +71,207 @@ negate`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m [error] at :1:1--1:4: - Unsolvable constraints: - • Integral Bit - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Bit' is not an integral type. + • `Bit` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 (%)`{Integer} : Integer -> Integer -> Integer [error] at :1:1--1:4: - Unsolvable constraints: - • Integral Rational - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Rational' is not an integral type. + • `Rational` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (Z ?n`1049) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Z ?n`1049' is not an integral type. + • `Z ?m` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?n`1049 is type wildcard (_) at :1:8--1:9 + ?m is type wildcard (_) at :1:8--1:9 (%)`{[_]_} : {n, a} (Integral ([n]a)) => [n]a -> [n]a -> [n]a [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (?a`1052 -> ?a`1053) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '?a`1052 -> ?a`1053' is not an integral type. + • `?a -> ?b` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?a`1052 is type wildcard (_) at :1:7--1:8 - ?a`1053 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:7--1:8 + ?b is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral () - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '()' is not an integral type. + • `()` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (?a`1052, ?a`1053) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '(?a`1052, ?a`1053)' is not an integral type. + • `(?a, ?b)` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?a`1052 is type wildcard (_) at :1:7--1:8 - ?a`1053 is type wildcard (_) at :1:10--1:11 + ?a is type wildcard (_) at :1:7--1:8 + ?b is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral {} - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '{}' is not an integral type. + • `{}` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral {x : ?a`1052, y : ?a`1053} - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type '{x : ?a`1052, y : ?a`1053}' is not an integral type. + • `{x : ?a, y : ?b}` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?a`1052 is type wildcard (_) at :1:11--1:12 - ?a`1053 is type wildcard (_) at :1:18--1:19 + ?a is type wildcard (_) at :1:11--1:12 + ?b is type wildcard (_) at :1:18--1:19 [error] at :1:1--1:4: - Unsolvable constraints: - • Integral (Float ?n`1052 ?n`1053) - arising from - use of expression (%) - at :1:1--1:4 - • Reason: Type 'Float ?n`1052 ?n`1053' is not an integral type. + • `Float ?m ?n` is not an integral type. + arising from + use of expression (%) + at :1:1--1:4 where - ?n`1052 is type wildcard (_) at :1:12--1:13 - ?n`1053 is type wildcard (_) at :1:14--1:15 + ?m is type wildcard (_) at :1:12--1:13 + ?n is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: - Unsolvable constraints: - • Field Bit - arising from - use of expression recip - at :1:1--1:6 - • Reason: Type 'Bit' does not support field operations. + • Type `Bit` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Field Integer - arising from - use of expression recip - at :1:1--1:6 - • Reason: Type 'Integer' does not support field operations. + • Type `Integer` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 recip`{Rational} : Rational -> Rational recip`{Z _} : {n} (prime n, n >= 1) => Z n -> Z n [error] at :1:1--1:6: - Unsolvable constraints: - • Field ([?n`1055]?a`1056) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Sequence types do not support field operations. + • Type `[?m]?a` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?n`1055 is type wildcard (_) at :1:9--1:10 - ?a`1056 is type wildcard (_) at :1:11--1:12 + ?m is type wildcard (_) at :1:9--1:10 + ?a is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: - Unsolvable constraints: - • Field (?a`1055 -> ?a`1056) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Function types do not support field operations. + • Type `?a -> ?b` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?a`1055 is type wildcard (_) at :1:9--1:10 - ?a`1056 is type wildcard (_) at :1:14--1:15 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: - Unsolvable constraints: - • Field () - arising from - use of expression recip - at :1:1--1:6 - • Reason: Tuple types do not support field operations. + • Type `()` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Field (?a`1055, ?a`1056) - arising from - use of expression recip - at :1:1--1:6 - • Reason: Tuple types do not support field operations. + • Type `(?a, ?b)` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?a`1055 is type wildcard (_) at :1:9--1:10 - ?a`1056 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: - Unsolvable constraints: - • Field {} - arising from - use of expression recip - at :1:1--1:6 - • Reason: Record types do not support field operations. + • Type `{}` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Field {x : ?a`1055, y : ?a`1056} - arising from - use of expression recip - at :1:1--1:6 - • Reason: Record types do not support field operations. + • Type `{x : ?a, y : ?b}` does not support field operations. + arising from + use of expression recip + at :1:1--1:6 where - ?a`1055 is type wildcard (_) at :1:13--1:14 - ?a`1056 is type wildcard (_) at :1:20--1:21 + ?a is type wildcard (_) at :1:13--1:14 + ?b is type wildcard (_) at :1:20--1:21 recip`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Float n m [error] at :1:1--1:6: - Unsolvable constraints: - • Round Bit - arising from - use of expression floor - at :1:1--1:6 - • Reason: Type 'Bit' does not support rounding operations. + • Type `Bit` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Round Integer - arising from - use of expression floor - at :1:1--1:6 - • Reason: Type 'Integer' does not support rounding operations. + • Type `Integer` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 floor`{Rational} : Rational -> Integer [error] at :1:1--1:6: - Unsolvable constraints: - • Round (Z ?n`1059) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Type 'Z' does not support rounding operations. + • Type `Z ?m` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?n`1059 is type wildcard (_) at :1:10--1:11 + ?m is type wildcard (_) at :1:10--1:11 [error] at :1:1--1:6: - Unsolvable constraints: - • Round ([?n`1059]?a`1060) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Sequence types do not support rounding operations. + • Type `[?m]?a` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?n`1059 is type wildcard (_) at :1:9--1:10 - ?a`1060 is type wildcard (_) at :1:11--1:12 + ?m is type wildcard (_) at :1:9--1:10 + ?a is type wildcard (_) at :1:11--1:12 [error] at :1:1--1:6: - Unsolvable constraints: - • Round (?a`1059 -> ?a`1060) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Function types do not support rounding operations. + • Type `?a -> ?b` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?a`1059 is type wildcard (_) at :1:9--1:10 - ?a`1060 is type wildcard (_) at :1:14--1:15 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:14--1:15 [error] at :1:1--1:6: - Unsolvable constraints: - • Round () - arising from - use of expression floor - at :1:1--1:6 - • Reason: Tuple types do not support rounding operations. + • Type `()` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Round (?a`1059, ?a`1060) - arising from - use of expression floor - at :1:1--1:6 - • Reason: Tuple types do not support rounding operations. + • Type `(?a, ?b)` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?a`1059 is type wildcard (_) at :1:9--1:10 - ?a`1060 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:9--1:10 + ?b is type wildcard (_) at :1:12--1:13 [error] at :1:1--1:6: - Unsolvable constraints: - • Round {} - arising from - use of expression floor - at :1:1--1:6 - • Reason: Record types do not support rounding operations. + • Type `{}` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 [error] at :1:1--1:6: - Unsolvable constraints: - • Round {x : ?a`1059, y : ?a`1060} - arising from - use of expression floor - at :1:1--1:6 - • Reason: Record types do not support rounding operations. + • Type `{x : ?a, y : ?b}` does not support rounding operations. + arising from + use of expression floor + at :1:1--1:6 where - ?a`1059 is type wildcard (_) at :1:13--1:14 - ?a`1060 is type wildcard (_) at :1:20--1:21 + ?a is type wildcard (_) at :1:13--1:14 + ?b is type wildcard (_) at :1:20--1:21 floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{Bit} : Bit -> Bit -> Bit (==)`{Integer} : Integer -> Integer -> Bit @@ -342,15 +280,13 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (==)`{[_]_} : {n, a} (Eq a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • Eq (?a`1070 -> ?a`1071) - arising from - use of expression (==) - at :1:1--1:5 - • Reason: Function types do not support comparisons. + • Type `?a -> ?b` does not support equality. + arising from + use of expression (==) + at :1:1--1:5 where - ?a`1070 is type wildcard (_) at :1:8--1:9 - ?a`1071 is type wildcard (_) at :1:13--1:14 + ?a is type wildcard (_) at :1:8--1:9 + ?b is type wildcard (_) at :1:13--1:14 (==)`{()} : () -> () -> Bit (==)`{(_, _)} : {a, b} (Eq b, Eq a) => (a, b) -> (a, b) -> Bit (==)`{{}} : {} -> {} -> Bit @@ -363,26 +299,22 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer (<)`{Rational} : Rational -> Rational -> Bit [error] at :1:1--1:4: - Unsolvable constraints: - • Cmp (Z ?n`1084) - arising from - use of expression (<) - at :1:1--1:4 - • Reason: Type 'Z' does not support order comparisons. + • Type `Z ?m` does not support comparisons. + arising from + use of expression (<) + at :1:1--1:4 where - ?n`1084 is type wildcard (_) at :1:8--1:9 + ?m is type wildcard (_) at :1:8--1:9 (<)`{[_]_} : {n, a} (Cmp a, fin n) => [n]a -> [n]a -> Bit [error] at :1:1--1:4: - Unsolvable constraints: - • Cmp (?a`1087 -> ?a`1088) - arising from - use of expression (<) - at :1:1--1:4 - • Reason: Function types do not support order comparisons. + • Type `?a -> ?b` does not support comparisons. + arising from + use of expression (<) + at :1:1--1:4 where - ?a`1087 is type wildcard (_) at :1:7--1:8 - ?a`1088 is type wildcard (_) at :1:12--1:13 + ?a is type wildcard (_) at :1:7--1:8 + ?b is type wildcard (_) at :1:12--1:13 (<)`{()} : () -> () -> Bit (<)`{(_, _)} : {a, b} (Cmp b, Cmp a) => (a, b) -> (a, b) -> Bit (<)`{{}} : {} -> {} -> Bit @@ -392,50 +324,40 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer Float n m -> Float n m -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp Bit - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Bit' does not support signed comparisons. + • Type `Bit` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp Integer - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Integer' does not support signed comparisons. + • Type `Integer` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp Rational - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Rational' does not support signed comparisons. + • Type `Rational` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp (Z ?n`1098) - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Z' does not support signed comparisons. + • Type `Z ?m` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 where - ?n`1098 is type wildcard (_) at :1:9--1:10 + ?m is type wildcard (_) at :1:9--1:10 (<$)`{[_]_} : {n, a} (SignedCmp ([n]a)) => [n]a -> [n]a -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp (?a`1101 -> ?a`1102) - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Function types do not support signed comparisons. + • Type `?a -> ?b` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 where - ?a`1101 is type wildcard (_) at :1:8--1:9 - ?a`1102 is type wildcard (_) at :1:13--1:14 + ?a is type wildcard (_) at :1:8--1:9 + ?b is type wildcard (_) at :1:13--1:14 (<$)`{()} : () -> () -> Bit (<$)`{(_, _)} : {a, b} (SignedCmp b, SignedCmp a) => (a, b) -> (a, b) -> Bit @@ -444,15 +366,13 @@ floor`{Float _ _} : {n, m} (ValidFloat n m) => Float n m -> Integer {x : a, y : b} -> {x : a, y : b} -> Bit [error] at :1:1--1:5: - Unsolvable constraints: - • SignedCmp (Float ?n`1109 ?n`1110) - arising from - use of expression (<$) - at :1:1--1:5 - • Reason: Type 'Float' does not support signed comparisons. + • Type `Float ?m ?n` does not support signed comparisons. + arising from + use of expression (<$) + at :1:1--1:5 where - ?n`1109 is type wildcard (_) at :1:13--1:14 - ?n`1110 is type wildcard (_) at :1:15--1:16 + ?m is type wildcard (_) at :1:13--1:14 + ?n is type wildcard (_) at :1:15--1:16 number`{rep = Bit} : {n} (1 >= n) => Bit [error] at :1:1--1:7: @@ -465,61 +385,50 @@ number`{rep = Z _} : {n, m} (m >= 1 + n, m >= 1, fin m, fin n) => number`{rep = [_]_} : {n, m} (m >= width n, fin m, fin n) => [m] [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 (?a`1119 -> ?a`1120) - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '?a`1119 -> ?a`1120' does not support integer literals. + • `?m` is not a valid literal of type `?a -> ?b` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1119 is type wildcard (_) at :1:15--1:16 - ?a`1120 is type wildcard (_) at :1:20--1:21 + ?m is type argument 'val' of 'number' at :1:1--1:7 + ?a is type wildcard (_) at :1:15--1:16 + ?b is type wildcard (_) at :1:20--1:21 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 () - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '()' does not support integer literals. + • `?m` is not a valid literal of type `()` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 + ?m is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 (?a`1119, ?a`1120) - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '(?a`1119, ?a`1120)' does not support integer literals. + • `?m` is not a valid literal of type `(?a, ?b)` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1119 is type wildcard (_) at :1:16--1:17 - ?a`1120 is type wildcard (_) at :1:19--1:20 + ?m is type argument 'val' of 'number' at :1:1--1:7 + ?a is type wildcard (_) at :1:16--1:17 + ?b is type wildcard (_) at :1:19--1:20 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 {} - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '{}' does not support integer literals. + • `?m` is not a valid literal of type `{}` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 + ?m is type argument 'val' of 'number' at :1:1--1:7 [error] at :1:1--1:7: - Unsolvable constraints: - • Literal ?val`1118 {x : ?a`1119, y : ?a`1120} - arising from - use of literal or demoted expression - at :1:1--1:7 - • Reason: Type '{x : ?a`1119, - y : ?a`1120}' does not support integer literals. + • `?m` is not a valid literal of type `{x : ?a, y : ?b}` + arising from + use of literal or demoted expression + at :1:1--1:7 where - ?val`1118 is type argument 'val' of 'number' at :1:1--1:7 - ?a`1119 is type wildcard (_) at :1:20--1:21 - ?a`1120 is type wildcard (_) at :1:27--1:28 + ?m is type argument 'val' of 'number' at :1:1--1:7 + ?a is type wildcard (_) at :1:20--1:21 + ?b is type wildcard (_) at :1:27--1:28 number`{rep = Float _ _} : {n, m, i} (ValidFloat m i, Literal n (Float m i)) => Float m i diff --git a/tests/regression/primes.icry.stdout b/tests/regression/primes.icry.stdout index 9a2ed204a..2233014d9 100644 --- a/tests/regression/primes.icry.stdout +++ b/tests/regression/primes.icry.stdout @@ -49,20 +49,18 @@ Expected test coverage: 0.00% (100 of 2^^1042 values) 1 [error] at :1:1--1:8: - Unsolvable constraints: - • prime 8 + • Unsolvable constraint: + prime 8 arising from use of expression z1prime at :1:1--1:8 - • Reason: 8 is not a prime number [error] at :1:1--1:8: - Unsolvable constraints: - • prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 + • Unsolvable constraint: + prime 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 arising from use of expression z1prime at :1:1--1:8 - • Reason: 43091033305484275771318189120554014028061750499173210735564075069516863836988716943216254409932734872431737796205873180054667648466751626159946491190398490019830895369540999907009814461968819338016648922197947056129 is not a prime number Q.E.D. Q.E.D. Q.E.D. diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout index 127121d75..a2bde3033 100644 --- a/tests/regression/tc-errors.icry.stdout +++ b/tests/regression/tc-errors.icry.stdout @@ -16,20 +16,19 @@ Loading module Cryptol [error] at :1:9--1:10: Matching would result in an infinite type. - The type: ?arg`771 - occurs in: ?arg`771 -> ?res + The type: ?b + occurs in: ?b -> ?a When checking type of function argument where - ?res is type of function result at :1:1--1:10 - ?arg`771 is type of function argument at :1:7--1:10 + ?a is type of function result at :1:1--1:10 + ?b is type of function argument at :1:7--1:10 [error] at :1:1--1:5: - Unsolvable constraints: - • fin inf + • Unsolvable constraint: + fin inf arising from use of expression take at :1:1--1:5 - • Reason: Expected a finite type, but found `inf`. Parse error at :1:8, unexpected: , @@ -85,18 +84,18 @@ Loading module Main [error] at tc-errors-5.cry:2:5--2:7: Inferred type is not sufficiently polymorphic. Quantified variable: a`767 - cannot match type: [0]?a`769 + cannot match type: [0]?a When checking the type of 'Main::f' where - ?a`769 is type of sequence member at tc-errors-5.cry:2:5--2:7 + ?a is type of sequence member at tc-errors-5.cry:2:5--2:7 a`767 is signature variable 'a' at tc-errors-5.cry:1:6--1:7 Loading module Cryptol Loading module Main [error] at tc-errors-6.cry:4:7--4:8: - The type ?x`770 is not sufficiently polymorphic. + The type ?a is not sufficiently polymorphic. It cannot depend on quantified variables: b`771 When checking the type of 'Main::g' where - ?x`770 is the type of 'x' at tc-errors-6.cry:1:3--1:4 + ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4 b`771 is signature variable 'b' at tc-errors-6.cry:3:8--3:9 From 1354cbdf39cee5b9f92ea131c6827faec9fa9b86 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 17 Nov 2020 09:06:11 -0800 Subject: [PATCH 6/6] Update for changes to errors --- cryptol-remote-api/src/CryptolServer/Data/Type.hs | 2 +- cryptol-remote-api/src/CryptolServer/Exceptions.hs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs index c7ea62672..94c9667e8 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Type.hs @@ -50,7 +50,7 @@ instance JSON.ToJSON JSONKind where instance JSON.ToJSON JSONType where toJSON (JSONType ns t) = convert t where - convert (TCon (TError _ _) _) = + convert (TCon (TError {}) _) = -- TODO: figure out what to do in this situation error "JSON conversion of errors is not yet supported" convert (TCon (TC tc) args) = diff --git a/cryptol-remote-api/src/CryptolServer/Exceptions.hs b/cryptol-remote-api/src/CryptolServer/Exceptions.hs index 9d36476d4..deede65bf 100644 --- a/cryptol-remote-api/src/CryptolServer/Exceptions.hs +++ b/cryptol-remote-api/src/CryptolServer/Exceptions.hs @@ -84,7 +84,7 @@ cryptolError modErr warns = (20720, [ ("source", jsonPretty src) , ("errors", jsonList (map jsonShow errs)) ]) - TypeCheckingFailed src errs -> + TypeCheckingFailed src _nameMap errs -> -- TODO: structured error here (20730, [ ("source", jsonPretty src) , ("errors", jsonList (map jsonShow errs)) @@ -119,7 +119,7 @@ cryptolError modErr warns = -- TODO: structured error here jsonList . concatMap (\w -> case w of - TypeCheckWarnings tcwarns -> + TypeCheckWarnings _nameMap tcwarns -> map (jsonPretty . snd) tcwarns RenamerWarnings rnwarns -> map jsonPretty rnwarns)