Qualify FromFunctorInst OrigNames by interface

src/Cryptol/ModuleSystem/Binds.hs

@@ -13,6 +13,7 @@ module Cryptol.ModuleSystem.Binds
   , topModuleDefs
   , topDeclsDefs
   , newModParam
+  , newFunctorInst
   , InModule(..)
   , ifaceToMod
   , ifaceSigToMod
@@ -420,6 +421,13 @@ newLocal ns thing rng = liftSupply (mkLocal ns (getIdent thing) rng)
 newModParam :: FreshM m => ModPath -> Ident -> Range -> Name -> m Name
 newModParam m i rng n = liftSupply (mkModParam m i rng n)
 
+-- | Given a name in a functor, make a fresh name for the corresponding thing in
+-- the instantiation.
+--
+-- The 'ModPath' should be the instantiation not the functor.
+newFunctorInst :: FreshM m => ModPath -> Name -> m Name
+newFunctorInst m n = liftSupply (freshNameFor m n)
+
 
 {- | Do something in the context of a module.
 If `Nothing` than we are working with a local declaration.

src/Cryptol/ModuleSystem/Name.hs

@@ -148,9 +148,9 @@ cmpNameDisplay disp l r =
                  NotInScope  ->
                     let m = Text.pack (show (pp (ogModule og)))
                     in
-                    case ogSource og of
-                      FromModParam q  -> m <> "::" <> Text.pack (show (pp q))
-                      _ -> m
+                    case ogFromParam og of
+                      Just q  -> m <> "::" <> Text.pack (show (pp q))
+                      Nothing -> m
 
   -- Note that this assumes that `xs` is `l` and `ys` is `r`
   cmpText xs ys =
@@ -229,8 +229,8 @@ nameLoc  = nLoc
 nameFixity :: Name -> Maybe Fixity
 nameFixity = nFixity
 
--- | We only qualify the 'PName' with the interface name from 'FromModParam' in
--- 'ogSource', if any. We don't qualify with the 'ModPath'.
+-- | We only qualify the 'PName' with the interface name from 'ogFromParam'. We
+-- don't qualify with the 'ogModule'.
 asPName :: Name -> PName
 asPName n =
   case nInfo n of
@@ -242,7 +242,7 @@ asPrim :: Name -> Maybe PrimIdent
 asPrim n =
   case nInfo n of
     GlobalName _ og
-      | TopModule m <- ogModule og, not (ogFromModParam og) ->
+      | TopModule m <- ogModule og, not (ogIsModParam og) ->
         Just $ PrimIdent m $ identText $ ogName og
 
     _ -> Nothing
@@ -381,6 +381,7 @@ mkDeclared ns m sys ident fixity loc s = (name, s')
                                 , ogModule    = m
                                 , ogName      = ident
                                 , ogSource    = FromDefinition
+                                , ogFromParam = Nothing
                                 }
               }
 
