{-# Language BlockArguments, ImplicitParams #-}
module Cryptol.TypeCheck.Module (doFunctorInst) where

import Data.List(partition,unzip4)
import Data.Text(Text)
import Data.Map(Map)
import qualified Data.Map as Map
import qualified Data.Map.Merge.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Control.Monad(unless,forM_,mapAndUnzipM)


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(newFunctorInst)
import Cryptol.ModuleSystem.Name(nameIdent)
import Cryptol.ModuleSystem.NamingEnv
          (NamingEnv(..), modParamNamingEnv, shadowing, without)
import Cryptol.ModuleSystem.Interface
          ( IfaceG(..), IfaceDecls(..), IfaceNames(..), IfaceDecl(..)
          , filterIfaceDecls
          )
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Subst(Subst,listParamSubst,apSubst,mergeDistinctSubst)
import Cryptol.TypeCheck.Solve(proveImplication)
import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Instantiate(instantiateWith)
import Cryptol.TypeCheck.ModuleInstance
import Cryptol.TypeCheck.ModuleBacktickInstance(MBQual, doBacktickInstance)

doFunctorInst ::
  Located (P.ImpName Name)    {- ^ Name for the new module -} ->
  Located (P.ImpName Name)    {- ^ Functor being instantiated -} ->
  P.ModuleInstanceArgs Name   {- ^ Instance arguments -} ->
  Map Name Name
  {- ^ Instantitation.  These is the renaming for the functor that arises from
       generativity (i.e., it is something that will make the names "fresh").
  -} ->
  NamingEnv
  {- ^ Names in the enclosing scope of the instantiated module -} ->
  Maybe Text                  {- ^ Documentation -} ->
  InferM (Maybe TCTopEntity)
doFunctorInst :: Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> Map Name Name
-> NamingEnv
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst Located (ImpName Name)
m Located (ImpName Name)
f ModuleInstanceArgs Name
as Map Name Name
instMap0 NamingEnv
enclosingInScope Maybe Text
doc =
  Range -> InferM (Maybe TCTopEntity) -> InferM (Maybe TCTopEntity)
forall a. Range -> InferM a -> InferM a
inRange (Located (ImpName Name) -> Range
forall a. Located a -> Range
srcRange Located (ImpName Name)
m)
  do ModuleG ()
mf    <- ImpName Name -> InferM (ModuleG ())
lookupFunctor (Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
f)
     [(Range, ModParam, ActualArg)]
argIs <- Range
-> ModuleG ()
-> ModuleInstanceArgs Name
-> InferM [(Range, ModParam, ActualArg)]
checkArity (Located (ImpName Name) -> Range
forall a. Located a -> Range
srcRange Located (ImpName Name)
f) ModuleG ()
mf ModuleInstanceArgs Name
as
     ModuleG (Located (ImpName Name))
m2 <- do let mpath :: ModPath
mpath = ImpName Name -> ModPath
P.impNameModPath (Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m)
              [ArgInst]
as2 <- ((Range, ModParam, ActualArg) -> InferM ArgInst)
-> [(Range, ModParam, ActualArg)] -> InferM [ArgInst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg ModPath
mpath) [(Range, ModParam, ActualArg)]
argIs
              let ([Subst]
tySus,[Map Name TySyn]
paramTySyns,[[Decl]]
decls,[Map Name Name]
paramInstMaps) =
                    [(Subst, Map Name TySyn, [Decl], Map Name Name)]
-> ([Subst], [Map Name TySyn], [[Decl]], [Map Name Name])
forall a b c d. [(a, b, c, d)] -> ([a], [b], [c], [d])
unzip4 [ (Subst
su,Map Name TySyn
ts,[Decl]
ds,Map Name Name
im) | DefinedInst Subst
su Map Name TySyn
ts [Decl]
ds Map Name Name
im <- [ArgInst]
as2 ]
              Map Name Name
instMap <- ModPath -> ModuleG () -> Map Name Name -> InferM (Map Name Name)
addMissingTySyns ModPath
mpath ModuleG ()
mf Map Name Name
instMap0
              let ?tVarSu = [Subst] -> Subst
mergeDistinctSubst [Subst]
tySus
                  ?nameSu = Map Name Name
instMap Map Name Name -> Map Name Name -> Map Name Name
forall a. Semigroup a => a -> a -> a
<> [Map Name Name] -> Map Name Name
forall a. Monoid a => [a] -> a
mconcat [Map Name Name]
paramInstMaps
              let m1 :: ModuleG ()
m1   = ModuleG () -> ModuleG ()
forall t.
(ModuleInstance t, (?tVarSu::Subst, ?nameSu::Map Name Name)) =>
t -> t
moduleInstance ModuleG ()
mf
                  m2 :: ModuleG (Located (ImpName Name))
m2   = ModuleG ()
m1 { mName             = m
                            , mDoc              = Nothing
                            , mParamTypes       = mempty
                            , mParamFuns        = mempty
                            , mParamConstraints = mempty
                            , mParams           = mempty
                            , mTySyns = mconcat paramTySyns <> mTySyns m1
                            , mDecls = map NonRecursive (concat decls) ++
                                      mDecls m1
                            }
              let ([Set (MBQual TParam)]
tps,[[Prop]]
tcs,[Map (MBQual Name) Prop]
vps) =
                      [(Set (MBQual TParam), [Prop], Map (MBQual Name) Prop)]
-> ([Set (MBQual TParam)], [[Prop]], [Map (MBQual Name) Prop])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [ (Set (MBQual TParam)
xs,[Prop]
cs,Map (MBQual Name) Prop
fs) | ParamInst Set (MBQual TParam)
xs [Prop]
cs Map (MBQual Name) Prop
fs <- [ArgInst]
as2 ]
                  tpSet :: Set (MBQual TParam)
tpSet  = [Set (MBQual TParam)] -> Set (MBQual TParam)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set (MBQual TParam)]
tps
                  tpSet' :: Set TParam
