-- (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 comparison
    eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
    nonDetCmpTypesX, nonDetCmpTc,
    eqVarBndrs,

    pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, tcEqTypeVis,
    tcEqTyConApps,

   -- * Visiblity comparision
   eqForAllVis, cmpForAllVis

   ) where

import GHC.Prelude

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

import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCon

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

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
*                                                                      *
********************************************************************* -}

{- 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 [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%.
-}


tcEqKind :: HasDebugCallStack => Kind -> Kind -> Bool
tcEqKind :: (() :: Constraint) => Type -> Type -> Bool
tcEqKind = (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
tcEqType

tcEqType :: HasDebugCallStack => Type -> Type -> Bool
-- ^ tcEqType implements typechecker equality
-- It behaves just like eqType, but is implemented
-- differently (for now)
tcEqType :: (() :: Constraint) => Type -> Type -> Bool
tcEqType Type
ty1 Type
ty2
  =  Type -> Type -> Bool
tcEqTypeNoSyns Type
ki1 Type
ki2
  Bool -> Bool -> Bool
&& Type -> Type -> Bool
tcEqTypeNoSyns Type
ty1 Type
ty2
  where
    ki1 :: Type
ki1 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty1
    ki2 :: Type
ki2 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty2

-- | 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
ty1 Type
ty2
  = Type -> Type -> Bool
tcEqTypeNoSyns Type
ty1 Type
ty2

-- | 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

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

To this end we place an INLINE on tc_eq_type, ensuring that it is inlined into
its publicly-visible interfaces (e.g. tcEqType). In addition to eliminating
some dynamic branches, this allows the simplifier to eliminate the closure
allocations that would otherwise be necessary to capture the two boolean "mode"
flags. This reduces allocations by a good fraction of a percent when compiling
Cabal.

See #19226.
-}

-- | Type equality comparing both visible and invisible arguments and expanding
-- type synonyms.
tcEqTypeNoSyns :: Type -> Type -> Bool
tcEqTypeNoSyns :: Type -> Type -> Bool
tcEqTypeNoSyns Type
ta Type
tb = Bool -> Bool -> Type -> Type -> Bool
tc_eq_type Bool
False Bool
False Type
ta Type
tb

-- | Like 'tcEqType', but returns True if the /visible/ part of the types
-- are equal, even if they are really unequal (in the invisible bits)
tcEqTypeVis :: Type -> Type -> Bool
tcEqTypeVis :: Type -> Type -> Bool
tcEqTypeVis Type
ty1 Type
ty2 = Bool -> Bool -> Type -> Type -> Bool
tc_eq_type Bool
False Bool
True Type
ty1 Type
ty2

-- | 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
ty1 Type
ty2 = Bool -> Bool -> Type -> Type -> Bool
tc_eq_type Bool
True Bool
False Type
ty1 Type
ty2

-- | Real worker for 'tcEqType'. No kind check!
tc_eq_type :: Bool          -- ^ True <=> do not expand type synonyms
           -> Bool          -- ^ True <=> compare visible args only
           -> Type -> Type
           -> Bool
-- Flags False, False is the usual setting for tc_eq_type
-- See Note [Computing equality on types] in Type
tc_eq_type :: Bool -> Bool -> Type -> Type -> Bool
tc_eq_type Bool
keep_syns Bool
vis_only Type
orig_ty1 Type
orig_ty2
  = RnEnv2 -> Type -> Type -> Bool
go RnEnv2
orig_env Type
orig_ty1 Type
orig_ty2
  where
    go :: RnEnv2 -> Type -> Type -> Bool
    -- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
    go :: RnEnv2 -> Type -> Type -> Bool
go RnEnv2
_   (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
      | TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
      = Bool
True

    go RnEnv2
env Type
t1 Type
t2 | Bool -> Bool
not Bool
keep_syns, 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 | Bool -> Bool
not Bool
keep_syns, 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 (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
&& (Bool
vis_only Bool -> Bool -> Bool
|| RnEnv2 -> Type -> Type -> Bool
go RnEnv2
env (Var -> Type
varType Var
tv1) (Var -> Type
varType Var
tv2))
      Bool -> Bool -> Bool
&& RnEnv2 -> Type -> Type -> Bool
go (RnEnv2 -> Var -> Var -> RnEnv2
rnBndr2 RnEnv2
env Var
tv1 Var
tv2) Type
ty1 Type
ty2

    -- 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
    go RnEnv2
env (FunTy FunTyFlag
_ Type
w1 Type
arg1 Type
res1) (FunTy FunTyFlag
_ Type
w2 Type
arg2 Type
res2)
      = Bool
kinds_eq Bool -> Bool -> Bool
&& 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
      where
        kinds_eq :: Bool
kinds_eq | Bool
vis_only  = Bool
True
                 | Bool
otherwise = RnEnv2 -> Type -> Type -> Bool
go RnEnv2
env ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
arg1) ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
arg2) Bool -> Bool -> Bool
&&
                               RnEnv2 -> Type -> Type -> Bool
go RnEnv2
env ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
res1) ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
res2)

      -- 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 -> [Bool] -> [Type] -> [Type] -> Bool
gos RnEnv2
env (TyCon -> [Bool]
tc_vis TyCon
tc1) [Type]
ts1 [Type]
ts2

    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
