From 0cefb92ba956eb99942be431d49feff016857955 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 13 Oct 2022 12:41:10 +0300 Subject: [PATCH] Don't use syntactic equality for numeric types, collect constraints instead Fixes #1451 --- src/Cryptol/ModuleSystem/Base.hs | 3 +- src/Cryptol/TypeCheck/Sanity.hs | 92 +++++++++++++++++++++++--------- 2 files changed, 70 insertions(+), 25 deletions(-) diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 4e39fc7a1..f3d36b9fe 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -565,7 +565,8 @@ exprLinter = TCLinter case TcSanity.tcExpr i e' of Left err -> Left err Right (s1,os) - | TcSanity.same s s1 -> Right os + | TcSanity.SameIf os' <- TcSanity.same s s1 -> + Right (map T.tMono os' ++ os) | otherwise -> Left ( fromMaybe emptyRange (getLoc e') , TcSanity.TypeMismatch "exprLinter" s s1 ) diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index 6eb8038c3..dcd5aa11e 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -12,6 +12,7 @@ module Cryptol.TypeCheck.Sanity , tcModule , ProofObligation , Error(..) + , AreSame(..) , same ) where @@ -110,23 +111,68 @@ checkSchema (Forall as ps t) = foldr withTVar check as where check = do mapM_ (checkTypeIs KProp) ps checkTypeIs KType t +data AreSame = SameIf [Prop] + | NotSame + +areSame :: AreSame +areSame = SameIf [] + +sameAnd :: AreSame -> AreSame -> AreSame +sameAnd x y = + case (x,y) of + (SameIf xs, SameIf ys) -> SameIf (xs ++ ys) + _ -> NotSame + +sameBool :: Bool -> AreSame +sameBool b = if b then areSame else NotSame + +sameTypes :: String -> Type -> Type -> TcM () +sameTypes msg x y = sameSchemas msg (tMono x) (tMono y) + +sameSchemas :: String -> Schema -> Schema -> TcM () +sameSchemas msg x y = + case same x y of + NotSame -> reportError (TypeMismatch msg x y) + SameIf ps -> mapM_ proofObligation ps + + + class Same a where - same :: a -> a -> Bool + same :: a -> a -> AreSame instance Same a => Same [a] where - same [] [] = True - same (x : xs) (y : ys) = same x y && same xs ys - same _ _ = False + same [] [] = areSame + same (x : xs) (y : ys) = same x y `sameAnd` same xs ys + same _ _ = NotSame + +data Field a b = Field a b + +instance (Eq a, Same b) => Same (Field a b) where + same (Field x a) (Field y b) = sameBool (x == y) `sameAnd` same a b instance Same Type where - same t1 t2 = tNoUser t1 == tNoUser t2 + same t1 t2 + | k1 /= k2 = NotSame + | k1 == KNum = if t1 == t2 then SameIf [] else SameIf [ t1 =#= t2 ] + | otherwise = + case (tNoUser t1, tNoUser t2) of + (TVar x, TVar y) -> sameBool (x == y) + (TRec x, TRec y) -> same (mkRec x) (mkRec y) + (TNewtype x xs, TNewtype y ys) -> same (Field x xs) (Field y ys) + (TCon x xs, TCon y ys) -> same (Field x xs) (Field y ys) + _ -> NotSame + where + k1 = kindOf t1 + k2 = kindOf t2 + mkRec r = [ Field x y | (x,y) <- canonicalFields r ] instance Same Schema where - same (Forall xs ps s) (Forall ys qs t) = same xs ys && same ps qs && same s t + same (Forall xs ps s) (Forall ys qs t) = + same xs ys `sameAnd` same ps qs `sameAnd` same s t instance Same TParam where - same x y = tpName x == tpName y && tpKind x == tpKind y + same x y = sameBool (tpName x == tpName y && tpKind x == tpKind y) @@ -156,8 +202,7 @@ exprSchema expr = do checkTypeIs KType t forM_ es $ \e -> do t1 <- exprType e - unless (same t1 t) $ - reportError $ TypeMismatch "EList" (tMono t) (tMono t1) + sameTypes "EList" t1 t return $ tMono $ tSeq (tNum (length es)) t @@ -172,9 +217,7 @@ exprSchema expr = do ty <- exprType e expe <- checkHas ty x has <- exprType v - unless (same expe has) $ - reportError $ - TypeMismatch "ESet" (tMono expe) (tMono has) + sameTypes "ESet" expe has return (tMono ty) ESel e sel -> do ty <- exprType e @@ -183,13 +226,11 @@ exprSchema expr = EIf e1 e2 e3 -> do ty <- exprType e1 - unless (same tBit ty) $ - reportError $ TypeMismatch "EIf_condition" (tMono tBit) (tMono ty) + sameTypes "EIf_condition" tBit ty t1 <- exprType e2 t2 <- exprType e3 - unless (same t1 t2) $ - reportError $ TypeMismatch "EIf_arms" (tMono t1) (tMono t2) + sameTypes "EIf_arms" t1 t2 return $ tMono t1 @@ -241,7 +282,9 @@ exprSchema expr = case tNoUser t1 of TCon (TC TCFun) [ a, b ] - | same a t2 -> return (tMono b) + | SameIf ps <- same a t2 -> + do mapM_ proofObligation ps + return (tMono b) tf -> reportError (BadApplication tf t1) @@ -412,12 +455,11 @@ checkDecl checkSig d = do let s = dSignature d when checkSig $ checkSchema s s1 <- exprSchema e - unless (same s s1) $ - let nm = dName d - loc = "definition of " ++ show (pp nm) ++ - ", at " ++ show (pp (nameLoc nm)) - in reportError $ TypeMismatch loc s s1 - + let nm = dName d + loc = "definition of " ++ show (pp nm) ++ + ", at " ++ show (pp (nameLoc nm)) + sameSchemas loc s s1 + return (dName d, s) checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)] @@ -441,7 +483,9 @@ checkMatch ma = t1 <- exprType e case tNoUser t1 of TCon (TC TCSeq) [ l, el ] - | same elt el -> return ((x, tMono elt), l) + | SameIf ps <- same elt el -> + do mapM_ proofObligation ps + return ((x, tMono elt), l) | otherwise -> reportError $ TypeMismatch "From" (tMono elt) (tMono el)