tpSet' = (MBQual TParam -> TParam) -> Set (MBQual TParam) -> Set TParam
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map MBQual TParam -> TParam
forall a b. (a, b) -> b
snd ([Set (MBQual TParam)] -> Set (MBQual TParam)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set (MBQual TParam)]
tps)
                  emit :: Located t -> Bool
emit Located t
p = Set TParam -> Bool
forall a. Set a -> Bool
Set.null (t -> Set TParam
forall t. FVS t => t -> Set TParam
freeParams (Located t -> t
forall a. Located a -> a
thing Located t
p)
                                                Set TParam -> Set TParam -> Set TParam
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set TParam
tpSet')

                  ([Located Prop]
emitPs,[Located Prop]
delayPs) = (Located Prop -> Bool)
-> [Located Prop] -> ([Located Prop], [Located Prop])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Located Prop -> Bool
forall {t}. FVS t => Located t -> Bool
emit (ModuleG () -> [Located Prop]
forall mname. ModuleG mname -> [Located Prop]
mParamConstraints ModuleG ()
m1)

              [Located Prop] -> (Located Prop -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Located Prop]
emitPs \Located Prop
lp ->
                ConstraintSource -> [Prop] -> InferM ()
newGoals (Range -> ConstraintSource
CtModuleInstance (Located Prop -> Range
forall a. Located a -> Range
srcRange Located Prop
lp)) [Located Prop -> Prop
forall a. Located a -> a
thing Located Prop
lp]

              Set (MBQual TParam)
-> [Prop]
-> Map (MBQual Name) Prop
-> ModuleG (Located (ImpName Name))
-> InferM (ModuleG (Located (ImpName Name)))
doBacktickInstance Set (MBQual TParam)
tpSet
                                 ((Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing [Located Prop]
delayPs [Prop] -> [Prop] -> [Prop]
forall a. [a] -> [a] -> [a]
++ [[Prop]] -> [Prop]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Prop]]
tcs)
                                 ([Map (MBQual Name) Prop] -> Map (MBQual Name) Prop
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Map (MBQual Name) Prop]
vps)
                                 ModuleG (Located (ImpName Name))
m2

     -- An instantiation doesn't really have anything "in scope" per se, but
     -- here we compute what would be in scope as if you hand wrote the
     -- instantiation by copy-pasting the functor then substituting the
     -- parameters. That is, it would be whatever is in scope in the functor,
     -- together with any names in the enclosing scope if this is a nested
     -- module, with the functor's names taking precedence. This is used to
     -- determine what is in scope at the REPL when the instantiation is loaded
     -- and focused.
     --
     -- The exception is when instantiating with _, in which case we must delete
     -- the module parameters from the naming environment.
     let inScope0 :: NamingEnv
inScope0 = ModuleG (Located (ImpName Name)) -> NamingEnv
forall mname. ModuleG mname -> NamingEnv
mInScope ModuleG (Located (ImpName Name))
m2 NamingEnv -> NamingEnv -> NamingEnv
`without`
           [NamingEnv] -> NamingEnv
forall a. Monoid a => [a] -> a
mconcat [ ModParam -> NamingEnv
modParamNamingEnv ModParam
mp | (Range
_, ModParam
mp, ActualArg
AddDeclParams) <- [(Range, ModParam, ActualArg)]
argIs ]
         inScope :: NamingEnv
inScope = NamingEnv
inScope0 NamingEnv -> NamingEnv -> NamingEnv
`shadowing` NamingEnv
enclosingInScope

     case Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m of
       P.ImpTop ModName
mn    -> ModName -> ExportSpec Name -> NamingEnv -> InferM ()
newModuleScope ModName
mn (ModuleG (Located (ImpName Name)) -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG (Located (ImpName Name))
m2) NamingEnv
inScope
       P.ImpNested Name
mn -> Name -> Maybe Text -> ExportSpec Name -> NamingEnv -> InferM ()
newSubmoduleScope Name
mn Maybe Text
doc (ModuleG (Located (ImpName Name)) -> ExportSpec Name
forall mname. ModuleG mname -> ExportSpec Name
mExports ModuleG (Located (ImpName Name))
m2) NamingEnv
inScope

     (TySyn -> InferM ()) -> [TySyn] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TySyn -> InferM ()
