    {-# Language FlexibleInstances, PatternGuards #-}
    -- | Assumes that local names do not shadow top level names.
    module Cryptol.ModuleSystem.InstantiateModule
      ( instantiateModule
      ) where

    import           Data.Set (Set)
    import qualified Data.Set as Set
    import           Data.Map (Map)
    import qualified Data.Map as Map
    import           MonadLib(ReaderT,runReaderT,ask)

    import Cryptol.Parser.Position(Located(..))
    import Cryptol.ModuleSystem.Name
    import Cryptol.ModuleSystem.Exports(ExportSpec(..))
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Subst(listParamSubst, apSubst)
    import Cryptol.Utils.Ident(ModName,modParamIdent)

    {-
    XXX: Should we simplify constraints in the instantiated modules?

    If so, we also need to adjust the constraint parameters on terms appropriately,
    especially when working with dictionaries.
    -}

    -- | Convert a module instantiation into a partial module.
    -- The resulting module is incomplete because it is missing the definitions
    -- from the instantiation.
    instantiateModule :: FreshM m =>
                         Module           {- ^ Parametrized module -} ->
                         ModName          {- ^ Name of the new module -} ->
                         Map TParam Type  {- ^ Type params -} ->
                         Map Name Expr    {- ^ Value parameters -} ->
                         m ([Located Prop], Module)
                         -- ^ Instantiated constraints, fresh module, new supply
    instantiateModule :: Module
    -> ModName
    -> Map TParam Type
    -> Map Name Expr
    -> m ([Located Type], Module)
    instantiateModule func :: Module
    func newName :: ModName
    newName tpMap :: Map TParam Type
    tpMap vpMap :: Map Name Expr
    vpMap =
      ModName
    -> ReaderT ModName m ([Located Type], Module)
    -> m ([Located Type], Module)
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT ModName
    newName (ReaderT ModName m ([Located Type], Module)
     -> m ([Located Type], Module))
    -> ReaderT ModName m ([Located Type], Module)
    -> m ([Located Type], Module)
    forall a b. (a -> b) -> a -> b
    $
        do let oldVpNames :: [Name]
    oldVpNames = Map Name Expr -> [Name]
    forall k a. Map k a -> [k]
    Map.keys Map Name Expr
    vpMap
           [Name]
    newVpNames <- (Name -> ReaderT ModName m Name)
    -> [Name] -> ReaderT ModName m [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Name -> ReaderT ModName m Name
    forall (m :: * -> *). FreshM m => Name -> InstM m Name
    freshParamName (Map Name Expr -> [Name]
    forall k a. Map k a -> [k]
    Map.keys Map Name Expr
    vpMap)
           let vpNames :: Map Name Name
    vpNames = [(Name, Name)] -> Map Name Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([Name] -> [Name] -> [(Name, Name)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    oldVpNames [Name]
    newVpNames)

           Env
    env <- Module -> Map TParam Type -> Map Name Name -> InstM m Env
    forall (m :: * -> *).
    FreshM m =>
    Module -> Map TParam Type -> Map Name Name -> InstM m Env
    computeEnv Module
    func Map TParam Type
    tpMap Map Name Name
    vpNames

           let rnMp :: Inst a => (a -> Name) -> Map Name a -> Map Name a
               rnMp :: (a -> Name) -> Map Name a -> Map Name a
    rnMp f :: a -> Name
    f m :: Map Name a
    m = [(Name, a)] -> Map Name a
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (a -> Name
    f a
    x, a
    x) | a
    a <- Map Name a -> [a]
    forall k a. Map k a -> [a]
    Map.elems Map Name a
    m
                                                  , let x :: a
    x = Env -> a -> a
    forall t. Inst t => Env -> t -> t
    inst Env
    env a
    a ]

               renamedExports :: ExportSpec Name
    renamedExports  = Env -> ExportSpec Name -> ExportSpec Name
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Module -> ExportSpec Name
    mExports Module
    func)
               renamedTySyns :: Map Name TySyn
    renamedTySyns   = (TySyn -> Name) -> Map Name TySyn -> Map Name TySyn
    forall a. Inst a => (a -> Name) -> Map Name a -> Map Name a
    rnMp TySyn -> Name
    tsName (Module -> Map Name TySyn
    mTySyns Module
    func)
               renamedNewtypes :: Map Name Newtype
    renamedNewtypes = (Newtype -> Name) -> Map Name Newtype -> Map Name Newtype
    forall a. Inst a => (a -> Name) -> Map Name a -> Map Name a
    rnMp Newtype -> Name
    ntName (Module -> Map Name Newtype
    mNewtypes Module
    func)
               renamedPrimTys :: Map Name AbstractType
    renamedPrimTys  = (AbstractType -> Name)
    -> Map Name AbstractType -> Map Name AbstractType
    forall a. Inst a => (a -> Name) -> Map Name a -> Map Name a
    rnMp AbstractType -> Name
    atName (Module -> Map Name AbstractType
    mPrimTypes Module
    func)

               su :: Subst
    su = [(TParam, Type)] -> Subst
    listParamSubst (Map TParam Type -> [(TParam, Type)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Env -> Map TParam Type
    tyParamMap Env
    env))

               goals :: [Located Type]
    goals = (Located Type -> Located Type) -> [Located Type] -> [Located Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Type -> Type) -> Located Type -> Located Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Subst -> Type -> Type
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su)) (Module -> [Located Type]
    mParamConstraints Module
    func)
               -- Constraints to discharge about the type instances

           let renamedDecls :: [DeclGroup]
    renamedDecls = Env -> [DeclGroup] -> [DeclGroup]
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Module -> [DeclGroup]
    mDecls Module
    func)
               paramDecls :: [DeclGroup]
    paramDecls = ((Name, Expr) -> DeclGroup) -> [(Name, Expr)] -> [DeclGroup]
    forall a b. (a -> b) -> [a] -> [b]
    map (Subst -> Map Name Name -> (Name, Expr) -> DeclGroup
    mkParamDecl Subst
    su Map Name Name
    vpNames) (Map Name Expr -> [(Name, Expr)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name Expr
    vpMap)

           ([Located Type], Module)
    -> ReaderT ModName m ([Located Type], Module)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( [Located Type]
    goals
                  , $WModule :: ModName
    -> ExportSpec Name
    -> [Import]
    -> Map Name TySyn
    -> Map Name Newtype
    -> Map Name AbstractType
    -> Map Name ModTParam
    -> [Located Type]
    -> Map Name ModVParam
    -> [DeclGroup]
    -> Module
    Module
                     { mName :: ModName
    mName              = ModName
    newName
                     , mExports :: ExportSpec Name
    mExports           = ExportSpec Name
    renamedExports
                     , mImports :: [Import]
    mImports           = Module -> [Import]
    mImports Module
    func
                     , mTySyns :: Map Name TySyn
    mTySyns            = Map Name TySyn
    renamedTySyns
                     , mNewtypes :: Map Name Newtype
    mNewtypes          = Map Name Newtype
    renamedNewtypes
                     , mPrimTypes :: Map Name AbstractType
    mPrimTypes         = Map Name AbstractType
    renamedPrimTys
                     , mParamTypes :: Map Name ModTParam
    mParamTypes        = Map Name ModTParam
    forall k a. Map k a
    Map.empty
                     , mParamConstraints :: [Located Type]
    mParamConstraints  = []
                     , mParamFuns :: Map Name ModVParam
    mParamFuns         = Map Name ModVParam
    forall k a. Map k a
    Map.empty
                     , mDecls :: [DeclGroup]
    mDecls             = [DeclGroup]
    paramDecls [DeclGroup] -> [DeclGroup] -> [DeclGroup]
    forall a. [a] -> [a] -> [a]
    ++ [DeclGroup]
    renamedDecls
                     } )

      where
      mkParamDecl :: Subst -> Map Name Name -> (Name, Expr) -> DeclGroup
    mkParamDecl su :: Subst
    su vpNames :: Map Name Name
    vpNames (x :: Name
    x,e :: Expr
    e) =
          Decl -> DeclGroup
    NonRecursive $WDecl :: Name
    -> Schema
    -> DeclDef
    -> [Pragma]
    -> Bool
    -> Maybe Fixity
    -> Maybe String
    -> Decl
    Decl
            { dName :: Name
    dName        = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault (String -> Name
    forall a. HasCallStack => String -> a
    error "OOPS") Name
    x Map Name Name
    vpNames
            , dSignature :: Schema
    dSignature   = Subst -> Schema -> Schema
    forall t. TVars t => Subst -> t -> t
    apSubst Subst
    su
                           (Schema -> Schema) -> Schema -> Schema
    forall a b. (a -> b) -> a -> b
    $ ModVParam -> Schema
    mvpType
                           (ModVParam -> Schema) -> ModVParam -> Schema
    forall a b. (a -> b) -> a -> b
    $ ModVParam -> Name -> Map Name ModVParam -> ModVParam
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault (String -> ModVParam
    forall a. HasCallStack => String -> a
    error "UUPS") Name
    x (Module -> Map Name ModVParam
    mParamFuns Module
    func)
            , dDefinition :: DeclDef
    dDefinition  = Expr -> DeclDef
    DExpr Expr
    e
            , dPragmas :: [Pragma]
    dPragmas     = []      -- XXX: which if any pragmas?
            , dInfix :: Bool
    dInfix       = Bool
    False   -- XXX: get from parameter?
            , dFixity :: Maybe Fixity
    dFixity      = Maybe Fixity
    forall a. Maybe a
    Nothing -- XXX: get from parameter
            , dDoc :: Maybe String
    dDoc         = Maybe String
    forall a. Maybe a
    Nothing -- XXX: get from parametr(or instance?)
            }

    --------------------------------------------------------------------------------
    -- Things that need to be renamed

    class Defines t where
      defines :: t -> Set Name

    instance Defines t => Defines [t] where
      defines :: [t] -> Set Name
    defines = [Set Name] -> Set Name
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Name] -> Set Name) -> ([t] -> [Set Name]) -> [t] -> Set Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (t -> Set Name) -> [t] -> [Set Name]
    forall a b. (a -> b) -> [a] -> [b]
    map t -> Set Name
    forall t. Defines t => t -> Set Name
    defines

    instance Defines Decl where
      defines :: Decl -> Set Name
    defines = Name -> Set Name
    forall a. a -> Set a
    Set.singleton (Name -> Set Name) -> (Decl -> Name) -> Decl -> Set Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Decl -> Name
    dName

    instance Defines DeclGroup where
      defines :: DeclGroup -> Set Name
    defines d :: DeclGroup
    d =
        case DeclGroup
    d of
          NonRecursive x :: Decl
    x -> Decl -> Set Name
    forall t. Defines t => t -> Set Name
    defines Decl
    x
          Recursive x :: [Decl]
    x    -> [Decl] -> Set Name
    forall t. Defines t => t -> Set Name
    defines [Decl]
    x

    --------------------------------------------------------------------------------

    type InstM = ReaderT ModName

    -- | Generate a new instance of a declared name.
    freshenName :: FreshM m => Name -> InstM m Name
    freshenName :: Name -> InstM m Name
    freshenName x :: Name
    x =
      do ModName
    m <- ReaderT ModName m ModName
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         let sys :: NameSource
    sys = case Name -> NameInfo
    nameInfo Name
    x of
                     Declared _ s :: NameSource
    s -> NameSource
    s
                     _            -> NameSource
    UserName
         (Supply -> (Name, Supply)) -> InstM m Name
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply (ModName
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    mkDeclared ModName
    m NameSource
    sys (Name -> Ident
    nameIdent Name
    x) (Name -> Maybe Fixity
    nameFixity Name
    x) (Name -> Range
    nameLoc Name
    x))

    freshParamName :: FreshM m => Name -> InstM m Name
    freshParamName :: Name -> InstM m Name
    freshParamName x :: Name
    x =
      do ModName
    m <- ReaderT ModName m ModName
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         let newName :: Ident
    newName = Ident -> Ident
    modParamIdent (Name -> Ident
    nameIdent Name
    x)
         (Supply -> (Name, Supply)) -> InstM m Name
    forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
    liftSupply (ModName
    -> NameSource
    -> Ident
    -> Maybe Fixity
    -> Range
    -> Supply
    -> (Name, Supply)
    mkDeclared ModName
    m NameSource
    UserName Ident
    newName (Name -> Maybe Fixity
    nameFixity Name
    x) (Name -> Range
    nameLoc Name
    x))

    -- | Compute renaming environment from a module instantiation.
    -- computeEnv :: ModInst -> InstM Env
    computeEnv :: FreshM m =>
                  Module {- ^ Functor being instantiated -} ->
                  Map TParam Type {- replace type params by type -} ->
                  Map Name Name {- replace value parameters by other names -} ->
                  InstM m Env
    computeEnv :: Module -> Map TParam Type -> Map Name Name -> InstM m Env
    computeEnv m :: Module
    m tpMap :: Map TParam Type
    tpMap vpMap :: Map Name Name
    vpMap =
      do [(Name, Name)]
    tss <- ((Name, TySyn) -> ReaderT ModName m (Name, Name))
    -> [(Name, TySyn)] -> ReaderT ModName m [(Name, Name)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name, TySyn) -> ReaderT ModName m (Name, Name)
    forall (m :: * -> *) b.
    FreshM m =>
    (Name, b) -> ReaderT ModName m (Name, Name)
    freshTy (Map Name TySyn -> [(Name, TySyn)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Module -> Map Name TySyn
    mTySyns Module
    m))
         [(Name, Name)]
    nts <- ((Name, Newtype) -> ReaderT ModName m (Name, Name))
    -> [(Name, Newtype)] -> ReaderT ModName m [(Name, Name)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name, Newtype) -> ReaderT ModName m (Name, Name)
    forall (m :: * -> *) b.
    FreshM m =>
    (Name, b) -> ReaderT ModName m (Name, Name)
    freshTy (Map Name Newtype -> [(Name, Newtype)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Module -> Map Name Newtype
    mNewtypes Module
    m))
         let tnMap :: Map Name Name
    tnMap = [(Name, Name)] -> Map Name Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Name, Name)]
    tss [(Name, Name)] -> [(Name, Name)] -> [(Name, Name)]
    forall a. [a] -> [a] -> [a]
    ++ [(Name, Name)]
    nts)

         [(Name, Name)]
    defHere <- (Name -> ReaderT ModName m (Name, Name))
    -> [Name] -> ReaderT ModName m [(Name, Name)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Name -> ReaderT ModName m (Name, Name)
    forall (m :: * -> *).
    FreshM m =>
    Name -> ReaderT ModName m (Name, Name)
    mkVParam (Set Name -> [Name]
    forall a. Set a -> [a]
    Set.toList ([DeclGroup] -> Set Name
    forall t. Defines t => t -> Set Name
    defines (Module -> [DeclGroup]
    mDecls Module
    m)))
         let fnMap :: Map Name Name
    fnMap = Map Name Name -> Map Name Name -> Map Name Name
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    Map.union Map Name Name
    vpMap ([(Name, Name)] -> Map Name Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, Name)]
    defHere)

         Env -> InstM m Env
    forall (m :: * -> *) a. Monad m => a -> m a
    return Env :: Map Name Name -> Map Name Name -> Map TParam Type -> Env
    Env { funNameMap :: Map Name Name
    funNameMap  = Map Name Name
    fnMap
                    , tyNameMap :: Map Name Name
    tyNameMap   = Map Name Name
    tnMap
                    , tyParamMap :: Map TParam Type
    tyParamMap  = Map TParam Type
    tpMap
                    }
      where
      freshTy :: (Name, b) -> ReaderT ModName m (Name, Name)
    freshTy (x :: Name
    x,_) = do Name
    y <- Name -> InstM m Name
    forall (m :: * -> *). FreshM m => Name -> InstM m Name
    freshenName Name
    x
                         (Name, Name) -> ReaderT ModName m (Name, Name)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    x,Name
    y)

      mkVParam :: Name -> ReaderT ModName m (Name, Name)
    mkVParam x :: Name
    x = do Name
    y <- Name -> InstM m Name
    forall (m :: * -> *). FreshM m => Name -> InstM m Name
    freshenName Name
    x
                      (Name, Name) -> ReaderT ModName m (Name, Name)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name
    x,Name
    y)

    --------------------------------------------------------------------------------
    -- Do the renaming

    data Env = Env
      { Env -> Map Name Name
    funNameMap  :: Map Name Name
      , Env -> Map Name Name
    tyNameMap   :: Map Name Name
      , Env -> Map TParam Type
    tyParamMap  :: Map TParam Type
      } deriving Int -> Env -> ShowS
    [Env] -> ShowS
    Env -> String
    (Int -> Env -> ShowS)
    -> (Env -> String) -> ([Env] -> ShowS) -> Show Env
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Env] -> ShowS
    $cshowList :: [Env] -> ShowS
    show :: Env -> String
    $cshow :: Env -> String
    showsPrec :: Int -> Env -> ShowS
    $cshowsPrec :: Int -> Env -> ShowS
    Show

    class Inst t where
      inst :: Env -> t -> t

    instance Inst a => Inst [a] where
      inst :: Env -> [a] -> [a]
    inst env :: Env
    env = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Env -> a -> a
    forall t. Inst t => Env -> t -> t
    inst Env
    env)

    instance Inst Expr where
      inst :: Env -> Expr -> Expr
    inst env :: Env
    env = Expr -> Expr
    go
        where
        go :: Expr -> Expr
    go expr :: Expr
    expr =
          case Expr
    expr of
            EVar x :: Name
    x -> case Name -> Map Name Name -> Maybe Name
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (Env -> Map Name Name
    funNameMap Env
    env) of
                        Just y :: Name
    y -> Name -> Expr
    EVar Name
    y
                        _      -> Expr
    expr

            EList xs :: [Expr]
    xs t :: Type
    t                -> [Expr] -> Type -> Expr
    EList (Env -> [Expr] -> [Expr]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [Expr]
    xs) (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t)
            ETuple es :: [Expr]
    es                 -> [Expr] -> Expr
    ETuple (Env -> [Expr] -> [Expr]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [Expr]
    es)
            ERec xs :: [(Ident, Expr)]
    xs                   -> [(Ident, Expr)] -> Expr
    ERec [ (Ident
    f,Expr -> Expr
    go Expr
    e) | (f :: Ident
    f,e :: Expr
    e) <- [(Ident, Expr)]
    xs ]
            ESel e :: Expr
    e s :: Selector
    s                  -> Expr -> Selector -> Expr
    ESel (Expr -> Expr
    go Expr
    e) Selector
    s
            ESet e :: Expr
    e x :: Selector
    x v :: Expr
    v                -> Expr -> Selector -> Expr -> Expr
    ESet (Expr -> Expr
    go Expr
    e) Selector
    x (Expr -> Expr
    go Expr
    v)
            EIf e1 :: Expr
    e1 e2 :: Expr
    e2 e3 :: Expr
    e3              -> Expr -> Expr -> Expr -> Expr
    EIf (Expr -> Expr
    go Expr
    e1) (Expr -> Expr
    go Expr
    e2) (Expr -> Expr
    go Expr
    e3)
            EComp t1 :: Type
    t1 t2 :: Type
    t2 e :: Expr
    e mss :: [[Match]]
    mss         -> Type -> Type -> Expr -> [[Match]] -> Expr
    EComp (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t1) (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t2)
                                               (Expr -> Expr
    go Expr
    e)
                                               (Env -> [[Match]] -> [[Match]]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [[Match]]
    mss)
            ETAbs t :: TParam
    t e :: Expr
    e                 -> TParam -> Expr -> Expr
    ETAbs TParam
    t (Expr -> Expr
    go Expr
    e)
            ETApp e :: Expr
    e t :: Type
    t                 -> Expr -> Type -> Expr
    ETApp (Expr -> Expr
    go Expr
    e) (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t)
            EApp e1 :: Expr
    e1 e2 :: Expr
    e2                -> Expr -> Expr -> Expr
    EApp (Expr -> Expr
    go Expr
    e1) (Expr -> Expr
    go Expr
    e2)
            EAbs x :: Name
    x t :: Type
    t e :: Expr
    e                -> Name -> Type -> Expr -> Expr
    EAbs Name
    x (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t) (Expr -> Expr
    go Expr
    e)
            EProofAbs p :: Type
    p e :: Expr
    e             -> Type -> Expr -> Expr
    EProofAbs (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    p) (Expr -> Expr
    go Expr
    e)
            EProofApp e :: Expr
    e               -> Expr -> Expr
    EProofApp (Expr -> Expr
    go Expr
    e)
            EWhere e :: Expr
    e ds :: [DeclGroup]
    ds               -> Expr -> [DeclGroup] -> Expr
    EWhere (Expr -> Expr
    go Expr
    e) (Env -> [DeclGroup] -> [DeclGroup]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [DeclGroup]
    ds)

    instance Inst DeclGroup where
      inst :: Env -> DeclGroup -> DeclGroup
    inst env :: Env
    env dg :: DeclGroup
    dg =
        case DeclGroup
    dg of
          NonRecursive d :: Decl
    d -> Decl -> DeclGroup
    NonRecursive (Env -> Decl -> Decl
    forall t. Inst t => Env -> t -> t
    inst Env
    env Decl
    d)
          Recursive ds :: [Decl]
    ds   -> [Decl] -> DeclGroup
    Recursive (Env -> [Decl] -> [Decl]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [Decl]
    ds)

    instance Inst DeclDef where
      inst :: Env -> DeclDef -> DeclDef
    inst env :: Env
    env d :: DeclDef
    d =
        case DeclDef
    d of
          DPrim   -> DeclDef
    DPrim
          DExpr e :: Expr
    e -> Expr -> DeclDef
    DExpr (Env -> Expr -> Expr
    forall t. Inst t => Env -> t -> t
    inst Env
    env Expr
    e)

    instance Inst Decl where
      inst :: Env -> Decl -> Decl
    inst env :: Env
    env d :: Decl
    d = Decl
    d { dSignature :: Schema
    dSignature = Env -> Schema -> Schema
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Decl -> Schema
    dSignature Decl
    d)
                     , dDefinition :: DeclDef
    dDefinition = Env -> DeclDef -> DeclDef
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Decl -> DeclDef
    dDefinition Decl
    d)
                     , dName :: Name
    dName = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault (Decl -> Name
    dName Decl
    d) (Decl -> Name
    dName Decl
    d)
                                                             (Env -> Map Name Name
    funNameMap Env
    env)
                     }

    instance Inst Match where
      inst :: Env -> Match -> Match
    inst env :: Env
    env m :: Match
    m =
        case Match
    m of
          From x :: Name
    x t1 :: Type
    t1 t2 :: Type
    t2 e :: Expr
    e -> Name -> Type -> Type -> Expr -> Match
    From Name
    x (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t1) (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t2) (Env -> Expr -> Expr
    forall t. Inst t => Env -> t -> t
    inst Env
    env Expr
    e)
          Let d :: Decl
    d          -> Decl -> Match
    Let (Env -> Decl -> Decl
    forall t. Inst t => Env -> t -> t
    inst Env
    env Decl
    d)

    instance Inst Schema where
      inst :: Env -> Schema -> Schema
    inst env :: Env
    env s :: Schema
    s = Schema
    s { sProps :: [Type]
    sProps = Env -> [Type] -> [Type]
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Schema -> [Type]
    sProps Schema
    s)
                     , sType :: Type
    sType  = Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Schema -> Type
    sType Schema
    s)
                     }

    instance Inst Type where
      inst :: Env -> Type -> Type
    inst env :: Env
    env ty :: Type
    ty =
        case Type
    ty of
          TCon tc :: TCon
    tc ts :: [Type]
    ts    -> TCon -> [Type] -> Type
    TCon (Env -> TCon -> TCon
    forall t. Inst t => Env -> t -> t
    inst Env
    env TCon
    tc) (Env -> [Type] -> [Type]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [Type]
    ts)
          TVar tv :: TVar
    tv       ->
            case TVar
    tv of
              TVBound tp :: TParam
    tp | Just t :: Type
    t <- TParam -> Map TParam Type -> Maybe Type
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TParam
    tp (Env -> Map TParam Type
    tyParamMap Env
    env) -> Type
    t
              _ -> Type
    ty
          TUser x :: Name
    x ts :: [Type]
    ts t :: Type
    t  -> Name -> [Type] -> Type -> Type
    TUser Name
    y (Env -> [Type] -> [Type]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [Type]
    ts) (Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t)
            where y :: Name
    y = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    x Name
    x (Env -> Map Name Name
    tyNameMap Env
    env)
          TRec fs :: [(Ident, Type)]
    fs       -> [(Ident, Type)] -> Type
    TRec [ (Ident
    f, Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t) | (f :: Ident
    f,t :: Type
    t) <- [(Ident, Type)]
    fs ]

    instance Inst TCon where
      inst :: Env -> TCon -> TCon
    inst env :: Env
    env tc :: TCon
    tc =
        case TCon
    tc of
          TC x :: TC
    x -> TC -> TCon
    TC (Env -> TC -> TC
    forall t. Inst t => Env -> t -> t
    inst Env
    env TC
    x)
          _    -> TCon
    tc

    instance Inst TC where
      inst :: Env -> TC -> TC
    inst env :: Env
    env tc :: TC
    tc =
        case TC
    tc of
          TCNewtype x :: UserTC
    x  -> UserTC -> TC
    TCNewtype (Env -> UserTC -> UserTC
    forall t. Inst t => Env -> t -> t
    inst Env
    env UserTC
    x)
          TCAbstract x :: UserTC
    x -> UserTC -> TC
    TCAbstract (Env -> UserTC -> UserTC
    forall t. Inst t => Env -> t -> t
    inst Env
    env UserTC
    x)
          _            -> TC
    tc

    instance Inst UserTC where
      inst :: Env -> UserTC -> UserTC
    inst env :: Env
    env (UserTC x :: Name
    x t :: Kind
    t) = Name -> Kind -> UserTC
    UserTC Name
    y Kind
    t
        where y :: Name
    y = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    x Name
    x (Env -> Map Name Name
    tyNameMap Env
    env)

    instance Inst (ExportSpec Name) where
      inst :: Env -> ExportSpec Name -> ExportSpec Name
    inst env :: Env
    env es :: ExportSpec Name
    es = ExportSpec :: forall name. Set name -> Set name -> ExportSpec name
    ExportSpec { eTypes :: Set Name
    eTypes = (Name -> Name) -> Set Name -> Set Name
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map Name -> Name
    instT (ExportSpec Name -> Set Name
    forall name. ExportSpec name -> Set name
    eTypes ExportSpec Name
    es)
                               , eBinds :: Set Name
    eBinds = (Name -> Name) -> Set Name -> Set Name
    forall b a. Ord b => (a -> b) -> Set a -> Set b
    Set.map Name -> Name
    instV (ExportSpec Name -> Set Name
    forall name. ExportSpec name -> Set name
    eBinds ExportSpec Name
    es)
                               }
        where instT :: Name -> Name
    instT x :: Name
    x = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    x Name
    x (Env -> Map Name Name
    tyNameMap Env
    env)
              instV :: Name -> Name
    instV x :: Name
    x = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    x Name
    x (Env -> Map Name Name
    funNameMap Env
    env)

    instance Inst TySyn where
      inst :: Env -> TySyn -> TySyn
    inst env :: Env
    env ts :: TySyn
    ts = $WTySyn :: Name -> [TParam] -> [Type] -> Type -> Maybe String -> TySyn
    TySyn { tsName :: Name
    tsName = Env -> Name -> Name
    instTyName Env
    env Name
    x
                          , tsParams :: [TParam]
    tsParams = TySyn -> [TParam]
    tsParams TySyn
    ts
                          , tsConstraints :: [Type]
    tsConstraints = Env -> [Type] -> [Type]
    forall t. Inst t => Env -> t -> t
    inst Env
    env (TySyn -> [Type]
    tsConstraints TySyn
    ts)
                          , tsDef :: Type
    tsDef = Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env (TySyn -> Type
    tsDef TySyn
    ts)
                          , tsDoc :: Maybe String
    tsDoc = TySyn -> Maybe String
    tsDoc TySyn
    ts
                          }
        where x :: Name
    x = TySyn -> Name
    tsName TySyn
    ts

    instance Inst Newtype where
      inst :: Env -> Newtype -> Newtype
    inst env :: Env
    env nt :: Newtype
    nt = Newtype :: Name
    -> [TParam] -> [Type] -> [(Ident, Type)] -> Maybe String -> Newtype
    Newtype { ntName :: Name
    ntName = Env -> Name -> Name
    instTyName Env
    env Name
    x
                            , ntParams :: [TParam]
    ntParams = Newtype -> [TParam]
    ntParams Newtype
    nt
                            , ntConstraints :: [Type]
    ntConstraints = Env -> [Type] -> [Type]
    forall t. Inst t => Env -> t -> t
    inst Env
    env (Newtype -> [Type]
    ntConstraints Newtype
    nt)
                            , ntFields :: [(Ident, Type)]
    ntFields = [ (Ident
    f,Env -> Type -> Type
    forall t. Inst t => Env -> t -> t
    inst Env
    env Type
    t) | (f :: Ident
    f,t :: Type
    t) <- Newtype -> [(Ident, Type)]
    ntFields Newtype
    nt ]
                            , ntDoc :: Maybe String
    ntDoc = Newtype -> Maybe String
    ntDoc Newtype
    nt
                            }
        where x :: Name
    x = Newtype -> Name
    ntName Newtype
    nt

    instance Inst AbstractType where
      inst :: Env -> AbstractType -> AbstractType
    inst env :: Env
    env a :: AbstractType
    a = AbstractType :: Name
    -> Kind
    -> ([TParam], [Type])
    -> Maybe Fixity
    -> Maybe String
    -> AbstractType
    AbstractType { atName :: Name
    atName    = Env -> Name -> Name
    instTyName Env
    env (AbstractType -> Name
    atName AbstractType
    a)
                                , atKind :: Kind
    atKind    = AbstractType -> Kind
    atKind AbstractType
    a
                                , atCtrs :: ([TParam], [Type])
    atCtrs    = case AbstractType -> ([TParam], [Type])
    atCtrs AbstractType
    a of
                                                (xs :: [TParam]
    xs,ps :: [Type]
    ps) -> ([TParam]
    xs, Env -> [Type] -> [Type]
    forall t. Inst t => Env -> t -> t
    inst Env
    env [Type]
    ps)
                                , atFixitiy :: Maybe Fixity
    atFixitiy = AbstractType -> Maybe Fixity
    atFixitiy AbstractType
    a
                                , atDoc :: Maybe String
    atDoc     = AbstractType -> Maybe String
    atDoc AbstractType
    a
                                }

    instTyName :: Env -> Name -> Name
    instTyName :: Env -> Name -> Name
    instTyName env :: Env
    env x :: Name
    x = Name -> Name -> Map Name Name -> Name
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Name
    x Name
    x (Env -> Map Name Name
    tyNameMap Env
    env)