Rearrange so that each functor parameter can be "backtick" instantiat…

…ed separately.

XXX: The order in which parameters should be added is very
unclear.

src/Cryptol/ModuleSystem/Base.hs

@@ -468,7 +468,6 @@ findDeps' m =
                   DefaultInstArg a -> loadInstArg a
                   DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds)
                   NamedInstArgs args -> mconcat (map loadNamedInstArg args)
-                  BacktickInstance -> mempty
       in fds <> ads
     InterfaceModule s -> mconcat (map loadImpD (sigImports s))
   where

src/Cryptol/ModuleSystem/Renamer.hs

@@ -292,7 +292,6 @@ checkFunctorArgs args =
       panic "checkFunctorArgs" ["Nested DefaultInstAnonArg"]
     DefaultInstArg l -> checkArg l
     NamedInstArgs as -> mapM_ checkNamedArg as
-    BacktickInstance -> pure ()
   where
   checkNamedArg (ModuleInstanceNamedArg _ l) = checkArg l
 
@@ -302,6 +301,7 @@ checkFunctorArgs args =
           | isFakeName m -> pure ()
           | otherwise    -> checkIsModule (srcRange l) m AModule
         ParameterArg {} -> pure () -- we check these in the type checker
+        AddParams -> pure ()
 
 mkInstMap :: Maybe Range -> Map Name Name -> ImpName Name -> ImpName Name ->
   RenameM (Map Name Name)
@@ -481,10 +481,10 @@ renameTopDecls' ds =
                   DefaultInstArg arg -> depsOfArg arg
                   NamedInstArgs args -> concatMap depsOfNamedArg args
                   DefaultInstAnonArg {} -> []
-                  BacktickInstance -> []
 
                where depsOfNamedArg (ModuleInstanceNamedArg _ a) = depsOfArg a
                      depsOfArg a = case thing a of
+                                     AddParams -> []
                                      ModuleArg {} -> []
                                      ParameterArg p ->
                                        case Map.lookup p localParams of
@@ -795,7 +795,6 @@ instance Rename ModuleInstanceArgs where
       DefaultInstArg a -> DefaultInstArg <$> rnLocated rename a
       NamedInstArgs xs -> NamedInstArgs  <$> traverse rename xs
       DefaultInstAnonArg {} -> panic "rename" ["DefaultInstAnonArg"]
-      BacktickInstance -> pure BacktickInstance
 
 instance Rename ModuleInstanceNamedArg where
   rename (ModuleInstanceNamedArg x m) =
@@ -806,7 +805,7 @@ instance Rename ModuleInstanceArg where
     case arg of
       ModuleArg m -> ModuleArg <$> rename m
       ParameterArg a -> pure (ParameterArg a)
-
+      AddParams -> pure AddParams
 
 instance Rename NestedModule where
   rename (NestedModule m) =

src/Cryptol/Parser/AST.hs

@@ -282,9 +282,6 @@ data ModuleInstanceArgs name =
 
   | NamedInstArgs  [ModuleInstanceNamedArg name]
 
-  | BacktickInstance
-    -- ^ The module instance is computed by adding the functor arguments
-    -- as explicit parameters to all declarations.
     deriving (Show, Generic, NFData)
 
 -- | A named argument in a functor instantiation
@@ -296,6 +293,8 @@ data ModuleInstanceNamedArg name =
 data ModuleInstanceArg name =
     ModuleArg (ImpName name)  -- ^ An argument that is a module
   | ParameterArg Ident        -- ^ An argument that is a parameter
+  | AddParams                 -- ^ Arguments adds extra parameters to decls.
+                              -- ("backtick" import)
     deriving (Show, Generic, NFData)
 
 
@@ -867,7 +866,6 @@ instance (Show name, PPName name) => PP (ModuleInstanceArgs name) where
       DefaultInstArg x -> braces (pp (thing x))
       DefaultInstAnonArg ds -> "where" $$ indent 2 (vcat (map pp ds))
       NamedInstArgs xs -> braces (commaSep (map pp xs))
-      BacktickInstance -> "{}"
 
 instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where
   ppPrec _ (ModuleInstanceNamedArg x y) = pp (thing x) <+> "=" <+> pp (thing y)
@@ -876,8 +874,9 @@ instance (Show name, PPName name) => PP (ModuleInstanceNamedArg name) where
 instance (Show name, PPName name) => PP (ModuleInstanceArg name) where
   ppPrec _ arg =
     case arg of