addTySyn     (Map Name TySyn -> [TySyn]
forall k a. Map k a -> [a]
Map.elems (ModuleG (Located (ImpName Name)) -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG (Located (ImpName Name))
m2))
     (NominalType -> InferM ()) -> [NominalType] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ NominalType -> InferM ()
addNominal   (Map Name NominalType -> [NominalType]
forall k a. Map k a -> [a]
Map.elems (ModuleG (Located (ImpName Name)) -> Map Name NominalType
forall mname. ModuleG mname -> Map Name NominalType
mNominalTypes ModuleG (Located (ImpName Name))
m2))
     Map Name ModParamNames -> InferM ()
addSignatures      (ModuleG (Located (ImpName Name)) -> Map Name ModParamNames
forall mname. ModuleG mname -> Map Name ModParamNames
mSignatures ModuleG (Located (ImpName Name))
m2)
     Map Name (IfaceNames Name) -> InferM ()
addSubmodules      (ModuleG (Located (ImpName Name)) -> Map Name (IfaceNames Name)
forall mname. ModuleG mname -> Map Name (IfaceNames Name)
mSubmodules ModuleG (Located (ImpName Name))
m2)
     Map Name (ModuleG Name) -> InferM ()
addFunctors        (ModuleG (Located (ImpName Name)) -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG (Located (ImpName Name))
m2)
     (DeclGroup -> InferM ()) -> [DeclGroup] -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ DeclGroup -> InferM ()
addDecls     (ModuleG (Located (ImpName Name)) -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG (Located (ImpName Name))
m2)

     case Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m of
       P.ImpTop {}    -> TCTopEntity -> Maybe TCTopEntity
forall a. a -> Maybe a
Just (TCTopEntity -> Maybe TCTopEntity)
-> InferM TCTopEntity -> InferM (Maybe TCTopEntity)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM TCTopEntity
endModule
       P.ImpNested {} -> InferM ()
endSubmodule InferM ()
-> InferM (Maybe TCTopEntity) -> InferM (Maybe TCTopEntity)
forall a b. InferM a -> InferM b -> InferM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe TCTopEntity -> InferM (Maybe TCTopEntity)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TCTopEntity
forall a. Maybe a
Nothing


data ActualArg =
    UseParameter ModParam     -- ^ Instantiate using this parameter
  | UseModule (IfaceG ())     -- ^ Instantiate using this module
  | AddDeclParams             -- ^ Instantiate by adding parameters




{- | Validate a functor application, just checking the argument names.
The result associates a module parameter with the concrete way it should
be instantiated.
-}
checkArity ::
  Range             {- ^ Location for reporting errors -} ->
  ModuleG ()        {- ^ The functor being instantiated -} ->
  P.ModuleInstanceArgs Name {- ^ The arguments -} ->
  InferM [(Range, ModParam, ActualArg)]
  {- ^ Associates functor parameters with the interfaces of the
       instantiating modules -}
checkArity :: Range
-> ModuleG ()
-> ModuleInstanceArgs Name
-> InferM [(Range, ModParam, ActualArg)]
checkArity Range
r ModuleG ()
mf ModuleInstanceArgs Name
args =
  case ModuleInstanceArgs Name
args of

    P.DefaultInstArg Located (ModuleInstanceArg Name)
arg ->
      let i :: Located Ident
i = Located { srcRange :: Range
srcRange = Located (ModuleInstanceArg Name) -> Range
forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
arg
                      , thing :: Ident
thing    = [Ident] -> Ident
forall a. HasCallStack => [a] -> a
head (FunctorParams -> [Ident]
forall k a. Map k a -> [k]
Map.keys FunctorParams
ps0)
                      }
      in [(Range, ModParam, ActualArg)]
-> FunctorParams
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, ModParam, ActualArg)]
forall {a}.
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [] FunctorParams
ps0 [ Located Ident
-> Located (ModuleInstanceArg Name) -> ModuleInstanceNamedArg Name
forall name.
Located Ident
-> Located (ModuleInstanceArg name) -> ModuleInstanceNamedArg name
P.ModuleInstanceNamedArg Located Ident
i Located (ModuleInstanceArg Name)
arg ]

    P.NamedInstArgs [ModuleInstanceNamedArg Name]
as -> [(Range, ModParam, ActualArg)]
-> FunctorParams
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, ModParam, ActualArg)]
forall {a}.
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [] FunctorParams
ps0 [ModuleInstanceNamedArg Name]
as

    P.DefaultInstAnonArg {} -> String -> [String] -> InferM [(Range, ModParam, ActualArg)]
forall a. HasCallStack => String -> [String] -> a
panic String
"checkArity" [ String
"DefaultInstAnonArg" ]
  where
  ps0 :: FunctorParams
ps0 = ModuleG () -> FunctorParams
forall mname. ModuleG mname -> FunctorParams
mParams ModuleG ()
mf

  checkArgs :: [(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [(Range, a, ActualArg)]
done Map Ident a
ps [ModuleInstanceNamedArg Name]
as =
    case [ModuleInstanceNamedArg Name]
as of

      [] -> do [Ident] -> (Ident -> InferM ()) -> InferM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Map Ident a -> [Ident]
forall k a. Map k a -> [k]
Map.keys Map Ident a
ps) \Ident
p ->
                 Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Ident -> Error
FunctorInstanceMissingArgument Ident
p)
               [(Range, a, ActualArg)] -> InferM [(Range, a, ActualArg)]
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Range, a, ActualArg)]
done

      P.ModuleInstanceNamedArg Located Ident