_ Type
_ Type
_ = Bool
False

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

    tc_vis :: TyCon -> [Bool]  -- True for the fields we should ignore
    tc_vis :: TyCon -> [Bool]
tc_vis TyCon
tc | Bool
vis_only  = [Bool]
inviss [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False    -- Ignore invisibles
              | Bool
otherwise = Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False              -- Ignore nothing
       -- The repeat False is necessary because tycons
       -- can legitimately be oversaturated
      where
        bndrs :: [TyConBinder]
bndrs = TyCon -> [TyConBinder]
tyConBinders TyCon
tc
        inviss :: [Bool]
inviss  = (TyConBinder -> Bool) -> [TyConBinder] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TyConBinder -> Bool
forall tv. VarBndr tv TyConBndrVis -> Bool
isInvisibleTyConBinder [TyConBinder]
bndrs

    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]

{-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].


-- | 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
        (We don't use instances so that we know where it happens)
*                                                                      *
************************************************************************

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 nullary type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the task of testing equality between two 'Type's of the form

  TyConApp tc []

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; it is
much better to rather compare the TyCons directly. Consequently, before
expanding type synonyms in type comparisons we first look for a nullary
TyConApp and simply compare the TyCons if we find one. 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.

We perform this optimisation in a number of places:

 * GHC.Core.Types.eqType
 * GHC.Core.Types.nonDetCmpType
 * GHC.Core.Unify.unify_ty
 * GHC.Tc.Solver.Equality.can_eq_nc'
 * TcUnify.uType

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.

-}

eqType :: Type -> Type -> Bool
-- ^ Type equality on source types. Does not look through @newtypes@,
-- 'PredType's or type families, but it does look through type synonyms.
-- This first checks that the kinds of the types are equal and then
-- checks whether the types are equal, ignoring casts and coercions.
-- (The kind check is a recursive call, but since all kinds have type
-- @Type@, there is no need to check the types of kinds.)
-- See also Note [Non-trivial definitional equality] in "GHC.Core.TyCo.Rep".
eqType :: Type -> Type -> Bool
eqType Type
t1 Type
t2 = Ordering -> Bool
isEqual (Ordering -> Bool) -> Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Ordering
nonDetCmpType Type
t1 Type
t2
  -- It's OK to use nonDetCmpType here and eqType is deterministic,
  -- nonDetCmpType does equality deterministically

-- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
eqTypeX :: RnEnv2 -> Type -> Type -> Bool
eqTypeX :: RnEnv2 -> Type -> Type -> Bool
eqTypeX RnEnv2
env Type
t1 Type
t2 = Ordering -> Bool
isEqual (Ordering -> Bool) -> Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
t1 Type
t2
  -- It's OK to use nonDetCmpType here and eqTypeX is deterministic,
  -- nonDetCmpTypeX does equality deterministically

-- | Type equality on lists of types, looking through type synonyms
-- but not newtypes.
eqTypes :: [Type] -> [Type] -> Bool
eqTypes :: [Type] -> [Type] -> Bool
eqTypes [Type]
tys1 [Type]
tys2 = Ordering -> Bool
isEqual (Ordering -> Bool) -> Ordering -> Bool
forall a b. (a -> b) -> a -> b
$ [Type] -> [Type] -> Ordering
nonDetCmpTypes [Type]
tys1 [Type]
tys2
  -- It's OK to use nonDetCmpType here and eqTypes is deterministic,
  -- nonDetCmpTypes does equality deterministically

eqVarBndrs :: 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 :: 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)
 | RnEnv2 -> Type -> Type -> Bool
eqTypeX RnEnv2
env (Var -> Type
varType Var
tv1) (Var -> Type
varType Var
tv2)
 = 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

-- 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
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]))
{-# INLINE nonDetCmpType #-}

nonDetCmpTypes :: [Type] -> [Type] -> Ordering
nonDetCmpTypes :: [Type] -> [Type] -> Ordering
nonDetCmpTypes [Type]
ts1 [Type]
ts2 = RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX RnEnv2
rn_env [Type]
ts1 [Type]
ts2
  where
    rn_env :: RnEnv2
rn_env = InScopeSet -> RnEnv2
mkRnEnv2 (VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
tyCoVarsOfTypes ([Type]
ts1 [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
ts2)))

-- | 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]
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 = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
orig_t1
    k2 :: Type
k2 = (() :: Constraint) => 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
    -- See Note [Comparing nullary type synonyms].
    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
    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) <- (() :: Constraint) => 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) <- (() :: Constraint) => 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

-------------
nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX RnEnv2
_   []        []        = Ordering
EQ
nonDetCmpTypesX RnEnv2
env (Type
t1:[Type]
tys1) (Type
t2:[Type]
tys2) = RnEnv2 -> Type -> Type -> Ordering
nonDetCmpTypeX RnEnv2
env Type
t1 Type
t2 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
S.<>
                                          RnEnv2 -> [Type] -> [Type] -> Ordering
nonDetCmpTypesX RnEnv2
env [Type]
tys1 [Type]
tys2
nonDetCmpTypesX RnEnv2
_   []        [Type]
_         = Ordering
LT
nonDetCmpTypesX RnEnv2
_   [Type]
_         []        = Ordering
GT

-------------
-- | 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