Merge pull request #1592 from GaloisInc/T1590

Apply functor instantiation map to types

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

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 = doTInst
+  moduleInstance = doInst
 
 instance ModuleInstance Schema where
-  moduleInstance = doTInst
+  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

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 }

tests/issues/issue1590.icry

@@ -0,0 +1 @@
+:l issue1590.cry

tests/issues/issue1590.icry.stdout

@@ -0,0 +1,3 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main