ll Located (ModuleInstanceArg Name)
lm : [ModuleInstanceNamedArg Name]
more ->
        case Ident -> Map Ident a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
ll) Map Ident a
ps of
          Just a
i ->
            do Maybe ActualArg
arg <- case Located (ModuleInstanceArg Name) -> ModuleInstanceArg Name
forall a. Located a -> a
thing Located (ModuleInstanceArg Name)
lm of
                        P.ModuleArg ImpName Name
m -> ActualArg -> Maybe ActualArg
forall a. a -> Maybe a
Just (ActualArg -> Maybe ActualArg)
-> (IfaceG () -> ActualArg) -> IfaceG () -> Maybe ActualArg
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IfaceG () -> ActualArg
UseModule (IfaceG () -> Maybe ActualArg)
-> InferM (IfaceG ()) -> InferM (Maybe ActualArg)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ImpName Name -> InferM (IfaceG ())
lookupModule ImpName Name
m
                        P.ParameterArg Ident
p ->
                           do Maybe ModParam
mb <- Ident -> InferM (Maybe ModParam)
lookupModParam Ident
p
                              case Maybe ModParam
mb of
                                Maybe ModParam
Nothing ->
                                   do Range -> InferM () -> InferM ()
forall a. Range -> InferM a -> InferM a
inRange (Located (ModuleInstanceArg Name) -> Range
forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
lm)
                                              (Error -> InferM ()
recordError (Ident -> Error
MissingModParam Ident
p))
                                      Maybe ActualArg -> InferM (Maybe ActualArg)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ActualArg
forall a. Maybe a
Nothing
                                Just ModParam
a -> Maybe ActualArg -> InferM (Maybe ActualArg)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ActualArg -> Maybe ActualArg
forall a. a -> Maybe a
Just (ModParam -> ActualArg
UseParameter ModParam
a))
                        ModuleInstanceArg Name
P.AddParams -> Maybe ActualArg -> InferM (Maybe ActualArg)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ActualArg -> Maybe ActualArg
forall a. a -> Maybe a
Just ActualArg
AddDeclParams)
               let next :: [(Range, a, ActualArg)]
next = case Maybe ActualArg
arg of
                            Maybe ActualArg
Nothing -> [(Range, a, ActualArg)]
done
                            Just ActualArg