-      ModuleArg x -> pp x
+      ModuleArg x    -> pp x
       ParameterArg i -> "parameter" <+> pp i
+      AddParams      -> "{}"
 
 
 instance (Show name, PPName name) => PP (Program name) where
@@ -1363,7 +1362,6 @@ instance NoPos (ModuleInstanceArgs name) where
       DefaultInstArg a      -> DefaultInstArg (noPos a)
       DefaultInstAnonArg ds -> DefaultInstAnonArg (noPos ds)
       NamedInstArgs xs      -> NamedInstArgs (noPos xs)
-      BacktickInstance      -> BacktickInstance
 
 instance NoPos (ModuleInstanceNamedArg name) where
   noPos (ModuleInstanceNamedArg x y) =

src/Cryptol/TypeCheck/Error.hs

@@ -155,6 +155,8 @@ data Error    = KindMismatch (Maybe TypeSource) Kind Kind
               | FunctorInstanceMissingArgument Ident
               | FunctorInstanceBadArgument Ident
               | FunctorInstanceMissingName Namespace Ident
+              | FunctorInstanceBadBacktickArgument Ident Ident
+                -- ^ Name of functor argument, name of bad value
 
               | UnsupportedFFIKind TypeSource TParam Kind
                 -- ^ Kind is not supported for FFI
@@ -191,6 +193,7 @@ errorImportance err =
     MissingModParam {}                                -> 10
     FunctorInstanceBadArgument {}                     -> 10
     FunctorInstanceMissingName {}                     ->  9
+    FunctorInstanceBadBacktickArgument {}             ->  9
 
 
     KindMismatch {}                                  -> 10
@@ -297,6 +300,7 @@ instance TVars Error where
       FunctorInstanceMissingArgument {} -> err
       FunctorInstanceBadArgument {} -> err
       FunctorInstanceMissingName {} -> err
+      FunctorInstanceBadBacktickArgument {} -> err
 
       UnsupportedFFIKind {}    -> err
       UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e
@@ -345,6 +349,7 @@ instance FVS Error where
       FunctorInstanceMissingArgument {} -> Set.empty
       FunctorInstanceBadArgument {} -> Set.empty
       FunctorInstanceMissingName {} -> Set.empty
+      FunctorInstanceBadBacktickArgument {} -> Set.empty
 
       UnsupportedFFIKind {}  -> Set.empty
       UnsupportedFFIType _ t -> fvs t
@@ -562,6 +567,15 @@ instance PP (WithNames Error) where
               NSType      -> "type"
               NSModule    -> "module"
 
+      FunctorInstanceBadBacktickArgument i x ->
+        nested "Value parameter may not have a polymorphic type:" $
+          vcat
+            [ "Module parameter:" <+> pp i
+            , "Value parameter:" <+> pp x
+            , "When instantiatiating a functor using parameterization,"
+            , "the value parameters need to have a simple type."
+            ]
+
       UnsupportedFFIKind src param k ->
         nested "Kind of type variable unsupported for FFI: " $
         vcat

src/Cryptol/TypeCheck/Module.hs