@@ -420,7 +421,8 @@ mkModParam own pname rng n s = (name, s')
                               { ogModule    = own
                               , ogName      = nameIdent n
                               , ogNamespace = nameNamespace n
-                              , ogSource    = FromModParam pname
+                              , ogSource    = FromModParam
+                              , ogFromParam = Just pname
                               }
               , nFixity = nFixity n
               , nLoc    = rng

src/Cryptol/ModuleSystem/NamingEnv.hs

@@ -73,8 +73,8 @@ namingEnvNames (NamingEnv xs) =
 
 -- | Get a naming environment for the given names
 --
--- We only qualify the PNames with the interface name from 'FromModParam' in
--- 'ogSource', if any. We don't qualify with the 'ModPath'.
+-- We only qualify the PNames with the interface name from 'ogFromParam'. We
+-- don't qualify with the 'ogModule'.
 namingEnvFromNames :: Set Name -> NamingEnv
 namingEnvFromNames xs = NamingEnv (foldl' add mempty xs)
   where

src/Cryptol/ModuleSystem/Renamer/Imports.hs

@@ -67,10 +67,11 @@ import Cryptol.Utils.Ident(ModName,ModPath(..),Namespace(..),OrigName(..))
 
 import Cryptol.Parser.AST
   ( ImportG(..),PName, ModuleInstanceArgs(..), ImpName(..) )
-import Cryptol.ModuleSystem.Binds (Mod(..), TopDef(..), modNested, ModKind(..))
+import Cryptol.ModuleSystem.Binds
+          ( Mod(..), TopDef(..), modNested, ModKind(..), newFunctorInst )
 import Cryptol.ModuleSystem.Name
-          ( Name, Supply, SupplyT, runSupplyT, liftSupply, freshNameFor
-          , asOrigName, nameIdent, nameTopModule )
+          ( Name, Supply, SupplyT, runSupplyT, asOrigName, nameIdent
+          , nameTopModule )
 import Cryptol.ModuleSystem.Names(Names(..))
 import Cryptol.ModuleSystem.NamingEnv
           ( NamingEnv(..), lookupNS, shadowing, travNamingEnv
@@ -511,7 +512,7 @@ doInstantiate keepArgs mpath def s = (newDef, Set.foldl' doSub newS nestedToDo)
 
   instName :: Name -> SupplyT (M.StateT (Set (Name,Name)) M.Id) Name
   instName x =
-    do y <- liftSupply (freshNameFor mpath x)
+    do y <- newFunctorInst mpath x
        when (x `Set.member` rmodNested def)
             (M.lift (M.sets_ (Set.insert (x,y))))
        pure y

src/Cryptol/Parser/Name.hs

@@ -46,16 +46,15 @@ mkUnqual  = UnQual
 mkQual :: ModName -> Ident -> PName
 mkQual  = Qual
 
--- | We only qualify the 'PName' with the interface name from 'FromModParam' in
--- 'ogSource', if any. We don't qualify with the 'ModPath'.
+-- | We only qualify the 'PName' with the interface name from 'ogFromParam'. We
+-- don't qualify with the 'ogModule'.
 fromOrigName :: OrigName -> PName
 fromOrigName og = toPName (ogName og)
   where
   toPName =
-    case ogSource og of
-      FromDefinition -> UnQual
-      FromFunctorInst -> UnQual
-      FromModParam sig -> Qual (identToModName sig)
+    case ogFromParam og of
+      Nothing -> UnQual
+      Just sig -> Qual (identToModName sig)
 
 getModName :: PName -> Maybe ModName
 getModName (Qual ns _) = Just ns

src/Cryptol/TypeCheck/Module.hs

@@ -14,8 +14,8 @@ import Cryptol.Utils.Panic(panic)
 import Cryptol.Utils.Ident(Ident,Namespace(..),ModPath,isInfixIdent)
 import Cryptol.Parser.Position (Range,Located(..), thing)
 import qualified Cryptol.Parser.AST as P
-import Cryptol.ModuleSystem.Binds(newModParam)
-import Cryptol.ModuleSystem.Name(nameIdent, nameLoc)
+import Cryptol.ModuleSystem.Binds(newFunctorInst)
+import Cryptol.ModuleSystem.Name(nameIdent)
 import Cryptol.ModuleSystem.NamingEnv
           (NamingEnv(..), modParamNamingEnv, shadowing, without)
 import Cryptol.ModuleSystem.Interface
@@ -220,14 +220,14 @@ checkArg mpath (r,expect,actual') =
     do let as = Set.fromList
                    (map (qual . mtpParam) (Map.elems (mpnTypes params)))
            cs = map thing (mpnConstraints params)
-           check = checkSimpleParameterValue r paramName
+           check = checkSimpleParameterValue r (mpName expect)
            qual a = (mpQual expect, a)
        fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params)
        pure (ParamInst as cs (Map.mapKeys qual fs))
 
   definedInst =
-    do (tRens, tSyns, tInstMaps) <- unzip3 <$> mapM
-         (checkParamType mpath r paramName tyMap) (Map.toList (mpnTypes params))
+    do (tRens, tSyns, tInstMaps) <- unzip3 <$>
+         mapM (checkParamType mpath r tyMap) (Map.toList (mpnTypes params))
        let renSu = listParamSubst (concat tRens)
 
        {- Note: the constraints from the signature are already added to the
@@ -236,7 +236,7 @@ checkArg mpath (r,expect,actual') =
 
 
        (vDecls, vInstMaps) <-
-         mapAndUnzipM (checkParamValue mpath r paramName vMap)
+         mapAndUnzipM (checkParamValue mpath r vMap)
            [ s { mvpType = apSubst renSu (mvpType s) }
            | s <- Map.elems (mpnFuns params) ]
 
@@ -245,10 +245,9 @@ checkArg mpath (r,expect,actual') =
 
 
   params = mpParameters expect
-  paramName = mpName expect
 
   -- Things provided by the argument module
-  tyMap :: Map Ident (Name, Kind, Type)
+  tyMap :: Map Ident (Kind, Type)
   vMap  :: Map Ident (Name, Schema)
   (tyMap,vMap) =
     case actual' of
@@ -258,7 +257,7 @@ checkArg mpath (r,expect,actual') =
         )
         where
         ps        = mpParameters mp
-        fromTP tp = (mtpName tp, mtpKind tp, TVar (TVBound (mtpParam tp)))
+        fromTP tp = (mtpKind tp, TVar (TVBound (mtpParam tp)))
         fromVP vp = (mvpName vp, mvpType vp)
 
       UseModule actual ->
@@ -278,9 +277,9 @@ checkArg mpath (r,expect,actual') =
         decls           = filterIfaceDecls isLocal (ifDefines actual)
 
         fromD d         = (ifDeclName d, ifDeclSig d)
-        fromTS ts       = (tsName ts, kindOf ts, tsDef ts)
-        fromNewtype nt  = (ntName nt, kindOf nt, TNewtype nt [])
-        fromPrimT pt    = (atName pt, kindOf pt, TCon (abstractTypeTC pt) [])
+        fromTS ts       = (kindOf ts, tsDef ts)
+        fromNewtype nt  = (kindOf nt, TNewtype nt [])
+        fromPrimT pt    = (kindOf pt, TCon (abstractTypeTC pt) [])
 
       AddDeclParams -> panic "checkArg" ["AddDeclParams"]
 
@@ -297,9 +296,7 @@ nameMapToIdentMap f m =
 checkParamType ::
   ModPath                    {- ^ The new module we are creating -} ->
   Range                      {- ^ Location for error reporting -} ->
-  Ident                      {- ^ Name of the _module_ parameter
-                                  (not value) -} ->
-  Map Ident (Name,Kind,Type) {- ^ Actual types -} ->
+  Map Ident (Kind,Type)      {- ^ Actual types -} ->
   (Name,ModTParam)           {- ^ Type parameter -} ->
   InferM ([(TParam,Type)], Map Name TySyn, Map Name Name)
     {- ^ Mapping from parameter name to actual type (for type substitution),
@@ -308,20 +305,20 @@ checkParamType ::
             type synonyms are fully inlined into types at this point),
          and a map from the old type name to the fresh type name
            (for instantiation) -}
-checkParamType mpath r modParamName tyMap (name,mp) =
+checkParamType mpath r tyMap (name,mp) =
   let i       = nameIdent name
       expectK = mtpKind mp
   in
   case Map.lookup i tyMap of
     Nothing ->
       do recordErrorLoc (Just r) (FunctorInstanceMissingName NSType i)
          pure ([], Map.empty, Map.empty)
-    Just (actualName,actualK,actualT) ->
+    Just (actualK,actualT) ->
       do unless (expectK == actualK)
            (recordErrorLoc (Just r)
                            (KindMismatch (Just (TVFromModParam name))
                                                   expectK actualK))
-         name' <- newModParam mpath modParamName (nameLoc actualName) name
+         name' <- newFunctorInst mpath name
          let tySyn = TySyn { tsName = name'
                            , tsParams = []
                            , tsConstraints = []
@@ -336,14 +333,13 @@ checkParamType mpath r modParamName tyMap (name,mp) =
 checkParamValue ::
   ModPath                 {- ^ The new module we are creating -} ->
   Range                   {- ^ Location for error reporting -} ->
-  Ident                   {- ^ Name of the _module_ parameter (not value) -} ->
   Map Ident (Name,Schema) {- ^ Actual values -} ->
   ModVParam               {- ^ The parameter we are checking -} ->
   InferM ([Decl], Map Name Name)
   {- ^ Decl mapping a new name to the actual value,
        and a map from the value param name in the functor to the new name
          (for instantiation) -}
-checkParamValue mpath r modParamName vMap mp =
+checkParamValue mpath r vMap mp =
   let name     = mvpName mp
       i        = nameIdent name
       expectT  = mvpType mp
@@ -353,7 +349,7 @@ checkParamValue mpath r modParamName vMap mp =
             pure ([], Map.empty)
        Just actual ->
          do e <- mkParamDef r (name,expectT) actual
-            name' <- newModParam mpath modParamName (nameLoc (fst actual)) name
+            name' <- newFunctorInst mpath name
             let d = Decl { dName        = name'
                          , dSignature   = expectT
                          , dDefinition  = DExpr e

src/Cryptol/Utils/Ident.hs

@@ -64,7 +64,7 @@ module Cryptol.Utils.Ident
     -- * Original names
   , OrigName(..)
   , OrigSource(..)
-  , ogFromModParam
+  , ogIsModParam
 
     -- * Identifiers for primitives
   , PrimIdent(..)
@@ -259,19 +259,21 @@ data OrigName = OrigName
   , ogModule    :: ModPath
   , ogSource    :: OrigSource
   , ogName      :: Ident
+  , ogFromParam :: !(Maybe Ident)
+    -- ^ Does this name come from a module parameter
   } deriving (Eq,Ord,Show,Generic,NFData)
 
 -- | Describes where a top-level name came from
 data OrigSource =
     FromDefinition
   | FromFunctorInst
-  | FromModParam Ident
+  | FromModParam
     deriving (Eq,Ord,Show,Generic,NFData)
 
 -- | Returns true iff the 'ogSource' of the given 'OrigName' is 'FromModParam'
-ogFromModParam :: OrigName -> Bool
-ogFromModParam og = case ogSource og of
-                      FromModParam _ -> True
+ogIsModParam :: OrigName -> Bool
+ogIsModParam og = case ogSource og of
+                      FromModParam -> True
                       _ -> False
 
 

src/Cryptol/Utils/PP.hs

@@ -410,16 +410,16 @@ instance PP OrigName where
         UnQualified -> pp (ogName og)
         Qualified m -> ppQual (TopModule m) (pp (ogName og))
         NotInScope  -> ppQual (ogModule og)
-                       case ogSource og of
-                         FromModParam x -> pp x <.> "::" <.> pp (ogName og)
-                         _ -> pp (ogName og)
+                       case ogFromParam og of
+                         Just x  -> pp x <.> "::" <.> pp (ogName og)
+                         Nothing -> pp (ogName og)
     where
-   ppQual mo x =
-    case mo of
-      TopModule m
-        | m == exprModName -> x
-        | otherwise -> pp m <.> "::" <.> x
-      Nested m y -> ppQual m (pp y <.> "::" <.> x)
+    ppQual mo x =
+      case mo of
+        TopModule m
+          | m == exprModName -> x
+          | otherwise -> pp m <.> "::" <.> x
+        Nested m y -> ppQual m (pp y <.> "::" <.> x)
 
 instance PP Namespace where
   ppPrec _ ns =