a  -> (Located (ModuleInstanceArg Name) -> Range
forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
lm, a
i, ActualArg
a) (Range, a, ActualArg)
-> [(Range, a, ActualArg)] -> [(Range, a, ActualArg)]
forall a. a -> [a] -> [a]
: [(Range, a, ActualArg)]
done
               [(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [(Range, a, ActualArg)]
next (Ident -> Map Ident a -> Map Ident a
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
ll) Map Ident a
ps) [ModuleInstanceNamedArg Name]
more

          Maybe a
Nothing ->
            do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just (Located Ident -> Range
forall a. Located a -> Range
srcRange Located Ident
ll))
                              (Ident -> Error
FunctorInstanceBadArgument (Located Ident -> Ident
forall a. Located a -> a
thing Located Ident
ll))
               [(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [(Range, a, ActualArg)]
done Map Ident a
ps [ModuleInstanceNamedArg Name]
more


data ArgInst = -- | Argument that defines the params
               DefinedInst Subst
                 (Map Name TySyn)
                 -- ^ Type synonyms created from the functor's type parameters
                 [Decl]
                 -- ^ Bindings for value parameters
                 (Map Name Name)
                 -- ^ Map from the functor's parameter names to the new names
                 --   created for the instantiation

             | ParamInst (Set (MBQual TParam)) [Prop] (Map (MBQual 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:

  * A substitution which will replace the parameter types with
    the concrete types that were provided

  * Some declarations that define the parameters in terms of the provided
    values.

  * XXX: Extra parameters for instantiation by adding params
-}
checkArg ::
  ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg :: ModPath -> (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg ModPath
mpath (Range
r,ModParam
expect,ActualArg
actual') =
  case ActualArg
actual' of
    ActualArg
AddDeclParams   -> InferM ArgInst
paramInst
    UseParameter {} -> InferM ArgInst
definedInst
    UseModule {}    -> InferM ArgInst
definedInst

  where
  paramInst :: InferM ArgInst
paramInst =
    do let as :: Set (MBQual TParam)
as = [MBQual TParam] -> Set (MBQual TParam)
forall a. Ord a => [a] -> Set a
Set.fromList
                   ((ModTParam -> MBQual TParam) -> [ModTParam] -> [MBQual TParam]
forall a b. (a -> b) -> [a] -> [b]
map (TParam -> MBQual TParam
forall {b}. b -> (Maybe ModName, b)
qual (TParam -> MBQual TParam)
-> (ModTParam -> TParam) -> ModTParam -> MBQual TParam
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModTParam -> TParam
mtpParam) (Map Name ModTParam -> [ModTParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
params)))
           cs :: [Prop]
cs = (Located Prop -> Prop) -> [Located Prop] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map Located Prop -> Prop
forall a. Located a -> a
thing (ModParamNames -> [Located Prop]
mpnConstraints ModParamNames
params)
           check :: ModVParam -> InferM (Maybe Prop)
check = Range -> Ident -> ModVParam -> InferM (Maybe Prop)
checkSimpleParameterValue Range
r (ModParam -> Ident
mpName ModParam
expect)
           qual :: b -> (Maybe ModName, b)
qual b
a = (ModParam -> Maybe ModName
mpQual ModParam
expect, b
a)
       Map Name Prop
fs <- (Name -> Maybe Prop -> Maybe Prop)
-> Map Name (Maybe Prop) -> Map Name Prop
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybeWithKey (\Name
_ Maybe Prop
v -> Maybe Prop
v) (Map Name (Maybe Prop) -> Map Name Prop)
-> InferM (Map Name (Maybe Prop)) -> InferM (Map Name Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ModVParam -> InferM (Maybe Prop))
-> Map Name ModVParam -> InferM (Map Name (Maybe Prop))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Map Name a -> m (Map Name b)
mapM ModVParam -> InferM (Maybe Prop)
check (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
params)
       ArgInst -> InferM ArgInst
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (MBQual TParam) -> [Prop] -> Map (MBQual Name) Prop -> ArgInst
ParamInst Set (MBQual TParam)
as [Prop]
cs ((Name -> MBQual Name) -> Map Name Prop -> Map (MBQual Name) Prop
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Name -> MBQual Name
forall {b}. b -> (Maybe ModName, b)
qual Map Name Prop
fs))

  definedInst :: InferM ArgInst
definedInst =
    do ([[(TParam, Prop)]]
tRens, [Map Name TySyn]
tSyns, [Map Name Name]
tInstMaps) <- [([(TParam, Prop)], Map Name TySyn, Map Name Name)]
-> ([[(TParam, Prop)]], [Map Name TySyn], [Map Name Name])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([(TParam, Prop)], Map Name TySyn, Map Name Name)]
 -> ([[(TParam, Prop)]], [Map Name TySyn], [Map Name Name]))
-> InferM [([(TParam, Prop)], Map Name TySyn, Map Name Name)]
-> InferM ([[(TParam, Prop)]], [Map Name TySyn], [Map Name Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
         ((Name, ModTParam)
 -> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name))
-> [(Name, ModTParam)]
-> InferM [([(TParam, Prop)], Map Name TySyn, Map Name Name)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ModPath
-> Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
checkParamType ModPath
mpath Range
r Map Ident (Kind, Prop)
tyMap) (Map Name ModTParam -> [(Name, ModTParam)]
forall k a. Map k a -> [(k, a)]
Map.toList (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
params))
       let renSu :: Subst
renSu = [(TParam, Prop)] -> Subst
listParamSubst ([[(TParam, Prop)]] -> [(TParam, Prop)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(TParam, Prop)]]
tRens)

       {- Note: the constraints from the signature are already added to the
          constraints for the functor and they are checked all at once in
          doFunctorInst -}


       ([[Decl]]
vDecls, [Map Name Name]
vInstMaps) <-
         (ModVParam -> InferM ([Decl], Map Name Name))
-> [ModVParam] -> InferM ([[Decl]], [Map Name Name])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM (ModPath
-> Range
-> Map Ident (Name, Schema)
-> ModVParam
-> InferM ([Decl], Map Name Name)
checkParamValue ModPath
mpath Range
r Map Ident (Name, Schema)
vMap)
           [ ModVParam
s { mvpType = apSubst renSu (mvpType s) }
           | ModVParam
s <- Map Name ModVParam -> [ModVParam]
forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
params) ]

       ArgInst -> InferM ArgInst
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ArgInst -> InferM ArgInst) -> ArgInst -> InferM ArgInst
forall a b. (a -> b) -> a -> b
$ Subst -> Map Name TySyn -> [Decl] -> Map Name Name -> ArgInst
DefinedInst Subst
renSu ([Map Name TySyn] -> Map Name TySyn
forall a. Monoid a => [a] -> a
mconcat [Map Name TySyn]
tSyns)
         ([[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl]]
vDecls) ([Map Name Name] -> Map Name Name
forall a. Monoid a => [a] -> a
mconcat [Map Name Name]
tInstMaps Map Name Name -> Map Name Name -> Map Name Name
forall a. Semigroup a => a -> a -> a
<> [Map Name Name] -> Map Name Name
forall a. Monoid a => [a] -> a
mconcat [Map Name Name]
vInstMaps)


  params :: ModParamNames
params = ModParam -> ModParamNames
mpParameters ModParam
expect

  -- Things provided by the argument module
  tyMap :: Map Ident (Kind, Type)
  vMap  :: Map Ident (Name, Schema)
  (Map Ident (Kind, Prop)
tyMap,Map Ident (Name, Schema)
vMap) =
    case ActualArg
