{-# 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_)


import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Ident(Ident,Namespace(..),isInfixIdent)
import Cryptol.Parser.Position (Range,Located(..), thing)
import qualified Cryptol.Parser.AST as P
import Cryptol.ModuleSystem.Name(nameIdent)
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").
  -} ->
  Maybe Text                  {- ^ Documentation -} ->
  InferM (Maybe TCTopEntity)
doFunctorInst :: Located (ImpName Name)
-> Located (ImpName Name)
-> ModuleInstanceArgs Name
-> Map Name Name
-> Maybe Text
-> InferM (Maybe TCTopEntity)
doFunctorInst Located (ImpName Name)
m Located (ImpName Name)
f ModuleInstanceArgs Name
as Map Name Name
inst Maybe Text
doc =
  forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange Located (ImpName Name)
m)
  do ModuleG ()
mf    <- ImpName Name -> InferM (ModuleG ())
lookupFunctor (forall a. Located a -> a
thing Located (ImpName Name)
f)
     [(Range, ModParam, ActualArg)]
argIs <- Range
-> ModuleG ()
-> ModuleInstanceArgs Name
-> InferM [(Range, ModParam, ActualArg)]
checkArity (forall a. Located a -> Range
srcRange Located (ImpName Name)
f) ModuleG ()
mf ModuleInstanceArgs Name
as
     ModuleG (Located (ImpName Name))
m2 <- do [ArgInst]
as2 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg [(Range, ModParam, ActualArg)]
argIs
              let ([Subst]
tySus,[[Decl]]
decls) = forall a b. [(a, b)] -> ([a], [b])
unzip [ (Subst
su,[Decl]
ds) | DefinedInst Subst
su [Decl]
ds <- [ArgInst]
as2 ]
              let ?tSu = [Subst] -> Subst
mergeDistinctSubst [Subst]
tySus
                  ?vSu = Map Name Name
inst
              let m1 :: ModuleG ()
m1   = forall t. (ModuleInstance t, Su) => t -> t
moduleInstance ModuleG ()
mf
                  m2 :: ModuleG (Located (ImpName Name))
m2   = ModuleG ()
m1 { mName :: Located (ImpName Name)
mName             = Located (ImpName Name)
m
                            , mDoc :: Maybe Text
mDoc              = forall a. Maybe a
Nothing
                            , mParamTypes :: Map Name ModTParam
mParamTypes       = forall a. Monoid a => a
mempty
                            , mParamFuns :: Map Name ModVParam
mParamFuns        = forall a. Monoid a => a
mempty
                            , mParamConstraints :: [Located Prop]
mParamConstraints = forall a. Monoid a => a
mempty
                            , mParams :: FunctorParams
mParams           = forall a. Monoid a => a
mempty
                            , mDecls :: [DeclGroup]
mDecls = forall a b. (a -> b) -> [a] -> [b]
map Decl -> DeclGroup
NonRecursive (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl]]
decls) forall a. [a] -> [a] -> [a]
++
                                      forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG ()
m1
                            }
              let ([Set (MBQual TParam)]
tps,[[Prop]]
tcs,[Map (MBQual Name) Prop]
vps) =
                      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  = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set (MBQual TParam)]
tps
                  tpSet' :: Set TParam
tpSet' = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall a b. (a, b) -> b
snd (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 = forall a. Set a -> Bool
Set.null (forall t. FVS t => t -> Set TParam
freeParams (forall a. Located a -> a
thing Located t
p)
                                                forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set TParam
tpSet')

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

              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 (forall a. Located a -> Range
srcRange Located Prop
lp)) [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
                                 (forall a b. (a -> b) -> [a] -> [b]
map forall a. Located a -> a
thing [Located Prop]
delayPs forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Prop]]
tcs)
                                 (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

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

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

     case forall a. Located a -> a
thing Located (ImpName Name)
m of
       P.ImpTop {}    -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InferM TCTopEntity
endModule
       P.ImpNested {} -> InferM ()
endSubmodule forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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, which could be:

  * `Left` instanciate using another parameter that is in scope
  * `Right` instanciate using a module, with the given interface
-}
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 = forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
arg
                      , thing :: Ident
thing    = forall a. [a] -> a
head (forall k a. Map k a -> [k]
Map.keys FunctorParams
ps0)
                      }
      in forall {a}.