@@ -1,9 +1,11 @@
 {-# Language BlockArguments, ImplicitParams #-}
 module Cryptol.TypeCheck.Module (doFunctorInst) where
 
+import Data.List(partition)
 import Data.Text(Text)
 import Data.Map(Map)
 import qualified Data.Map as Map
+import Data.Set (Set)
 import qualified Data.Set as Set
 import Control.Monad(unless,forM_)
 
@@ -40,25 +42,34 @@ doFunctorInst m f as inst doc =
   inRange (srcRange m)
   do mf    <- lookupFunctor (thing f)
      argIs <- checkArity (srcRange f) mf as
-     m2 <- case argIs of
-             UseArgs ais ->
-               do (tySus,decls) <- unzip <$> mapM checkArg ais
-                  let ?tSu = mergeDistinctSubst tySus
-                      ?vSu = inst
-                  let m1   = moduleInstance mf
-                      m2   = m1 { mName             = m
-                                , mDoc              = Nothing
-                                , mParamTypes       = mempty
-                                , mParamFuns        = mempty
-                                , mParamConstraints = mempty
-                                , mParams           = mempty
-                                , mDecls = map NonRecursive (concat decls) ++
-                                          mDecls m1
-                                }
-                  newGoals CtModuleInstance (map thing (mParamConstraints m1))
-                  pure m2
-
-             AddParamsToDecls -> doBacktickInstance m mf inst
+     m2 <- do as2 <- mapM checkArg argIs
+              let (tySus,decls) = unzip [ (su,ds) | DefinedInst su ds <- as2 ]
+              let ?tSu = mergeDistinctSubst tySus
+                  ?vSu = inst
+              let m1   = moduleInstance mf
+                  m2   = m1 { mName             = m
+                            , mDoc              = Nothing
+                            , mParamTypes       = mempty
+                            , mParamFuns        = mempty
+                            , mParamConstraints = mempty
+                            , mParams           = mempty
+                            , mDecls = map NonRecursive (concat decls) ++
+                                      mDecls m1
+                            }
+              let (tps,tcs,vps) =
+                      unzip3 [ (xs,cs,fs) | ParamInst xs cs fs <- as2 ]
+                  tpSet = Set.unions tps
+                  emit p = Set.null (freeParams p `Set.intersection` tpSet)
+
+                  (emitPs,delayPs) =
+                          partition emit (map thing (mParamConstraints m1))
+
+              newGoals CtModuleInstance emitPs
+
+              doBacktickInstance (Set.toList tpSet)
+                                 (delayPs ++ concat tcs)
+                                 (Map.unions vps)
+                                 m2
 
      case thing m of
        P.ImpTop mn    -> newModuleScope mn (mExports m2)
@@ -77,14 +88,11 @@ doFunctorInst m f as inst doc =
        P.ImpNested {} -> endSubmodule >> pure Nothing
 
 
-
 data ActualArg =
     UseParameter ModParam     -- ^ Instantiate using this parameter
   | UseModule (IfaceG ())     -- ^ Instantiate using this module
+  | AddDeclParams             -- ^ Instantiate by adding parameters
 
-data ActualArgs =
-    UseArgs [(Range, ModParam, ActualArg)]
-  | AddParamsToDecls
 
 
 
@@ -99,7 +107,7 @@ checkArity ::
   Range             {- ^ Location for reporting errors -} ->
   ModuleG ()        {- ^ The functor being instantiated -} ->
   P.ModuleInstanceArgs Name {- ^ The arguments -} ->
-  InferM ActualArgs
+  InferM [(Range, ModParam, ActualArg)]
   {- ^ Associates functor parameters with the interfaces of the
        instantiating modules -}
 checkArity r mf args =
@@ -113,8 +121,6 @@ checkArity r mf args =
 
     P.NamedInstArgs as -> checkArgs [] ps0 as
 
-    P.BacktickInstance -> pure AddParamsToDecls
-
     P.DefaultInstAnonArg {} -> panic "checkArity" [ "DefaultInstAnonArg" ]
   where
   ps0 = mParams mf
@@ -124,7 +130,7 @@ checkArity r mf args =
 
       [] -> do forM_ (Map.keys ps) \p ->
                  recordErrorLoc (Just r) (FunctorInstanceMissingArgument p)
-               pure (UseArgs done)
+               pure done
 
       P.ModuleInstanceNamedArg ll lm : more ->
         case Map.lookup (thing ll) ps of
@@ -139,6 +145,7 @@ checkArity r mf args =
                                               (recordError (MissingModParam p))
                                       pure Nothing
                                 Just a -> pure (Just (UseParameter a))
+                        P.AddParams -> pure (Just AddDeclParams)
                let next = case arg of
                             Nothing -> done
                             Just a  -> (srcRange lm, i, a) : done
@@ -150,6 +157,13 @@ checkArity r mf args =
                checkArgs done ps more
 
 
+data ArgInst = DefinedInst Subst [Decl] -- ^ Argument that defines the params
+             | ParamInst (Set TParam) [Prop] (Map Name Type)
+               -- ^ Argument that add parameters
+               -- The type parameters are in their module type parameter
+               -- form (i.e., tpFlav is TPModParam)
+
+
 {- | Check the argument to a functor parameter.
 Returns:
 
@@ -158,31 +172,45 @@ Returns:
 
   * Some declarations that define the parameters in terms of the provided
     values.
+
+  * XXX: Extra parameters for instantiation by adding params
 -}
 checkArg ::
-  (Range, ModParam, ActualArg) -> InferM (Subst, [Decl])
+  (Range, ModParam, ActualArg) -> InferM ArgInst
 checkArg (r,expect,actual') =
-  do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params))
-     let renSu = listParamSubst (concat tRens)
+  case actual' of
+    AddDeclParams   -> paramInst
+    UseParameter {} -> definedInst
+    UseModule {}    -> definedInst
 
