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

    {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

    module GHC.Tc.TyCl.Build (
            buildDataCon,
            buildPatSyn,
            TcMethInfo, MethInfo, buildClass,
            mkNewTyConRhs,
            newImplicitBinder, newTyConRepName
        ) where

    import GHC.Prelude

    import GHC.Iface.Env
    import GHC.Builtin.Types

    import GHC.Tc.Utils.TcType
    import GHC.Tc.Utils.Monad

    import GHC.Core.DataCon
    import GHC.Core.PatSyn
    import GHC.Core.Class
    import GHC.Core.TyCon
    import GHC.Core.Type
    import GHC.Core.Multiplicity
    import GHC.Core.FamInstEnv( FamInstEnvs, mkNewTypeCoAxiom )

    import GHC.Types.SrcLoc( SrcSpan, noSrcSpan )
    import GHC.Types.Var
    import GHC.Types.Var.Set
    import GHC.Types.Basic
    import GHC.Types.Name
    import GHC.Types.Name.Env
    import GHC.Types.Id.Make
    import GHC.Types.SourceText
    import GHC.Types.Unique.Supply

    import GHC.Utils.Misc
    import GHC.Utils.Outputable
    import GHC.Utils.Panic

    mkNewTyConRhs :: Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
    -- ^ Monadic because it makes a Name for the coercion TyCon
    --   We pass the Name of the parent TyCon, as well as the TyCon itself,
    --   because the latter is part of a knot, whereas the former is not.
    mkNewTyConRhs :: forall m n. Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
    mkNewTyConRhs Name
    tycon_name TyCon
    tycon DataCon
    con
      = do  { co_tycon_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
    forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
    newImplicitBinder Name
    tycon_name OccName -> OccName
    mkNewTyCoOcc
            ; let nt_ax = Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
    mkNewTypeCoAxiom Name
    co_tycon_name TyCon
    tycon [TyVar]
    etad_tvs [Role]
    etad_roles Type
    etad_rhs
            ; traceIf (text "mkNewTyConRhs" <+> ppr nt_ax)
            ; return (NewTyCon { data_con     = con,
                                 nt_rhs       = rhs_ty,
                                 nt_etad_rhs  = (etad_tvs, etad_rhs),
                                 nt_co        = nt_ax,
                                 nt_fixed_rep = isFixedRuntimeRepKind res_kind } ) }
                                 -- Coreview looks through newtypes with a Nothing
                                 -- for nt_co, or uses explicit coercions otherwise
      where
        tvs :: [TyVar]
    tvs      = TyCon -> [TyVar]
    tyConTyVars TyCon
    tycon
        roles :: [Role]
    roles    = TyCon -> [Role]
    tyConRoles TyCon
    tycon
        res_kind :: Type
    res_kind = TyCon -> Type
    tyConResKind TyCon
    tycon
        rhs_ty :: Type
    rhs_ty
          -- Only try if the newtype is actually valid (see "otherwise" below).
          | [Scaled Type
    _ Type
    arg_ty] <- DataCon -> [Scaled Type]
    dataConRepArgTys DataCon
    con
          , [TyVar] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([TyVar] -> Bool) -> [TyVar] -> Bool
    forall a b. (a -> b) -> a -> b
    $ DataCon -> [TyVar]
    dataConExTyCoVars DataCon
    con
          = [TyVar] -> ThetaType -> Type -> Type
    HasDebugCallStack => [TyVar] -> ThetaType -> Type -> Type
    substTyWith (DataCon -> [TyVar]
    dataConUnivTyVars DataCon
    con)
                             ([TyVar] -> ThetaType
    mkTyVarTys [TyVar]
    tvs) Type
    arg_ty
            -- Instantiate the newtype's RHS with the
            -- type variables from the tycon
            -- NB: a newtype DataCon has a type that must look like
            --        forall tvs.  <arg-ty> -> T tvs
            -- Note that we *can't* use dataConInstOrigArgTys here because
            -- the newtype arising from   class Foo a => Bar a where {}
            -- has a single argument (Foo a) that is a *type class*, so
            -- dataConInstOrigArgTys returns [].
          | Bool
    otherwise
          -- If the newtype is invalid (e.g. doesn't have a single argument),
          -- we fake up a type here. The newtype will get rejected once we're
          -- outside the knot-tied loop, in GHC.Tc.TyCl.checkNewDataCon.
          -- See the various test cases in T23308.
          = Type
    unitTy -- Might be ill-kinded, but checkNewDataCon should reject this
                   -- whole declaration soon enough, before that causes any problems.

        -- Eta-reduce the newtype
        -- See Note [Newtype eta] in GHC.Core.TyCon
        etad_tvs   :: [TyVar]  -- Matched lazily, so that mkNewTypeCo can
        etad_roles :: [Role]   -- return a TyCon without pulling on rhs_ty
        etad_rhs   :: Type     -- See Note [Tricky iface loop] in GHC.Iface.Load
        ([TyVar]
    etad_tvs, [Role]
    etad_roles, Type
    etad_rhs) = [TyVar] -> [Role] -> Type -> ([TyVar], [Role], Type)
    eta_reduce ([TyVar] -> [TyVar]
    forall a. [a] -> [a]
    reverse [TyVar]
    tvs) ([Role] -> [Role]
    forall a. [a] -> [a]
    reverse [Role]
    roles) Type
    rhs_ty

        eta_reduce :: [TyVar]       -- Reversed
                   -> [Role]        -- also reversed
                   -> Type          -- Rhs type
                   -> ([TyVar], [Role], Type)  -- Eta-reduced version
                                               -- (tyvars in normal order)
        eta_reduce :: [TyVar] -> [Role] -> Type -> ([TyVar], [Role], Type)
    eta_reduce (TyVar
    a:[TyVar]
    as) (Role
    _:[Role]
    rs) Type
    ty
          | Just (Type
    fun, Type
    arg) <- Type -> Maybe (Type, Type)
    splitAppTy_maybe Type
    ty
          , Just TyVar
    tv <- Type -> Maybe TyVar
    getTyVar_maybe Type
    arg
          , TyVar
    tv TyVar -> TyVar -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyVar
    a
          , Bool -> Bool
    not (TyVar
    a TyVar -> VarSet -> Bool
    `elemVarSet` Type -> VarSet
    tyCoVarsOfType Type
    fun)
          , HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    fun Type -> Type -> Bool
    `eqType` HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind (TyCon -> ThetaType -> Type
    mkTyConApp TyCon
    tycon ([TyVar] -> ThetaType
    mkTyVarTys ([TyVar] -> ThetaType) -> [TyVar] -> ThetaType
    forall a b. (a -> b) -> a -> b
    $ [TyVar] -> [TyVar]
    forall a. [a] -> [a]
    reverse [TyVar]
    as))
            -- Why this kind-check?  See Note [Newtype eta and homogeneous axioms]
          = [TyVar] -> [Role] -> Type -> ([TyVar], [Role], Type)
    eta_reduce [TyVar]
    as [Role]
    rs Type
    fun
        eta_reduce [TyVar]
    as [Role]
    rs Type
    ty = ([TyVar] -> [TyVar]
    forall a. [a] -> [a]
    reverse [TyVar]
    as, [Role] -> [Role]
    forall a. [a] -> [a]
    reverse [Role]
    rs, Type
    ty)

    {- Note [Newtype eta and homogeneous axioms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    When eta-reducing a newtype, we must be careful to make sure the axiom
    is homogeneous.  (That is, the two types related by the axiom must
    have the same kind.)  All known proofs of type safety for Core rely on
    the homogeneity of axioms, so let's not monkey with that.

    It is easy to mistakenly make an inhomogeneous axiom (#19739):
      type T :: forall (a :: Type) -> Type
      newtype T a = MkT (Proxy a)

    Can we eta-reduce, thus?
      axT :: T ~ Proxy

    No!  Because
       T     :: forall a -> Type
       Proxy :: Type     -> Type

    This is inhomogeneous. Hence, we have an extra kind-check in eta_reduce,
    to make sure the reducts have the same kind. This is simple, although
    perhaps quadratic in complexity, if we eta-reduce many arguments (which
    seems vanishingly unlikely in practice).  But NB that the free-variable
    check, which immediately precedes the kind check, is also potentially
    quadratic.

    There are other ways we could do the check (discussion on #19739):

    * We could look at the sequence of binders on the newtype and on the
      head of the representation type, and make sure the visibilities on
      the binders match up. This is quite a bit more code, and the reasoning
      is subtler.

    * We could, say, do the kind-check at the end and then backtrack until the
      kinds match up. Hard to know whether that's more performant or not.
    -}

    ------------------------------------------------------
    buildDataCon :: FamInstEnvs
                -> DataConBangOpts
                -> Name
                -> Bool                     -- Declared infix
                -> TyConRepName
                -> [HsSrcBang]
               -> [FieldLabel]             -- Field labels
               -> [TyVar]                  -- Universals
               -> [TyCoVar]                -- Existentials
               -> [InvisTVBinder]          -- User-written 'TyVarBinder's
               -> [EqSpec]                 -- Equality spec
               -> KnotTied ThetaType       -- Does not include the "stupid theta"
                                           -- or the GADT equalities
               -> [KnotTied (Scaled Type)] -- Arguments
               -> KnotTied Type            -- Result types
               -> KnotTied TyCon           -- Rep tycon
               -> NameEnv ConTag           -- Maps the Name of each DataCon to its
                                           -- ConTag
               -> TcRnIf m n DataCon
    -- A wrapper for DataCon.mkDataCon that
    --   a) makes the worker Id
    --   b) makes the wrapper Id if necessary, including
    --      allocating its unique (hence monadic)
    buildDataCon :: forall m n.
    FamInstEnvs
    -> DataConBangOpts
    -> Name
    -> Bool
    -> Name
    -> [HsSrcBang]
    -> [FieldLabel]
    -> [TyVar]
    -> [TyVar]
    -> [InvisTVBinder]
    -> [EqSpec]
    -> ThetaType
    -> [Scaled Type]
    -> Type
    -> TyCon
    -> NameEnv ConTag
    -> TcRnIf m n DataCon
    buildDataCon FamInstEnvs
    fam_envs DataConBangOpts
    dc_bang_opts Name
    src_name Bool
    declared_infix Name
    prom_info [HsSrcBang]
    src_bangs
                 [FieldLabel]
    field_lbls [TyVar]
    univ_tvs [TyVar]
    ex_tvs [InvisTVBinder]
    user_tvbs [EqSpec]
    eq_spec ThetaType
    ctxt [Scaled Type]
    arg_tys Type
    res_ty
                 TyCon
    rep_tycon NameEnv ConTag
    tag_map
      = do  { wrap_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
    forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
    newImplicitBinder Name
    src_name OccName -> OccName
    mkDataConWrapperOcc
            ; work_name <- newImplicitBinder src_name mkDataConWorkerOcc
            -- This last one takes the name of the data constructor in the source
            -- code, which (for Haskell source anyway) will be in the DataName name
            -- space, and puts it into the VarName name space

            ; traceIf (text "buildDataCon 1" <+> ppr src_name)
            ; us <- newUniqueSupply
            ; let stupid_ctxt = TyCon -> ThetaType -> [TyVar] -> ThetaType
    mkDataConStupidTheta TyCon
    rep_tycon ((Scaled Type -> Type) -> [Scaled Type] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Scaled Type -> Type
    forall a. Scaled a -> a
    scaledThing [Scaled Type]
    arg_tys) [TyVar]
    univ_tvs
                  tag = NameEnv ConTag -> Name -> ConTag
    forall a. NameEnv a -> Name -> a
    lookupNameEnv_NF NameEnv ConTag
    tag_map Name
    src_name
                  -- See Note [Constructor tag allocation], fixes #14657
                  data_con = Name
    -> Bool
    -> Name
    -> [HsSrcBang]
    -> [FieldLabel]
    -> [TyVar]
    -> [TyVar]
    -> ConcreteTyVars
    -> [InvisTVBinder]
    -> [EqSpec]
    -> ThetaType
    -> [Scaled Type]
    -> Type
    -> PromDataConInfo
    -> TyCon
    -> ConTag
    -> ThetaType
    -> TyVar
    -> DataConRep
    -> DataCon
    mkDataCon Name
    src_name Bool
    declared_infix Name
    prom_info
                                       [HsSrcBang]
    src_bangs [FieldLabel]
    field_lbls
                                       [TyVar]
    univ_tvs [TyVar]
    ex_tvs
                                       ConcreteTyVars
    noConcreteTyVars
                                       [InvisTVBinder]
    user_tvbs [EqSpec]
    eq_spec ThetaType
    ctxt
                                       [Scaled Type]
    arg_tys Type
    res_ty PromDataConInfo
    NoPromInfo TyCon
    rep_tycon ConTag
    tag
                                       ThetaType
    stupid_ctxt TyVar
    dc_wrk DataConRep
    dc_rep
                  dc_wrk = Name -> DataCon -> TyVar
    mkDataConWorkId Name
    work_name DataCon
    data_con
                  dc_rep = UniqSupply -> UniqSM DataConRep -> DataConRep
    forall a. UniqSupply -> UniqSM a -> a
    initUs_ UniqSupply
    us (DataConBangOpts
    -> FamInstEnvs -> Name -> DataCon -> UniqSM DataConRep
    mkDataConRep DataConBangOpts
    dc_bang_opts FamInstEnvs
    fam_envs Name
    wrap_name DataCon
    data_con)

            ; traceIf (text "buildDataCon 2" <+> ppr src_name)
            ; return data_con }

    -- The stupid context for a data constructor should be limited to
    -- the type variables mentioned in the arg_tys
    -- ToDo: Or functionally dependent on?
    --       This whole stupid theta thing is, well, stupid.
    --
    -- See Note [The stupid context] in GHC.Core.DataCon.
    mkDataConStupidTheta :: TyCon -> [Type] -> [TyVar] -> [PredType]
    mkDataConStupidTheta :: TyCon -> ThetaType -> [TyVar] -> ThetaType
    mkDataConStupidTheta TyCon
    tycon ThetaType
    arg_tys [TyVar]
    univ_tvs
      | ThetaType -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ThetaType
    stupid_theta = []      -- The common case
      | Bool
    otherwise         = (Type -> Bool) -> ThetaType -> ThetaType
    forall a. (a -> Bool) -> [a] -> [a]
    filter Type -> Bool
    in_arg_tys ThetaType
    stupid_theta
      where
        tc_subst :: Subst
    tc_subst     = [TyVar] -> ThetaType -> Subst
    HasDebugCallStack => [TyVar] -> ThetaType -> Subst
    zipTvSubst (TyCon -> [TyVar]
    tyConTyVars TyCon
    tycon)
                                  ([TyVar] -> ThetaType
    mkTyVarTys [TyVar]
    univ_tvs)
        stupid_theta :: ThetaType
    stupid_theta = HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTheta Subst
    tc_subst (TyCon -> ThetaType
    tyConStupidTheta TyCon
    tycon)
            -- Start by instantiating the master copy of the
            -- stupid theta, taken from the TyCon

        arg_tyvars :: VarSet
    arg_tyvars      = ThetaType -> VarSet
    tyCoVarsOfTypes ThetaType
    arg_tys
        in_arg_tys :: Type -> Bool
    in_arg_tys Type
    pred = Type -> VarSet
    tyCoVarsOfType Type
    pred VarSet -> VarSet -> Bool
    `intersectsVarSet` VarSet
    arg_tyvars

    ------------------------------------------------------
    buildPatSyn :: Name -> Bool
                -> PatSynMatcher -> PatSynBuilder
                -> ([InvisTVBinder], ThetaType) -- ^ Univ and req
                -> ([InvisTVBinder], ThetaType) -- ^ Ex and prov
                -> [FRRType]                    -- ^ Argument types
                -> Type                         -- ^ Result type
                -> [FieldLabel]                 -- ^ Field labels for
                                                --   a record pattern synonym
                -> PatSyn
    buildPatSyn :: Name
    -> Bool
    -> PatSynMatcher
    -> PatSynBuilder
    -> ([InvisTVBinder], ThetaType)
    -> ([InvisTVBinder], ThetaType)
    -> ThetaType
    -> Type
    -> [FieldLabel]
    -> PatSyn
    buildPatSyn Name
    src_name Bool
    declared_infix matcher :: PatSynMatcher
    matcher@(Name
    _, Type
    matcher_ty,Bool
    _) PatSynBuilder
    builder
                ([InvisTVBinder]
    univ_tvs, ThetaType
    req_theta) ([InvisTVBinder]
    ex_tvs, ThetaType
    prov_theta) ThetaType
    arg_tys
                Type
    pat_ty [FieldLabel]
    field_labels
      = -- The assertion checks that the matcher is
        -- compatible with the pattern synonym
        Bool -> SDoc -> PatSyn -> PatSyn
    forall a. HasCallStack => Bool -> SDoc -> a -> a
    assertPpr ([Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [ [InvisTVBinder]
    univ_tvs [InvisTVBinder] -> [TyVar] -> Bool
    forall a b. [a] -> [b] -> Bool
    `equalLength` [TyVar]
    univ_tvs1
                       , [InvisTVBinder]
    ex_tvs [InvisTVBinder] -> [TyVar] -> Bool
    forall a b. [a] -> [b] -> Bool
    `equalLength` [TyVar]
    ex_tvs1
                       , Type
    pat_ty Type -> Type -> Bool
    `eqType` HasDebugCallStack => Subst -> Type -> Type
    Subst -> Type -> Type
    substTy Subst
    subst (Scaled Type -> Type
    forall a. Scaled a -> a
    scaledThing Scaled Type
    pat_ty1)
                       , ThetaType
    prov_theta ThetaType -> ThetaType -> Bool
    `eqTypes` HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTys Subst
    subst ThetaType
    prov_theta1
                       , ThetaType
    req_theta ThetaType -> ThetaType -> Bool
    `eqTypes` HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTys Subst
    subst ThetaType
    req_theta1
                       , ThetaType -> ThetaType -> Bool
    compareArgTys ThetaType
    arg_tys (HasDebugCallStack => Subst -> ThetaType -> ThetaType
    Subst -> ThetaType -> ThetaType
    substTys Subst
    subst ((Scaled Type -> Type) -> [Scaled Type] -> ThetaType
    forall a b. (a -> b) -> [a] -> [b]
    map Scaled Type -> Type
    forall a. Scaled a -> a
    scaledThing [Scaled Type]
    arg_tys1))
                       ])
                  ([SDoc] -> SDoc
    forall doc. IsDoc doc => [doc] -> doc
    vcat [ [InvisTVBinder] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [InvisTVBinder]
    univ_tvs SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    twiddle SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [TyVar] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [TyVar]
    univ_tvs1
                        , [InvisTVBinder] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [InvisTVBinder]
    ex_tvs SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    twiddle SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [TyVar] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [TyVar]
    ex_tvs1
                        , Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Type
    pat_ty SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    twiddle SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> Scaled Type -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr Scaled Type
    pat_ty1
                        , ThetaType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    prov_theta SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    twiddle SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ThetaType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    prov_theta1
                        , ThetaType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    req_theta SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    twiddle SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> ThetaType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    req_theta1
                        , ThetaType -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr ThetaType
    arg_tys SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> SDoc
    twiddle SDoc -> SDoc -> SDoc
    forall doc. IsLine doc => doc -> doc -> doc
    <+> [Scaled Type] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Scaled Type]
    arg_tys1]) (PatSyn -> PatSyn) -> PatSyn -> PatSyn
    forall a b. (a -> b) -> a -> b
    $
        Name
    -> Bool
    -> ([InvisTVBinder], ThetaType)
    -> ([InvisTVBinder], ThetaType)
    -> ThetaType
    -> Type
    -> PatSynMatcher
    -> PatSynBuilder
    -> [FieldLabel]
    -> PatSyn
    mkPatSyn Name
    src_name Bool
    declared_infix
                 ([InvisTVBinder]
    univ_tvs, ThetaType
    req_theta) ([InvisTVBinder]
    ex_tvs, ThetaType
    prov_theta)
                 ThetaType
    arg_tys Type
    pat_ty
                 PatSynMatcher
    matcher PatSynBuilder
    builder [FieldLabel]
    field_labels
      where
        ((TyVar
    _:TyVar
    _:[TyVar]
    univ_tvs1), ThetaType
    req_theta1, Type
    tau) = Type -> ([TyVar], ThetaType, Type)
    tcSplitSigmaTy (Type -> ([TyVar], ThetaType, Type))
    -> Type -> ([TyVar], ThetaType, Type)
    forall a b. (a -> b) -> a -> b
    $ Type
    matcher_ty
        ([Scaled Type
    pat_ty1, Scaled Type
    cont_sigma, Scaled Type
    _], Type
    _)      = Type -> ([Scaled Type], Type)
    tcSplitFunTys Type
    tau
        ([TyVar]
    ex_tvs1, ThetaType
    prov_theta1, Type
    cont_tau)   = Type -> ([TyVar], ThetaType, Type)
    tcSplitSigmaTy (Scaled Type -> Type
    forall a. Scaled a -> a
    scaledThing Scaled Type
    cont_sigma)
        ([Scaled Type]
    arg_tys1, Type
    _) = (Type -> ([Scaled Type], Type)
    tcSplitFunTys Type
    cont_tau)
        twiddle :: SDoc
    twiddle = Char -> SDoc
    forall doc. IsLine doc => Char -> doc
    char Char
    '~'
        subst :: Subst
    subst = [TyVar] -> ThetaType -> Subst
    HasDebugCallStack => [TyVar] -> ThetaType -> Subst
    zipTvSubst ([TyVar]
    univ_tvs1 [TyVar] -> [TyVar] -> [TyVar]
    forall a. [a] -> [a] -> [a]
    ++ [TyVar]
    ex_tvs1)
                           ([TyVar] -> ThetaType
    mkTyVarTys ([InvisTVBinder] -> [TyVar]
    forall tv argf. [VarBndr tv argf] -> [tv]
    binderVars ([InvisTVBinder]
    univ_tvs [InvisTVBinder] -> [InvisTVBinder] -> [InvisTVBinder]
    forall a. [a] -> [a] -> [a]
    ++ [InvisTVBinder]
    ex_tvs)))

        -- For a nullary pattern synonym we add a single (# #) argument to the
        -- matcher to preserve laziness in the case of unlifted types.
        -- See #12746
        compareArgTys :: [Type] -> [Type] -> Bool
        compareArgTys :: ThetaType -> ThetaType -> Bool
    compareArgTys [] [Type
    x] = Type
    x Type -> Type -> Bool
    `eqType` Type
    unboxedUnitTy
        compareArgTys ThetaType
    arg_tys ThetaType
    matcher_arg_tys = ThetaType
    arg_tys ThetaType -> ThetaType -> Bool
    `eqTypes` ThetaType
    matcher_arg_tys

    ------------------------------------------------------
    type TcMethInfo = MethInfo  -- this variant needs zonking
    type MethInfo       -- A temporary intermediate, to communicate
                        -- between tcClassSigs and buildClass.
      = ( Name   -- Name of the class op
        , Type   -- Type of the class op
        , Maybe (DefMethSpec (SrcSpan, Type)))
             -- Nothing                    => no default method
             --
             -- Just VanillaDM             => There is an ordinary
             --                               polymorphic default method
             --
             -- Just (GenericDM (loc, ty)) => There is a generic default metho
             --                               Here is its type, and the location
             --                               of the type signature
             --    We need that location /only/ to attach it to the
             --    generic default method's Name; and we need /that/
             --    only to give the right location of an ambiguity error
             --    for the generic default method, spat out by checkValidClass

    buildClass :: Name  -- Name of the class/tycon (they have the same Name)
               -> [TyConBinder]                -- Of the tycon
               -> [Role]
               -> [FunDep TyVar]               -- Functional dependencies
               -- Super classes, associated types, method info, minimal complete def.
               -- This is Nothing if the class is abstract.
               -> Maybe (KnotTied ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
               -> TcRnIf m n Class

    buildClass :: forall m n.
    Name
    -> [TyConBinder]
    -> [Role]
    -> [FunDep TyVar]
    -> Maybe
         (ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
    -> TcRnIf m n Class
    buildClass Name
    tycon_name [TyConBinder]
    binders [Role]
    roles [FunDep TyVar]
    fds Maybe
      (ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
    Nothing
      = (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
    forall a env. (a -> IOEnv env a) -> IOEnv env a
    fixM  ((Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class)
    -> (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
    forall a b. (a -> b) -> a -> b
    $ \ Class
    rec_clas ->       -- Only name generation inside loop
        do  { SDoc -> TcRnIf m n ()
    forall m n. SDoc -> TcRnIf m n ()
    traceIf (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "buildClass")

            ; tc_rep_name  <- Name -> TcRnIf m n Name
    forall gbl lcl. Name -> TcRnIf gbl lcl Name
    newTyConRepName Name
    tycon_name
            ; let univ_tvs = [TyConBinder] -> [TyVar]
    forall tv argf. [VarBndr tv argf] -> [tv]
    binderVars [TyConBinder]
    binders
                  tycon = Name
    -> [TyConBinder] -> [Role] -> AlgTyConRhs -> Class -> Name -> TyCon
    mkClassTyCon Name
    tycon_name [TyConBinder]
    binders [Role]
    roles
                                       AlgTyConRhs
    AbstractTyCon
                                       Class
    rec_clas Name
    tc_rep_name
                  result = Name -> [TyVar] -> [FunDep TyVar] -> TyCon -> Class
    mkAbstractClass Name
    tycon_name [TyVar]
    univ_tvs [FunDep TyVar]
    fds TyCon
    tycon
            ; traceIf (text "buildClass" <+> ppr tycon)
            ; return result }

    buildClass Name
    tycon_name [TyConBinder]
    binders [Role]
    roles [FunDep TyVar]
    fds
               (Just (ThetaType
    sc_theta, [ClassATItem]
    at_items, [KnotTied MethInfo]
    sig_stuff, ClassMinimalDef
    mindef))
      = (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
    forall a env. (a -> IOEnv env a) -> IOEnv env a
    fixM  ((Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class)
    -> (Class -> IOEnv (Env m n) Class) -> IOEnv (Env m n) Class
    forall a b. (a -> b) -> a -> b
    $ \ Class
    rec_clas ->       -- Only name generation inside loop
        do  { SDoc -> TcRnIf m n ()
    forall m n. SDoc -> TcRnIf m n ()
    traceIf (String -> SDoc
    forall doc. IsLine doc => String -> doc
    text String
    "buildClass")

            ; datacon_name <- Name -> (OccName -> OccName) -> TcRnIf m n Name
    forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
    newImplicitBinder Name
    tycon_name OccName -> OccName
    mkClassDataConOcc
            ; tc_rep_name  <- newTyConRepName tycon_name

            ; op_items <- mapM (mk_op_item rec_clas) sig_stuff
                            -- Build the selector id and default method id

                  -- Make selectors for the superclasses
            ; sc_sel_names <- mapM  (newImplicitBinder tycon_name . mkSuperDictSelOcc)
                                    (takeList sc_theta [fIRST_TAG..])
            ; let sc_sel_ids = [ Name -> Class -> TyVar
    mkDictSelId Name
    sc_name Class
    rec_clas
                               | Name
    sc_name <- [Name]
    sc_sel_names]
                  -- We number off the Dict superclass selectors, 1, 2, 3 etc so that we
                  -- can construct names for the selectors. Thus
                  --      class (C a, C b) => D a b where ...
                  -- gives superclass selectors
                  --      D_sc1, D_sc2
                  -- (We used to call them D_C, but now we can have two different
                  --  superclasses both called C!)

            ; let use_newtype = ThetaType -> Bool
    forall a. [a] -> Bool
    isSingleton (ThetaType
    sc_theta ThetaType -> ThetaType -> ThetaType
    forall a. [a] -> [a] -> [a]
    ++ ThetaType
    op_tys)
                    -- Use a newtype if the data constructor
                    --   (a) has exactly one value field
                    --       i.e. exactly one operation or superclass taken together
                    --   (b) that value is of lifted type (which they always are, because
                    --       we box equality superclasses)
                    -- See Note [Class newtypes and equality predicates]
                    --
                    -- In the case of
                    --     class C a => D a
                    -- we use a newtype, but with one superclass and no arguments
                  args       = [Name]
    sc_sel_names [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name]
    op_names
                  op_tys     = [Type
    ty | (Name
    _,Type
    ty,Maybe (DefMethSpec (SrcSpan, Type))
    _) <- [KnotTied MethInfo]
    sig_stuff]
                  op_names   = [Name
    op | (Name
    op,Type
    _,Maybe (DefMethSpec (SrcSpan, Type))
    _) <- [KnotTied MethInfo]
    sig_stuff]
                  rec_tycon  = Class -> TyCon
    classTyCon Class
    rec_clas
                  univ_bndrs = [TyConBinder] -> [InvisTVBinder]
    tyConInvisTVBinders [TyConBinder]
    binders
                  univ_tvs   = [InvisTVBinder] -> [TyVar]
    forall tv argf. [VarBndr tv argf] -> [tv]
    binderVars [InvisTVBinder]
    univ_bndrs
                  bang_opts  = [HsImplBang] -> DataConBangOpts
    FixedBangOpts ((Name -> HsImplBang) -> [Name] -> [HsImplBang]
    forall a b. (a -> b) -> [a] -> [b]
    map (HsImplBang -> Name -> HsImplBang
    forall a b. a -> b -> a
    const HsImplBang
    HsLazy) [Name]
    args)

            ; rep_nm   <- newTyConRepName datacon_name
            ; dict_con <- buildDataCon (panic "buildClass: FamInstEnvs")
                                       bang_opts
                                       datacon_name
                                       False        -- Not declared infix
                                       rep_nm
                                       (map (const no_bang) args)
                                       [{- No fields -}]
                                       univ_tvs
                                       [{- no existentials -}]
                                       univ_bndrs
                                       [{- No GADT equalities -}]
                                       sc_theta
                                       (map unrestricted op_tys) -- type classes are unrestricted
                                       (mkTyConApp rec_tycon (mkTyVarTys univ_tvs))
                                       rec_tycon
                                       (mkTyConTagMap rec_tycon)

            ; rhs <- case () of
                      ()
    _ | Bool
    use_newtype
                        -> Name -> TyCon -> DataCon -> IOEnv (Env m n) AlgTyConRhs
    forall m n. Name -> TyCon -> DataCon -> TcRnIf m n AlgTyConRhs
    mkNewTyConRhs Name
    tycon_name TyCon
    rec_tycon DataCon
    dict_con
                        | Name -> Bool
    isCTupleTyConName Name
    tycon_name
                        -> AlgTyConRhs -> IOEnv (Env m n) AlgTyConRhs
    forall a. a -> IOEnv (Env m n) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TupleTyCon { data_con :: DataCon
    data_con = DataCon
    dict_con
                                              , tup_sort :: TupleSort
    tup_sort = TupleSort
    ConstraintTuple })
                        | Bool
    otherwise
                        -> AlgTyConRhs -> IOEnv (Env m n) AlgTyConRhs
    forall a. a -> IOEnv (Env m n) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DataCon] -> AlgTyConRhs
    mkDataTyConRhs [DataCon
    dict_con])

            ; let { tycon = Name
    -> [TyConBinder] -> [Role] -> AlgTyConRhs -> Class -> Name -> TyCon
    mkClassTyCon Name
    tycon_name [TyConBinder]
    binders [Role]
    roles
                                         AlgTyConRhs
    rhs Class
    rec_clas Name
    tc_rep_name
                    -- A class can be recursive, and in the case of newtypes
                    -- this matters.  For example
                    --      class C a where { op :: C b => a -> b -> Int }
                    -- Because C has only one operation, it is represented by
                    -- a newtype, and it should be a *recursive* newtype.
                    -- [If we don't make it a recursive newtype, we'll expand the
                    -- newtype like a synonym, but that will lead to an infinite
                    -- type]

                  ; result = Name
    -> [TyVar]
    -> [FunDep TyVar]
    -> ThetaType
    -> [TyVar]
    -> [ClassATItem]
    -> [ClassOpItem]
    -> ClassMinimalDef
    -> TyCon
    -> Class
    mkClass Name
    tycon_name [TyVar]
    univ_tvs [FunDep TyVar]
    fds
                                     ThetaType
    sc_theta [TyVar]
    sc_sel_ids [ClassATItem]
    at_items
                                     [ClassOpItem]
    op_items ClassMinimalDef
    mindef TyCon
    tycon
                  }
            ; traceIf (text "buildClass" <+> ppr tycon)
            ; return result }
      where
        no_bang :: HsSrcBang
    no_bang = SourceText -> SrcUnpackedness -> SrcStrictness -> HsSrcBang
    HsSrcBang SourceText
    NoSourceText SrcUnpackedness
    NoSrcUnpack SrcStrictness
    NoSrcStrict

        mk_op_item :: Class -> TcMethInfo -> TcRnIf n m ClassOpItem
        mk_op_item :: forall n m. Class -> KnotTied MethInfo -> TcRnIf n m ClassOpItem
    mk_op_item Class
    rec_clas (Name
    op_name, Type
    _, Maybe (DefMethSpec (SrcSpan, Type))
    dm_spec)
          = do { dm_info <- Name
    -> Maybe (DefMethSpec (SrcSpan, Type))
    -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
    forall n m.
    Name
    -> Maybe (DefMethSpec (SrcSpan, Type))
    -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
    mk_dm_info Name
    op_name Maybe (DefMethSpec (SrcSpan, Type))
    dm_spec
               ; return (mkDictSelId op_name rec_clas, dm_info) }

        mk_dm_info :: Name -> Maybe (DefMethSpec (SrcSpan, Type))
                   -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
        mk_dm_info :: forall n m.
    Name
    -> Maybe (DefMethSpec (SrcSpan, Type))
    -> TcRnIf n m (Maybe (Name, DefMethSpec Type))
    mk_dm_info Name
    _ Maybe (DefMethSpec (SrcSpan, Type))
    Nothing
          = Maybe (Name, DefMethSpec Type)
    -> IOEnv (Env n m) (Maybe (Name, DefMethSpec Type))
    forall a. a -> IOEnv (Env n m) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (Name, DefMethSpec Type)
    forall a. Maybe a
    Nothing
        mk_dm_info Name
    op_name (Just DefMethSpec (SrcSpan, Type)
    VanillaDM)
          = do { dm_name <- Name -> (OccName -> OccName) -> TcRnIf n m Name
    forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
    newImplicitBinder Name
    op_name OccName -> OccName
    mkDefaultMethodOcc
               ; return (Just (dm_name, VanillaDM)) }
        mk_dm_info Name
    op_name (Just (GenericDM (SrcSpan
    loc, Type
    dm_ty)))
          = do { dm_name <- Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf n m Name
    forall m n.
    Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
    newImplicitBinderLoc Name
    op_name OccName -> OccName
    mkDefaultMethodOcc SrcSpan
    loc
               ; return (Just (dm_name, GenericDM dm_ty)) }

    {-
    Note [Class newtypes and equality predicates]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider
            class (a ~ F b) => C a b where
              op :: a -> b

    We cannot represent this by a newtype, even though it's not
    existential, because there are two value fields (the equality
    predicate and op. See #2238

    Moreover,
              class (a ~ F b) => C a b where {}
    Here we can't use a newtype either, even though there is only
    one field, because equality predicates are unboxed, and classes
    are boxed.
    -}

    newImplicitBinder :: Name                       -- Base name
                      -> (OccName -> OccName)       -- Occurrence name modifier
                      -> TcRnIf m n Name            -- Implicit name
    -- Called in GHC.Tc.TyCl.Build to allocate the implicit binders of type/class decls
    -- For source type/class decls, this is the first occurrence
    -- For iface ones, GHC.Iface.Load has already allocated a suitable name in the cache
    newImplicitBinder :: forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
    newImplicitBinder Name
    base_name OccName -> OccName
    mk_sys_occ
      = Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
    forall m n.
    Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
    newImplicitBinderLoc Name
    base_name OccName -> OccName
    mk_sys_occ (Name -> SrcSpan
    nameSrcSpan Name
    base_name)

    newImplicitBinderLoc :: Name                       -- Base name
                         -> (OccName -> OccName)       -- Occurrence name modifier
                         -> SrcSpan
                         -> TcRnIf m n Name            -- Implicit name
    -- Just the same, but lets you specify the SrcSpan
    newImplicitBinderLoc :: forall m n.
    Name -> (OccName -> OccName) -> SrcSpan -> TcRnIf m n Name
    newImplicitBinderLoc Name
    base_name OccName -> OccName
    mk_sys_occ SrcSpan
    loc
      | Just Module
    mod <- Name -> Maybe Module
    nameModule_maybe Name
    base_name
      = Module -> OccName -> SrcSpan -> TcRnIf m n Name
    forall a b. Module -> OccName -> SrcSpan -> TcRnIf a b Name
    newGlobalBinder Module
    mod OccName
    occ SrcSpan
    loc
      | Bool
    otherwise           -- When typechecking a [d| decl bracket |],
                            -- TH generates types, classes etc with Internal names,
                            -- so we follow suit for the implicit binders
      = do  { uniq <- TcRnIf m n Unique
    forall gbl lcl. TcRnIf gbl lcl Unique
    newUnique
            ; return (mkInternalName uniq occ loc) }
      where
        occ :: OccName
    occ = OccName -> OccName
    mk_sys_occ (Name -> OccName
    nameOccName Name
    base_name)

    -- | Make the 'TyConRepName' for this 'TyCon'
    newTyConRepName :: Name -> TcRnIf gbl lcl TyConRepName
    newTyConRepName :: forall gbl lcl. Name -> TcRnIf gbl lcl Name
    newTyConRepName Name
    tc_name
      | Just Module
    mod <- Name -> Maybe Module
    nameModule_maybe Name
    tc_name
      , (Module
    mod, OccName
    occ) <- Module -> OccName -> (Module, OccName)
    tyConRepModOcc Module
    mod (Name -> OccName
    nameOccName Name
    tc_name)
      = Module -> OccName -> SrcSpan -> TcRnIf gbl lcl Name
    forall a b. Module -> OccName -> SrcSpan -> TcRnIf a b Name
    newGlobalBinder Module
    mod OccName
    occ SrcSpan
    noSrcSpan
      | Bool
    otherwise
      = Name -> (OccName -> OccName) -> TcRnIf gbl lcl Name
    forall m n. Name -> (OccName -> OccName) -> TcRnIf m n Name
    newImplicitBinder Name
    tc_name OccName -> OccName
    mkTyConRepOcc