[(Range, a, ActualArg)]
-> Map Ident a
-> [ModuleInstanceNamedArg Name]
-> InferM [(Range, a, ActualArg)]
checkArgs [] FunctorParams
ps0 [ forall name.
Located Ident
-> Located (ModuleInstanceArg name) -> ModuleInstanceNamedArg name
P.ModuleInstanceNamedArg Located Ident
i Located (ModuleInstanceArg Name)
arg ]

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

    P.DefaultInstAnonArg {} -> forall a. HasCallStack => String -> [String] -> a
panic String
"checkArity" [ String
"DefaultInstAnonArg" ]
  where
  ps0 :: FunctorParams
ps0 = 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 forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [k]
Map.keys Map Ident a
ps) \Ident
p ->
                 Maybe Range -> Error -> InferM ()
recordErrorLoc (forall a. a -> Maybe a
Just Range
r) (Ident -> Error
FunctorInstanceMissingArgument Ident
p)
               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 forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall a. Located a -> a
thing Located Ident
ll) Map Ident a
ps of
          Just a
i ->
            do Maybe ActualArg
arg <- case forall a. Located a -> a
thing Located (ModuleInstanceArg Name)
lm of
                        P.ModuleArg ImpName Name
m -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. IfaceG () -> ActualArg
UseModule 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 forall a. Range -> InferM a -> InferM a
inRange (forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
lm)
                                              (Error -> InferM ()
recordError (Ident -> Error
MissingModParam Ident
p))
                                      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
                                Just ModParam
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just (ModParam -> ActualArg
UseParameter ModParam
a))
                        ModuleInstanceArg Name