-     {- Note: the constraints from the signature are already added to the
-        constraints for the functor and they are checked all at once in
-        doFunctorInst -}
+  where
+  paramInst =
+    do let as = Set.fromList (map mtpParam (Map.elems (mpnTypes params)))
+           cs = map thing (mpnConstraints params)
+           check = checkSimpleParameterValue r (mpName expect)
+       fs <- Map.mapMaybeWithKey (\_ v -> v) <$> mapM check (mpnFuns params)
+       pure (ParamInst as cs fs)
 
+  definedInst =
+    do tRens <- mapM (checkParamType r tyMap) (Map.toList (mpnTypes params))
+       let renSu = listParamSubst (concat tRens)
 
-     vDecls <- concat <$>
-                mapM (checkParamValue r vMap)
-                     [ s { mvpType = apSubst renSu (mvpType s) }
-                     | s <- Map.elems (mpnFuns params) ]
+       {- Note: the constraints from the signature are already added to the
+          constraints for the functor and they are checked all at once in
+          doFunctorInst -}
 
-     pure (renSu, vDecls)
 
+       vDecls <- concat <$>
+                  mapM (checkParamValue r vMap)
+                       [ s { mvpType = apSubst renSu (mvpType s) }
+                       | s <- Map.elems (mpnFuns params) ]
 
+       pure (DefinedInst renSu vDecls)
 
 
-  where
   params = mpParameters expect
 
+  -- Things provided by the argument module
   tyMap :: Map Ident (Kind, Type)
   vMap  :: Map Ident (Name, Schema)
   (tyMap,vMap) =
@@ -209,13 +237,16 @@ checkArg (r,expect,actual') =
         localNames      = ifsPublic (ifNames actual)
         isLocal x       = x `Set.member` localNames
 
+        -- Things defined by the argument module
         decls           = filterIfaceDecls isLocal (ifDefines actual)
 
         fromD d         = (ifDeclName d, ifDeclSig d)
         fromTS ts       = (kindOf ts, tsDef ts)
         fromNewtype nt  = (kindOf nt, TNewtype nt [])
         fromPrimT pt    = (kindOf pt, TCon (abstractTypeTC pt) [])
 
+      AddDeclParams -> panic "checkArg" ["AddDeclParams"]
+
 
 
 nameMapToIdentMap :: (a -> b) -> Map Name a -> Map Ident b
@@ -273,6 +304,24 @@ checkParamValue r vMap mp =
 
             pure [d]
 
+
+
+checkSimpleParameterValue ::
+  Range                       {- ^ Location for error reporting -} ->
+  Ident                       {- ^ Name of functor parameter -} ->
+  ModVParam                   {- ^ Module parameter -} ->
+  InferM (Maybe Type)  {- ^ Type to add to things, `Nothing` on err -}
+checkSimpleParameterValue r i mp =
+  case (sVars sch, sProps sch) of
+    ([],[]) -> pure (Just (sType sch))
+    _ ->
+      do recordErrorLoc (Just r)
+            (FunctorInstanceBadBacktickArgument i (nameIdent (mvpName mp)))
+         pure Nothing
+  where
+  sch = mvpType mp
+
+
 {- | Make an "adaptor" that instantiates the paramter into the form expected
 by the functor.  If the actual type is:
 

src/Cryptol/TypeCheck/ModuleBacktickInstance.hs

@@ -8,9 +8,12 @@ import qualified Cryptol.Parser.AST as P
 import Cryptol.TypeCheck.AST
 import Cryptol.TypeCheck.Monad
 
+-- | Rewrite declarations to add the given module parameters.
+-- Assumes the renaming due to the instantiation has already happened.
 doBacktickInstance ::
-  Located (P.ImpName Name)    {- ^ Name for the new module -} ->
-  ModuleG ()                  {- ^ The functor -} ->
-  Map Name Name {- ^ The instantiation: functor name -> instance name -} ->
-  InferM (ModuleG (Located (P.ImpName Name)))
-doBacktickInstance m mf inst = undefined
+  [TParam] ->
+  [Prop] ->
+  Map Name Type ->
+  ModuleG name ->
+  InferM (ModuleG name)
+doBacktickInstance = undefined