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

import Data.List(partition,unzip4)
import Data.Text(Text)
import Data.Map(Map)
import Data.Maybe (maybeToList)
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 for the module being generated -} ->
  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              = mempty
                            , 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

     -- Combine the docstrings of:
     -- * The functor being instantiated
     -- * The module being generated
     let newDoc :: [Text]
newDoc = Maybe Text -> [Text]
forall a. Maybe a -> [a]
maybeToList Maybe Text
doc [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ModuleG () -> [Text]
forall mname. ModuleG mname -> [Text]
mDoc ModuleG ()
mf

     case Located (ImpName Name) -> ImpName Name
forall a. Located a -> a
thing Located (ImpName Name)
m of
       P.ImpTop ModName
mn    -> [Text] -> ModName -> ExportSpec Name -> NamingEnv -> InferM ()
newModuleScope [Text]
newDoc 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 -> [Text] -> ExportSpec Name -> NamingEnv -> InferM ()
newSubmoduleScope Name
mn [Text]
newDoc (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 Submodule -> InferM ()
addSubmodules      (ModuleG (Located (ImpName Name)) -> Map Name Submodule
forall mname. ModuleG mname -> Map Name Submodule
mSubmodules ModuleG (Located (ImpName Name))
m2)
     Set Name -> InferM ()
setNested          (ModuleG (Located (ImpName Name)) -> Set Name
forall mname. ModuleG mname -> Set Name
mNested 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 p0 :: Ident
p0 = case FunctorParams -> [Ident]
forall k a. Map k a -> [k]
Map.keys FunctorParams
ps0 of
                 Ident
p':[Ident]
_ -> Ident
p'
                 [] -> String -> [String] -> Ident
forall a. HasCallStack => String -> [String] -> a
panic String
"checkArity" [String
"functor with no parameters"]
          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
p0
                      }
      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)