P.AddParams -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (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  -> (forall a. Located a -> Range
srcRange Located (ModuleInstanceArg Name)
lm, a
i, ActualArg
a) 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 (forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (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 (forall a. a -> Maybe a
Just (forall a. Located a -> Range
srcRange Located Ident
ll))
                              (Ident -> Error
FunctorInstanceBadArgument (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 = DefinedInst Subst [Decl] -- ^ Argument that defines the params
             | 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 ::
  (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg :: (Range, ModParam, ActualArg) -> InferM ArgInst
checkArg (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 = forall a. Ord a => [a] -> Set a
Set.fromList
                   (forall a b. (a -> b) -> [a] -> [b]
map (forall {b}. b -> (Maybe ModName, b)
qual forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModTParam -> TParam
mtpParam) (forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
params)))
           cs :: [Prop]
cs = forall a b. (a -> b) -> [a] -> [b]
map 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 <- forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybeWithKey (\Name
_ Maybe Prop
v -> Maybe Prop
v) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ModVParam -> InferM (Maybe Prop)
check (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
params)
       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 (forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys forall {b}. b -> (Maybe ModName, b)
qual Map Name Prop
fs))

  definedInst :: InferM ArgInst
definedInst =
    do [[(TParam, Prop)]]
tRens <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM [(TParam, Prop)]
checkParamType Range
r Map Ident (Kind, Prop)
tyMap) (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 (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 <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Range -> Map Ident (Name, Schema) -> ModVParam -> InferM [Decl]
checkParamValue Range
r Map Ident (Name, Schema)
vMap)
                       [ ModVParam
s { mvpType :: Schema
mvpType = forall t. TVars t => Subst -> t -> t
apSubst Subst
renSu (ModVParam -> Schema
mvpType ModVParam
s) }
                       | ModVParam
s <- forall k a. Map k a -> [a]
Map.elems (ModParamNames -> Map Name ModVParam
mpnFuns ModParamNames
params) ]

       forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst -> [Decl] -> ArgInst
DefinedInst Subst
renSu [Decl]
vDecls)


  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 ->
        ( forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap ModTParam -> (Kind, Prop)
fromTP (ModParamNames -> Map Name ModTParam
mpnTypes ModParamNames
ps)
        , 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 ->
        ( forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [ forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap TySyn -> (Kind, Prop)
fromTS      (IfaceDecls -> Map Name TySyn
ifTySyns IfaceDecls
decls)
                     , forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap Newtype -> (Kind, Prop)
fromNewtype (IfaceDecls -> Map Name Newtype
ifNewtypes IfaceDecls
decls)
                     , forall a b. (a -> b) -> Map Name a -> Map Ident b
nameMapToIdentMap AbstractType -> (Kind, Prop)
fromPrimT   (IfaceDecls -> Map Name AbstractType
ifAbstractTypes IfaceDecls
decls)
                     ]

        , 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      = forall name. IfaceNames name -> Set Name
ifsPublic (forall name. IfaceG name -> IfaceNames name
ifNames IfaceG ()
actual)
        isLocal :: Name -> Bool
isLocal Name
x       = Name
x 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 (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       = (forall t. HasKind t => t -> Kind
kindOf TySyn
ts, TySyn -> Prop
tsDef TySyn
ts)
        fromNewtype :: Newtype -> (Kind, Prop)
fromNewtype Newtype
nt  = (forall t. HasKind t => t -> Kind
kindOf Newtype
nt, Newtype -> [Prop] -> Prop
TNewtype Newtype
nt [])
        fromPrimT :: AbstractType -> (Kind, Prop)
fromPrimT AbstractType
pt    = (forall t. HasKind t => t -> Kind
kindOf AbstractType
pt, TCon -> [Prop] -> Prop
TCon (AbstractType -> TCon
abstractTypeTC AbstractType
pt) [])

      ActualArg
AddDeclParams -> 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 =
  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) <- forall k a. Map k a -> [(k, a)]
Map.toList Map Name a
m ]




-- | Check a type parameter to a module.
checkParamType ::
  Range                 {- ^ Location for error reporting -} ->
  Map Ident (Kind,Type) {- ^ Actual types -} ->
  (Name,ModTParam)      {- ^ Type parameter -} ->
  InferM [(TParam,Type)]  {- ^ Mapping from parameter name to actual type -}
checkParamType :: Range
-> Map Ident (Kind, Prop)
-> (Name, ModTParam)
-> InferM [(TParam, Prop)]
checkParamType 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 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 (forall a. a -> Maybe a
Just Range
r) (Namespace -> Ident -> Error
FunctorInstanceMissingName Namespace
NSType Ident
i)
         forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    Just (Kind
actualK,Prop
actualT) ->
      do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Kind
expectK forall a. Eq a => a -> a -> Bool
== Kind
actualK)
           (Maybe Range -> Error -> InferM ()
recordErrorLoc (forall a. a -> Maybe a
Just Range
r)
                           (Maybe TypeSource -> Kind -> Kind -> Error
KindMismatch (forall a. a -> Maybe a
Just (Name -> TypeSource
TVFromModParam Name
name))
                                                  Kind
expectK Kind
actualK))
         forall (f :: * -> *) a. Applicative f => a -> f a
pure [(ModTParam -> TParam
mtpParam ModTParam
mp, Prop
actualT)]

-- | Check a value parameter to a module.
checkParamValue ::
  Range                   {- ^ Location for error reporting -} ->
  Map Ident (Name,Schema) {- ^ Actual values -} ->
  ModVParam               {- ^ The parameter we are checking -} ->
  InferM [Decl]           {- ^ Mapping from parameter name to definition -}
checkParamValue :: Range -> Map Ident (Name, Schema) -> ModVParam -> InferM [Decl]
checkParamValue 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 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 (forall a. a -> Maybe a
Just Range
r) (Namespace -> Ident -> Error
FunctorInstanceMissingName Namespace
NSValue Ident
i)
            forall (f :: * -> *) a. Applicative f => a -> f a
pure []
       Just (Name, Schema)
actual ->
         do Expr
e <- Range -> (Name, Schema) -> (Name, Schema) -> InferM Expr
mkParamDef Range
r (Name
name,Schema
expectT) (Name, Schema)
actual
            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
                         }

            forall (f :: * -> *) a. Applicative f => a -> f a
pure [Decl
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 :: 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
    ([],[]) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> Maybe a
Just (Schema -> Prop
sType Schema
sch))
    ([TParam], [Prop])
_ ->
      do Maybe Range -> Error -> InferM ()
recordErrorLoc (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))))
         forall (f :: * -> *) a. Applicative f => a -> f a
pure 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) <- forall a. InferM a -> InferM (a, [Goal])
collectGoals
          forall a b. (a -> b) -> a -> b
$ 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  = forall a. a -> Maybe a
Just Range
r
                                         }
                        Prop
t
               ConstraintSource -> [Prop] -> InferM ()
newGoals (Range -> ConstraintSource
CtModuleInstance Range
r) [Prop]
props
               forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e
     Subst
su <- Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
proveImplication Bool
False
                            (forall a. a -> Maybe a
Just Name
pname)
                            (Schema -> [TParam]
sVars Schema
wantedS)
                            (Schema -> [Prop]
sProps Schema
wantedS)
                            [Goal]
todo
     let res :: Expr
res  = 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Expr -> Expr
EProofAbs (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)  (Schema -> [Prop]
sProps Schema
wantedS)

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