diff --git a/src/Cryptol/TypeCheck/Default.hs b/src/Cryptol/TypeCheck/Default.hs index fb9263bcc..a6831a1cb 100644 --- a/src/Cryptol/TypeCheck/Default.hs +++ b/src/Cryptol/TypeCheck/Default.hs @@ -25,8 +25,8 @@ defaultLiterals as gs = let (binds,warns) = unzip (mapMaybe tryDefVar as) gSet = goalsFromList gs tryDefVar a = do gt <- Map.lookup a (literalGoals gSet) - d <- tvInfo a - let defT = tWord (tWidth (goal gt)) + let d = tvInfo a + defT = tWord (tWidth (goal gt)) w = DefaultingTo d defT guard (not (Set.member a (fvs defT))) -- Currently shouldn't happen -- but future proofing. diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index 31143ebeb..1d5d9ab18 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -179,14 +179,15 @@ instance FVS Error where UnsolvedGoals _ gs -> fvs gs UnsolvedDelayedCt g -> fvs g UnexpectedTypeWildCard -> Set.empty - TypeVariableEscaped t _ -> fvs t - NotForAll _ t -> fvs t + TypeVariableEscaped t xs -> fvs t `Set.union` + Set.fromList (map TVBound xs) + NotForAll x t -> Set.insert x (fvs t) UnusableFunction _ p -> fvs p TooManyPositionalTypeParams -> Set.empty CannotMixPositionalAndNamedTypeParams -> Set.empty - AmbiguousType _ _vs -> Set.empty - UndefinedTypeParameter {} -> Set.empty - RepeatedTypeParameter {} -> Set.empty + AmbiguousType _ _vs -> Set.empty + UndefinedTypeParameter {} -> Set.empty + RepeatedTypeParameter {} -> Set.empty diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 023f0d548..e9df8ad43 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -39,7 +39,7 @@ import Cryptol.Utils.PP import qualified Data.Map as Map import Data.Map (Map) import qualified Data.Set as Set -import Data.List(foldl') +import Data.List(foldl',sortBy) import Data.Either(partitionEithers) import Data.Maybe(mapMaybe,isJust, fromMaybe) import Data.List(partition,find) @@ -236,7 +236,7 @@ checkE expr tGoal = do let src = case l of RecordSel la _ -> TypeOfRecordField la TupleSel n _ -> TypeOfTupleField n - ListSel n _ -> TypeOfSeqAt n + ListSel _ _ -> TypeOfSeqElement t <- newType src KType e' <- checkE e t f <- newHasGoal l t tGoal @@ -727,7 +727,8 @@ generalize bs0 gs0 = {- This is the variables we'll be generalizing: * any ones that survived the defaulting * and vars in the inferred types that do not appear anywhere else. -} - let as = as0 ++ Set.toList (Set.difference inSigs asmpVs) + let as = sortBy numFst + $ as0 ++ Set.toList (Set.difference inSigs asmpVs) asPs = [ TParam { tpUnique = x, tpKind = k, tpFlav = TPOther Nothing , tpInfo = i } | TVFree x k _ i <- as ] @@ -750,6 +751,12 @@ generalize bs0 gs0 = return (map genB bs) + where + numFst x y = case (kindOf x, kindOf y) of + (KNum, KNum) -> EQ + (KNum, _) -> LT + (_,KNum) -> GT + _ -> EQ -- | Check a monomorphic binding. checkMonoB :: P.Bind Name -> Type -> InferM Decl diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index fac38092f..5020f5c1c 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -242,9 +242,8 @@ addTVarsDescs nm t d | Set.null vs = d | otherwise = d $$ text "where" $$ vcat (map desc (Set.toList vs)) where - vs = Set.filter isFreeTV (fvs t) - desc v@(TVFree _ _ _ x) = ppWithNames nm v <+> text "is" <+> pp x - desc (TVBound {}) = empty + vs = fvs t -- Set.filter isFreeTV (fvs t) + desc v = ppWithNames nm v <+> text "is" <+> pp (tvInfo v) diff --git a/src/Cryptol/TypeCheck/PP.hs b/src/Cryptol/TypeCheck/PP.hs index e7da23ff9..c6b4440a1 100644 --- a/src/Cryptol/TypeCheck/PP.hs +++ b/src/Cryptol/TypeCheck/PP.hs @@ -12,7 +12,7 @@ module Cryptol.TypeCheck.PP ( NameMap, WithNames(..) , emptyNameMap , ppWithNamesPrec, ppWithNames - , intToName, nameList + , nameList , dump , module Cryptol.Utils.PP ) where @@ -57,6 +57,4 @@ nameList names = concat $ transpose $ map nameVariants baseNames baseNames | null names = map (:[]) [ 'a' .. 'z' ] | otherwise = names -intToName :: Int -> String -intToName x = nameList [] !! x diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index fa77b55bc..ce2f2f98c 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -124,11 +124,11 @@ data TVar = TVFree !Int Kind (Set TParam) TVarInfo | TVBound {-# UNPACK #-} !TParam deriving (Show, Generic, NFData) -tvInfo :: TVar -> Maybe TVarInfo +tvInfo :: TVar -> TVarInfo tvInfo tv = case tv of - TVFree _ _ _ d -> Just d - _ -> Nothing + TVFree _ _ _ d -> d + TVBound tp -> tpInfo tp data TVarInfo = TVarInfo { tvarSource :: Range -- ^ Source code that gave rise , tvarDesc :: TVarSource -- ^ Description @@ -141,7 +141,6 @@ data TVarSource = TVFromModParam Name -- ^ Name of module parameter | TypeWildCard | TypeOfRecordField Ident | TypeOfTupleField Int - | TypeOfSeqAt Int | TypeOfSeqElement | LenOfSeq | TypeParamInstNamed {-Fun-}Name {-Param-}Ident @@ -784,14 +783,18 @@ instance PP (WithNames TParam) where addTNames :: [TParam] -> NameMap -> NameMap addTNames as ns = foldr (uncurry IntMap.insert) ns - $ named ++ zip unnamed avail + $ named ++ zip unnamed_nums numNames + ++ zip unnamed_vals valNames - where avail = filter (`notElem` used) (nameList []) + where avail xs = filter (`notElem` used) (nameList xs) + numNames = avail ["n","m","i","j","k"] + valNames = avail ["a","b","c","d","e"] - nm x = (tpUnique x, tpName x) + nm x = (tpUnique x, tpName x, tpKind x) - named = [ (u,show (pp n)) | (u,Just n) <- map nm as ] - unnamed = [ u | (u,Nothing) <- map nm as ] + named = [ (u,show (pp n)) | (u,Just n,_) <- map nm as ] + unnamed_nums = [ u | (u,Nothing,KNum) <- map nm as ] + unnamed_vals = [ u | (u,Nothing,KType) <- map nm as ] used = map snd named ++ IntMap.elems ns @@ -809,7 +812,7 @@ instance PP Schema where instance PP (WithNames Schema) where ppPrec _ (WithNames s ns) | null (sVars s) && null (sProps s) = body - | otherwise = hang (vars <+> props) 2 body + | otherwise = hang (vars <+> props) 2 body where body = ppWithNames ns1 (sType s) @@ -921,11 +924,39 @@ instance PP (WithNames TVar) where Just a -> text a Nothing -> case tpFlav x of - TPModParam n -> ppPrefixName n - _ -> text ("a`" ++ show (tpUnique x)) - - ppPrec _ (WithNames (TVFree x _ _ _) _) = - char '?' <.> text (intToName x) + 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 + +pickTVarName :: Kind -> TVarSource -> Int -> Doc +pickTVarName k src uni = + text $ + case src of + TVFromModParam n -> using n + TVFromSignature n -> using n + TypeWildCard -> case k of + KNum -> "n" + _ -> "a" + TypeOfRecordField i -> using i + TypeOfTupleField n -> mk ("tup_" ++ show n) + TypeOfSeqElement -> mk "a" + LenOfSeq -> mk "n" + TypeParamInstNamed _ i -> using i + TypeParamInstPos f n -> mk (sh f ++ "_" ++ show n) + DefinitionOf x -> using x + LenOfCompGen -> mk "n" + TypeOfArg mb -> mk (case mb of + Nothing -> "arg" + Just n -> "arg_" ++ show n) + TypeOfRes -> "res" + TypeErrorPlaceHolder -> "err" + where + sh a = show (pp a) + using a = mk (sh a) + mk a = a ++ "`" ++ show uni instance PP TVar where ppPrec = ppWithNamesPrec IntMap.empty @@ -1006,11 +1037,10 @@ instance PP TVarSource where ppPrec _ tvsrc = case tvsrc of TVFromModParam m -> "module parameter" <+> pp m - TVFromSignature x -> "type variable" <+> quotes (pp x) + TVFromSignature x -> "signature variable" <+> quotes (pp x) TypeWildCard -> "type wildcard (_)" TypeOfRecordField l -> "type of field" <+> quotes (pp l) TypeOfTupleField n -> "type of" <+> ordinal n <+> "tuple field" - TypeOfSeqAt n -> "type of" <+> ordinal n <+> "sequence member" TypeOfSeqElement -> "type of sequence member" LenOfSeq -> "length of sequnce" TypeParamInstNamed f i -> "type argument" <+> quotes (pp i) <+> diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index 2086ca48f..b368fe949 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -3,12 +3,14 @@ Loading module Cryptol Loading module Main [error] at ./T146.cry:1:18--6:10: - The type ?s33 is not sufficiently polymorphic. - It cannot depend on quantified variables: a`860 + The type ?fv`876 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`860 where - ?s33 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24 + ?fv`876 is type argument 'fv' of 'Main::ec_v1' at ./T146.cry:4:19--4:24 + fv`860 is signature variable 'fv' at ./T146.cry:11:10--11:12 [error] at ./T146.cry:5:19--5:24: - The type ?u33 is not sufficiently polymorphic. - It cannot depend on quantified variables: a`860 + The type ?fv`878 is not sufficiently polymorphic. + It cannot depend on quantified variables: fv`860 where - ?u33 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24 + ?fv`878 is type argument 'fv' of 'Main::ec_v2' at ./T146.cry:5:19--5:24 + fv`860 is signature variable 'fv' at ./T146.cry:11:10--11:12 diff --git a/tests/issues/issue150.icry.stdout b/tests/issues/issue150.icry.stdout index 1d3bf0f96..e42f8b36e 100644 --- a/tests/issues/issue150.icry.stdout +++ b/tests/issues/issue150.icry.stdout @@ -1,4 +1,4 @@ Loading module Cryptol Loading module Cryptol Loading module Main -maxSeq' : {a, b} (Cmp a, Literal 0 a) => [b]a -> [1 + b]a +maxSeq' : {n, a} (Cmp a, Literal 0 a) => [n]a -> [1 + n]a diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 0ba5e9c4e..d8ee3ccf6 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,7 +4,9 @@ Loading module Main [error] at ./issue290v2.cry:2:1--2:19: Unsolved constraints: - a`857 == 1 + n`857 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at ./issue290v2.cry:2:8--2:11 + where + n`857 is signature variable 'n' at ./issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue410.icry.stdout b/tests/issues/issue410.icry.stdout index 19021e877..3388e4c21 100644 --- a/tests/issues/issue410.icry.stdout +++ b/tests/issues/issue410.icry.stdout @@ -1,8 +1,8 @@ Loading module Cryptol -{a, b} (Logic b) => a == min (1 + a) a -{a, b} (Logic b) => Logic b -{a, b} (Logic b) => Logic b -{a, b} (Logic b) => True +{n, a} (Logic a) => n == min (1 + n) n +{n, a} (Logic a) => Logic a +{n, a} (Logic a) => Logic a +{n, a} (Logic a) => True (s where s x = @@ -11,11 +11,11 @@ Loading module Cryptol bs = [complement b | b <- [complement x] # bs | _ <- bs] ) - ) : {a, b} (Logic b) => b -> [a]b -{a, b} a == a + ) : {n, a} (Logic a) => a -> [n]a +{n, a} n == n (bs where bs = [b | b <- bs] - ) : {a, b} [a]b + ) : {n, a} [n]a 1 == 1 [b | b <- [True]] : [1] diff --git a/tests/mono-binds/test01.icry.stdout b/tests/mono-binds/test01.icry.stdout index bcb9eaaf0..7eca45cc3 100644 --- a/tests/mono-binds/test01.icry.stdout +++ b/tests/mono-binds/test01.icry.stdout @@ -4,13 +4,13 @@ Loading module test01 module test01 import Cryptol /* Not recursive */ -test01::a : {a, b} (fin a) => [a]b -> [2 * a]b -test01::a = \{a, b} (fin a) (x : [a]b) -> - test01::f a x +test01::a : {n, a} (fin n) => [n]a -> [2 * n]a +test01::a = \{n, a} (fin n) (x : [n]a) -> + test01::f n x where /* Not recursive */ - test01::f : {c} [c]b -> [a + c]b - test01::f = \{c} (y : [c]b) -> (Cryptol::#) a c b <> x y + test01::f : {m} [m]a -> [n + m]a + test01::f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y @@ -19,13 +19,13 @@ Loading module test01 module test01 import Cryptol /* Not recursive */ -test01::a : {a, b} (fin a) => [a]b -> [2 * a]b -test01::a = \{a, b} (fin a) (x : [a]b) -> +test01::a : {n, a} (fin n) => [n]a -> [2 * n]a +test01::a = \{n, a} (fin n) (x : [n]a) -> test01::f x where /* Not recursive */ - test01::f : [a]b -> [2 * a]b - test01::f = \ (y : [a]b) -> (Cryptol::#) a a b <> x y + test01::f : [n]a -> [2 * n]a + test01::f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y diff --git a/tests/mono-binds/test05.icry.stdout b/tests/mono-binds/test05.icry.stdout index f3ae1e198..18814fd77 100644 --- a/tests/mono-binds/test05.icry.stdout +++ b/tests/mono-binds/test05.icry.stdout @@ -14,27 +14,27 @@ test05::foo : [10] test05::foo = Cryptol::demote 10 [10] <> /* Not recursive */ -test05::test : {a, b, c} (Zero b, Literal 10 c) => [a]b -> c -test05::test = \{a, b, c} (Zero b, Literal 10 c) (a : [a]b) -> - Cryptol::demote 10 c <> +test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b +test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) -> + Cryptol::demote 10 b <> where /* Not recursive */ test05::foo : [10] test05::foo = Cryptol::demote 10 [10] <> /* Not recursive */ - test05::f : {d} (fin d) => [a + d]b - test05::f = \{d} (fin d) -> - test05::bar d <> + test05::f : {m} (fin m) => [n + m]a + test05::f = \{m} (fin m) -> + test05::bar m <> where /* Not recursive */ - test05::foo : [a]b + test05::foo : [n]a test05::foo = a /* Not recursive */ - test05::bar : {e} (fin e) => [e + a]b - test05::bar = \{e} (fin e) -> - (Cryptol::#) e a b <> (Cryptol::zero ([e]b) <>) test05::foo + test05::bar : {i} (fin i) => [i + n]a + test05::bar = \{i} (fin i) -> + (Cryptol::#) i n a <> (Cryptol::zero ([i]a) <>) test05::foo @@ -57,25 +57,25 @@ test05::foo : [10] test05::foo = Cryptol::demote 10 [10] <> /* Not recursive */ -test05::test : {a, b, c} (Zero b, Literal 10 c) => [a]b -> c -test05::test = \{a, b, c} (Zero b, Literal 10 c) (a : [a]b) -> - Cryptol::demote 10 c <> +test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b +test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) -> + Cryptol::demote 10 b <> where /* Not recursive */ test05::foo : [10] test05::foo = Cryptol::demote 10 [10] <> /* Not recursive */ - test05::f : [a]b + test05::f : [n]a test05::f = test05::bar where /* Not recursive */ - test05::foo : [a]b + test05::foo : [n]a test05::foo = a /* Not recursive */ - test05::bar : [a]b - test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b) <>) test05::foo + test05::bar : [n]a + test05::bar = (Cryptol::#) 0 n a <> (Cryptol::zero ([0]a) <>) test05::foo