actual' of
      UseParameter ModParam
mp ->
        ( (ModTParam -> (Kind, Prop))
-> Map Name ModTParam -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap ModTParam -> (Kind, Prop)
fromTP (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ps)
        , (ModVParam -> (Name, Schema))
-> Map Name ModVParam -> Map Ident (Name, Schema)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap ModVParam -> (Name, Schema)
fromVP (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
ps)
        )
        where
        ps :: ModParamNames
ps        = ModParam -> ModParamNames
mpParameters ModParam
mp
        fromTP :: ModTParam -> (Kind, Prop)
fromTP ModTParam
tp = (ModTParam -> Kind
mtpKind ModTParam
tp, TVar -> Prop
TVar (TParam -> TVar
TVBound (ModTParam -> TParam
mtpParam ModTParam
tp)))
        fromVP :: ModVParam -> (Name, Schema)
fromVP ModVParam
vp = (ModVParam -> Name
mvpName ModVParam
vp, ModVParam -> Schema
mvpType ModVParam
vp)

      UseModule IfaceG ()
actual ->
        ( [Map Ident (Kind, Prop)] -> Map Ident (Kind, Prop)
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [ (TySyn -> (Kind, Prop)) -> Map Name TySyn -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap TySyn -> (Kind, Prop)
fromTS      (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
decls)
                     , (NominalType -> (Kind, Prop))
-> Map Name NominalType -> Map Ident (Kind, Prop)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap NominalType -> (Kind, Prop)
fromNominal (IfaceDecls -> Map Name NominalType
ifNominalTypes IfaceDecls
decls)
                     ]

        , (IfaceDecl -> (Name, Schema))
-> Map Name IfaceDecl -> Map Ident (Name, Schema)
forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap IfaceDecl -> (Name, Schema)
fromD (IfaceDecls -> Map Name IfaceDecl
ifDecls IfaceDecls
decls)
        )

        where
        localNames :: Set Name
localNames      = IfaceNames () -> Set Name
forall name. IfaceNames name -> Set Name
ifsPublic (IfaceG () -> IfaceNames ()
forall name. IfaceG name -> IfaceNames name
ifNames IfaceG ()
actual)
        isLocal :: Name -> Bool
isLocal Name
x       = Name
x Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
localNames

        -- Things defined by the argument module
        decls :: IfaceDecls
decls           = (Name -> Bool) -> IfaceDecls -> IfaceDecls
filterIfaceDecls Name -> Bool
isLocal (IfaceG () -> IfaceDecls
forall name. IfaceG name -> IfaceDecls
ifDefines IfaceG ()
actual)

        fromD :: IfaceDecl -> (Name, Schema)
fromD IfaceDecl
d         = (IfaceDecl -> Name
ifDeclName IfaceDecl
d, IfaceDecl -> Schema
ifDeclSig IfaceDecl
d)
        fromTS :: TySyn -> (Kind, Prop)
fromTS TySyn
ts       = (TySyn -> Kind
forall t. HasKind t => t -> Kind
kindOf TySyn
ts, TySyn -> Prop
tsDef TySyn
ts)
        fromNominal :: NominalType -> (Kind, Prop)
fromNominal NominalType
nt  = (NominalType -> Kind
forall t. HasKind t => t -> Kind
kindOf NominalType
nt, NominalType -> [Prop] -> Prop
TNominal NominalType
nt [])

      ActualArg
AddDeclParams -> String
-> [String] -> (Map Ident (Kind, Prop), Map Ident (Name, Schema))
forall a. HasCallStack => String -> [String] -> a
panic String
"checkArg" [String
"AddDeclParams"]



nameMapToIdentMap :: (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap :: forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap a -> b
f Map Name a
m =
  [(Ident, b)] -> Map Ident b
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Name -> Ident
nameIdent Name
n, a -> b
f a
v) | (Name
n,a
v) <- Map Name a -> [(Name, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name a
m ]




-- | Check a type parameter to a module.
checkParamType ::
  ModPath                    {- ^ The new module we are creating -} ->
  Range                      {- ^ Location for error reporting -} ->
  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),
         type synonym map from a fresh type name to the actual type
           (only so that the type can be referred to in the REPL;
            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 :: ModPath
-> Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
checkParamType ModPath
mpath Range
r Map Ident (Kind, Prop)
tyMap (Name
name,ModTParam
mp) =
  let i :: Ident
i       = Name -> Ident
nameIdent Name
name
      expectK :: Kind
expectK = ModTParam -> Kind
mtpKind ModTParam
mp
  in
  case Ident -> Map Ident (Kind, Prop) -> Maybe (Kind, Prop)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i Map Ident (Kind, Prop)
tyMap of
    Maybe (Kind, Prop)
Nothing ->
      do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Namespace -> Ident -> Error
FunctorInstanceMissingName Namespace
NSType Ident
i)
         ([(TParam, Prop)], Map Name TySyn, Map Name Name)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Map Name TySyn
forall k a. Map k a
Map.empty, Map Name Name
forall k a. Map k a
Map.empty)
    Just (Kind
actualK,Prop
actualT) ->
      do Bool -> InferM () -> InferM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
