    {-# 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 =
      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 [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 (Range, ModParam, ActualArg) -> InferM ArgInst
    checkArg [(Range, ModParam, ActualArg)]
    argIs
                  let ([Subst]
    tySus,[[Decl]]
    decls) = [(Subst, [Decl])] -> ([Subst], [[Decl]])
    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 = ?vSu::Map Name Name
    Map Name Name
    inst
                  let m1 :: ModuleG ()
    m1   = ModuleG () -> ModuleG ()
    forall t.
    (ModuleInstance t, (?tSu::Subst, ?vSu::Map Name Name)) =>
    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              = Maybe Text
    forall a. Maybe a
    Nothing
                                , mParamTypes :: Map Name ModTParam
    mParamTypes       = Map Name ModTParam
    forall a. Monoid a => a
    mempty
                                , mParamFuns :: Map Name ModVParam
    mParamFuns        = Map Name ModVParam
    forall a. Monoid a => a
    mempty
                                , mParamConstraints :: [Located Prop]
    mParamConstraints = [Located Prop]
    forall a. Monoid a => a
    mempty
                                , mParams :: FunctorParams
    mParams           = FunctorParams
    forall a. Monoid a => a
    mempty
                                , mDecls :: [DeclGroup]
    mDecls = (Decl -> DeclGroup) -> [Decl] -> [DeclGroup]
    forall a b. (a -> b) -> [a] -> [b]
    map Decl -> DeclGroup
    NonRecursive ([[Decl]] -> [Decl]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Decl]]
    decls) [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++
                                          ModuleG () -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls ModuleG ()
    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

         case Located (ImpName Name) -> ImpName Name
    forall a. Located a -> a
    thing Located (ImpName Name)
    m of
           P.ImpTop ModName
    mn    -> ModName -> ExportSpec Name -> InferM ()
    newModuleScope ModName
    mn (ModuleG (Located (ImpName Name)) -> ExportSpec Name
    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 (ModuleG (Located (ImpName Name)) -> ExportSpec Name
    forall mname. ModuleG mname -> ExportSpec Name
    mExports ModuleG (Located (ImpName Name))
    m2)

         (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))
         (Newtype -> InferM ()) -> [Newtype] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ Newtype -> InferM ()
    addNewtype   (Map Name Newtype -> [Newtype]
    forall k a. Map k a -> [a]
    Map.elems (ModuleG (Located (ImpName Name)) -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes ModuleG (Located (ImpName Name))
    m2))
         (AbstractType -> InferM ()) -> [AbstractType] -> InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ AbstractType -> InferM ()
    addPrimType  (Map Name AbstractType -> [AbstractType]
    forall k a. Map k a -> [a]
    Map.elems (ModuleG (Located (ImpName Name)) -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes 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, 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 = 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 = 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 = [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 <- ((Name, ModTParam) -> InferM [(TParam, Prop)])
    -> [(Name, ModTParam)] -> InferM [[(TParam, 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) -> [a] -> m [b]
    mapM (Range
    -> Map Ident (Kind, Prop)
    -> (Name, ModTParam)
    -> InferM [(TParam, Prop)]
    checkParamType 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 <- [[Decl]] -> [Decl]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Decl]] -> [Decl]) -> InferM [[Decl]] -> InferM [Decl]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                      (ModVParam -> InferM [Decl]) -> [ModVParam] -> InferM [[Decl]]
    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 (Range -> Map Ident (Name, Schema) -> ModVParam -> InferM [Decl]
    checkParamValue Range
    r Map Ident (Name, Schema)
    vMap)
                           [ ModVParam
    s { mvpType :: Schema
    mvpType = Subst -> Schema -> Schema
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    renSu (ModVParam -> Schema
    mvpType ModVParam
    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 (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 ->
            ( (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)
                         , (Newtype -> (Kind, Prop))
    -> Map Name Newtype -> Map Ident (Kind, Prop)
    forall a b. (a -> b) -> Map Name a -> Map Ident b
    nameMapToIdentMap Newtype -> (Kind, Prop)
    fromNewtype (IfaceDecls -> Map Name Newtype
    ifNewtypes IfaceDecls
    decls)
                         , (AbstractType -> (Kind, Prop))
    -> Map Name AbstractType -> Map Ident (Kind, Prop)
    forall a b. (a -> b) -> Map Name a -> Map Ident b
    nameMapToIdentMap AbstractType -> (Kind, Prop)
    fromPrimT   (IfaceDecls -> Map Name AbstractType
    ifAbstractTypes 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)
            fromNewtype :: Newtype -> (Kind, Prop)
    fromNewtype Newtype
    nt  = (Newtype -> Kind
    forall t. HasKind t => t -> Kind
    kindOf Newtype
    nt, Newtype -> [Prop] -> Prop
    TNewtype Newtype
    nt [])
            fromPrimT :: AbstractType -> (Kind, Prop)
    fromPrimT AbstractType
    pt    = (AbstractType -> Kind
    forall t. HasKind t => t -> Kind
    kindOf AbstractType
    pt, TCon -> [Prop] -> Prop
    TCon (AbstractType -> TCon
    abstractTypeTC AbstractType
    pt) [])

          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 ::
      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 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)] -> InferM [(TParam, Prop)]
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
        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))
             [(TParam, Prop)] -> InferM [(TParam, Prop)]
    forall a. a -> InferM a
    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 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] -> InferM [Decl]
    forall a. a -> InferM a
    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
                             }

                [Decl] -> InferM [Decl]
    forall a. a -> InferM a
    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
        ([],[]) -> 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