    -- | Transformed a parametrized module into an ordinary module
    -- where everything is parameterized by the module's parameters.
    -- Note that this reuses the names from the original parameterized module.
    module Cryptol.Transform.AddModParams (addModParams) where

    import           Data.Map ( Map )
    import qualified Data.Map as Map
    import           Data.Set ( Set )
    import qualified Data.Set as Set
    import           Data.Either(partitionEithers)
    import           Data.List(find,sortBy)
    import           Data.Ord(comparing)

    import Cryptol.TypeCheck.AST
    import Cryptol.Parser.Position(thing)
    import Cryptol.ModuleSystem.Name(toParamInstName,asParamName,nameIdent
                                    ,paramModRecParam)
    import Cryptol.Utils.Ident(paramInstModName)

    {-
    Note that we have to be careful when doing this transformation on
    polyomorphic values.  In particular,

    Consider type parameters AS, with constraints CS, and value
    parameters (xs : TS).

        f : {as} PS => t
        f = f`{as} (<> ..)

        ~~>

        f : {AS ++ as} (CS ++ PS) => { TS } -> t
        f = /\ (AS ++ as) ->
            \\ (CS ++ PS) ->
            \r -> f`{AS ++ as} (<> ...) r

    The tricky bit is that we can't just replace `f` with
    a new version of `f` with some arguments, instead ew have
    to modify the whole instantiation of `f` : f`{as} (<>...)

    -}

    addModParams :: Module -> Either [Name] Module
    addModParams :: Module -> Either [Name] Module
    addModParams m :: Module
    m =
      case Module -> Either [Name] Params
    getParams Module
    m of
        Left errs :: [Name]
    errs -> [Name] -> Either [Name] Module
    forall a b. a -> Either a b
    Left [Name]
    errs
        Right ps :: Params
    ps ->
         let toInst :: Set Name
    toInst = [Set Name] -> Set Name
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ( Map Name TySyn -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (Module -> Map Name TySyn
    mTySyns Module
    m)
                                 Set Name -> [Set Name] -> [Set Name]
    forall a. a -> [a] -> [a]
    : Map Name Newtype -> Set Name
    forall k a. Map k a -> Set k
    Map.keysSet (Module -> Map Name Newtype
    mNewtypes Module
    m)
                                 Set Name -> [Set Name] -> [Set Name]
    forall a. a -> [a] -> [a]
    : (DeclGroup -> Set Name) -> [DeclGroup] -> [Set Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DeclGroup -> Set Name
    defs (Module -> [DeclGroup]
    mDecls Module
    m)
                                 )
             inp :: (Set Name, Params)
    inp = (Set Name
    toInst, Params
    ps { pTypeConstraints :: [Prop]
    pTypeConstraints = (Set Name, Params) -> [Prop] -> [Prop]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    inp (Params -> [Prop]
    pTypeConstraints Params
    ps) })

         in Module -> Either [Name] Module
    forall a b. b -> Either a b
    Right Module
    m { mName :: ModName
    mName = ModName -> ModName
    paramInstModName (Module -> ModName
    mName Module
    m)
                    , mTySyns :: Map Name TySyn
    mTySyns = (Set Name, Params) -> Map Name TySyn -> Map Name TySyn
    forall a.
    (AddParams a, Inst a) =>
    (Set Name, Params) -> Map Name a -> Map Name a
    fixMap (Set Name, Params)
    inp (Module -> Map Name TySyn
    mTySyns Module
    m)
                    , mNewtypes :: Map Name Newtype
    mNewtypes = (Set Name, Params) -> Map Name Newtype -> Map Name Newtype
    forall a.
    (AddParams a, Inst a) =>
    (Set Name, Params) -> Map Name a -> Map Name a
    fixMap (Set Name, Params)
    inp (Module -> Map Name Newtype
    mNewtypes Module
    m)
                    , mDecls :: [DeclGroup]
    mDecls = (Set Name, Params) -> [DeclGroup] -> [DeclGroup]
    forall a. (AddParams a, Inst a) => (Set Name, Params) -> a -> a
    fixUp (Set Name, Params)
    inp (Module -> [DeclGroup]
    mDecls Module
    m)
                    , mParamTypes :: Map Name ModTParam
    mParamTypes = Map Name ModTParam
    forall k a. Map k a
    Map.empty
                    , mParamConstraints :: [Located Prop]
    mParamConstraints = []
                    , mParamFuns :: Map Name ModVParam
    mParamFuns = Map Name ModVParam
    forall k a. Map k a
    Map.empty
                    }

    defs :: DeclGroup -> Set Name
    defs :: DeclGroup -> Set Name
    defs dg :: DeclGroup
    dg =
      case DeclGroup
    dg of
        Recursive ds :: [Decl]
    ds -> [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList ((Decl -> Name) -> [Decl] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Decl -> Name
    dName [Decl]
    ds)
        NonRecursive d :: Decl
    d -> Name -> Set Name
    forall a. a -> Set a
    Set.singleton (Decl -> Name
    dName Decl
    d)

    fixUp :: (AddParams a, Inst a) => Inp -> a -> a
    fixUp :: (Set Name, Params) -> a -> a
    fixUp i :: (Set Name, Params)
    i = Params -> a -> a
    forall a. AddParams a => Params -> a -> a
    addParams ((Set Name, Params) -> Params
    forall a b. (a, b) -> b
    snd (Set Name, Params)
    i) (a -> a) -> (a -> a) -> a -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Set Name, Params) -> a -> a
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    i

    fixMap :: (AddParams a, Inst a) => Inp -> Map Name a -> Map Name a
    fixMap :: (Set Name, Params) -> Map Name a -> Map Name a
    fixMap i :: (Set Name, Params)
    i m :: Map Name a
    m =
      [(Name, a)] -> Map Name a
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Name -> Name
    toParamInstName Name
    x, (Set Name, Params) -> a -> a
    forall a. (AddParams a, Inst a) => (Set Name, Params) -> a -> a
    fixUp (Set Name, Params)
    i a
    a) | (x :: Name
    x,a :: a
    a) <- Map Name a -> [(Name, a)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map Name a
    m ]

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

    data Params = Params
      { Params -> [TParam]
    pTypes            :: [TParam]
      , Params -> [Prop]
    pTypeConstraints  :: [Prop]
      , Params -> [(Name, Prop)]
    pFuns             :: [(Name,Type)]
      }

    getParams :: Module -> Either [Name] Params
    getParams :: Module -> Either [Name] Params
    getParams m :: Module
    m
      | [Name] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Name]
    errs =
         let ps :: Params
    ps = Params :: [TParam] -> [Prop] -> [(Name, Prop)] -> Params
    Params { pTypes :: [TParam]
    pTypes = (ModTParam -> TParam) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map ModTParam -> TParam
    rnTP
                                  ([ModTParam] -> [TParam]) -> [ModTParam] -> [TParam]
    forall a b. (a -> b) -> a -> b
    $ (ModTParam -> ModTParam -> Ordering) -> [ModTParam] -> [ModTParam]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    sortBy ((ModTParam -> Int) -> ModTParam -> ModTParam -> Ordering
    forall a b. Ord a => (b -> a) -> b -> b -> Ordering
    comparing ModTParam -> Int
    mtpNumber)
                                  ([ModTParam] -> [ModTParam]) -> [ModTParam] -> [ModTParam]
    forall a b. (a -> b) -> a -> b
    $ Map Name ModTParam -> [ModTParam]
    forall k a. Map k a -> [a]
    Map.elems
                                  (Map Name ModTParam -> [ModTParam])
    -> Map Name ModTParam -> [ModTParam]
    forall a b. (a -> b) -> a -> b
    $ Module -> Map Name ModTParam
    mParamTypes Module
    m
                         , pTypeConstraints :: [Prop]
    pTypeConstraints = (Located Prop -> Prop) -> [Located Prop] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map Located Prop -> Prop
    forall a. Located a -> a
    thing (Module -> [Located Prop]
    mParamConstraints Module
    m)
                         , pFuns :: [(Name, Prop)]
    pFuns = [(Name, Prop)]
    oks
                         }
         in Params -> Either [Name] Params
    forall a b. b -> Either a b
    Right Params
    ps
      | Bool
    otherwise = [Name] -> Either [Name] Params
    forall a b. a -> Either a b
    Left [Name]
    errs
      where
      (errs :: [Name]
    errs,oks :: [(Name, Prop)]
    oks) = [Either Name (Name, Prop)] -> ([Name], [(Name, Prop)])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers (((Name, ModVParam) -> Either Name (Name, Prop))
    -> [(Name, ModVParam)] -> [Either Name (Name, Prop)]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, ModVParam) -> Either Name (Name, Prop)
    checkFunP (Map Name ModVParam -> [(Name, ModVParam)]
    forall k a. Map k a -> [(k, a)]
    Map.toList (Module -> Map Name ModVParam
    mParamFuns Module
    m)))

      checkFunP :: (Name, ModVParam) -> Either Name (Name, Prop)
    checkFunP (x :: Name
    x,s :: ModVParam
    s) = case Schema -> Maybe Prop
    isMono (ModVParam -> Schema
    mvpType ModVParam
    s) of
                          Just t :: Prop
    t  -> (Name, Prop) -> Either Name (Name, Prop)
    forall a b. b -> Either a b
    Right (Name -> Name
    asParamName Name
    x, Prop
    t)
                          Nothing -> Name -> Either Name (Name, Prop)
    forall a b. a -> Either a b
    Left Name
    x

      rnTP :: ModTParam -> TParam
    rnTP tp :: ModTParam
    tp = ModTParam -> TParam
    mtpParam ModTParam
    tp { mtpName :: Name
    mtpName = Name -> Name
    asParamName (ModTParam -> Name
    mtpName ModTParam
    tp) }

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

    class AddParams a where
      addParams :: Params -> a -> a

    instance AddParams a => AddParams [a] where
      addParams :: Params -> [a] -> [a]
    addParams ps :: Params
    ps = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map (Params -> a -> a
    forall a. AddParams a => Params -> a -> a
    addParams Params
    ps)

    instance AddParams Schema where
      addParams :: Params -> Schema -> Schema
    addParams ps :: Params
    ps s :: Schema
    s = Schema
    s { sVars :: [TParam]
    sVars  = Params -> [TParam]
    pTypes Params
    ps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ Schema -> [TParam]
    sVars Schema
    s
                         , sProps :: [Prop]
    sProps = Params -> [Prop]
    pTypeConstraints Params
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ Schema -> [Prop]
    sProps Schema
    s
                         , sType :: Prop
    sType  = Params -> Prop -> Prop
    forall a. AddParams a => Params -> a -> a
    addParams Params
    ps (Schema -> Prop
    sType Schema
    s)
                         }

    instance AddParams Type where
      addParams :: Params -> Prop -> Prop
    addParams ps :: Params
    ps t :: Prop
    t
        | [(Name, Prop)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Params -> [(Name, Prop)]
    pFuns Params
    ps) = Prop
    t
        | Bool
    otherwise       = Prop -> Prop -> Prop
    tFun (Params -> Prop
    paramRecTy Params
    ps) Prop
    t

    instance AddParams Expr where
      addParams :: Params -> Expr -> Expr
    addParams ps :: Params
    ps e :: Expr
    e = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> Expr -> Expr
    ETAbs Expr
    withProps (Params -> [TParam]
    pTypes Params
    ps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ [TParam]
    as)
        where (as :: [TParam]
    as,rest1 :: Expr
    rest1) = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (TParam, Expr)
    splitTAbs Expr
    e
              (bs :: [Prop]
    bs,rest2 :: Expr
    rest2) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (Prop, Expr)
    splitProofAbs Expr
    rest1
              withProps :: Expr
    withProps = (Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> Expr -> Expr
    EProofAbs Expr
    withArgs (Params -> [Prop]
    pTypeConstraints Params
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    bs)
              withArgs :: Expr
    withArgs
                | [(Name, Prop)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Params -> [(Name, Prop)]
    pFuns Params
    ps) = Expr
    rest2
                | Bool
    otherwise       = Name -> Prop -> Expr -> Expr
    EAbs Name
    paramModRecParam (Params -> Prop
    paramRecTy Params
    ps) Expr
    rest2

    instance AddParams DeclGroup where
      addParams :: Params -> DeclGroup -> DeclGroup
    addParams ps :: Params
    ps dg :: DeclGroup
    dg =
        case DeclGroup
    dg of
          Recursive ds :: [Decl]
    ds -> [Decl] -> DeclGroup
    Recursive (Params -> [Decl] -> [Decl]
    forall a. AddParams a => Params -> a -> a
    addParams Params
    ps [Decl]
    ds)
          NonRecursive d :: Decl
    d -> Decl -> DeclGroup
    NonRecursive (Params -> Decl -> Decl
    forall a. AddParams a => Params -> a -> a
    addParams Params
    ps Decl
    d)

    instance AddParams Decl where
      addParams :: Params -> Decl -> Decl
    addParams ps :: Params
    ps d :: Decl
    d =
        case Decl -> DeclDef
    dDefinition Decl
    d of
          DPrim   -> Decl
    d
          DExpr e :: Expr
    e -> Decl
    d { dSignature :: Schema
    dSignature = Params -> Schema -> Schema
    forall a. AddParams a => Params -> a -> a
    addParams Params
    ps (Decl -> Schema
    dSignature Decl
    d)
                       , dDefinition :: DeclDef
    dDefinition = Expr -> DeclDef
    DExpr (Params -> Expr -> Expr
    forall a. AddParams a => Params -> a -> a
    addParams Params
    ps Expr
    e)
                       , dName :: Name
    dName = Name -> Name
    toParamInstName (Decl -> Name
    dName Decl
    d)
                       }

    instance AddParams TySyn where
      addParams :: Params -> TySyn -> TySyn
    addParams ps :: Params
    ps ts :: TySyn
    ts = TySyn
    ts { tsParams :: [TParam]
    tsParams = Params -> [TParam]
    pTypes Params
    ps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ TySyn -> [TParam]
    tsParams TySyn
    ts
                           , tsConstraints :: [Prop]
    tsConstraints = Params -> [Prop]
    pTypeConstraints Params
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ TySyn -> [Prop]
    tsConstraints TySyn
    ts
                              --  do we need these here ^ ?
                           , tsName :: Name
    tsName = Name -> Name
    toParamInstName (TySyn -> Name
    tsName TySyn
    ts)
                           }

    instance AddParams Newtype where
      addParams :: Params -> Newtype -> Newtype
    addParams ps :: Params
    ps nt :: Newtype
    nt = Newtype
    nt { ntParams :: [TParam]
    ntParams = Params -> [TParam]
    pTypes Params
    ps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ Newtype -> [TParam]
    ntParams Newtype
    nt
                           , ntConstraints :: [Prop]
    ntConstraints = Params -> [Prop]
    pTypeConstraints Params
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ Newtype -> [Prop]
    ntConstraints Newtype
    nt
                           , ntName :: Name
    ntName = Name -> Name
    toParamInstName (Newtype -> Name
    ntName Newtype
    nt)
                           }

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

    -- | Adjust uses of names to account for the new parameters.
    -- Assumes unique names---no capture or shadowing.
    class Inst a where
      inst :: Inp -> a -> a

    -- | Set of top-level names which need to be instantiate, and module parameters.
    type Inp = (Set Name, Params)

    paramRecTy :: Params -> Type
    paramRecTy :: Params -> Prop
    paramRecTy ps :: Params
    ps = [(Ident, Prop)] -> Prop
    tRec [ (Name -> Ident
    nameIdent Name
    x, Prop
    t) | (x :: Name
    x,t :: Prop
    t) <- Params -> [(Name, Prop)]
    pFuns Params
    ps ]

    nameInst :: Inp -> Name -> [Type] -> Int -> Expr
    nameInst :: (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
    nameInst (_,ps :: Params
    ps) x :: Name
    x ts :: [Prop]
    ts prfs :: Int
    prfs
      | [(Name, Prop)] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null (Params -> [(Name, Prop)]
    pFuns Params
    ps) = Expr
    withProofs
      | Bool
    otherwise       = Expr -> Expr -> Expr
    EApp Expr
    withProofs (Name -> Expr
    EVar Name
    paramModRecParam)
      where
      withProofs :: Expr
    withProofs = (Expr -> Expr) -> Expr -> [Expr]
    forall a. (a -> a) -> a -> [a]
    iterate Expr -> Expr
    EProofApp Expr
    withTys [Expr] -> Int -> Expr
    forall a. [a] -> Int -> a
    !!
                                            ([Prop] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Params -> [Prop]
    pTypeConstraints Params
    ps) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    prfs)

      withTys :: Expr
    withTys    = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Expr -> Prop -> Expr
    ETApp (Name -> Expr
    EVar (Name -> Name
    toParamInstName Name
    x))
                               ((TParam -> Prop) -> [TParam] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar -> Prop
    TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TVar
    tpVar) (Params -> [TParam]
    pTypes Params
    ps) [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ts)

    -- | Extra parameters to dd when instantiating a type
    instTyParams :: Inp -> [Type]
    instTyParams :: (Set Name, Params) -> [Prop]
    instTyParams (_,ps :: Params
    ps) = (TParam -> Prop) -> [TParam] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar -> Prop
    TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TVar
    tpVar) (Params -> [TParam]
    pTypes Params
    ps)

    needsInst :: Inp -> Name -> Bool
    needsInst :: (Set Name, Params) -> Name -> Bool
    needsInst (xs :: Set Name
    xs,_) x :: Name
    x = Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Name
    x Set Name
    xs

    isVParam :: Inp -> Name -> Bool
    isVParam :: (Set Name, Params) -> Name -> Bool
    isVParam (_,ps :: Params
    ps) x :: Name
    x = Name
    x Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((Name, Prop) -> Name) -> [(Name, Prop)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Prop) -> Name
    forall a b. (a, b) -> a
    fst (Params -> [(Name, Prop)]
    pFuns Params
    ps)

    isTParam :: Inp -> TVar -> Maybe TParam
    isTParam :: (Set Name, Params) -> TVar -> Maybe TParam
    isTParam (_,ps :: Params
    ps) x :: TVar
    x =
      case TVar
    x of
        TVBound tp :: TParam
    tp -> (TParam -> Bool) -> [TParam] -> Maybe TParam
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    find TParam -> Bool
    thisName (Params -> [TParam]
    pTypes Params
    ps)
          where thisName :: TParam -> Bool
    thisName y :: TParam
    y = TParam -> Maybe Name
    tpName TParam
    tp Maybe Name -> Maybe Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == TParam -> Maybe Name
    tpName TParam
    y
        _ -> Maybe TParam
    forall a. Maybe a
    Nothing

    instance Inst a => Inst [a] where
      inst :: (Set Name, Params) -> [a] -> [a]
    inst ps :: (Set Name, Params)
    ps = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Set Name, Params) -> a -> a
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps)

    instance Inst Expr where
      inst :: (Set Name, Params) -> Expr -> Expr
    inst ps :: (Set Name, Params)
    ps expr :: Expr
    expr =
        case Expr
    expr of
         EVar x :: Name
    x
          | (Set Name, Params) -> Name -> Bool
    needsInst (Set Name, Params)
    ps Name
    x -> (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
    nameInst (Set Name, Params)
    ps Name
    x [] 0
          | (Set Name, Params) -> Name -> Bool
    isVParam (Set Name, Params)
    ps Name
    x ->
            let sh :: [Ident]
    sh = ((Name, Prop) -> Ident) -> [(Name, Prop)] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Ident
    nameIdent (Name -> Ident) -> ((Name, Prop) -> Name) -> (Name, Prop) -> Ident
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, Prop) -> Name
    forall a b. (a, b) -> a
    fst) (Params -> [(Name, Prop)]
    pFuns ((Set Name, Params) -> Params
    forall a b. (a, b) -> b
    snd (Set Name, Params)
    ps))
            in Expr -> Selector -> Expr
    ESel (Name -> Expr
    EVar Name
    paramModRecParam) (Ident -> Maybe [Ident] -> Selector
    RecordSel (Name -> Ident
    nameIdent Name
    x) ([Ident] -> Maybe [Ident]
    forall a. a -> Maybe a
    Just [Ident]
    sh))
          | Bool
    otherwise -> Name -> Expr
    EVar Name
    x

         EList es :: [Expr]
    es t :: Prop
    t -> [Expr] -> Prop -> Expr
    EList ((Set Name, Params) -> [Expr] -> [Expr]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [Expr]
    es) ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t)
         ETuple es :: [Expr]
    es -> [Expr] -> Expr
    ETuple ((Set Name, Params) -> [Expr] -> [Expr]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [Expr]
    es)
         ERec fs :: [(Ident, Expr)]
    fs   -> [(Ident, Expr)] -> Expr
    ERec [ (Ident
    f,(Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e) | (f :: Ident
    f,e :: Expr
    e) <- [(Ident, Expr)]
    fs ]
         ESel e :: Expr
    e s :: Selector
    s  -> Expr -> Selector -> Expr
    ESel ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e) Selector
    s
         ESet e :: Expr
    e s :: Selector
    s v :: Expr
    v -> Expr -> Selector -> Expr -> Expr
    ESet ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e) Selector
    s ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    v)

         EIf e1 :: Expr
    e1 e2 :: Expr
    e2 e3 :: Expr
    e3 -> Expr -> Expr -> Expr -> Expr
    EIf ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e1) ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e2) ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e3)
         EComp t1 :: Prop
    t1 t2 :: Prop
    t2 e :: Expr
    e ms :: [[Match]]
    ms -> Prop -> Prop -> Expr -> [[Match]] -> Expr
    EComp ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t1) ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t2)
                                   ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e) ((Set Name, Params) -> [[Match]] -> [[Match]]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [[Match]]
    ms)

         ETAbs x :: TParam
    x e :: Expr
    e -> TParam -> Expr -> Expr
    ETAbs TParam
    x ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e)
         ETApp e1 :: Expr
    e1 t :: Prop
    t ->
          case Expr -> (Expr, [Prop], Int)
    splitExprInst Expr
    expr of
             (EVar x :: Name
    x, ts :: [Prop]
    ts, prfs :: Int
    prfs) | (Set Name, Params) -> Name -> Bool
    needsInst (Set Name, Params)
    ps Name
    x -> (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
    nameInst (Set Name, Params)
    ps Name
    x [Prop]
    ts Int
    prfs
             _ -> Expr -> Prop -> Expr
    ETApp ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e1) Prop
    t

         EApp e1 :: Expr
    e1 e2 :: Expr
    e2 -> Expr -> Expr -> Expr
    EApp ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e1) ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e2)
         EAbs x :: Name
    x t :: Prop
    t e :: Expr
    e -> Name -> Prop -> Expr -> Expr
    EAbs Name
    x ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t) ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e)

         EProofAbs p :: Prop
    p e :: Expr
    e -> Prop -> Expr -> Expr
    EProofAbs ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    p) ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e)
         EProofApp e1 :: Expr
    e1 ->
           case Expr -> (Expr, [Prop], Int)
    splitExprInst Expr
    expr of
             (EVar x :: Name
    x, ts :: [Prop]
    ts, prfs :: Int
    prfs) | (Set Name, Params) -> Name -> Bool
    needsInst (Set Name, Params)
    ps Name
    x -> (Set Name, Params) -> Name -> [Prop] -> Int -> Expr
    nameInst (Set Name, Params)
    ps Name
    x [Prop]
    ts Int
    prfs
             _ -> Expr -> Expr
    EProofApp ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e1)

         EWhere e :: Expr
    e dgs :: [DeclGroup]
    dgs  -> Expr -> [DeclGroup] -> Expr
    EWhere ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e) ((Set Name, Params) -> [DeclGroup] -> [DeclGroup]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [DeclGroup]
    dgs)

    instance Inst Match where
      inst :: (Set Name, Params) -> Match -> Match
    inst ps :: (Set Name, Params)
    ps m :: Match
    m =
        case Match
    m of
          From x :: Name
    x t1 :: Prop
    t1 t2 :: Prop
    t2 e :: Expr
    e -> Name -> Prop -> Prop -> Expr -> Match
    From Name
    x ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t1) ((Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t2) ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e)
          Let d :: Decl
    d          -> Decl -> Match
    Let ((Set Name, Params) -> Decl -> Decl
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Decl
    d)

    instance Inst DeclGroup where
      inst :: (Set Name, Params) -> DeclGroup -> DeclGroup
    inst ps :: (Set Name, Params)
    ps dg :: DeclGroup
    dg =
        case DeclGroup
    dg of
          Recursive ds :: [Decl]
    ds -> [Decl] -> DeclGroup
    Recursive ((Set Name, Params) -> [Decl] -> [Decl]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [Decl]
    ds)
          NonRecursive d :: Decl
    d -> Decl -> DeclGroup
    NonRecursive ((Set Name, Params) -> Decl -> Decl
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Decl
    d)

    instance Inst Decl where
      inst :: (Set Name, Params) -> Decl -> Decl
    inst ps :: (Set Name, Params)
    ps d :: Decl
    d = Decl
    d { dDefinition :: DeclDef
    dDefinition = (Set Name, Params) -> DeclDef -> DeclDef
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps (Decl -> DeclDef
    dDefinition Decl
    d) }

    instance Inst DeclDef where
      inst :: (Set Name, Params) -> DeclDef -> DeclDef
    inst ps :: (Set Name, Params)
    ps d :: DeclDef
    d =
        case DeclDef
    d of
          DPrim -> DeclDef
    DPrim
          DExpr e :: Expr
    e -> Expr -> DeclDef
    DExpr ((Set Name, Params) -> Expr -> Expr
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Expr
    e)

    instance Inst Type where
      inst :: (Set Name, Params) -> Prop -> Prop
    inst ps :: (Set Name, Params)
    ps ty :: Prop
    ty =
        case Prop
    ty of
          TUser x :: Name
    x ts :: [Prop]
    ts t :: Prop
    t
            | (Set Name, Params) -> Name -> Bool
    needsInst (Set Name, Params)
    ps Name
    x -> Name -> [Prop] -> Prop -> Prop
    TUser Name
    x ((Set Name, Params) -> [Prop]
    instTyParams (Set Name, Params)
    ps [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ts1) Prop
    t1
            | Bool
    otherwise      -> Name -> [Prop] -> Prop -> Prop
    TUser Name
    x [Prop]
    ts1 Prop
    t1
            where ts1 :: [Prop]
    ts1 = (Set Name, Params) -> [Prop] -> [Prop]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [Prop]
    ts
                  t1 :: Prop
    t1  = (Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t

          TCon tc :: TCon
    tc ts :: [Prop]
    ts ->
            case TCon
    tc of
              TC (TCNewtype (UserTC x :: Name
    x k :: Kind
    k))
                | (Set Name, Params) -> Name -> Bool
    needsInst (Set Name, Params)
    ps Name
    x -> TCon -> [Prop] -> Prop
    TCon (TC -> TCon
    TC (UserTC -> TC
    TCNewtype (Name -> Kind -> UserTC
    UserTC Name
    x (Kind -> Kind
    k1 Kind
    k))))
                                         ([Prop]
    newTs [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ts1)
              _ -> TCon -> [Prop] -> Prop
    TCon TCon
    tc [Prop]
    ts1
            where
            ts1 :: [Prop]
    ts1 = (Set Name, Params) -> [Prop] -> [Prop]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps [Prop]
    ts
            newTs :: [Prop]
    newTs = (Set Name, Params) -> [Prop]
    instTyParams (Set Name, Params)
    ps
            k1 :: Kind -> Kind
    k1 k :: Kind
    k = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Kind -> Kind -> Kind
    (:->) Kind
    k ((Prop -> Kind) -> [Prop] -> [Kind]
    forall a b. (a -> b) -> [a] -> [b]
    map Prop -> Kind
    forall t. HasKind t => t -> Kind
    kindOf [Prop]
    newTs)

          TVar x :: TVar
    x | Just x' :: TParam
    x' <- (Set Name, Params) -> TVar -> Maybe TParam
    isTParam (Set Name, Params)
    ps TVar
    x -> TVar -> Prop
    TVar (TParam -> TVar
    TVBound TParam
    x')
                 | Bool
    otherwise  -> Prop
    ty

          TRec xs :: [(Ident, Prop)]
    xs -> [(Ident, Prop)] -> Prop
    TRec [ (Ident
    f,(Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t) | (f :: Ident
    f,t :: Prop
    t) <- [(Ident, Prop)]
    xs ]

    instance Inst TySyn where
      inst :: (Set Name, Params) -> TySyn -> TySyn
    inst ps :: (Set Name, Params)
    ps ts :: TySyn
    ts = TySyn
    ts { tsConstraints :: [Prop]
    tsConstraints = (Set Name, Params) -> [Prop] -> [Prop]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps (TySyn -> [Prop]
    tsConstraints TySyn
    ts)
                      , tsDef :: Prop
    tsDef = (Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps (TySyn -> Prop
    tsDef TySyn
    ts)
                      }

    instance Inst Newtype where
      inst :: (Set Name, Params) -> Newtype -> Newtype
    inst ps :: (Set Name, Params)
    ps nt :: Newtype
    nt = Newtype
    nt { ntConstraints :: [Prop]
    ntConstraints = (Set Name, Params) -> [Prop] -> [Prop]
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps (Newtype -> [Prop]
    ntConstraints Newtype
    nt)
                      , ntFields :: [(Ident, Prop)]
    ntFields = [ (Ident
    f, (Set Name, Params) -> Prop -> Prop
    forall a. Inst a => (Set Name, Params) -> a -> a
    inst (Set Name, Params)
    ps Prop
    t) | (f :: Ident
    f,t :: Prop
    t) <- Newtype -> [(Ident, Prop)]
    ntFields Newtype
    nt ]
                      }