expectK Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
actualK)
           (Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r)
                           (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch (TypeSource -> Maybe TypeSource
forall a. a -> Maybe a
Just (Name -> TypeSource
TVFromModParam Name
name))
                                                  Kind
expectK Kind
actualK))
         Name
name' <- ModPath -> Name -> InferM Name
forall (m :: * -> *). FreshM m => ModPath -> Name -> m Name
newFunctorInst ModPath
mpath Name
name
         let tySyn :: TySyn
tySyn = TySyn { tsName :: Name
tsName = Name
name'
                           , tsParams :: [TParam]
tsParams = []
                           , tsConstraints :: [Prop]
tsConstraints = []
                           , tsDef :: Prop
tsDef = Prop
actualT
                           , tsDoc :: Maybe Text
tsDoc = ModTParam -> Maybe Text
mtpDoc ModTParam
mp }
         ([(TParam, Prop)], Map Name TySyn, Map Name Name)
-> InferM ([(TParam, Prop)], Map Name TySyn, Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [(ModTParam -> TParam
mtpParam ModTParam
mp, Prop
actualT)]
              , Name -> TySyn -> Map Name TySyn
forall k a. k -> a -> Map k a
Map.singleton Name
name' TySyn
tySyn
              , Name -> Name -> Map Name Name
forall k a. k -> a -> Map k a
Map.singleton Name
name Name
name'
              )

-- | Check a value parameter to a module.
checkParamValue ::
  ModPath                 {- ^ The new module we are creating -} ->
  Range                   {- ^ Location for error reporting -} ->
  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 :: ModPath
-> Range
-> Map Ident (Name, Schema)
-> ModVParam
-> InferM ([Decl], Map Name Name)
checkParamValue ModPath
mpath Range
r Map Ident (Name, Schema)
vMap ModVParam
mp =
  let name :: Name
name     = ModVParam -> Name
mvpName ModVParam
mp
      i :: Ident
i        = Name -> Ident
nameIdent Name
name
      expectT :: Schema
expectT  = ModVParam -> Schema
mvpType ModVParam
mp
  in case Ident -> Map Ident (Name, Schema) -> Maybe (Name, Schema)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Ident
i Map Ident (Name, Schema)
vMap of
       Maybe (Name, Schema)
Nothing ->
         do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r) (Namespace -> Ident -> Error
FunctorInstanceMissingName Namespace
NSValue Ident
i)
            ([Decl], Map Name Name) -> InferM ([Decl], Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Map Name Name
forall k a. Map k a
Map.empty)
       Just (Name, Schema)
actual ->
         do Expr
e <- Range -> (Name, Schema) -> (Name, Schema) -> InferM Expr
mkParamDef Range
r (Name
name,Schema
expectT) (Name, Schema)
actual
            Name
name' <- ModPath -> Name -> InferM Name
forall (m :: * -> *). FreshM m => ModPath -> Name -> m Name
newFunctorInst ModPath
mpath Name
name
            let d :: Decl
d = Decl { dName :: Name
dName        = Name
name'
                         , dSignature :: Schema
dSignature   = Schema
expectT
                         , dDefinition :: DeclDef
dDefinition  = Expr -> DeclDef
DExpr Expr
e
                         , dPragmas :: [Pragma]
dPragmas     = []
                         , dInfix :: Bool
dInfix       = Ident -> Bool
isInfixIdent (Name -> Ident
nameIdent Name
name')
                         , dFixity :: Maybe Fixity
dFixity      = ModVParam -> Maybe Fixity
mvpFixity ModVParam
mp
                         , dDoc :: Maybe Text
dDoc         = ModVParam -> Maybe Text
mvpDoc ModVParam
mp
                         }

            ([Decl], Map Name Name) -> InferM ([Decl], Map Name Name)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Decl
d], Name -> Name -> Map Name Name
forall k a. k -> a -> Map k a
Map.singleton Name
name Name
name')



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 :: Range -> Ident -> ModVParam -> InferM (Maybe Prop)
checkSimpleParameterValue Range
r Ident
i ModVParam
mp =
  case (Schema -> [TParam]
sVars Schema
sch, Schema -> [Prop]
sProps Schema
sch) of
    ([],[]) -> Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> Maybe Prop
forall a. a -> Maybe a
Just (Schema -> Prop
sType Schema
sch))
    ([TParam], [Prop])
_ ->
      do Maybe Range -> Error -> InferM ()
recordErrorLoc (Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r)
            (BadBacktickInstance -> Error
FunctorInstanceBadBacktick
               (Ident -> Ident -> BadBacktickInstance
BIPolymorphicArgument Ident
i (Name -> Ident
nameIdent (ModVParam -> Name
mvpName ModVParam
mp))))
         Maybe Prop -> InferM (Maybe Prop)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Prop
forall a. Maybe a
Nothing
  where
  sch :: Schema
sch = ModVParam -> Schema
mvpType ModVParam
mp


{- | Make an "adaptor" that instantiates the paramter into the form expected
by the functor.  If the actual type is:

> {x} P => t

and the provided type is:

> f : {y} Q => s

The result, if successful would be:

  /\x \{P}. f @a {Q}

To do this we need to find types `a` to instantiate `y`, and prove that:
  {x} P => Q[a/y] /\ s = t
-}

