Pass in top level signatures to the type checker

src/Cryptol/ModuleSystem/Base.hs

@@ -573,6 +573,7 @@ genInferInput r prims params env = do
   callStacks <- getCallStacks
 
   topMods <- getAllLoaded
+  topSigs <- getAllLoadedSignatures
 
   return T.InferInput
     { T.inpRange            = r
@@ -590,6 +591,7 @@ genInferInput r prims params env = do
     , T.inpPrimNames        = prims
     , T.inpSolver           = solver
     , T.inpTopModules       = topMods
+    , T.inpTopSignatures    = topSigs
     }
 
 

src/Cryptol/ModuleSystem/Env.hs

@@ -299,7 +299,7 @@ data LoadedModules = LoadedModules
   , lmLoadedParamModules :: [LoadedModule]
     -- ^ Loaded parameterized modules.
 
-  , lmLoadedSignatures :: ![LoadedSinature]
+  , lmLoadedSignatures :: ![LoadedSignature]
 
   } deriving (Show, Generic, NFData)
 
@@ -360,7 +360,7 @@ data LoadedModuleData = LoadedModuleData
   } deriving (Show, Generic, NFData)
 
 
-type LoadedSinature = LoadedModuleG T.ModParamNames
+type LoadedSignature = LoadedModuleG T.ModParamNames
 
 
 -- | Has this module been loaded already.
@@ -377,6 +377,10 @@ lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules
   where
   search how = List.find ((mn ==) . lmName) (how (meLoadedModules me))
 
+lookupSignature :: ModName -> ModuleEnv -> Maybe LoadedSignature
+lookupSignature mn me =
+  List.find ((mn ==) . lmName) (lmLoadedSignatures (meLoadedModules me))
+
 
 -- | Add a freshly loaded module.  If it was previously loaded, then
 -- the new version is ignored.

src/Cryptol/ModuleSystem/Monad.hs

@@ -492,6 +492,11 @@ getAllLoaded = ModuleT
                          , ifaceForgetName (lmInterface lm)
                          )
 
+getAllLoadedSignatures :: ModuleM (P.ModName -> Maybe T.ModParamNames)
+getAllLoadedSignatures = ModuleT
+  do env <- get
+     pure \nm -> lmData <$> lookupSignature nm env
+
 
 getNameSeeds :: ModuleM T.NameSeeds
 getNameSeeds  = ModuleT (meNameSeeds `fmap` get)

src/Cryptol/TypeCheck/Monad.hs

@@ -68,7 +68,8 @@ data InferInput = InferInput
   , inpAbstractTypes :: Map Name AbstractType   -- ^ Abstract types in scope
   , inpSignatures :: !(Map Name ModParamNames)  -- ^ Signatures in scope
 
-  , inpTopModules :: ModName -> Maybe (ModuleG (), If.IfaceG ())
+  , inpTopModules    :: ModName -> Maybe (ModuleG (), If.IfaceG ())
+  , inpTopSignatures :: ModName -> Maybe ModParamNames
 
     -- When typechecking a module these start off empty.
     -- We need them when type-checking an expression at the command
@@ -132,6 +133,7 @@ runInferM info (IM m) =
      rec ro <- return RO { iRange     = inpRange info
                          , iVars      = env
                          , iExtModules = inpTopModules info
+                         , iExtSignatures = inpTopSignatures info
                          , iExtScope = (emptyModule ExternalScope)
                              { mTySyns           = inpTSyns info
                              , mNewtypes         = inpNewtypes info
@@ -227,8 +229,12 @@ data RO = RO
   , iTVars    :: [TParam]    -- ^ Type variable that are in scope
 
   , iExtModules :: ModName -> Maybe (ModuleG (), If.IfaceG ())
-    -- ^ An exteral top-level module.  Used the find functors that
-    -- need to be instantiated.
+    -- ^ An exteral top-level module.
+    -- We need the actual module when we instantiate functors,
+    -- because currently the type-checker desugars such modules.
+
+  , iExtSignatures :: ModName -> Maybe ModParamNames
+    -- ^ External top-level signatures.
 
   , iExtScope :: ModuleG ScopeName
     -- ^ These are things we know about, but are not part of the
@@ -709,6 +715,13 @@ lookupSignature nx =
            Nothing  -> panic "lookupSignature"
                         [ "Missing signature", show x ]
 
+    P.ImpTop t ->
+      do loaded <- iExtSignatures <$> IM ask
+         case loaded t of
+           Just ps -> pure ps
+           Nothing -> panic "lookupSignature"
+                        [ "Top level signature is not loaded", show (pp nx) ]
+
 -- | Lookup an external (i.e., previously loaded) top module.
 lookupTopModule :: ModName -> InferM (Maybe (ModuleG (), If.IfaceG ()))
 lookupTopModule m =