    {-# LANGUAGE NondecreasingIndentation #-}
    {-# LANGUAGE LambdaCase #-}

    {-
    (c) The University of Glasgow 2006-2008
    (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
    -}

    -- | Module for constructing interface declaration values
    -- from the corresponding 'TyThing's.

    module GHC.Iface.Decl
       ( coAxiomToIfaceDecl
       , tyThingToIfaceDecl -- Converting things to their Iface equivalents
       , toIfaceBooleanFormula
       )
    where

    import GHC.Prelude

    import GHC.Tc.Utils.TcType

    import GHC.Iface.Syntax

    import GHC.CoreToIface

    import GHC.Core.Class
    import GHC.Core.TyCon
    import GHC.Core.Coercion.Axiom
    import GHC.Core.ConLike
    import GHC.Core.DataCon
    import GHC.Core.Type
    import GHC.Core.Multiplicity

    import GHC.Types.Id
    import GHC.Types.Var.Env
    import GHC.Types.Var
    import GHC.Types.Name
    import GHC.Types.Basic
    import GHC.Types.TyThing
    import GHC.Types.SrcLoc

    import GHC.Utils.Panic.Plain
    import GHC.Utils.Misc

    import GHC.Data.FastString
    import GHC.Data.Maybe
    import GHC.Data.BooleanFormula

    import Data.List ( findIndex, mapAccumL )

    {-
    ************************************************************************
    *                                                                      *
                    Converting things to their Iface equivalents
    *                                                                      *
    ************************************************************************
    -}

    tyThingToIfaceDecl :: Bool -> TyThing -> IfaceDecl
    tyThingToIfaceDecl :: Bool -> TyThing -> IfaceDecl
    tyThingToIfaceDecl Bool
    _ (AnId TyCoVar
    id)      = TyCoVar -> IfaceDecl
    idToIfaceDecl TyCoVar
    id
    tyThingToIfaceDecl Bool
    _ (ATyCon TyCon
    tycon) = (TidyEnv, IfaceDecl) -> IfaceDecl
    forall a b. (a, b) -> b
    snd (TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
    tyConToIfaceDecl TidyEnv
    emptyTidyEnv TyCon
    tycon)
    tyThingToIfaceDecl Bool
    _ (ACoAxiom CoAxiom Branched
    ax)  = CoAxiom Branched -> IfaceDecl
    forall (br :: BranchFlag). CoAxiom br -> IfaceDecl
    coAxiomToIfaceDecl CoAxiom Branched
    ax
    tyThingToIfaceDecl Bool
    show_linear_types (AConLike ConLike
    cl)  = case ConLike
    cl of
        RealDataCon DataCon
    dc -> Bool -> DataCon -> IfaceDecl
    dataConToIfaceDecl Bool
    show_linear_types DataCon
    dc -- for ppr purposes only
        PatSynCon PatSyn
    ps   -> PatSyn -> IfaceDecl
    patSynToIfaceDecl PatSyn
    ps

    --------------------------
    idToIfaceDecl :: Id -> IfaceDecl
    -- The Id is already tidied, so that locally-bound names
    -- (lambdas, for-alls) already have non-clashing OccNames
    -- We can't tidy it here, locally, because it may have
    -- free variables in its type or IdInfo
    idToIfaceDecl :: TyCoVar -> IfaceDecl
    idToIfaceDecl TyCoVar
    id
      = IfaceId { ifName :: Name
    ifName      = TyCoVar -> Name
    forall a. NamedThing a => a -> Name
    getName TyCoVar
    id,
                  ifType :: IfaceType
    ifType      = Type -> IfaceType
    toIfaceType (TyCoVar -> Type
    idType TyCoVar
    id),
                  ifIdDetails :: IfaceIdDetails
    ifIdDetails = IdDetails -> IfaceIdDetails
    toIfaceIdDetails (TyCoVar -> IdDetails
    idDetails TyCoVar
    id),
                  ifIdInfo :: IfaceIdInfo
    ifIdInfo    = IdInfo -> IfaceIdInfo
    toIfaceIdInfo (HasDebugCallStack => TyCoVar -> IdInfo
    TyCoVar -> IdInfo
    idInfo TyCoVar
    id) }

    --------------------------
    dataConToIfaceDecl :: Bool -> DataCon -> IfaceDecl
    dataConToIfaceDecl :: Bool -> DataCon -> IfaceDecl
    dataConToIfaceDecl Bool
    show_linear_types DataCon
    dataCon
      = IfaceId { ifName :: Name
    ifName      = DataCon -> Name
    forall a. NamedThing a => a -> Name
    getName DataCon
    dataCon,
                  ifType :: IfaceType
    ifType      = Type -> IfaceType
    toIfaceType (Bool -> DataCon -> Type
    dataConDisplayType Bool
    show_linear_types DataCon
    dataCon),
                  ifIdDetails :: IfaceIdDetails
    ifIdDetails = IfaceIdDetails
    IfVanillaId,
                  ifIdInfo :: IfaceIdInfo
    ifIdInfo    = [] }

    --------------------------
    coAxiomToIfaceDecl :: CoAxiom br -> IfaceDecl
    -- We *do* tidy Axioms, because they are not (and cannot
    -- conveniently be) built in tidy form
    coAxiomToIfaceDecl :: forall (br :: BranchFlag). CoAxiom br -> IfaceDecl
    coAxiomToIfaceDecl ax :: CoAxiom br
    ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
    co_ax_tc = TyCon
    tycon, co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
    co_ax_branches = Branches br
    branches
                                   , co_ax_role :: forall (br :: BranchFlag). CoAxiom br -> Role
    co_ax_role = Role
    role })
     = IfaceAxiom { ifName :: Name
    ifName       = CoAxiom br -> Name
    forall a. NamedThing a => a -> Name
    getName CoAxiom br
    ax
                  , ifTyCon :: IfaceTyCon
    ifTyCon      = TyCon -> IfaceTyCon
    toIfaceTyCon TyCon
    tycon
                  , ifRole :: Role
    ifRole       = Role
    role
                  , ifAxBranches :: [IfaceAxBranch]
    ifAxBranches = (CoAxBranch -> IfaceAxBranch) -> [CoAxBranch] -> [IfaceAxBranch]
    forall a b. (a -> b) -> [a] -> [b]
    map (TyCon -> [[Type]] -> CoAxBranch -> IfaceAxBranch
    coAxBranchToIfaceBranch TyCon
    tycon
                                         ((CoAxBranch -> [Type]) -> [CoAxBranch] -> [[Type]]
    forall a b. (a -> b) -> [a] -> [b]
    map CoAxBranch -> [Type]
    coAxBranchLHS [CoAxBranch]
    branch_list))
                                       [CoAxBranch]
    branch_list }
     where
       branch_list :: [CoAxBranch]
    branch_list = Branches br -> [CoAxBranch]
    forall (br :: BranchFlag). Branches br -> [CoAxBranch]
    fromBranches Branches br
    branches

    -- 2nd parameter is the list of branch LHSs, in case of a closed type family,
    -- for conversion from incompatible branches to incompatible indices.
    -- For an open type family the list should be empty.
    -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom
    coAxBranchToIfaceBranch :: TyCon -> [[Type]] -> CoAxBranch -> IfaceAxBranch
    coAxBranchToIfaceBranch :: TyCon -> [[Type]] -> CoAxBranch -> IfaceAxBranch
    coAxBranchToIfaceBranch TyCon
    tc [[Type]]
    lhs_s
                            (CoAxBranch { cab_tvs :: CoAxBranch -> [TyCoVar]
    cab_tvs = [TyCoVar]
    tvs, cab_cvs :: CoAxBranch -> [TyCoVar]
    cab_cvs = [TyCoVar]
    cvs
                                        , cab_eta_tvs :: CoAxBranch -> [TyCoVar]
    cab_eta_tvs = [TyCoVar]
    eta_tvs
                                        , cab_lhs :: CoAxBranch -> [Type]
    cab_lhs = [Type]
    lhs, cab_roles :: CoAxBranch -> [Role]
    cab_roles = [Role]
    roles
                                        , cab_rhs :: CoAxBranch -> Type
    cab_rhs = Type
    rhs, cab_incomps :: CoAxBranch -> [CoAxBranch]
    cab_incomps = [CoAxBranch]
    incomps })

      = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr]
    ifaxbTyVars  = [TyCoVar] -> [IfaceTvBndr]
    toIfaceTvBndrs [TyCoVar]
    tvs
                      , ifaxbCoVars :: [IfaceIdBndr]
    ifaxbCoVars  = (TyCoVar -> IfaceIdBndr) -> [TyCoVar] -> [IfaceIdBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map TyCoVar -> IfaceIdBndr
    toIfaceIdBndr [TyCoVar]
    cvs
                      , ifaxbEtaTyVars :: [IfaceTvBndr]
    ifaxbEtaTyVars = [TyCoVar] -> [IfaceTvBndr]
    toIfaceTvBndrs [TyCoVar]
    eta_tvs
                      , ifaxbLHS :: IfaceAppArgs
    ifaxbLHS     = TyCon -> [Type] -> IfaceAppArgs
    toIfaceTcArgs TyCon
    tc [Type]
    lhs
                      , ifaxbRoles :: [Role]
    ifaxbRoles   = [Role]
    roles
                      , ifaxbRHS :: IfaceType
    ifaxbRHS     = Type -> IfaceType
    toIfaceType Type
    rhs
                      , ifaxbIncomps :: [BranchIndex]
    ifaxbIncomps = [BranchIndex]
    iface_incomps }
      where
        iface_incomps :: [BranchIndex]
    iface_incomps = (CoAxBranch -> BranchIndex) -> [CoAxBranch] -> [BranchIndex]
    forall a b. (a -> b) -> [a] -> [b]
    map (String -> Maybe BranchIndex -> BranchIndex
    forall a. HasCallStack => String -> Maybe a -> a
    expectJust String
    "iface_incomps"
                            (Maybe BranchIndex -> BranchIndex)
    -> (CoAxBranch -> Maybe BranchIndex) -> CoAxBranch -> BranchIndex
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (([Type] -> Bool) -> [[Type]] -> Maybe BranchIndex)
    -> [[Type]] -> ([Type] -> Bool) -> Maybe BranchIndex
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ([Type] -> Bool) -> [[Type]] -> Maybe BranchIndex
    forall a. (a -> Bool) -> [a] -> Maybe BranchIndex
    findIndex [[Type]]
    lhs_s
                            (([Type] -> Bool) -> Maybe BranchIndex)
    -> (CoAxBranch -> [Type] -> Bool)
    -> CoAxBranch
    -> Maybe BranchIndex
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Type] -> [Type] -> Bool
    eqTypes
                            ([Type] -> [Type] -> Bool)
    -> (CoAxBranch -> [Type]) -> CoAxBranch -> [Type] -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CoAxBranch -> [Type]
    coAxBranchLHS) [CoAxBranch]
    incomps

    -----------------
    tyConToIfaceDecl :: TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
    -- We *do* tidy TyCons, because they are not (and cannot
    -- conveniently be) built in tidy form
    -- The returned TidyEnv is the one after tidying the tyConTyVars
    tyConToIfaceDecl :: TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
    tyConToIfaceDecl TidyEnv
    env TyCon
    tycon
      | Just Class
    clas <- TyCon -> Maybe Class
    tyConClass_maybe TyCon
    tycon
      = TidyEnv -> Class -> (TidyEnv, IfaceDecl)
    classToIfaceDecl TidyEnv
    env Class
    clas

      | Just Type
    syn_rhs <- TyCon -> Maybe Type
    synTyConRhs_maybe TyCon
    tycon
      = ( TidyEnv
    tc_env1
        , IfaceSynonym { ifName :: Name
    ifName    = TyCon -> Name
    forall a. NamedThing a => a -> Name
    getName TyCon
    tycon,
                         ifRoles :: [Role]
    ifRoles   = TyCon -> [Role]
    tyConRoles TyCon
    tycon,
                         ifSynRhs :: IfaceType
    ifSynRhs  = Type -> IfaceType
    if_syn_type Type
    syn_rhs,
                         ifBinders :: [IfaceTyConBinder]
    ifBinders = [IfaceTyConBinder]
    if_binders,
                         ifResKind :: IfaceType
    ifResKind = IfaceType
    if_res_kind
                       })

      | Just FamTyConFlav
    fam_flav <- TyCon -> Maybe FamTyConFlav
    famTyConFlav_maybe TyCon
    tycon
      = ( TidyEnv
    tc_env1
        , IfaceFamily { ifName :: Name
    ifName    = TyCon -> Name
    forall a. NamedThing a => a -> Name
    getName TyCon
    tycon,
                        ifResVar :: Maybe IfLclName
    ifResVar  = Maybe IfLclName
    if_res_var,
                        ifFamFlav :: IfaceFamTyConFlav
    ifFamFlav = FamTyConFlav -> IfaceFamTyConFlav
    to_if_fam_flav FamTyConFlav
    fam_flav,
                        ifBinders :: [IfaceTyConBinder]
    ifBinders = [IfaceTyConBinder]
    if_binders,
                        ifResKind :: IfaceType
    ifResKind = IfaceType
    if_res_kind,
                        ifFamInj :: Injectivity
    ifFamInj  = TyCon -> Injectivity
    tyConInjectivityInfo TyCon
    tycon
                      })

      | TyCon -> Bool
    isAlgTyCon TyCon
    tycon
      = ( TidyEnv
    tc_env1
        , IfaceData { ifName :: Name
    ifName    = TyCon -> Name
    forall a. NamedThing a => a -> Name
    getName TyCon
    tycon,
                      ifBinders :: [IfaceTyConBinder]
    ifBinders = [IfaceTyConBinder]
    if_binders,
                      ifResKind :: IfaceType
    ifResKind = IfaceType
    if_res_kind,
                      ifCType :: Maybe CType
    ifCType   = TyCon -> Maybe CType
    tyConCType_maybe TyCon
    tycon,
                      ifRoles :: [Role]
    ifRoles   = TyCon -> [Role]
    tyConRoles TyCon
    tycon,
                      ifCtxt :: IfaceContext
    ifCtxt    = TidyEnv -> [Type] -> IfaceContext
    tidyToIfaceContext TidyEnv
    tc_env1 (TyCon -> [Type]
    tyConStupidTheta TyCon
    tycon),
                      ifCons :: IfaceConDecls
    ifCons    = AlgTyConRhs -> IfaceConDecls
    ifaceConDecls (TyCon -> AlgTyConRhs
    algTyConRhs TyCon
    tycon),
                      ifGadtSyntax :: Bool
    ifGadtSyntax = TyCon -> Bool
    isGadtSyntaxTyCon TyCon
    tycon,
                      ifParent :: IfaceTyConParent
    ifParent  = IfaceTyConParent
    parent })

      | Bool
    otherwise  -- FunTyCon, PrimTyCon, promoted TyCon/DataCon
      -- We only convert these TyCons to IfaceTyCons when we are
      -- just about to pretty-print them, not because we are going
      -- to put them into interface files
      = ( TidyEnv
    env
        , IfaceData { ifName :: Name
    ifName       = TyCon -> Name
    forall a. NamedThing a => a -> Name
    getName TyCon
    tycon,
                      ifBinders :: [IfaceTyConBinder]
    ifBinders    = [IfaceTyConBinder]
    if_binders,
                      ifResKind :: IfaceType
    ifResKind    = IfaceType
    if_res_kind,
                      ifCType :: Maybe CType
    ifCType      = Maybe CType
    forall a. Maybe a
    Nothing,
                      ifRoles :: [Role]
    ifRoles      = TyCon -> [Role]
    tyConRoles TyCon
    tycon,
                      ifCtxt :: IfaceContext
    ifCtxt       = [],
                      ifCons :: IfaceConDecls
    ifCons       = Bool -> [IfaceConDecl] -> IfaceConDecls
    IfDataTyCon Bool
    False [],
                      ifGadtSyntax :: Bool
    ifGadtSyntax = Bool
    False,
                      ifParent :: IfaceTyConParent
    ifParent     = IfaceTyConParent
    IfNoParent })
      where
        -- NOTE: Not all TyCons have `tyConTyVars` field. Forcing this when `tycon`
        -- is one of these TyCons (FunTyCon, PrimTyCon, PromotedDataCon) will cause
        -- an error.
        (TidyEnv
    tc_env1, [TyConBinder]
    tc_binders) = TidyEnv -> [TyConBinder] -> (TidyEnv, [TyConBinder])
    tidyTyConBinders TidyEnv
    env (TyCon -> [TyConBinder]
    tyConBinders TyCon
    tycon)
        tc_tyvars :: [TyCoVar]
    tc_tyvars      = [TyConBinder] -> [TyCoVar]
    forall tv argf. [VarBndr tv argf] -> [tv]
    binderVars [TyConBinder]
    tc_binders
        if_binders :: [IfaceTyConBinder]
    if_binders     = [TyConBinder] -> [IfaceTyConBinder]
    forall vis. [VarBndr TyCoVar vis] -> [VarBndr IfaceBndr vis]
    toIfaceForAllBndrs [TyConBinder]
    tc_binders
                         -- No tidying of the binders; they are already tidy
        if_res_kind :: IfaceType
    if_res_kind    = TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    tc_env1 (TyCon -> Type
    tyConResKind TyCon
    tycon)
        if_syn_type :: Type -> IfaceType
    if_syn_type Type
    ty = TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    tc_env1 Type
    ty
        if_res_var :: Maybe IfLclName
    if_res_var     = Name -> IfLclName
    forall a. NamedThing a => a -> IfLclName
    getOccFS (Name -> IfLclName) -> Maybe Name -> Maybe IfLclName
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` TyCon -> Maybe Name
    tyConFamilyResVar_maybe TyCon
    tycon

        parent :: IfaceTyConParent
    parent = case TyCon -> Maybe (TyCon, [Type], CoAxiom Unbranched)
    tyConFamInstSig_maybe TyCon
    tycon of
                   Just (TyCon
    tc, [Type]
    ty, CoAxiom Unbranched
    ax) -> Name -> IfaceTyCon -> IfaceAppArgs -> IfaceTyConParent
    IfDataInstance (CoAxiom Unbranched -> Name
    forall (br :: BranchFlag). CoAxiom br -> Name
    coAxiomName CoAxiom Unbranched
    ax)
                                                       (TyCon -> IfaceTyCon
    toIfaceTyCon TyCon
    tc)
                                                       (TidyEnv -> TyCon -> [Type] -> IfaceAppArgs
    tidyToIfaceTcArgs TidyEnv
    tc_env1 TyCon
    tc [Type]
    ty)
                   Maybe (TyCon, [Type], CoAxiom Unbranched)
    Nothing           -> IfaceTyConParent
    IfNoParent

        to_if_fam_flav :: FamTyConFlav -> IfaceFamTyConFlav
    to_if_fam_flav FamTyConFlav
    OpenSynFamilyTyCon             = IfaceFamTyConFlav
    IfaceOpenSynFamilyTyCon
        to_if_fam_flav FamTyConFlav
    AbstractClosedSynFamilyTyCon   = IfaceFamTyConFlav
    IfaceAbstractClosedSynFamilyTyCon
        to_if_fam_flav (DataFamilyTyCon {})           = IfaceFamTyConFlav
    IfaceDataFamilyTyCon
        to_if_fam_flav (BuiltInSynFamTyCon {})        = IfaceFamTyConFlav
    IfaceBuiltInSynFamTyCon
        to_if_fam_flav (ClosedSynFamilyTyCon Maybe (CoAxiom Branched)
    Nothing) = Maybe (Name, [IfaceAxBranch]) -> IfaceFamTyConFlav
    IfaceClosedSynFamilyTyCon Maybe (Name, [IfaceAxBranch])
    forall a. Maybe a
    Nothing
        to_if_fam_flav (ClosedSynFamilyTyCon (Just CoAxiom Branched
    ax))
          = Maybe (Name, [IfaceAxBranch]) -> IfaceFamTyConFlav
    IfaceClosedSynFamilyTyCon ((Name, [IfaceAxBranch]) -> Maybe (Name, [IfaceAxBranch])
    forall a. a -> Maybe a
    Just (Name
    axn, [IfaceAxBranch]
    ibr))
          where defs :: [CoAxBranch]
    defs = Branches Branched -> [CoAxBranch]
    forall (br :: BranchFlag). Branches br -> [CoAxBranch]
    fromBranches (Branches Branched -> [CoAxBranch])
    -> Branches Branched -> [CoAxBranch]
    forall a b. (a -> b) -> a -> b
    $ CoAxiom Branched -> Branches Branched
    forall (br :: BranchFlag). CoAxiom br -> Branches br
    coAxiomBranches CoAxiom Branched
    ax
                lhss :: [[Type]]
    lhss = (CoAxBranch -> [Type]) -> [CoAxBranch] -> [[Type]]
    forall a b. (a -> b) -> [a] -> [b]
    map CoAxBranch -> [Type]
    coAxBranchLHS [CoAxBranch]
    defs
                ibr :: [IfaceAxBranch]
    ibr  = (CoAxBranch -> IfaceAxBranch) -> [CoAxBranch] -> [IfaceAxBranch]
    forall a b. (a -> b) -> [a] -> [b]
    map (TyCon -> [[Type]] -> CoAxBranch -> IfaceAxBranch
    coAxBranchToIfaceBranch TyCon
    tycon [[Type]]
    lhss) [CoAxBranch]
    defs
                axn :: Name
    axn  = CoAxiom Branched -> Name
    forall (br :: BranchFlag). CoAxiom br -> Name
    coAxiomName CoAxiom Branched
    ax

        ifaceConDecls :: AlgTyConRhs -> IfaceConDecls
    ifaceConDecls (NewTyCon { data_con :: AlgTyConRhs -> DataCon
    data_con = DataCon
    con })    = IfaceConDecl -> IfaceConDecls
    IfNewTyCon  (DataCon -> IfaceConDecl
    ifaceConDecl DataCon
    con)
        ifaceConDecls (DataTyCon { data_cons :: AlgTyConRhs -> [DataCon]
    data_cons = [DataCon]
    cons, is_type_data :: AlgTyConRhs -> Bool
    is_type_data = Bool
    type_data })
          = Bool -> [IfaceConDecl] -> IfaceConDecls
    IfDataTyCon Bool
    type_data ((DataCon -> IfaceConDecl) -> [DataCon] -> [IfaceConDecl]
    forall a b. (a -> b) -> [a] -> [b]
    map DataCon -> IfaceConDecl
    ifaceConDecl [DataCon]
    cons)
        ifaceConDecls (TupleTyCon { data_con :: AlgTyConRhs -> DataCon
    data_con = DataCon
    con })  = Bool -> [IfaceConDecl] -> IfaceConDecls
    IfDataTyCon Bool
    False [DataCon -> IfaceConDecl
    ifaceConDecl DataCon
    con]
        ifaceConDecls (SumTyCon { data_cons :: AlgTyConRhs -> [DataCon]
    data_cons = [DataCon]
    cons })  = Bool -> [IfaceConDecl] -> IfaceConDecls
    IfDataTyCon Bool
    False ((DataCon -> IfaceConDecl) -> [DataCon] -> [IfaceConDecl]
    forall a b. (a -> b) -> [a] -> [b]
    map DataCon -> IfaceConDecl
    ifaceConDecl [DataCon]
    cons)
        ifaceConDecls AlgTyConRhs
    AbstractTyCon                    = IfaceConDecls
    IfAbstractTyCon
            -- The AbstractTyCon case happens when a TyCon has been trimmed
            -- during tidying.
            -- Furthermore, tyThingToIfaceDecl is also used in GHC.Tc.Module
            -- for GHCi, when browsing a module, in which case the
            -- AbstractTyCon and TupleTyCon cases are perfectly sensible.
            -- (Tuple declarations are not serialised into interface files.)

        ifaceConDecl :: DataCon -> IfaceConDecl
    ifaceConDecl DataCon
    data_con
            = IfCon   { ifConName :: Name
    ifConName    = DataCon -> Name
    dataConName DataCon
    data_con,
                        ifConInfix :: Bool
    ifConInfix   = DataCon -> Bool
    dataConIsInfix DataCon
    data_con,
                        ifConWrapper :: Bool
    ifConWrapper = Maybe TyCoVar -> Bool
    forall a. Maybe a -> Bool
    isJust (DataCon -> Maybe TyCoVar
    dataConWrapId_maybe DataCon
    data_con),
                        ifConExTCvs :: [IfaceBndr]
    ifConExTCvs  = (TyCoVar -> IfaceBndr) -> [TyCoVar] -> [IfaceBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map TyCoVar -> IfaceBndr
    toIfaceBndr [TyCoVar]
    ex_tvs',
                        ifConUserTvBinders :: [IfaceForAllSpecBndr]
    ifConUserTvBinders = [VarBndr TyCoVar Specificity] -> [IfaceForAllSpecBndr]
    forall vis. [VarBndr TyCoVar vis] -> [VarBndr IfaceBndr vis]
    toIfaceForAllBndrs [VarBndr TyCoVar Specificity]
    user_bndrs',
                        ifConEqSpec :: [IfaceTvBndr]
    ifConEqSpec  = (EqSpec -> IfaceTvBndr) -> [EqSpec] -> [IfaceTvBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map ((TyCoVar, Type) -> IfaceTvBndr
    to_eq_spec ((TyCoVar, Type) -> IfaceTvBndr)
    -> (EqSpec -> (TyCoVar, Type)) -> EqSpec -> IfaceTvBndr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . EqSpec -> (TyCoVar, Type)
    eqSpecPair) [EqSpec]
    eq_spec,
                        ifConCtxt :: IfaceContext
    ifConCtxt    = TidyEnv -> [Type] -> IfaceContext
    tidyToIfaceContext TidyEnv
    con_env2 [Type]
    theta,
                        ifConArgTys :: [(IfaceType, IfaceType)]
    ifConArgTys  =
                          (Scaled Type -> (IfaceType, IfaceType))
    -> [Scaled Type] -> [(IfaceType, IfaceType)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\(Scaled Type
    w Type
    t) -> (TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    con_env2 Type
    w
                                              , (TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    con_env2 Type
    t))) [Scaled Type]
    arg_tys,
                        ifConFields :: [FieldLabel]
    ifConFields  = DataCon -> [FieldLabel]
    dataConFieldLabels DataCon
    data_con,
                        ifConStricts :: [IfaceBang]
    ifConStricts = (HsImplBang -> IfaceBang) -> [HsImplBang] -> [IfaceBang]
    forall a b. (a -> b) -> [a] -> [b]
    map (TidyEnv -> HsImplBang -> IfaceBang
    toIfaceBang TidyEnv
    con_env2)
                                           (DataCon -> [HsImplBang]
    dataConImplBangs DataCon
    data_con),
                        ifConSrcStricts :: [IfaceSrcBang]
    ifConSrcStricts = (HsSrcBang -> IfaceSrcBang) -> [HsSrcBang] -> [IfaceSrcBang]
    forall a b. (a -> b) -> [a] -> [b]
    map HsSrcBang -> IfaceSrcBang
    toIfaceSrcBang
                                              (DataCon -> [HsSrcBang]
    dataConSrcBangs DataCon
    data_con)}
            where
              ([TyCoVar]
    univ_tvs, [TyCoVar]
    ex_tvs, [EqSpec]
    eq_spec, [Type]
    theta, [Scaled Type]
    arg_tys, Type
    _)
                = DataCon
    -> ([TyCoVar], [TyCoVar], [EqSpec], [Type], [Scaled Type], Type)
    dataConFullSig DataCon
    data_con
              user_bndrs :: [VarBndr TyCoVar Specificity]
    user_bndrs = DataCon -> [VarBndr TyCoVar Specificity]
    dataConUserTyVarBinders DataCon
    data_con

              -- Tidy the univ_tvs of the data constructor to be identical
              -- to the tyConTyVars of the type constructor.  This means
              -- (a) we don't need to redundantly put them into the interface file
              -- (b) when pretty-printing an Iface data declaration in H98-style syntax,
              --     we know that the type variables will line up
              -- The latter (b) is important because we pretty-print type constructors
              -- by converting to Iface syntax and pretty-printing that
              con_env1 :: TidyEnv
    con_env1 = (TidyEnv -> TidyOccEnv
    forall a b. (a, b) -> a
    fst TidyEnv
    tc_env1, [(TyCoVar, TyCoVar)] -> VarEnv TyCoVar
    forall a. [(TyCoVar, a)] -> VarEnv a
    mkVarEnv (String -> [TyCoVar] -> [TyCoVar] -> [(TyCoVar, TyCoVar)]
    forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
    zipEqual String
    "ifaceConDecl" [TyCoVar]
    univ_tvs [TyCoVar]
    tc_tyvars))
                         -- A bit grimy, perhaps, but it's simple!

              (TidyEnv
    con_env2, [TyCoVar]
    ex_tvs') = TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
    tidyVarBndrs TidyEnv
    con_env1 [TyCoVar]
    ex_tvs
              user_bndrs' :: [VarBndr TyCoVar Specificity]
    user_bndrs' = (VarBndr TyCoVar Specificity -> VarBndr TyCoVar Specificity)
    -> [VarBndr TyCoVar Specificity] -> [VarBndr TyCoVar Specificity]
    forall a b. (a -> b) -> [a] -> [b]
    map (TidyEnv
    -> VarBndr TyCoVar Specificity -> VarBndr TyCoVar Specificity
    tidyUserForAllTyBinder TidyEnv
    con_env2) [VarBndr TyCoVar Specificity]
    user_bndrs
              to_eq_spec :: (TyCoVar, Type) -> IfaceTvBndr
    to_eq_spec (TyCoVar
    tv,Type
    ty) = (TidyEnv -> TyCoVar -> IfLclName
    tidyTyVar TidyEnv
    con_env2 TyCoVar
    tv, TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    con_env2 Type
    ty)

              -- By this point, we have tidied every universal and existential
              -- tyvar. Because of the dcUserForAllTyBinders invariant
              -- (see Note [DataCon user type variable binders]), *every*
              -- user-written tyvar must be contained in the substitution that
              -- tidying produced. Therefore, tidying the user-written tyvars is a
              -- simple matter of looking up each variable in the substitution,
              -- which tidyTyCoVarOcc accomplishes.
              tidyUserForAllTyBinder :: TidyEnv -> InvisTVBinder -> InvisTVBinder
              tidyUserForAllTyBinder :: TidyEnv
    -> VarBndr TyCoVar Specificity -> VarBndr TyCoVar Specificity
    tidyUserForAllTyBinder TidyEnv
    env (Bndr TyCoVar
    tv Specificity
    vis) =
                TyCoVar -> Specificity -> VarBndr TyCoVar Specificity
    forall var argf. var -> argf -> VarBndr var argf
    Bndr (TidyEnv -> TyCoVar -> TyCoVar
    tidyTyCoVarOcc TidyEnv
    env TyCoVar
    tv) Specificity
    vis

    classToIfaceDecl :: TidyEnv -> Class -> (TidyEnv, IfaceDecl)
    classToIfaceDecl :: TidyEnv -> Class -> (TidyEnv, IfaceDecl)
    classToIfaceDecl TidyEnv
    env Class
    clas
      = ( TidyEnv
    env1
        , IfaceClass { ifName :: Name
    ifName   = TyCon -> Name
    forall a. NamedThing a => a -> Name
    getName TyCon
    tycon,
                       ifRoles :: [Role]
    ifRoles  = TyCon -> [Role]
    tyConRoles (Class -> TyCon
    classTyCon Class
    clas),
                       ifBinders :: [IfaceTyConBinder]
    ifBinders = [TyConBinder] -> [IfaceTyConBinder]
    forall vis. [VarBndr TyCoVar vis] -> [VarBndr IfaceBndr vis]
    toIfaceForAllBndrs [TyConBinder]
    tc_binders,
                       ifBody :: IfaceClassBody
    ifBody   = IfaceClassBody
    body,
                       ifFDs :: [FunDep IfLclName]
    ifFDs    = (([TyCoVar], [TyCoVar]) -> FunDep IfLclName)
    -> [([TyCoVar], [TyCoVar])] -> [FunDep IfLclName]
    forall a b. (a -> b) -> [a] -> [b]
    map ([TyCoVar], [TyCoVar]) -> FunDep IfLclName
    toIfaceFD [([TyCoVar], [TyCoVar])]
    clas_fds })
      where
        ([TyCoVar]
    _, [([TyCoVar], [TyCoVar])]
    clas_fds, [Type]
    sc_theta, [TyCoVar]
    _, [ClassATItem]
    clas_ats, [ClassOpItem]
    op_stuff)
          = Class
    -> ([TyCoVar], [([TyCoVar], [TyCoVar])], [Type], [TyCoVar],
        [ClassATItem], [ClassOpItem])
    classExtraBigSig Class
    clas
        tycon :: TyCon
    tycon = Class -> TyCon
    classTyCon Class
    clas

        body :: IfaceClassBody
    body | TyCon -> Bool
    isAbstractTyCon TyCon
    tycon = IfaceClassBody
    IfAbstractClass
             | Bool
    otherwise
             = IfConcreteClass {
                    ifClassCtxt :: IfaceContext
    ifClassCtxt   = TidyEnv -> [Type] -> IfaceContext
    tidyToIfaceContext TidyEnv
    env1 [Type]
    sc_theta,
                    ifATs :: [IfaceAT]
    ifATs    = (ClassATItem -> IfaceAT) -> [ClassATItem] -> [IfaceAT]
    forall a b. (a -> b) -> [a] -> [b]
    map ClassATItem -> IfaceAT
    toIfaceAT [ClassATItem]
    clas_ats,
                    ifSigs :: [IfaceClassOp]
    ifSigs   = (ClassOpItem -> IfaceClassOp) -> [ClassOpItem] -> [IfaceClassOp]
    forall a b. (a -> b) -> [a] -> [b]
    map ClassOpItem -> IfaceClassOp
    toIfaceClassOp [ClassOpItem]
    op_stuff,
                    ifMinDef :: IfaceBooleanFormula
    ifMinDef = BooleanFormula IfLclName -> IfaceBooleanFormula
    toIfaceBooleanFormula (BooleanFormula IfLclName -> IfaceBooleanFormula)
    -> BooleanFormula IfLclName -> IfaceBooleanFormula
    forall a b. (a -> b) -> a -> b
    $ (Name -> IfLclName)
    -> BooleanFormula Name -> BooleanFormula IfLclName
    forall a b. (a -> b) -> BooleanFormula a -> BooleanFormula b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> IfLclName
    forall a. NamedThing a => a -> IfLclName
    getOccFS (Class -> BooleanFormula Name
    classMinimalDef Class
    clas)
                }

        (TidyEnv
    env1, [TyConBinder]
    tc_binders) = TidyEnv -> [TyConBinder] -> (TidyEnv, [TyConBinder])
    tidyTyConBinders TidyEnv
    env (TyCon -> [TyConBinder]
    tyConBinders TyCon
    tycon)

        toIfaceAT :: ClassATItem -> IfaceAT
        toIfaceAT :: ClassATItem -> IfaceAT
    toIfaceAT (ATI TyCon
    tc Maybe (Type, TyFamEqnValidityInfo)
    def)
          = IfaceDecl -> Maybe IfaceType -> IfaceAT
    IfaceAT IfaceDecl
    if_decl (((Type, TyFamEqnValidityInfo) -> IfaceType)
    -> Maybe (Type, TyFamEqnValidityInfo) -> Maybe IfaceType
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    env2 (Type -> IfaceType)
    -> ((Type, TyFamEqnValidityInfo) -> Type)
    -> (Type, TyFamEqnValidityInfo)
    -> IfaceType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Type, TyFamEqnValidityInfo) -> Type
    forall a b. (a, b) -> a
    fst) Maybe (Type, TyFamEqnValidityInfo)
    def)
          where
            (TidyEnv
    env2, IfaceDecl
    if_decl) = TidyEnv -> TyCon -> (TidyEnv, IfaceDecl)
    tyConToIfaceDecl TidyEnv
    env1 TyCon
    tc

        toIfaceClassOp :: ClassOpItem -> IfaceClassOp
    toIfaceClassOp (TyCoVar
    sel_id, Maybe (Name, DefMethSpec Type)
    def_meth)
            = Bool -> IfaceClassOp -> IfaceClassOp
    forall a. HasCallStack => Bool -> a -> a
    assert ([TyCoVar]
    sel_tyvars [TyCoVar] -> [TyCoVar] -> Bool
    forall a. Eq a => a -> a -> Bool
    == [TyConBinder] -> [TyCoVar]
    forall tv argf. [VarBndr tv argf] -> [tv]
    binderVars [TyConBinder]
    tc_binders) (IfaceClassOp -> IfaceClassOp) -> IfaceClassOp -> IfaceClassOp
    forall a b. (a -> b) -> a -> b
    $
              Name -> IfaceType -> Maybe (DefMethSpec IfaceType) -> IfaceClassOp
    IfaceClassOp (TyCoVar -> Name
    forall a. NamedThing a => a -> Name
    getName TyCoVar
    sel_id)
                           (TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    env1 Type
    op_ty)
                           (((Name, DefMethSpec Type) -> DefMethSpec IfaceType)
    -> Maybe (Name, DefMethSpec Type) -> Maybe (DefMethSpec IfaceType)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (Name, DefMethSpec Type) -> DefMethSpec IfaceType
    toDmSpec Maybe (Name, DefMethSpec Type)
    def_meth)
            where
                    -- Be careful when splitting the type, because of things
                    -- like         class Foo a where
                    --                op :: (?x :: String) => a -> a
                    -- and          class Baz a where
                    --                op :: (Ord a) => a -> a
              ([TyCoVar]
    sel_tyvars, Type
    rho_ty) = Type -> ([TyCoVar], Type)
    splitForAllTyCoVars (TyCoVar -> Type
    idType TyCoVar
    sel_id)
              op_ty :: Type
    op_ty                = HasDebugCallStack => Type -> Type
    Type -> Type
    funResultTy Type
    rho_ty

        toDmSpec :: (Name, DefMethSpec Type) -> DefMethSpec IfaceType
        toDmSpec :: (Name, DefMethSpec Type) -> DefMethSpec IfaceType
    toDmSpec (Name
    _, DefMethSpec Type
    VanillaDM)       = DefMethSpec IfaceType
    forall ty. DefMethSpec ty
    VanillaDM
        toDmSpec (Name
    _, GenericDM Type
    dm_ty) = IfaceType -> DefMethSpec IfaceType
    forall ty. ty -> DefMethSpec ty
    GenericDM (TidyEnv -> Type -> IfaceType
    tidyToIfaceType TidyEnv
    env1 Type
    dm_ty)

        toIfaceFD :: ([TyCoVar], [TyCoVar]) -> FunDep IfLclName
    toIfaceFD ([TyCoVar]
    tvs1, [TyCoVar]
    tvs2) = ((TyCoVar -> IfLclName) -> [TyCoVar] -> [IfLclName]
    forall a b. (a -> b) -> [a] -> [b]
    map (TidyEnv -> TyCoVar -> IfLclName
    tidyTyVar TidyEnv
    env1) [TyCoVar]
    tvs1
                                 ,(TyCoVar -> IfLclName) -> [TyCoVar] -> [IfLclName]
    forall a b. (a -> b) -> [a] -> [b]
    map (TidyEnv -> TyCoVar -> IfLclName
    tidyTyVar TidyEnv
    env1) [TyCoVar]
    tvs2)

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

    tidyTyConBinder :: TidyEnv -> TyConBinder -> (TidyEnv, TyConBinder)
    -- If the type variable "binder" is in scope, don't re-bind it
    -- In a class decl, for example, the ATD binders mention
    -- (amd must mention) the class tyvars
    tidyTyConBinder :: TidyEnv -> TyConBinder -> (TidyEnv, TyConBinder)
    tidyTyConBinder env :: TidyEnv
    env@(TidyOccEnv
    _, VarEnv TyCoVar
    subst) tvb :: TyConBinder
    tvb@(Bndr TyCoVar
    tv TyConBndrVis
    vis)
     = case VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
    forall a. VarEnv a -> TyCoVar -> Maybe a
    lookupVarEnv VarEnv TyCoVar
    subst TyCoVar
    tv of
         Just TyCoVar
    tv' -> (TidyEnv
    env,  TyCoVar -> TyConBndrVis -> TyConBinder
    forall var argf. var -> argf -> VarBndr var argf
    Bndr TyCoVar
    tv' TyConBndrVis
    vis)
         Maybe TyCoVar
    Nothing  -> TidyEnv -> TyConBinder -> (TidyEnv, TyConBinder)
    forall vis.
    TidyEnv -> VarBndr TyCoVar vis -> (TidyEnv, VarBndr TyCoVar vis)
    tidyForAllTyBinder TidyEnv
    env TyConBinder
    tvb

    tidyTyConBinders :: TidyEnv -> [TyConBinder] -> (TidyEnv, [TyConBinder])
    tidyTyConBinders :: TidyEnv -> [TyConBinder] -> (TidyEnv, [TyConBinder])
    tidyTyConBinders = (TidyEnv -> TyConBinder -> (TidyEnv, TyConBinder))
    -> TidyEnv -> [TyConBinder] -> (TidyEnv, [TyConBinder])
    forall (t :: * -> *) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    mapAccumL TidyEnv -> TyConBinder -> (TidyEnv, TyConBinder)
    tidyTyConBinder

    tidyTyVar :: TidyEnv -> TyVar -> FastString
    tidyTyVar :: TidyEnv -> TyCoVar -> IfLclName
    tidyTyVar (TidyOccEnv
    _, VarEnv TyCoVar
    subst) TyCoVar
    tv = TyCoVar -> IfLclName
    toIfaceTyVar (VarEnv TyCoVar -> TyCoVar -> Maybe TyCoVar
    forall a. VarEnv a -> TyCoVar -> Maybe a
    lookupVarEnv VarEnv TyCoVar
    subst TyCoVar
    tv Maybe TyCoVar -> TyCoVar -> TyCoVar
    forall a. Maybe a -> a -> a
    `orElse` TyCoVar
    tv)

    toIfaceBooleanFormula :: BooleanFormula IfLclName -> IfaceBooleanFormula
    toIfaceBooleanFormula :: BooleanFormula IfLclName -> IfaceBooleanFormula
    toIfaceBooleanFormula = \case
        Var IfLclName
    nm    -> IfLclName -> IfaceBooleanFormula
    IfVar    IfLclName
    nm
        And [LBooleanFormula IfLclName]
    bfs   -> [IfaceBooleanFormula] -> IfaceBooleanFormula
    IfAnd    ((LBooleanFormula IfLclName -> IfaceBooleanFormula)
    -> [LBooleanFormula IfLclName] -> [IfaceBooleanFormula]
    forall a b. (a -> b) -> [a] -> [b]
    map (BooleanFormula IfLclName -> IfaceBooleanFormula
    toIfaceBooleanFormula (BooleanFormula IfLclName -> IfaceBooleanFormula)
    -> (LBooleanFormula IfLclName -> BooleanFormula IfLclName)
    -> LBooleanFormula IfLclName
    -> IfaceBooleanFormula
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LBooleanFormula IfLclName -> BooleanFormula IfLclName
    forall l e. GenLocated l e -> e
    unLoc) [LBooleanFormula IfLclName]
    bfs)
        Or [LBooleanFormula IfLclName]
    bfs    -> [IfaceBooleanFormula] -> IfaceBooleanFormula
    IfOr     ((LBooleanFormula IfLclName -> IfaceBooleanFormula)
    -> [LBooleanFormula IfLclName] -> [IfaceBooleanFormula]
    forall a b. (a -> b) -> [a] -> [b]
    map (BooleanFormula IfLclName -> IfaceBooleanFormula
    toIfaceBooleanFormula (BooleanFormula IfLclName -> IfaceBooleanFormula)
    -> (LBooleanFormula IfLclName -> BooleanFormula IfLclName)
    -> LBooleanFormula IfLclName
    -> IfaceBooleanFormula
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LBooleanFormula IfLclName -> BooleanFormula IfLclName
    forall l e. GenLocated l e -> e
    unLoc) [LBooleanFormula IfLclName]
    bfs)
        Parens LBooleanFormula IfLclName
    bf -> IfaceBooleanFormula -> IfaceBooleanFormula
    IfParens (BooleanFormula IfLclName -> IfaceBooleanFormula
    toIfaceBooleanFormula (BooleanFormula IfLclName -> IfaceBooleanFormula)
    -> (LBooleanFormula IfLclName -> BooleanFormula IfLclName)
    -> LBooleanFormula IfLclName
    -> IfaceBooleanFormula
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LBooleanFormula IfLclName -> BooleanFormula IfLclName
    forall l e. GenLocated l e -> e
    unLoc (LBooleanFormula IfLclName -> IfaceBooleanFormula)
    -> LBooleanFormula IfLclName -> IfaceBooleanFormula
    forall a b. (a -> b) -> a -> b
    $ LBooleanFormula IfLclName
    bf)