mkParamDef ::
  Range           {- ^ Location of instantiation for error reporting -} ->
  (Name,Schema)   {- ^ Name and type of parameter -} ->
  (Name,Schema)   {- ^ Name and type of actual argument -} ->
  InferM Expr
mkParamDef :: Range -> (Name, Schema) -> (Name, Schema) -> InferM Expr
mkParamDef Range
r (Name
pname,Schema
wantedS) (Name
arg,Schema
actualS) =
  do (Expr
e,[Goal]
todo) <- InferM Expr -> InferM (Expr, [Goal])
forall a. InferM a -> InferM (a, [Goal])
collectGoals
          (InferM Expr -> InferM (Expr, [Goal]))
-> InferM Expr -> InferM (Expr, [Goal])
forall a b. (a -> b) -> a -> b
$ [TParam] -> InferM Expr -> InferM Expr
forall a. [TParam] -> InferM a -> InferM a
withTParams (Schema -> [TParam]
sVars Schema
wantedS)
            do (Expr
e,Prop
t) <- Name -> Expr -> Schema -> [TypeArg] -> InferM (Expr, Prop)
instantiateWith Name
pname(Name -> Expr
EVar Name
arg) Schema
actualS []
               [Prop]
props <- TypeWithSource -> Prop -> InferM [Prop]
unify WithSource { twsType :: Prop
twsType   = Schema -> Prop
sType Schema
wantedS
                                         , twsSource :: TypeSource
twsSource = Name -> TypeSource
TVFromModParam Name
arg
                                         , twsRange :: Maybe Range
twsRange  = Range -> Maybe Range
forall a. a -> Maybe a
Just Range
r
                                         }
                        Prop
t
               ConstraintSource -> [Prop] -> InferM ()
newGoals (Range -> ConstraintSource
CtModuleInstance Range
r) [Prop]
props
               Expr -> InferM Expr
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e
     Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
False
                            (Name -> Maybe Name
forall a. a -> Maybe a
Just Name
pname)
                            (Schema -> [TParam]
sVars Schema
wantedS)
                            (Schema -> [Prop]
sProps Schema
wantedS)
                            [Goal]
todo
     let res :: Expr
res  = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TParam -> Expr -> Expr
ETAbs     Expr
res1            (Schema -> [TParam]
sVars Schema
wantedS)
         res1 :: Expr
res1 = (Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)  (Schema -> [Prop]
sProps Schema
wantedS)

     Expr -> InferM Expr
forall t. TVars t => t -> InferM t
applySubst Expr
res


-- | The instMap we get from the renamer will not contain the fresh names for
-- certain things in the functor generated in the typechecking stage, if we are
-- instantiating a functor that is in the same file, since renaming and
-- typechecking happens together with the instantiation. In particular, if the
-- functor's interface has type synonyms, they will only get copied over into
-- the functor in the typechecker, so the renamer will not see them. Here we
-- make the fresh names for those missing type synonyms and add them to the
-- instMap.
addMissingTySyns ::
  ModPath                  {- ^ The new module we are creating -} ->
  ModuleG ()               {- ^ The functor -} ->
  Map Name Name            {- ^ instMap we get from renamer -} ->
  InferM (Map Name Name)   {- ^ the complete instMap -}
addMissingTySyns :: ModPath -> ModuleG () -> Map Name Name -> InferM (Map Name Name)
addMissingTySyns ModPath
mpath ModuleG ()
f = WhenMissing InferM Name TySyn Name
-> WhenMissing InferM Name Name Name
-> WhenMatched InferM Name TySyn Name Name
-> Map Name TySyn
-> Map Name Name
-> InferM (Map Name Name)
forall (f :: * -> *) k a c b.
(Applicative f, Ord k) =>
WhenMissing f k a c
-> WhenMissing f k b c
-> WhenMatched f k a b c
-> Map k a
-> Map k b
-> f (Map k c)
Map.mergeA
  ((Name -> TySyn -> InferM Name)
-> WhenMissing InferM Name TySyn Name
forall (f :: * -> *) k x y.
Applicative f =>
(k -> x -> f y) -> WhenMissing f k x y
Map.traverseMissing \Name
name TySyn
_ -> ModPath -> Name -> InferM Name
forall (m :: * -> *). FreshM m => ModPath -> Name -> m Name
newFunctorInst ModPath
mpath Name
name)
  WhenMissing InferM Name Name Name
forall (f :: * -> *) k x. Applicative f => WhenMissing f k x x
Map.preserveMissing
  ((Name -> TySyn -> Name -> Name)
-> WhenMatched InferM Name TySyn Name Name
forall (f :: * -> *) k x y z.
Applicative f =>
(k -> x -> y -> z) -> WhenMatched f k x y z
Map.zipWithMatched \Name
_ TySyn
_ Name
name' -> Name
name')
  (ModuleG () -> Map Name TySyn
forall mname. ModuleG mname -> Map Name TySyn
mTySyns ModuleG ()
f)