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

    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE MagicHash #-}

    -- | Type equality and comparison
    module GHC.Core.TyCo.Compare (

        -- * Type equality
        eqType, eqTypeIgnoringMultiplicity, eqTypeX, eqTypes,
        eqVarBndrs,

        pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck,
        tcEqTyConApps,
        mayLookIdentical,

        -- * Type comparison
        nonDetCmpType,

       -- * Visiblity comparision
       eqForAllVis, cmpForAllVis

       ) where

    import GHC.Prelude

    import GHC.Core.Type( typeKind, coreView, tcSplitAppTyNoView_maybe, splitAppTyNoView_maybe
                        , isLevityTy, isRuntimeRepTy, isMultiplicityTy )

    import GHC.Core.TyCo.Rep
    import GHC.Core.TyCo.FVs
    import GHC.Core.TyCon
    import GHC.Core.Multiplicity( MultiplicityFlag(..) )

    import GHC.Types.Var
    import GHC.Types.Unique
    import GHC.Types.Var.Env
    import GHC.Types.Var.Set

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

    import GHC.Base (reallyUnsafePtrEquality#)

    import qualified Data.Semigroup as S

    {- GHC.Core.TyCo.Compare overview
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    This module implements type equality and comparison

    It uses a few functions from GHC.Core.Type, notably `typeKind`,
    so it currently sits "on top of" GHC.Core.Type.
    -}

    {- *********************************************************************
    *                                                                      *
                           Type equality

         We don't use (==) from class Eq, partly so that we know where
         type equality is called, and partly because there are multiple
         variants.
    *                                                                      *
    ********************************************************************* -}

    {- Note [Computing equality on types]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    This module implements type equality, notably `eqType`. This is
    "definitional equality" or just "equality" for short.

    There are several places within GHC that depend on the precise choice of
    definitional equality used. If we change that definition, all these places
    must be updated. This Note merely serves as a place for all these places
    to refer to, so searching for references to this Note will find every place
    that needs to be updated.

    * See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep.

    * See Historical Note [Typechecker equality vs definitional equality]
      below

    Note [Casts and coercions in type comparision]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    As (EQTYPE) in Note [Non-trivial definitional equality] says, our
    general plan, implemented by `fullEq`, is:
     (1) ignore both casts and coercions when comparing types,
     (2) instead, compare the /kinds/ of the two types,
         as well as the types themselves

    If possible we want to avoid step (2), comparing the kinds; doing so involves
    calling `typeKind` and doing another comparision.

    When can we avoid doing so?  Answer: we can certainly avoid doing so if the
    types we are comparing have no casts or coercions.  But we can do better.
    Consider
        eqType (TyConApp T [s1, ..., sn]) (TyConApp T [t1, .., tn])
    We are going to call (eqType s1 t1), (eqType s2 t2) etc.

    The kinds of `s1` and `t1` must be equal, because these TyConApps are well-kinded,
    and both TyConApps are headed by the same T. So the first recursive call to `eqType`
    certainly doesn't need to check kinds. If that call returns False, we stop. Otherwise,
    we know that `s1` and `t1` are themselves equal (not just their kinds). This
    makes the kinds of `s2` and `t2` to be equal, because those kinds come from the
    kind of T instantiated with `s1` and `t1` -- which are the same. Thus we do not
    need to check the kinds of `s2` and `t2`. By induction, we don't need to check
    the kinds of *any* of the types in a TyConApp, and we also do not need to check
    the kinds of the TyConApps themselves.

    Conclusion:

    * casts and coercions under a TyConApp don't matter -- even including type synonyms

    * In step (2), use `hasCasts` to tell if there are any casts to worry about. It
      does not look very deep, because TyConApps and FunTys are so common, and it
      doesn't allocate.  The only recursive cases are AppTy and ForAllTy.

    Alternative implementation.  Instead of `hasCasts`, we could make the
    generic_eq_type function return
      data EqResult = NotEq | EqWithNoCasts | EqWithCasts
    Practically free; but stylistically I prefer useing `hasCasts`:
      * `generic_eq_type` can just uses familiar booleans
      * There is a lot more branching with the three-value variant.
      * It separates concerns.  No need to think about cast-tracking when doing the
        equality comparison.
      * Indeed sometimes we omit the kind check unconditionally, so tracking it is just wasted
        work.
    I did try both; there was no perceptible perf difference so I chose `hasCasts` version.

    Note [Equality on AppTys]
    ~~~~~~~~~~~~~~~~~~~~~~~~~
    In our cast-ignoring equality, we want to say that the following two
    are equal:

      (Maybe |> co) (Int |> co')   ~?       Maybe Int

    But the left is an AppTy while the right is a TyConApp. The solution is
    to use splitAppTyNoView_maybe to break up the TyConApp into its pieces and
    then continue. Easy to do, but also easy to forget to do.

    Note [Comparing type synonyms]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider the task of testing equality between two 'Type's of the form

      TyConApp tc tys1  =  TyConApp tc tys2

    where `tc` is a type synonym. A naive way to perform this comparison these
    would first expand the synonym and then compare the resulting expansions.

    However, this is obviously wasteful and the RHS of `tc` may be large. We'd
    prefer to compare `tys1 = tys2`.  When is that sound?  Precisely when the
    synonym is not /forgetful/; that is, all its type variables appear in its
    RHS -- see `GHC.Core.TyCon.isForgetfulSynTyCon`.

    Of course, if we find that the TyCons are *not* equal then we still need to
    perform the expansion as their RHSs may still be equal.

    This works fine for /equality/, but not for /comparison/.  Consider
       type S a b = (b, a)
    Now consider
       S Int Bool `compare` S Char Char
    The ordering may depend on whether we expand the synonym or not, and we
    don't want the result to depend on that. So for comparison we stick to
    /nullary/ synonyms only, which is still useful.

    We perform this optimisation in a number of places:

     * GHC.Core.TyCo.Compare.eqType      (works for non-nullary synonyms)
     * GHC.Core.Map.TYpe.eqDeBruijnType  (works for non-nullary synonyms)
     * GHC.Core.Types.nonDetCmpType      (nullary only)

    This optimisation is especially helpful for the ubiquitous GHC.Types.Type,
    since GHC prefers to use the type synonym over @TYPE 'LiftedRep@ applications
    whenever possible. See Note [Using synonyms to compress types] in
    GHC.Core.Type for details.

    Currently-missed opportunity (#25009):
    * In the case of forgetful synonyms, we could still compare the args, pairwise,
      and then compare the RHS's with a suitably extended RnEnv2.  That would avoid
      comparing the same arg repeatedly.  e.g.
          type S a b = (a,a)
      Compare   S <big> y ~ S <big> y
      If we expand, we end up compare <big> with itself twice.

      But since forgetful synonyms are rare, we have not tried this.

    Note [Type comparisons using object pointer comparisons]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Quite often we substitute the type from a definition site into
    occurrences without a change. This means for code like:
        \x -> (x,x,x)
    The type of every `x` will often be represented by a single object
    in the heap. We can take advantage of this by shortcutting the equality
    check if two types are represented by the same pointer under the hood.
    In some cases this reduces compiler allocations by ~2%.

    See Note [Pointer comparison operations] in GHC.Builtin.primops.txt.pp

    Note [Respecting multiplicity when comparing types]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Generally speaking, we respect multiplicities (i.e. the linear part of the type
    system) when comparing types.  Doing so is of course crucial during typechecking.

    But for reasons described in Note [Linting linearity] in GHC.Core.Lint, it is hard
    to ensure that Core is always type-correct when it comes to linearity.  So
    * `eqTypeIgnoringMultiplicity` provides a way to compare types that /ignores/ multiplicities
    * We use this multiplicity-blind comparison very occasionally, notably
        - in Core Lint: see Note [Linting linearity] in GHC.Core.Lint
        - in rule matching: see Note [Rewrite rules ignore multiplicities in FunTy]
          in GHC.Core.Unify
    -}

    tcEqKind :: HasDebugCallStack => Kind -> Kind -> Bool
    tcEqKind :: HasDebugCallStack => Type -> Type -> Bool
    tcEqKind = HasDebugCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    tcEqType

    tcEqType :: HasDebugCallStack => Type -> Type -> Bool
    tcEqType :: HasDebugCallStack => Type -> Type -> Bool
    tcEqType = HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    eqType

    -- | Just like 'tcEqType', but will return True for types of different kinds
    -- as long as their non-coercion structure is identical.
    tcEqTypeNoKindCheck :: Type -> Type -> Bool
    tcEqTypeNoKindCheck :: Type -> Type -> Bool
    tcEqTypeNoKindCheck = Type -> Type -> Bool
    eqTypeNoKindCheck

    -- | Check whether two TyConApps are the same; if the number of arguments
    -- are different, just checks the common prefix of arguments.
    tcEqTyConApps :: TyCon -> [Type] -> TyCon -> [Type] -> Bool
    tcEqTyConApps :: TyCon -> [Type] -> TyCon -> [Type] -> Bool
    tcEqTyConApps TyCon
    tc1 [Type]
    args1 TyCon
    tc2 [Type]
    args2
      = TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2 Bool -> Bool -> Bool
    &&
        [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ((Type -> Type -> Bool) -> [Type] -> [Type] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Type -> Type -> Bool
    tcEqTypeNoKindCheck [Type]
    args1 [Type]
    args2)
        -- No kind check necessary: if both arguments are well typed, then
        -- any difference in the kinds of later arguments would show up
        -- as differences in earlier (dependent) arguments

    -- | Type equality on lists of types, looking through type synonyms
    eqTypes :: [Type] -> [Type] -> Bool
    eqTypes :: [Type] -> [Type] -> Bool
    eqTypes []       []       = Bool
    True
    eqTypes (Type
    t1:[Type]
    ts1) (Type
    t2:[Type]
    ts2) = HasCallStack => Type -> Type -> Bool
    Type -> Type -> Bool
    eqType Type
    t1 Type
    t2 Bool -> Bool -> Bool
    && [Type] -> [Type] -> Bool
    eqTypes [Type]
    ts1 [Type]
    ts2
    eqTypes [Type]
    _        [Type]
    _        = Bool
    False

    eqVarBndrs :: HasCallStack => RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
    -- Check that the var lists are the same length
    -- and have matching kinds; if so, extend the RnEnv2
    -- Returns Nothing if they don't match
    eqVarBndrs :: HasCallStack => RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
    eqVarBndrs RnEnv2
    env [] []
     = RnEnv2 -> Maybe RnEnv2
    forall a. a -> Maybe a
    Just RnEnv2
    env
    eqVarBndrs RnEnv2
    env (Var
    tv1:[Var]
    tvs1) (Var
    tv2:[Var]
    tvs2)
     | HasCallStack => RnEnv2 -> Type -> Type -> Bool
    RnEnv2 -> Type -> Type -> Bool
    eqTypeX RnEnv2
    env (Var -> Type
    varType Var
    tv1) (Var -> Type
    varType Var
    tv2)
     = HasCallStack => RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
    RnEnv2 -> [Var] -> [Var] -> Maybe RnEnv2
    eqVarBndrs (RnEnv2 -> Var -> Var -> RnEnv2
    rnBndr2 RnEnv2
    env Var
    tv1 Var
    tv2) [Var]
    tvs1 [Var]
    tvs2
    eqVarBndrs RnEnv2
    _ [Var]
    _ [Var]
    _= Maybe RnEnv2
    forall a. Maybe a
    Nothing

    initRnEnv :: Type -> Type -> RnEnv2
    initRnEnv :: Type -> Type -> RnEnv2
    initRnEnv Type
    ta Type
    tb = InScopeSet -> RnEnv2
    mkRnEnv2 (InScopeSet -> RnEnv2) -> InScopeSet -> RnEnv2
    forall a b. (a -> b) -> a -> b
    $ VarSet -> InScopeSet
    mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
    forall a b. (a -> b) -> a -> b
    $
                      Type -> VarSet
    tyCoVarsOfType Type
    ta VarSet -> VarSet -> VarSet
    `unionVarSet` Type -> VarSet
    tyCoVarsOfType Type
    tb

    eqTypeNoKindCheck :: Type -> Type -> Bool
    eqTypeNoKindCheck :: Type -> Type -> Bool
    eqTypeNoKindCheck Type
    ty1 Type
    ty2 = Type -> Type -> Bool
    eq_type_expand_respect Type
    ty1 Type
    ty2

    -- | Type equality comparing both visible and invisible arguments,
    -- expanding synonyms and respecting multiplicities.
    eqType :: HasCallStack => Type -> Type -> Bool
    eqType :: HasCallStack => Type -> Type -> Bool
    eqType Type
    ta Type
    tb = (Type -> Type -> Bool) -> Type -> Type -> Bool
    fullEq Type -> Type -> Bool
    eq_type_expand_respect Type
    ta Type
    tb

    -- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
    eqTypeX :: HasCallStack => RnEnv2 -> Type -> Type -> Bool
    eqTypeX :: HasCallStack => RnEnv2 -> Type -> Type -> Bool
    eqTypeX RnEnv2
    env Type
    ta Type
    tb = (Type -> Type -> Bool) -> Type -> Type -> Bool
    fullEq (RnEnv2 -> Type -> Type -> Bool
    eq_type_expand_respect_x RnEnv2
    env) Type
    ta Type
    tb

    eqTypeIgnoringMultiplicity :: Type -> Type -> Bool
    -- See Note [Respecting multiplicity when comparing types]
    eqTypeIgnoringMultiplicity :: Type -> Type -> Bool
    eqTypeIgnoringMultiplicity Type
    ta Type
    tb = (Type -> Type -> Bool) -> Type -> Type -> Bool
    fullEq Type -> Type -> Bool
    eq_type_expand_ignore Type
    ta Type
    tb

    -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
    pickyEqType :: Type -> Type -> Bool
    -- Check when two types _look_ the same, _including_ synonyms.
    -- So (pickyEqType String [Char]) returns False
    -- This ignores kinds and coercions, because this is used only for printing.
    pickyEqType :: Type -> Type -> Bool
    pickyEqType Type
    ta Type
    tb = Type -> Type -> Bool
    eq_type_keep_respect Type
    ta Type
    tb

    {- Note [Specialising type equality]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The type equality predicates in Type are hit pretty hard by GHC.  Consequently
    we take pains to ensure that these paths are compiled to efficient,
    minimally-allocating code.  Plan:

    * The main workhorse is `inline_generic_eq_type_x`.  It is /non-recursive/
      and is marked INLINE.

    * `inline_generic_eq_type_x` has various parameters that control what it does:
      * syn_flag::SynFlag            whether type synonyms are expanded or kept.
      * mult_flag::MultiplicityFlag  whether multiplicities are ignored or respected
      * mb_env::Maybe RnEnv2         an optional RnEnv2.

    * `inline_generic_eq_type_x` has a handful of call sites, namely the ones
      in `eq_type_expand_respect`, `eq_type_expand_repect_x` etc.  It inlines
      at all these sites, specialising to the data values passed for the
      control parameters.

    * All /other/ calls to `inline_generic_eq_type_x` go via
         generic_eq_type_x = inline_generic_eq_type_x
         {-# NOINLNE generic_eq_type_x #-}
      The idea is that all calls to `generic_eq_type_x` are specialised by the
      RULES, so this NOINLINE version is seldom, if ever, actually called.

    * For each of specialised copy of `inline_generic_eq_type_x, there is a
      corresponding rewrite RULE that rewrites a call to (generic_eq_type_x args)
      into the appropriate specialied version.

    See #19226.
    -}

    -- | This flag controls whether we expand synonyms during comparison
    data SynFlag = ExpandSynonyms | KeepSynonyms

    eq_type_expand_respect, eq_type_expand_ignore, eq_type_keep_respect
      :: Type -> Type -> Bool
    eq_type_expand_respect_x, eq_type_expand_ignore_x, eq_type_keep_respect_x
       :: RnEnv2 -> Type -> Type -> Bool

    eq_type_expand_respect :: Type -> Type -> Bool
    eq_type_expand_respect       = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    ExpandSynonyms MultiplicityFlag
    RespectMultiplicities Maybe RnEnv2
    forall a. Maybe a
    Nothing
    eq_type_expand_respect_x :: RnEnv2 -> Type -> Type -> Bool
    eq_type_expand_respect_x RnEnv2
    env = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    ExpandSynonyms MultiplicityFlag
    RespectMultiplicities (RnEnv2 -> Maybe RnEnv2
    forall a. a -> Maybe a
    Just RnEnv2
    env)
    eq_type_expand_ignore :: Type -> Type -> Bool
    eq_type_expand_ignore        = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    ExpandSynonyms MultiplicityFlag
    IgnoreMultiplicities  Maybe RnEnv2
    forall a. Maybe a
    Nothing
    eq_type_expand_ignore_x :: RnEnv2 -> Type -> Type -> Bool
    eq_type_expand_ignore_x RnEnv2
    env  = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    ExpandSynonyms MultiplicityFlag
    IgnoreMultiplicities  (RnEnv2 -> Maybe RnEnv2
    forall a. a -> Maybe a
    Just RnEnv2
    env)
    eq_type_keep_respect :: Type -> Type -> Bool
    eq_type_keep_respect         = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    KeepSynonyms   MultiplicityFlag
    RespectMultiplicities Maybe RnEnv2
    forall a. Maybe a
    Nothing
    eq_type_keep_respect_x :: RnEnv2 -> Type -> Type -> Bool
    eq_type_keep_respect_x RnEnv2
    env   = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    KeepSynonyms   MultiplicityFlag
    RespectMultiplicities (RnEnv2 -> Maybe RnEnv2
    forall a. a -> Maybe a
    Just RnEnv2
    env)

    {-# RULES
    "eqType1" generic_eq_type_x ExpandSynonyms RespectMultiplicities Nothing
                 = eq_type_expand_respect
    "eqType2" forall env. generic_eq_type_x ExpandSynonyms RespectMultiplicities (Just env)
                 = eq_type_expand_respect_x env
    "eqType3" generic_eq_type_x ExpandSynonyms IgnoreMultiplicities Nothing
                 = eq_type_expand_ignore
    "eqType4" forall env. generic_eq_type_x ExpandSynonyms IgnoreMultiplicities (Just env)
                 = eq_type_expand_ignore_x env
    "eqType5" generic_eq_type_x KeepSynonyms RespectMultiplicities Nothing
                 = eq_type_keep_respect
    "eqType6" forall env. generic_eq_type_x KeepSynonyms RespectMultiplicities (Just env)
                 = eq_type_keep_respect_x env
     #-}

    -- ---------------------------------------------------------------
    -- | Real worker for 'eqType'. No kind check!
    -- Inline it at the (handful of local) call sites
    -- The "generic" bit refers to the flag paramerisation
    -- See Note [Specialising type equality].
    generic_eq_type_x, inline_generic_eq_type_x
      :: SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool

    {-# NOINLINE generic_eq_type_x #-}
    generic_eq_type_x :: SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    generic_eq_type_x = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x
    -- See Note [Computing equality on types] in Type

    {-# INLINE inline_generic_eq_type_x #-}
    -- This non-recursive function can inline at its (few) call sites.  The
    -- recursion goes via generic_eq_type_x, which is the loop-breaker.
    inline_generic_eq_type_x :: SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    inline_generic_eq_type_x SynFlag
    syn_flag MultiplicityFlag
    mult_flag Maybe RnEnv2
    mb_env
      = \ Type
    t1 Type
    t2 -> Type
    t1 Type -> Bool -> Bool
    forall a b. a -> b -> b
    `seq` Type
    t2 Type -> Bool -> Bool
    forall a b. a -> b -> b
    `seq`
        let go :: Type -> Type -> Bool
    go = SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    generic_eq_type_x SynFlag
    syn_flag MultiplicityFlag
    mult_flag Maybe RnEnv2
    mb_env
                 -- Abbreviation for recursive calls

            gos :: [Type] -> [Type] -> Bool
    gos []       []       = Bool
    True
            gos (Type
    t1:[Type]
    ts1) (Type
    t2:[Type]
    ts2) = Type -> Type -> Bool
    go Type
    t1 Type
    t2 Bool -> Bool -> Bool
    && [Type] -> [Type] -> Bool
    gos [Type]
    ts1 [Type]
    ts2
            gos [Type]
    _ [Type]
    _               = Bool
    False

        in case (Type
    t1,Type
    t2) of
          (Type, Type)
    _ | Int#
    1# <- Type -> Type -> Int#
    forall a b. a -> b -> Int#
    reallyUnsafePtrEquality# Type
    t1 Type
    t2 -> Bool
    True
          -- See Note [Type comparisons using object pointer comparisons]

          (TyConApp TyCon
    tc1 [Type]
    tys1, TyConApp TyCon
    tc2 [Type]
    tys2)
            | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2, Bool -> Bool
    not (TyCon -> Bool
    isForgetfulSynTyCon TyCon
    tc1)   -- See Note [Comparing type synonyms]
            -> [Type] -> [Type] -> Bool
    gos [Type]
    tys1 [Type]
    tys2

          (Type, Type)
    _ | SynFlag
    ExpandSynonyms <- SynFlag
    syn_flag, Just Type
    t1' <- Type -> Maybe Type
    coreView Type
    t1 -> Type -> Type -> Bool
    go Type
    t1' Type
    t2
            | SynFlag
    ExpandSynonyms <- SynFlag
    syn_flag, Just Type
    t2' <- Type -> Maybe Type
    coreView Type
    t2 -> Type -> Type -> Bool
    go Type
    t1 Type
    t2'

          (TyConApp TyCon
    tc1 [Type]
    ts1, TyConApp TyCon
    tc2 [Type]
    ts2)
            | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2 -> [Type] -> [Type] -> Bool
    gos [Type]
    ts1 [Type]
    ts2
            | Bool
    otherwise  -> Bool
    False

          (TyVarTy Var
    tv1, TyVarTy Var
    tv2)
            -> case Maybe RnEnv2
    mb_env of
                  Maybe RnEnv2
    Nothing  -> Var
    tv1 Var -> Var -> Bool
    forall a. Eq a => a -> a -> Bool
    == Var
    tv2
                  Just RnEnv2
    env -> RnEnv2 -> Var -> Var
    rnOccL RnEnv2
    env Var
    tv1 Var -> Var -> Bool
    forall a. Eq a => a -> a -> Bool
    == RnEnv2 -> Var -> Var
    rnOccR RnEnv2
    env Var
    tv2

          (LitTy TyLit
    lit1,    LitTy TyLit
    lit2)    -> TyLit
    lit1 TyLit -> TyLit -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyLit
    lit2
          (CastTy Type
    t1' KindCoercion
    _,   Type
    _)            -> Type -> Type -> Bool
    go Type
    t1' Type
    t2 -- Ignore casts
          (Type
    _,             CastTy Type
    t2' KindCoercion
    _)  -> Type -> Type -> Bool
    go Type
    t1 Type
    t2' -- Ignore casts
          (CoercionTy {}, CoercionTy {}) -> Bool
    True      -- Ignore coercions

        -- Make sure we handle all FunTy cases since falling through to the
        -- AppTy case means that tcSplitAppTyNoView_maybe may see an unzonked
        -- kind variable, which causes things to blow up.
        -- See Note [Equality on FunTys] in GHC.Core.TyCo.Rep: we must check
        -- kinds here
          (FunTy FunTyFlag
    _ Type
    w1 Type
    arg1 Type
    res1, FunTy FunTyFlag
    _ Type
    w2 Type
    arg2 Type
    res2)
            ->   (Type -> Type -> Bool) -> Type -> Type -> Bool
    fullEq Type -> Type -> Bool
    go Type
    arg1 Type
    arg2
              Bool -> Bool -> Bool
    && (Type -> Type -> Bool) -> Type -> Type -> Bool
    fullEq Type -> Type -> Bool
    go Type
    res1 Type
    res2
              Bool -> Bool -> Bool
    && (case MultiplicityFlag
    mult_flag of
                      MultiplicityFlag
    RespectMultiplicities -> Type -> Type -> Bool
    go Type
    w1 Type
    w2
                      MultiplicityFlag
    IgnoreMultiplicities  -> Bool
    True)

          -- See Note [Equality on AppTys] in GHC.Core.Type
          (AppTy Type
    s1 Type
    t1', Type
    _)
            | Just (Type
    s2, Type
    t2') <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    t2
            -> Type -> Type -> Bool
    go Type
    s1 Type
    s2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    go Type
    t1' Type
    t2'
          (Type
    _,  AppTy Type
    s2 Type
    t2')
            | Just (Type
    s1, Type
    t1') <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    t1
            -> Type -> Type -> Bool
    go Type
    s1 Type
    s2 Bool -> Bool -> Bool
    && Type -> Type -> Bool
    go Type
    t1' Type
    t2'

          (ForAllTy (Bndr Var
    tv1 ForAllTyFlag
    vis1) Type
    body1, ForAllTy (Bndr Var
    tv2 ForAllTyFlag
    vis2) Type
    body2)
            -> case Maybe RnEnv2
    mb_env of
                  Maybe RnEnv2
    Nothing -> SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    generic_eq_type_x SynFlag
    syn_flag MultiplicityFlag
    mult_flag
                                (RnEnv2 -> Maybe RnEnv2
    forall a. a -> Maybe a
    Just (Type -> Type -> RnEnv2
    initRnEnv Type
    t1 Type
    t2)) Type
    t1 Type
    t2
                  Just RnEnv2
    env
                    | ForAllTyFlag
    vis1 ForAllTyFlag -> ForAllTyFlag -> Bool
    `eqForAllVis` ForAllTyFlag
    vis2         -- See Note [ForAllTy and type equality]
                    -> Type -> Type -> Bool
    go (Var -> Type
    varType Var
    tv1) (Var -> Type
    varType Var
    tv2)  -- Always do kind-check
                       Bool -> Bool -> Bool
    && SynFlag -> MultiplicityFlag -> Maybe RnEnv2 -> Type -> Type -> Bool
    generic_eq_type_x SynFlag
    syn_flag MultiplicityFlag
    mult_flag
                                 (RnEnv2 -> Maybe RnEnv2
    forall a. a -> Maybe a
    Just (RnEnv2 -> Var -> Var -> RnEnv2
    rnBndr2 RnEnv2
    env Var
    tv1 Var
    tv2)) Type
    body1 Type
    body2
                    | Bool
    otherwise
                    -> Bool
    False

          (Type, Type)
    _ -> Bool
    False

    fullEq :: (Type -> Type -> Bool) -> Type -> Type -> Bool
    -- Do "full equality" including the kind check
    -- See Note [Casts and coercions in type comparision]
    {-# INLINE fullEq #-}
    fullEq :: (Type -> Type -> Bool) -> Type -> Type -> Bool
    fullEq Type -> Type -> Bool
    eq Type
    ty1 Type
    ty2
      = case Type -> Type -> Bool
    eq Type
    ty1 Type
    ty2 of
              Bool
    False    -> Bool
    False
              Bool
    True | Type -> Bool
    hasCasts Type
    ty1 Bool -> Bool -> Bool
    || Type -> Bool
    hasCasts Type
    ty2
                   -> Type -> Type -> Bool
    eq (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty1) (HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    ty2)
                   | Bool
    otherwise
                   -> Bool
    True

    hasCasts :: Type -> Bool
    -- Fast, does not look deep, does not allocate
    hasCasts :: Type -> Bool
    hasCasts (CastTy {})     = Bool
    True
    hasCasts (CoercionTy {}) = Bool
    True
    hasCasts (AppTy Type
    t1 Type
    t2)   = Type -> Bool
    hasCasts Type
    t1 Bool -> Bool -> Bool
    || Type -> Bool
    hasCasts Type
    t2
    hasCasts (ForAllTy VarBndr Var ForAllTyFlag
    _ Type
    ty) = Type -> Bool
    hasCasts Type
    ty
    hasCasts Type
    _               = Bool
    False   -- TyVarTy, TyConApp, FunTy, LitTy

    {- *********************************************************************
    *                                                                      *
                    Comparing ForAllTyFlags
    *                                                                      *
    ********************************************************************* -}

    -- | Do these denote the same level of visibility? 'Required'
    -- arguments are visible, others are not. So this function
    -- equates 'Specified' and 'Inferred'. Used for printing.
    eqForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Bool
    -- See Note [ForAllTy and type equality]
    eqForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Bool
    eqForAllVis ForAllTyFlag
    Required      ForAllTyFlag
    Required      = Bool
    True
    eqForAllVis (Invisible Specificity
    _) (Invisible Specificity
    _) = Bool
    True
    eqForAllVis ForAllTyFlag
    _             ForAllTyFlag
    _             = Bool
    False

    -- | Do these denote the same level of visibility? 'Required'
    -- arguments are visible, others are not. So this function
    -- equates 'Specified' and 'Inferred'. Used for printing.
    cmpForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Ordering
    -- See Note [ForAllTy and type equality]
    cmpForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Ordering
    cmpForAllVis ForAllTyFlag
    Required      ForAllTyFlag
    Required       = Ordering
    EQ
    cmpForAllVis ForAllTyFlag
    Required      (Invisible {}) = Ordering
    LT
    cmpForAllVis (Invisible Specificity
    _) ForAllTyFlag
    Required       = Ordering
    GT
    cmpForAllVis (Invisible Specificity
    _) (Invisible Specificity
    _)  = Ordering
    EQ

    {- Note [ForAllTy and type equality]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    When we compare (ForAllTy (Bndr tv1 vis1) ty1)
             and    (ForAllTy (Bndr tv2 vis2) ty2)
    what should we do about `vis1` vs `vis2`?

    We had a long debate about this: see #22762 and GHC Proposal 558.
    Here is the conclusion.

    * In Haskell, we really do want (forall a. ty) and (forall a -> ty) to be
      distinct types, not interchangeable.  The latter requires a type argument,
      but the former does not.  See GHC Proposal 558.

    * We /really/ do not want the typechecker and Core to have different notions of
      equality.  That is, we don't want `tcEqType` and `eqType` to differ.  Why not?
      Not so much because of code duplication but because it is virtually impossible
      to cleave the two apart. Here is one particularly awkward code path:
         The type checker calls `substTy`, which calls `mkAppTy`,
         which calls `mkCastTy`, which calls `isReflexiveCo`, which calls `eqType`.

    * Moreover the resolution of the TYPE vs CONSTRAINT story was to make the
      typechecker and Core have a single notion of equality.

    * So in GHC:
      - `tcEqType` and `eqType` implement the same equality
      - (forall a. ty) and (forall a -> ty) are distinct types in both Core and typechecker
      - That is, both `eqType` and `tcEqType` distinguish them.

    * But /at representational role/ we can relate the types. That is,
        (forall a. ty) ~R (forall a -> ty)
      After all, since types are erased, they are represented the same way.
      See Note [ForAllCo] and the typing rule for ForAllCo given there

    * What about (forall a. ty) and (forall {a}. ty)?  See Note [Comparing visibility].

    Note [Comparing visibility]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~
    We are sure that we want to distinguish (forall a. ty) and (forall a -> ty); see
    Note [ForAllTy and type equality].  But we have /three/ settings for the ForAllTyFlag:
      * Specified: forall a. ty
      * Inferred:  forall {a}. ty
      * Required:  forall a -> ty

    We could (and perhaps should) distinguish all three. But for now we distinguish
    Required from Specified/Inferred, and ignore the distinction between Specified
    and Inferred.

    The answer doesn't matter too much, provided we are consistent. And we are consistent
    because we always compare ForAllTyFlags with
      * `eqForAllVis`
      * `cmpForAllVis`.
    (You can only really check this by inspecting all pattern matches on ForAllTyFlags.)
    So if we change the decision, we just need to change those functions.

    Why don't we distinguish all three? Should GHC type-check the following program
    (adapted from #15740)?

      {-# LANGUAGE PolyKinds, ... #-}
      data D a
      type family F :: forall k. k -> Type
      type instance F = D

    Due to the way F is declared, any instance of F must have a right-hand side
    whose kind is equal to `forall k. k -> Type`. The kind of D is
    `forall {k}. k -> Type`, which is very close, but technically uses distinct
    Core:

      -----------------------------------------------------------
      | Source Haskell    | Core                                |
      -----------------------------------------------------------
      | forall  k.  <...> | ForAllTy (Bndr k Specified) (<...>) |
      | forall {k}. <...> | ForAllTy (Bndr k Inferred)  (<...>) |
      -----------------------------------------------------------

    We could deem these kinds to be unequal, but that would imply rejecting
    programs like the one above. Whether a kind variable binder ends up being
    specified or inferred can be somewhat subtle, however, especially for kinds
    that aren't explicitly written out in the source code (like in D above).

    For now, we decide

        the specified/inferred status of an invisible type variable binder
        does not affect GHC's notion of equality.

    That is, we have the following:

      --------------------------------------------------
      | Type 1            | Type 2            | Equal? |
      --------------------|-----------------------------
      | forall k. <...>   | forall k. <...>   | Yes    |
      |                   | forall {k}. <...> | Yes    |
      |                   | forall k -> <...> | No     |
      --------------------------------------------------
      | forall {k}. <...> | forall k. <...>   | Yes    |
      |                   | forall {k}. <...> | Yes    |
      |                   | forall k -> <...> | No     |
      --------------------------------------------------
      | forall k -> <...> | forall k. <...>   | No     |
      |                   | forall {k}. <...> | No     |
      |                   | forall k -> <...> | Yes    |
      --------------------------------------------------

    Examples: T16946, T15079.

    Historical Note [Typechecker equality vs definitional equality]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    This Note describes some history, in case there are vestiges of this
    history lying around in the code.

    Summary: prior to summer 2022, GHC had have two notions of equality
    over Core types.  But now there is only one: definitional equality,
    or just equality for short.

    The old setup was:

    * Definitional equality, as implemented by GHC.Core.Type.eqType.
      See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep.

    * Typechecker equality, as implemented by tcEqType.
      GHC.Tc.Solver.Equality.canonicaliseEquality also respects typechecker equality.

    Typechecker equality implied definitional equality: if two types are equal
    according to typechecker equality, then they are also equal according to
    definitional equality. The converse is not always true, as typechecker equality
    is more finer-grained than definitional equality in two places:

    * Constraint vs Type.  Definitional equality equated Type and
      Constraint, but typechecker treats them as distinct types.

    * Unlike definitional equality, which does not care about the ForAllTyFlag of a
      ForAllTy, typechecker equality treats Required type variable binders as
      distinct from Invisible type variable binders.
      See Note [ForAllTy and type equality]

    ************************************************************************
    *                                                                      *
                    Comparison for types

          Not so heavily used, less carefully optimised
    *                                                                      *
    ************************************************************************

    -- Now here comes the real worker

    Note [nonDetCmpType nondeterminism]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
    uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
    ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
    comparing type variables is nondeterministic, note the call to nonDetCmpVar in
    nonDetCmpTypeX.
    See Note [Unique Determinism] for more details.
    -}

    nonDetCmpType :: Type -> Type -> Ordering
    {-# INLINE nonDetCmpType #-}
    nonDetCmpType :: Type -> Type -> Ordering
    nonDetCmpType !Type
    t1 !Type
    t2
      -- See Note [Type comparisons using object pointer comparisons]
      | Int#
    1# <- Type -> Type -> Int#
    forall a b. a -> b -> Int#
    reallyUnsafePtrEquality# Type
    t1 Type
    t2
      = Ordering
    EQ
    nonDetCmpType (TyConApp TyCon
    tc1 []) (TyConApp TyCon
    tc2 []) | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
      = Ordering
    EQ
    nonDetCmpType Type
    t1 Type
    t2
      -- we know k1 and k2 have the same kind, because they both have kind *.
      = RnEnv2 -> Type -> Type -> Ordering
    nonDetCmpTypeX RnEnv2
    rn_env Type
    t1 Type
    t2
      where
        rn_env :: RnEnv2
    rn_env = InScopeSet -> RnEnv2
    mkRnEnv2 (VarSet -> InScopeSet
    mkInScopeSet ([Type] -> VarSet
    tyCoVarsOfTypes [Type
    t1, Type
    t2]))

    -- | An ordering relation between two 'Type's (known below as @t1 :: k1@
    -- and @t2 :: k2@)
    data TypeOrdering = TLT  -- ^ @t1 < t2@
                      | TEQ  -- ^ @t1 ~ t2@ and there are no casts in either,
                             -- therefore we can conclude @k1 ~ k2@
                      | TEQX -- ^ @t1 ~ t2@ yet one of the types contains a cast so
                             -- they may differ in kind.
                      | TGT  -- ^ @t1 > t2@
                      deriving (TypeOrdering -> TypeOrdering -> Bool
    (TypeOrdering -> TypeOrdering -> Bool)
    -> (TypeOrdering -> TypeOrdering -> Bool) -> Eq TypeOrdering
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: TypeOrdering -> TypeOrdering -> Bool
    == :: TypeOrdering -> TypeOrdering -> Bool
    $c/= :: TypeOrdering -> TypeOrdering -> Bool
    /= :: TypeOrdering -> TypeOrdering -> Bool
    Eq, Eq TypeOrdering
    Eq TypeOrdering =>
    (TypeOrdering -> TypeOrdering -> Ordering)
    -> (TypeOrdering -> TypeOrdering -> Bool)
    -> (TypeOrdering -> TypeOrdering -> Bool)
    -> (TypeOrdering -> TypeOrdering -> Bool)
    -> (TypeOrdering -> TypeOrdering -> Bool)
    -> (TypeOrdering -> TypeOrdering -> TypeOrdering)
    -> (TypeOrdering -> TypeOrdering -> TypeOrdering)
    -> Ord TypeOrdering
    TypeOrdering -> TypeOrdering -> Bool
    TypeOrdering -> TypeOrdering -> Ordering
    TypeOrdering -> TypeOrdering -> TypeOrdering
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: TypeOrdering -> TypeOrdering -> Ordering
    compare :: TypeOrdering -> TypeOrdering -> Ordering
    $c< :: TypeOrdering -> TypeOrdering -> Bool
    < :: TypeOrdering -> TypeOrdering -> Bool
    $c<= :: TypeOrdering -> TypeOrdering -> Bool
    <= :: TypeOrdering -> TypeOrdering -> Bool
    $c> :: TypeOrdering -> TypeOrdering -> Bool
    > :: TypeOrdering -> TypeOrdering -> Bool
    $c>= :: TypeOrdering -> TypeOrdering -> Bool
    >= :: TypeOrdering -> TypeOrdering -> Bool
    $cmax :: TypeOrdering -> TypeOrdering -> TypeOrdering
    max :: TypeOrdering -> TypeOrdering -> TypeOrdering
    $cmin :: TypeOrdering -> TypeOrdering -> TypeOrdering
    min :: TypeOrdering -> TypeOrdering -> TypeOrdering
    Ord, Int -> TypeOrdering
    TypeOrdering -> Int
    TypeOrdering -> [TypeOrdering]
    TypeOrdering -> TypeOrdering
    TypeOrdering -> TypeOrdering -> [TypeOrdering]
    TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering]
    (TypeOrdering -> TypeOrdering)
    -> (TypeOrdering -> TypeOrdering)
    -> (Int -> TypeOrdering)
    -> (TypeOrdering -> Int)
    -> (TypeOrdering -> [TypeOrdering])
    -> (TypeOrdering -> TypeOrdering -> [TypeOrdering])
    -> (TypeOrdering -> TypeOrdering -> [TypeOrdering])
    -> (TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering])
    -> Enum TypeOrdering
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: TypeOrdering -> TypeOrdering
    succ :: TypeOrdering -> TypeOrdering
    $cpred :: TypeOrdering -> TypeOrdering
    pred :: TypeOrdering -> TypeOrdering
    $ctoEnum :: Int -> TypeOrdering
    toEnum :: Int -> TypeOrdering
    $cfromEnum :: TypeOrdering -> Int
    fromEnum :: TypeOrdering -> Int
    $cenumFrom :: TypeOrdering -> [TypeOrdering]
    enumFrom :: TypeOrdering -> [TypeOrdering]
    $cenumFromThen :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
    enumFromThen :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
    $cenumFromTo :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
    enumFromTo :: TypeOrdering -> TypeOrdering -> [TypeOrdering]
    $cenumFromThenTo :: TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering]
    enumFromThenTo :: TypeOrdering -> TypeOrdering -> TypeOrdering -> [TypeOrdering]
    Enum, TypeOrdering
    TypeOrdering -> TypeOrdering -> Bounded TypeOrdering
    forall a. a -> a -> Bounded a
    $cminBound :: TypeOrdering
    minBound :: TypeOrdering
    $cmaxBound :: TypeOrdering
    maxBound :: TypeOrdering
    Bounded)

    nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering  -- Main workhorse
        -- See Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep
        -- See Note [Computing equality on types]
        -- Always respects multiplicities, unlike eqType
    nonDetCmpTypeX :: RnEnv2 -> Type -> Type -> Ordering
    nonDetCmpTypeX RnEnv2
    env Type
    orig_t1 Type
    orig_t2 =
        case RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    orig_t1 Type
    orig_t2 of
          -- If there are casts then we also need to do a comparison of
          -- the kinds of the types being compared
          TypeOrdering
    TEQX          -> TypeOrdering -> Ordering
    toOrdering (TypeOrdering -> Ordering) -> TypeOrdering -> Ordering
    forall a b. (a -> b) -> a -> b
    $ RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    k1 Type
    k2
          TypeOrdering
    ty_ordering   -> TypeOrdering -> Ordering
    toOrdering TypeOrdering
    ty_ordering
      where
        k1 :: Type
    k1 = HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    orig_t1
        k2 :: Type
    k2 = HasDebugCallStack => Type -> Type
    Type -> Type
    typeKind Type
    orig_t2

        toOrdering :: TypeOrdering -> Ordering
        toOrdering :: TypeOrdering -> Ordering
    toOrdering TypeOrdering
    TLT  = Ordering
    LT
        toOrdering TypeOrdering
    TEQ  = Ordering
    EQ
        toOrdering TypeOrdering
    TEQX = Ordering
    EQ
        toOrdering TypeOrdering
    TGT  = Ordering
    GT

        liftOrdering :: Ordering -> TypeOrdering
        liftOrdering :: Ordering -> TypeOrdering
    liftOrdering Ordering
    LT = TypeOrdering
    TLT
        liftOrdering Ordering
    EQ = TypeOrdering
    TEQ
        liftOrdering Ordering
    GT = TypeOrdering
    TGT

        thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
        thenCmpTy :: TypeOrdering -> TypeOrdering -> TypeOrdering
    thenCmpTy TypeOrdering
    TEQ  TypeOrdering
    rel  = TypeOrdering
    rel
        thenCmpTy TypeOrdering
    TEQX TypeOrdering
    rel  = TypeOrdering -> TypeOrdering
    hasCast TypeOrdering
    rel
        thenCmpTy TypeOrdering
    rel  TypeOrdering
    _    = TypeOrdering
    rel

        hasCast :: TypeOrdering -> TypeOrdering
        hasCast :: TypeOrdering -> TypeOrdering
    hasCast TypeOrdering
    TEQ = TypeOrdering
    TEQX
        hasCast TypeOrdering
    rel = TypeOrdering
    rel

        -- Returns both the resulting ordering relation between
        -- the two types and whether either contains a cast.
        go :: RnEnv2 -> Type -> Type -> TypeOrdering

        go :: RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    _   (TyConApp TyCon
    tc1 []) (TyConApp TyCon
    tc2 [])
          | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2
          = TypeOrdering
    TEQ    -- See Note [Comparing type synonyms]

        go RnEnv2
    env Type
    t1 Type
    t2
          | Just Type
    t1' <- Type -> Maybe Type
    coreView Type
    t1 = RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    t1' Type
    t2
          | Just Type
    t2' <- Type -> Maybe Type
    coreView Type
    t2 = RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    t1 Type
    t2'

        go RnEnv2
    env (TyVarTy Var
    tv1)       (TyVarTy Var
    tv2)
          = Ordering -> TypeOrdering
    liftOrdering (Ordering -> TypeOrdering) -> Ordering -> TypeOrdering
    forall a b. (a -> b) -> a -> b
    $ RnEnv2 -> Var -> Var
    rnOccL RnEnv2
    env Var
    tv1 Var -> Var -> Ordering
    `nonDetCmpVar` RnEnv2 -> Var -> Var
    rnOccR RnEnv2
    env Var
    tv2
        go RnEnv2
    env (ForAllTy (Bndr Var
    tv1 ForAllTyFlag
    vis1) Type
    t1) (ForAllTy (Bndr Var
    tv2 ForAllTyFlag
    vis2) Type
    t2)
          = Ordering -> TypeOrdering
    liftOrdering (ForAllTyFlag
    vis1 ForAllTyFlag -> ForAllTyFlag -> Ordering
    `cmpForAllVis` ForAllTyFlag
    vis2)   -- See Note [ForAllTy and type equality]
            TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env (Var -> Type
    varType Var
    tv1) (Var -> Type
    varType Var
    tv2)
            TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
    go (RnEnv2 -> Var -> Var -> RnEnv2
    rnBndr2 RnEnv2
    env Var
    tv1 Var
    tv2) Type
    t1 Type
    t2

            -- See Note [Equality on AppTys]
        go RnEnv2
    env (AppTy Type
    s1 Type
    t1) Type
    ty2
          | Just (Type
    s2, Type
    t2) <- HasDebugCallStack => Type -> Maybe (Type, Type)
    Type -> Maybe (Type, Type)
    splitAppTyNoView_maybe Type
    ty2
          = RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    s1 Type
    s2 TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    t1 Type
    t2
        go RnEnv2
    env Type
    ty1 (AppTy Type
    s2 Type
    t2)
          | Just (Type
    s1, Type
    t1) <- HasDebugCallStack => Type -> Maybe (Type, Type)
    Type -> Maybe (Type, Type)
    splitAppTyNoView_maybe Type
    ty1
          = RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    s1 Type
    s2 TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    t1 Type
    t2

        go RnEnv2
    env (FunTy FunTyFlag
    _ Type
    w1 Type
    s1 Type
    t1) (FunTy FunTyFlag
    _ Type
    w2 Type
    s2 Type
    t2)
            -- NB: nonDepCmpTypeX does the kind check requested by
            -- Note [Equality on FunTys] in GHC.Core.TyCo.Rep
          = Ordering -> TypeOrdering
    liftOrdering (RnEnv2 -> Type -> Type -> Ordering
    nonDetCmpTypeX RnEnv2
    env Type
    s1 Type
    s2 Ordering -> Ordering -> Ordering
    forall a. Semigroup a => a -> a -> a
    S.<> RnEnv2 -> Type -> Type -> Ordering
    nonDetCmpTypeX RnEnv2
    env Type
    t1 Type
    t2)
              TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    w1 Type
    w2
            -- Comparing multiplicities last because the test is usually true

        go RnEnv2
    env (TyConApp TyCon
    tc1 [Type]
    tys1) (TyConApp TyCon
    tc2 [Type]
    tys2)
          = Ordering -> TypeOrdering
    liftOrdering (TyCon
    tc1 TyCon -> TyCon -> Ordering
    `nonDetCmpTc` TyCon
    tc2) TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> [Type] -> [Type] -> TypeOrdering
    gos RnEnv2
    env [Type]
    tys1 [Type]
    tys2

        go RnEnv2
    _   (LitTy TyLit
    l1)          (LitTy TyLit
    l2)          = Ordering -> TypeOrdering
    liftOrdering (TyLit -> TyLit -> Ordering
    nonDetCmpTyLit TyLit
    l1 TyLit
    l2)
        go RnEnv2
    env (CastTy Type
    t1 KindCoercion
    _)       Type
    t2                  = TypeOrdering -> TypeOrdering
    hasCast (TypeOrdering -> TypeOrdering) -> TypeOrdering -> TypeOrdering
    forall a b. (a -> b) -> a -> b
    $ RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    t1 Type
    t2
        go RnEnv2
    env Type
    t1                  (CastTy Type
    t2 KindCoercion
    _)       = TypeOrdering -> TypeOrdering
    hasCast (TypeOrdering -> TypeOrdering) -> TypeOrdering -> TypeOrdering
    forall a b. (a -> b) -> a -> b
    $ RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    t1 Type
    t2

        go RnEnv2
    _   (CoercionTy {})     (CoercionTy {})     = TypeOrdering
    TEQ

            -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
        go RnEnv2
    _ Type
    ty1 Type
    ty2
          = Ordering -> TypeOrdering
    liftOrdering (Ordering -> TypeOrdering) -> Ordering -> TypeOrdering
    forall a b. (a -> b) -> a -> b
    $ (Type -> Int
    get_rank Type
    ty1) Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    `compare` (Type -> Int
    get_rank Type
    ty2)
          where get_rank :: Type -> Int
                get_rank :: Type -> Int
    get_rank (CastTy {})
                  = String -> SDoc -> Int
    forall a. HasCallStack => String -> SDoc -> a
    pprPanic String
    "nonDetCmpTypeX.get_rank" ([Type] -> SDoc
    forall a. Outputable a => a -> SDoc
    ppr [Type
    ty1,Type
    ty2])
                get_rank (TyVarTy {})    = Int
    0
                get_rank (CoercionTy {}) = Int
    1
                get_rank (AppTy {})      = Int
    3
                get_rank (LitTy {})      = Int
    4
                get_rank (TyConApp {})   = Int
    5
                get_rank (FunTy {})      = Int
    6
                get_rank (ForAllTy {})   = Int
    7

        gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
        gos :: RnEnv2 -> [Type] -> [Type] -> TypeOrdering
    gos RnEnv2
    _   []         []         = TypeOrdering
    TEQ
        gos RnEnv2
    _   []         [Type]
    _          = TypeOrdering
    TLT
        gos RnEnv2
    _   [Type]
    _          []         = TypeOrdering
    TGT
        gos RnEnv2
    env (Type
    ty1:[Type]
    tys1) (Type
    ty2:[Type]
    tys2) = RnEnv2 -> Type -> Type -> TypeOrdering
    go RnEnv2
    env Type
    ty1 Type
    ty2 TypeOrdering -> TypeOrdering -> TypeOrdering
    `thenCmpTy` RnEnv2 -> [Type] -> [Type] -> TypeOrdering
    gos RnEnv2
    env [Type]
    tys1 [Type]
    tys2

    -------------
    -- | Compare two 'TyCon's.
    -- See Note [nonDetCmpType nondeterminism]
    nonDetCmpTc :: TyCon -> TyCon -> Ordering
    nonDetCmpTc :: TyCon -> TyCon -> Ordering
    nonDetCmpTc TyCon
    tc1 TyCon
    tc2
      = Unique
    u1 Unique -> Unique -> Ordering
    `nonDetCmpUnique` Unique
    u2
      where
        u1 :: Unique
    u1  = TyCon -> Unique
    tyConUnique TyCon
    tc1
        u2 :: Unique
    u2  = TyCon -> Unique
    tyConUnique TyCon
    tc2

    {- *********************************************************************
    *                                                                      *
                      mayLookIdentical
    *                                                                      *
    ********************************************************************* -}

    mayLookIdentical :: Type -> Type -> Bool
    -- | Returns True if the /visible/ part of the types
    -- might look equal, even if they are really unequal (in the invisible bits)
    --
    -- This function is very similar to tc_eq_type but it is much more
    -- heuristic.  Notably, it is always safe to return True, even with types
    -- that might (in truth) be unequal  -- this affects error messages only
    -- (Originally this test was done by eqType with an extra flag, but the result
    --  was hard to understand.)
    mayLookIdentical :: Type -> Type -> Bool
    mayLookIdentical Type
    orig_ty1 Type
    orig_ty2
      = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    orig_env Type
    orig_ty1 Type
    orig_ty2
      where
        orig_env :: RnEnv2
    orig_env = InScopeSet -> RnEnv2
    mkRnEnv2 (InScopeSet -> RnEnv2) -> InScopeSet -> RnEnv2
    forall a b. (a -> b) -> a -> b
    $ VarSet -> InScopeSet
    mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
    forall a b. (a -> b) -> a -> b
    $ [Type] -> VarSet
    tyCoVarsOfTypes [Type
    orig_ty1, Type
    orig_ty2]

        go :: RnEnv2 -> Type -> Type -> Bool

        go :: RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env (TyConApp TyCon
    tc1 [Type]
    ts1) (TyConApp TyCon
    tc2 [Type]
    ts2)
          | TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2, Bool -> Bool
    not (TyCon -> Bool
    isForgetfulSynTyCon TyCon
    tc1) -- See Note [Comparing type synonyms]
          = RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
    gos RnEnv2
    env (TyCon -> [TyConBinder]
    tyConBinders TyCon
    tc1) [Type]
    ts1 [Type]
    ts2

        go RnEnv2
    env Type
    t1 Type
    t2 | Just Type
    t1' <- Type -> Maybe Type
    coreView Type
    t1 = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1' Type
    t2
        go RnEnv2
    env Type
    t1 Type
    t2 | Just Type
    t2' <- Type -> Maybe Type
    coreView Type
    t2 = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1 Type
    t2'

        go RnEnv2
    env (TyVarTy Var
    tv1)   (TyVarTy Var
    tv2)   = RnEnv2 -> Var -> Var
    rnOccL RnEnv2
    env Var
    tv1 Var -> Var -> Bool
    forall a. Eq a => a -> a -> Bool
    == RnEnv2 -> Var -> Var
    rnOccR RnEnv2
    env Var
    tv2
        go RnEnv2
    _   (LitTy TyLit
    lit1)    (LitTy TyLit
    lit2)    = TyLit
    lit1 TyLit -> TyLit -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyLit
    lit2
        go RnEnv2
    env (CastTy Type
    t1 KindCoercion
    _)   Type
    t2              = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1 Type
    t2
        go RnEnv2
    env Type
    t1              (CastTy Type
    t2 KindCoercion
    _)   = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1 Type
    t2
        go RnEnv2
    _   (CoercionTy {}) (CoercionTy {}) = Bool
    True

        go RnEnv2
    env (ForAllTy (Bndr Var
    tv1 ForAllTyFlag
    vis1) Type
    ty1)
               (ForAllTy (Bndr Var
    tv2 ForAllTyFlag
    vis2) Type
    ty2)
          =  ForAllTyFlag
    vis1 ForAllTyFlag -> ForAllTyFlag -> Bool
    `eqForAllVis` ForAllTyFlag
    vis2  -- See Note [ForAllTy and type equality]
          Bool -> Bool -> Bool
    && RnEnv2 -> Type -> Type -> Bool
    go (RnEnv2 -> Var -> Var -> RnEnv2
    rnBndr2 RnEnv2
    env Var
    tv1 Var
    tv2) Type
    ty1 Type
    ty2
             -- Visible stuff only: ignore kinds of binders

        -- If we have (forall (r::RunTimeRep). ty1  ~   blah) then respond
        -- with True.  Reason: the type pretty-printer defaults RuntimeRep
        -- foralls (see Ghc.Iface.Type.hideNonStandardTypes).  That can make,
        -- say (forall r. TYPE r -> Type) into (Type -> Type), so it looks the
        -- same as a very different type (#24553).  By responding True, we
        -- tell GHC (see calls of mayLookIdentical) to display without defaulting.
        -- See Note [Showing invisible bits of types in error messages]
        -- in GHC.Tc.Errors.Ppr
        go RnEnv2
    _ (ForAllTy VarBndr Var ForAllTyFlag
    b Type
    _) Type
    _ | VarBndr Var ForAllTyFlag -> Bool
    isDefaultableBndr VarBndr Var ForAllTyFlag
    b = Bool
    True
        go RnEnv2
    _ Type
    _ (ForAllTy VarBndr Var ForAllTyFlag
    b Type
    _) | VarBndr Var ForAllTyFlag -> Bool
    isDefaultableBndr VarBndr Var ForAllTyFlag
    b = Bool
    True

        go RnEnv2
    env (FunTy FunTyFlag
    _ Type
    w1 Type
    arg1 Type
    res1) (FunTy FunTyFlag
    _ Type
    w2 Type
    arg2 Type
    res2)
          = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    arg1 Type
    arg2 Bool -> Bool -> Bool
    && RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    res1 Type
    res2 Bool -> Bool -> Bool
    && RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    w1 Type
    w2
            -- Visible stuff only: ignore agg kinds

          -- See Note [Equality on AppTys] in GHC.Core.Type
        go RnEnv2
    env (AppTy Type
    s1 Type
    t1) Type
    ty2
          | Just (Type
    s2, Type
    t2) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty2
          = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    s1 Type
    s2 Bool -> Bool -> Bool
    && RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1 Type
    t2
        go RnEnv2
    env Type
    ty1 (AppTy Type
    s2 Type
    t2)
          | Just (Type
    s1, Type
    t1) <- Type -> Maybe (Type, Type)
    tcSplitAppTyNoView_maybe Type
    ty1
          = RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    s1 Type
    s2 Bool -> Bool -> Bool
    && RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1 Type
    t2

        go RnEnv2
    env (TyConApp TyCon
    tc1 [Type]
    ts1)   (TyConApp TyCon
    tc2 [Type]
    ts2)
          = TyCon
    tc1 TyCon -> TyCon -> Bool
    forall a. Eq a => a -> a -> Bool
    == TyCon
    tc2 Bool -> Bool -> Bool
    && RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
    gos RnEnv2
    env (TyCon -> [TyConBinder]
    tyConBinders TyCon
    tc1) [Type]
    ts1 [Type]
    ts2

        go RnEnv2
    _ Type
    _ Type
    _ = Bool
    False

        gos :: RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
        gos :: RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
    gos RnEnv2
    _   [TyConBinder]
    _         []       []      = Bool
    True
        gos RnEnv2
    env [TyConBinder]
    bs (Type
    t1:[Type]
    ts1) (Type
    t2:[Type]
    ts2)
          | (Bool
    invisible, [TyConBinder]
    bs') <- case [TyConBinder]
    bs of
                                   []     -> (Bool
    False,                    [])
                                   (TyConBinder
    b:[TyConBinder]
    bs) -> (TyConBinder -> Bool
    forall tv. VarBndr tv TyConBndrVis -> Bool
    isInvisibleTyConBinder TyConBinder
    b, [TyConBinder]
    bs)
          = (Bool
    invisible Bool -> Bool -> Bool
    || RnEnv2 -> Type -> Type -> Bool
    go RnEnv2
    env Type
    t1 Type
    t2) Bool -> Bool -> Bool
    && RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
    gos RnEnv2
    env [TyConBinder]
    bs' [Type]
    ts1 [Type]
    ts2

        gos RnEnv2
    _ [TyConBinder]
    _ [Type]
    _ [Type]
    _ = Bool
    False

    isDefaultableBndr :: ForAllTyBinder -> Bool
    -- This function should line up with the defaulting done
    --   by GHC.Iface.Type.defaultIfaceTyVarsOfKind
    -- See Note [Showing invisible bits of types in error messages]
    --   in GHC.Tc.Errors.Ppr
    isDefaultableBndr :: VarBndr Var ForAllTyFlag -> Bool
    isDefaultableBndr (Bndr Var
    tv ForAllTyFlag
    vis)
      = ForAllTyFlag -> Bool
    isInvisibleForAllTyFlag ForAllTyFlag
    vis Bool -> Bool -> Bool
    && Type -> Bool
    is_defaultable (Var -> Type
    tyVarKind Var
    tv)
      where
        is_defaultable :: Type -> Bool
    is_defaultable Type
    ki = Type -> Bool
    isLevityTy Type
    ki Bool -> Bool -> Bool
    || Type -> Bool
    isRuntimeRepTy Type
    ki  Bool -> Bool -> Bool
    || Type -> Bool
    isMultiplicityTy Type
    ki