From 89264d68962ac0995e73a9a2204e9c38207f38b7 Mon Sep 17 00:00:00 2001 From: Bretton Date: Tue, 28 Nov 2023 23:09:25 -0600 Subject: [PATCH 1/4] Apply functor instantiation map to types If a functor contains both a newtype and a type synonym referring to the newtype, then during instantiation we must apply the instantiation map to the types in the functor, so that the type synonym now refers to the instantiated newtype instead. Previously, we only applied type substitutions to the types in the functor, which would replace type variables with concrete types defined in the functor arguments, but would not replace any actual names. (Confusingly, the code refers to the instantiation map as "value substitutions" even though it can contain names in the type namespace. The "type substitutions" and "value substitutions" are better thought of as "TVar -> Type mappings" and "Name -> Name mappings".) Fixes #1590. --- src/Cryptol/TypeCheck/ModuleInstance.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 5839e916d..53a77abfc 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -82,7 +82,7 @@ instance ModuleInstance (ModuleG name) where } instance ModuleInstance Type where - moduleInstance = doTInst + moduleInstance = doTVInst instance ModuleInstance Schema where moduleInstance = doTInst From 9081a0992388749e8cd27b4d4735044d6657d659 Mon Sep 17 00:00:00 2001 From: Bretton Date: Mon, 4 Dec 2023 21:10:40 -0600 Subject: [PATCH 2/4] Add test for #1590 --- tests/issues/issue1590.cry | 14 ++++++++++++++ tests/issues/issue1590.icry | 1 + tests/issues/issue1590.icry.stdout | 3 +++ 3 files changed, 18 insertions(+) create mode 100644 tests/issues/issue1590.cry create mode 100644 tests/issues/issue1590.icry create mode 100644 tests/issues/issue1590.icry.stdout diff --git a/tests/issues/issue1590.cry b/tests/issues/issue1590.cry new file mode 100644 index 000000000..d06d8b0f1 --- /dev/null +++ b/tests/issues/issue1590.cry @@ -0,0 +1,14 @@ +module Main where + +submodule F where + parameter + x : Bit + newtype T = { bit : Bit } + type U = T + +submodule M = submodule F where x = False + +import submodule M + +foo : U +foo = T { bit = True } diff --git a/tests/issues/issue1590.icry b/tests/issues/issue1590.icry new file mode 100644 index 000000000..375899450 --- /dev/null +++ b/tests/issues/issue1590.icry @@ -0,0 +1 @@ +:l issue1590.cry diff --git a/tests/issues/issue1590.icry.stdout b/tests/issues/issue1590.icry.stdout new file mode 100644 index 000000000..57a1d7a1c --- /dev/null +++ b/tests/issues/issue1590.icry.stdout @@ -0,0 +1,3 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main From 75a72205c5c392714eea41a37e45ee1730d133c5 Mon Sep 17 00:00:00 2001 From: Bretton Date: Fri, 8 Dec 2023 12:08:53 -0600 Subject: [PATCH 3/4] Apply functor instantiation map to schemas --- src/Cryptol/TypeCheck/ModuleInstance.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 53a77abfc..49c3c3f8a 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -85,7 +85,7 @@ instance ModuleInstance Type where moduleInstance = doTVInst instance ModuleInstance Schema where - moduleInstance = doTInst + moduleInstance = doTVInst instance ModuleInstance TySyn where moduleInstance ts = From c55df0494b7ca12a881a57e4e8283786bfb76c07 Mon Sep 17 00:00:00 2001 From: Bretton Date: Fri, 8 Dec 2023 12:50:24 -0600 Subject: [PATCH 4/4] Rename confusing names in ModuleInstance --- src/Cryptol/TypeCheck/Module.hs | 4 +-- src/Cryptol/TypeCheck/ModuleInstance.hs | 38 +++++++++++++------------ 2 files changed, 22 insertions(+), 20 deletions(-) diff --git a/src/Cryptol/TypeCheck/Module.hs b/src/Cryptol/TypeCheck/Module.hs index 4852591c6..58cd440b6 100644 --- a/src/Cryptol/TypeCheck/Module.hs +++ b/src/Cryptol/TypeCheck/Module.hs @@ -53,8 +53,8 @@ doFunctorInst m f as instMap0 enclosingInScope doc = let (tySus,paramTySyns,decls,paramInstMaps) = unzip4 [ (su,ts,ds,im) | DefinedInst su ts ds im <- as2 ] instMap <- addMissingTySyns mpath mf instMap0 - let ?tSu = mergeDistinctSubst tySus - ?vSu = instMap <> mconcat paramInstMaps + let ?tVarSu = mergeDistinctSubst tySus + ?nameSu = instMap <> mconcat paramInstMaps let m1 = moduleInstance mf m2 = m1 { mName = m , mDoc = Nothing diff --git a/src/Cryptol/TypeCheck/ModuleInstance.hs b/src/Cryptol/TypeCheck/ModuleInstance.hs index 49c3c3f8a..fdc6a893b 100644 --- a/src/Cryptol/TypeCheck/ModuleInstance.hs +++ b/src/Cryptol/TypeCheck/ModuleInstance.hs @@ -14,21 +14,23 @@ import Cryptol.TypeCheck.AST import Cryptol.TypeCheck.Subst(Subst,TVars,apSubst) -{- | `?tSu` should be applied to all types. - `?vSu` shoudl be applied to all values. -} -type Su = (?tSu :: Subst, ?vSu :: Map Name Name) +{- | `?tVarSu` substitutes 'Type's for 'TVar's which are module type parameters. + `?nameSu` substitutes fresh 'Name's for the functor's 'Name's + (in all namespaces). -} +type Su = (?tVarSu :: Subst, ?nameSu :: Map Name Name) --- | Has value names but no types. -doVInst :: (Su, TraverseNames a) => a -> a -doVInst = mapNames (\x -> Map.findWithDefault x x ?vSu) +-- | Instantiate something that has 'Name's. +doNameInst :: (Su, TraverseNames a) => a -> a +doNameInst = mapNames (\x -> Map.findWithDefault x x ?nameSu) --- | Has types but not values. -doTInst :: (Su, TVars a) => a -> a -doTInst = apSubst ?tSu +-- | Instantiate something that has 'TVar's. +doTVarInst :: (Su, TVars a) => a -> a +doTVarInst = apSubst ?tVarSu --- | Has both value names and types. -doTVInst :: (Su, TVars a, TraverseNames a) => a -> a -doTVInst = doVInst . doTInst +-- | Instantiate something that has both 'TVar's and 'Name's. +-- Order is important here because '?tVarSu' might insert 'Name's. +doInst :: (Su, TVars a, TraverseNames a) => a -> a +doInst = doNameInst . doTVarInst doMap :: (Su, ModuleInstance a) => Map Name a -> Map Name a doMap mp = @@ -50,10 +52,10 @@ instance ModuleInstance a => ModuleInstance (Located a) where moduleInstance l = moduleInstance <$> l instance ModuleInstance Name where - moduleInstance = doVInst + moduleInstance = doNameInst instance ModuleInstance NamingEnv where - moduleInstance = mapNamingEnv doVInst + moduleInstance = mapNamingEnv doNameInst instance ModuleInstance name => ModuleInstance (ImpName name) where moduleInstance x = @@ -65,7 +67,7 @@ instance ModuleInstance (ModuleG name) where moduleInstance m = Module { mName = mName m , mDoc = Nothing - , mExports = doVInst (mExports m) + , mExports = doNameInst (mExports m) , mParamTypes = doMap (mParamTypes m) , mParamFuns = doMap (mParamFuns m) , mParamConstraints = moduleInstance (mParamConstraints m) @@ -82,10 +84,10 @@ instance ModuleInstance (ModuleG name) where } instance ModuleInstance Type where - moduleInstance = doTVInst + moduleInstance = doInst instance ModuleInstance Schema where - moduleInstance = doTVInst + moduleInstance = doInst instance ModuleInstance TySyn where moduleInstance ts = @@ -123,7 +125,7 @@ instance ModuleInstance DeclGroup where NonRecursive d -> NonRecursive (moduleInstance d) instance ModuleInstance Decl where - moduleInstance = doTVInst + moduleInstance = doInst instance ModuleInstance name => ModuleInstance (IfaceNames name) where