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

{-# LANGUAGE DerivingStrategies #-}
{-# 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, tcEqTyConAppArgs,

    -- ** Dealing with invisible bits in types
    mayLookIdentical, pprWithInvisibleBits,
    InvisibleBit(..), InvisibleBits,

    -- * 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 {-# SOURCE #-} GHC.Tc.Utils.TcType (isMetaTyVar)

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

import GHC.Base (reallyUnsafePtrEquality#)

import Control.Monad ( unless )
import Control.Monad.Trans.Writer.CPS ( Writer )
import qualified Control.Monad.Trans.Writer.CPS as Writer
import qualified Data.Semigroup as S
import Data.Set ( Set )
import qualified Data.Set as Set

{- 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
&& [Type] -> [Type] -> Bool
tcEqTyConAppArgs [Type]
args1 [Type]
args2

tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
-- Args do not have to have equal length;
-- we discard the excess of the longer one
tcEqTyConAppArgs :: [Type] -> [Type] -> Bool
tcEqTyConAppArgs [Type]
args1 [Type]
args2
  = [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
*                                                                      *
********************************************************************* -}

-- | Something in a type which might be invisible.
--
-- Used to avoid reporting confusing errors to the user, like:
--
-- > Couldn't match (a -> b) with (a -> b)
--
-- When in fact it is e.g. (a %1 -> b) vs (a %Many -> b), but the multiplicites
-- have been suppressed.
--
-- See Note [Showing invisible bits of types in error messages] in GHC.Tc.Errors.Ppr.
data InvisibleBit
  = InvisibleKind
  | InvisibleRuntimeRep
  | InvisibleMultiplicity
  deriving stock (InvisibleBit -> InvisibleBit -> Bool
(InvisibleBit -> InvisibleBit -> Bool)
-> (InvisibleBit -> InvisibleBit -> Bool) -> Eq InvisibleBit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InvisibleBit -> InvisibleBit -> Bool
== :: InvisibleBit -> InvisibleBit -> Bool
$c/= :: InvisibleBit -> InvisibleBit -> Bool
/= :: InvisibleBit -> InvisibleBit -> Bool
Eq, Eq InvisibleBit
Eq InvisibleBit =>
(InvisibleBit -> InvisibleBit -> Ordering)
-> (InvisibleBit -> InvisibleBit -> Bool)
-> (InvisibleBit -> InvisibleBit -> Bool)
-> (InvisibleBit -> InvisibleBit -> Bool)
-> (InvisibleBit -> InvisibleBit -> Bool)
-> (InvisibleBit -> InvisibleBit -> InvisibleBit)
-> (InvisibleBit -> InvisibleBit -> InvisibleBit)
-> Ord InvisibleBit
InvisibleBit -> InvisibleBit -> Bool
InvisibleBit -> InvisibleBit -> Ordering
InvisibleBit -> InvisibleBit -> InvisibleBit
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 :: InvisibleBit -> InvisibleBit -> Ordering
compare :: InvisibleBit -> InvisibleBit -> Ordering
$c< :: InvisibleBit -> InvisibleBit -> Bool
< :: InvisibleBit -> InvisibleBit -> Bool
$c<= :: InvisibleBit -> InvisibleBit -> Bool
<= :: InvisibleBit -> InvisibleBit -> Bool
$c> :: InvisibleBit -> InvisibleBit -> Bool
> :: InvisibleBit -> InvisibleBit -> Bool
$c>= :: InvisibleBit -> InvisibleBit -> Bool
>= :: InvisibleBit -> InvisibleBit -> Bool
$cmax :: InvisibleBit -> InvisibleBit -> InvisibleBit
max :: InvisibleBit -> InvisibleBit -> InvisibleBit
$cmin :: InvisibleBit -> InvisibleBit -> InvisibleBit
min :: InvisibleBit -> InvisibleBit -> InvisibleBit
Ord, Int -> InvisibleBit -> ShowS
[InvisibleBit] -> ShowS
InvisibleBit -> String
(Int -> InvisibleBit -> ShowS)
-> (InvisibleBit -> String)
-> ([InvisibleBit] -> ShowS)
-> Show InvisibleBit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InvisibleBit -> ShowS
showsPrec :: Int -> InvisibleBit -> ShowS
$cshow :: InvisibleBit -> String
show :: InvisibleBit -> String
$cshowList :: [InvisibleBit] -> ShowS
showList :: [InvisibleBit] -> ShowS
Show)
instance Outputable InvisibleBit where
  ppr :: InvisibleBit -> SDoc
ppr InvisibleBit
thing = String -> SDoc
forall doc. IsLine doc => String -> doc
text (InvisibleBit -> String
forall a. Show a => a -> String
show InvisibleBit
thing)

-- | A collection of 'InvisibleBit's.
type InvisibleBits = Set InvisibleBit

-- | Make the sure the given invisible bits are displayed.
--
-- See Note [Showing invisible bits of types in error messages] in GHC.Tc.Errors.Ppr.
pprWithInvisibleBits :: Set InvisibleBit -> SDoc -> SDoc
pprWithInvisibleBits :: InvisibleBits -> SDoc -> SDoc
pprWithInvisibleBits InvisibleBits
invis_bits
  = (SDocContext -> SDocContext) -> SDoc -> SDoc
updSDocContext ((SDocContext -> SDocContext) -> SDoc -> SDoc)
-> (SDocContext -> SDocContext) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ \SDocContext
ctx ->
      SDocContext
ctx { sdocPrintExplicitKinds
              = show_kinds || sdocPrintExplicitKinds ctx
          , sdocPrintExplicitRuntimeReps
              = show_reps  || sdocPrintExplicitRuntimeReps ctx
          , sdocLinearTypes
              = show_mults || sdocLinearTypes ctx
  -- Question: what about 'sdocPrintExplicitCoercions'?
  -- Currently, we never enable that automatically; it's always up to the user
  -- to enable it.
          }
  where
    show_kinds :: Bool
show_kinds = InvisibleBit
InvisibleKind         InvisibleBit -> InvisibleBits -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` InvisibleBits
invis_bits
    show_reps :: Bool
show_reps  = InvisibleBit
InvisibleRuntimeRep   InvisibleBit -> InvisibleBits -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` InvisibleBits
invis_bits
    show_mults :: Bool
show_mults = InvisibleBit
InvisibleMultiplicity InvisibleBit -> InvisibleBits -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` InvisibleBits
invis_bits

mayLookIdentical :: Type -> Type -> InvisibleBits
-- | 'mayLookIdentical' returns:
--
--  - An empty set if the two types are distinct unequal, and remain distinct
--    even if we hide explicit kinds, runtime-reps, multiplicities.
--  - A non-empty set of 'invis_bits', if the two types might look equal, but
--    are in fact distinct in the returned 'invis_bits'.
--
-- See Note [mayLookIdentical], as well as
-- Note [Showing invisible bits of types in error messages] in GHC.Tc.Errors.Ppr.
mayLookIdentical :: Type -> Type -> InvisibleBits
mayLookIdentical Type
orig_ty1 Type
orig_ty2
  = case Writer InvisibleBits Bool -> (Bool, InvisibleBits)
forall w a. Monoid w => Writer w a -> (a, w)
Writer.runWriter (Writer InvisibleBits Bool -> (Bool, InvisibleBits))
-> Writer InvisibleBits Bool -> (Bool, InvisibleBits)
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
orig_env Bool
True Type
orig_ty1 Type
orig_ty2 of
      (Bool
eq, InvisibleBits
invis_things) ->
        if Bool
eq
        then InvisibleBits
invis_things
        else InvisibleBits
forall a. Set a
Set.empty
  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]

    tell_on_mismatch :: InvisibleBit -> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
    tell_on_mismatch :: InvisibleBit
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
tell_on_mismatch InvisibleBit
what Writer InvisibleBits Bool
inner
      = do { let (Bool
inner_vis_ok, InvisibleBits
inner_invis) = Writer InvisibleBits Bool -> (Bool, InvisibleBits)
forall w a. Monoid w => Writer w a -> (a, w)
Writer.runWriter Writer InvisibleBits Bool
inner
                 ok :: Bool
ok = Bool
inner_vis_ok Bool -> Bool -> Bool
&& InvisibleBits -> Bool
forall a. Set a -> Bool
Set.null InvisibleBits
inner_invis
           ; Bool
-> WriterT InvisibleBits Identity ()
-> WriterT InvisibleBits Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ok (WriterT InvisibleBits Identity ()
 -> WriterT InvisibleBits Identity ())
-> WriterT InvisibleBits Identity ()
-> WriterT InvisibleBits Identity ()
forall a b. (a -> b) -> a -> b
$
               InvisibleBits -> WriterT InvisibleBits Identity ()
forall w (m :: * -> *). (Monoid w, Monad m) => w -> WriterT w m ()
Writer.tell (InvisibleBits -> WriterT InvisibleBits Identity ())
-> InvisibleBits -> WriterT InvisibleBits Identity ()
forall a b. (a -> b) -> a -> b
$
                 if Bool
inner_vis_ok
                 then -- If the inner mismatch is invisible,
                      -- we need to print those invisible bits as well.
                      --
                      -- See Note [mayLookIdentical]
                      InvisibleBit -> InvisibleBits -> InvisibleBits
forall a. Ord a => a -> Set a -> Set a
Set.insert InvisibleBit
what InvisibleBits
inner_invis
                 else InvisibleBit -> InvisibleBits
forall a. a -> Set a
Set.singleton InvisibleBit
what
           ; Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ok
           }

    -- See Note [mayLookIdentical]
    go :: RnEnv2
       -> Bool -- are we at the top-level? used only for Wrinkle [MetaTv mismatch at top-level only]
       -> Type -- lhs type
       -> Type -- rhs type
       -> Writer InvisibleBits Bool
        -- True  <=> types might be visibly equal
        -- False <=> types are definitely not visibly equal
        -- Invisible bits: the invisible bits in which the types differ (if any)
    go :: RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
_top (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] -> Writer InvisibleBits Bool
gos RnEnv2
env (TyCon -> [TyConBinder]
tyConBinders TyCon
tc1) [Type]
ts1 [Type]
ts2

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

    go RnEnv2
env Bool
_top (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
      = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    go RnEnv2
env Bool
top (TyVarTy Var
tv) Type
ty
      | Var -> Bool
isDefaultableTyVar Var
tv
      -- See Note [Defaultable tyvars in mayLookIdentical]
      = Var -> Writer InvisibleBits Bool
discard_defaultable_tyvar Var
tv
      | Var -> Bool
isMetaTyVar Var
tv
      -- See Note [Metavariables in mayLookIdentical]
      = if Bool -> Bool
not Bool
top -- Wrinkle [MetaTv mismatch at top-level only]
        then Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        else
          do { kind_ok <- InvisibleBit
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
tell_on_mismatch InvisibleBit
InvisibleKind (Writer InvisibleBits Bool -> Writer InvisibleBits Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False (Var -> Type
tyVarKind Var
tv) (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty)
             ; return $ not kind_ok }
    go RnEnv2
env Bool
top Type
ty (TyVarTy Var
tv)
      | Var -> Bool
isDefaultableTyVar Var
tv
      -- See Note [Defaultable tyvars in mayLookIdentical]
      = Var -> Writer InvisibleBits Bool
discard_defaultable_tyvar Var
tv
      | Var -> Bool
isMetaTyVar Var
tv
      -- See Note [Metavariables in mayLookIdentical]
      = if Bool -> Bool
not Bool
top -- Wrinkle [MetaTv mismatch at top-level only]
        then Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        else
          do { kind_ok <- InvisibleBit
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
tell_on_mismatch InvisibleBit
InvisibleKind (Writer InvisibleBits Bool -> Writer InvisibleBits Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty) (Var -> Type
tyVarKind Var
tv)
             ; return $ not kind_ok }
    go RnEnv2
_ Bool
_ (TyVarTy {}) (TyVarTy {}) = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    go RnEnv2
_   Bool
_   (LitTy TyLit
lit1)    (LitTy TyLit
lit2)    = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Writer InvisibleBits Bool)
-> Bool -> Writer InvisibleBits Bool
forall a b. (a -> b) -> a -> b
$ TyLit
lit1 TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
lit2
    go RnEnv2
top Bool
vis (CastTy Type
t1 KindCoercion
_)   Type
t2              = RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
top Bool
vis Type
t1 Type
t2
    go RnEnv2
top Bool
vis Type
t1              (CastTy Type
t2 KindCoercion
_)   = RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
top Bool
vis Type
t1 Type
t2
    go RnEnv2
_   Bool
_   (CoercionTy {}) (CoercionTy {}) = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

    go RnEnv2
env Bool
_top (ForAllTy (Bndr Var
tv1 ForAllTyFlag
vis1) Type
ty1)
                (ForAllTy (Bndr Var
tv2 ForAllTyFlag
vis2) Type
ty2)
      = if ForAllTyFlag
vis1 ForAllTyFlag -> ForAllTyFlag -> Bool
`eqForAllVis` ForAllTyFlag
vis2  -- See Note [ForAllTy and type equality]
        then do { _kind_ok <- InvisibleBit
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
tell_on_mismatch InvisibleBit
InvisibleKind (Writer InvisibleBits Bool -> Writer InvisibleBits Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False (Var -> Type
tyVarKind Var
tv1) (Var -> Type
tyVarKind Var
tv2)
                ; go (rnBndr2 env tv1 tv2) False ty1 ty2 }
        else Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    -- See Note [Defaultable tyvars in mayLookIdentical]
    go RnEnv2
_ Bool
_ (ForAllTy b :: VarBndr Var ForAllTyFlag
b@(Bndr Var
tv ForAllTyFlag
_) Type
_) Type
_ | VarBndr Var ForAllTyFlag -> Bool
isDefaultableBndr VarBndr Var ForAllTyFlag
b = Var -> Writer InvisibleBits Bool
discard_defaultable_tyvar Var
tv
    go RnEnv2
_ Bool
_ Type
_ (ForAllTy b :: VarBndr Var ForAllTyFlag
b@(Bndr Var
tv ForAllTyFlag
_) Type
_) | VarBndr Var ForAllTyFlag -> Bool
isDefaultableBndr VarBndr Var ForAllTyFlag
b = Var -> Writer InvisibleBits Bool
discard_defaultable_tyvar Var
tv

    go RnEnv2
env Bool
_top (FunTy FunTyFlag
_ Type
w1 Type
arg1 Type
res1) (FunTy FunTyFlag
_ Type
w2 Type
arg2 Type
res2)
      = do { _mult_ok <- InvisibleBit
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
tell_on_mismatch InvisibleBit
InvisibleMultiplicity (Writer InvisibleBits Bool -> Writer InvisibleBits Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
w1 Type
w2
           ; _reps_ok <- tell_on_mismatch InvisibleRuntimeRep $
               (&&) <$> go env False (typeKind arg1) (typeKind arg2)
                    <*> go env False (typeKind res1) (typeKind res2)
           ; (&&) <$> go env False arg1 arg2 <*> go env False res1 res2 }

      -- See Note [Equality on AppTys] in GHC.Core.Type
    go RnEnv2
env Bool
_top (AppTy Type
s1 Type
t1) Type
ty2
      | Just (Type
s2, Type
t2) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty2
      = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> Writer InvisibleBits Bool
-> WriterT InvisibleBits Identity (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
s1 Type
s2 WriterT InvisibleBits Identity (Bool -> Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b.
WriterT InvisibleBits Identity (a -> b)
-> WriterT InvisibleBits Identity a
-> WriterT InvisibleBits Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
t1 Type
t2
    go RnEnv2
env Bool
_top Type
ty1 (AppTy Type
s2 Type
t2)
      | Just (Type
s1, Type
t1) <- Type -> Maybe (Type, Type)
tcSplitAppTyNoView_maybe Type
ty1
      = Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> Writer InvisibleBits Bool
-> WriterT InvisibleBits Identity (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
s1 Type
s2 WriterT InvisibleBits Identity (Bool -> Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b.
WriterT InvisibleBits Identity (a -> b)
-> WriterT InvisibleBits Identity a
-> WriterT InvisibleBits Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
t1 Type
t2

    go RnEnv2
_ Bool
_ Type
_ Type
_ = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    discard_defaultable_tyvar :: TyVar -> Writer InvisibleBits Bool
    discard_defaultable_tyvar :: Var -> Writer InvisibleBits Bool
discard_defaultable_tyvar Var
tv =
      do { let what :: InvisibleBit
what =
                 if Type -> Bool
isMultiplicityTy (Var -> Type
tyVarKind Var
tv)
                 then InvisibleBit
InvisibleMultiplicity
                 else InvisibleBit
InvisibleRuntimeRep
        ; InvisibleBits -> WriterT InvisibleBits Identity ()
forall w (m :: * -> *). (Monoid w, Monad m) => w -> WriterT w m ()
Writer.tell (InvisibleBits -> WriterT InvisibleBits Identity ())
-> InvisibleBits -> WriterT InvisibleBits Identity ()
forall a b. (a -> b) -> a -> b
$ InvisibleBit -> InvisibleBits
forall a. a -> Set a
Set.singleton InvisibleBit
what
        ; Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True }

    gos :: RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Writer InvisibleBits Bool
    gos :: RnEnv2
-> [TyConBinder] -> [Type] -> [Type] -> Writer InvisibleBits Bool
gos RnEnv2
_   [TyConBinder]
_  []       []      = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return 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)
      = if Bool
invisible
        then do { _kind_ok <- InvisibleBit
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
tell_on_mismatch InvisibleBit
InvisibleKind (Writer InvisibleBits Bool -> Writer InvisibleBits Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b. (a -> b) -> a -> b
$ RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
t1 Type
t2
                ; gos env bs' ts1 ts2 }
        else do { Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> Writer InvisibleBits Bool
-> WriterT InvisibleBits Identity (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RnEnv2 -> Bool -> Type -> Type -> Writer InvisibleBits Bool
go RnEnv2
env Bool
False Type
t1 Type
t2 WriterT InvisibleBits Identity (Bool -> Bool)
-> Writer InvisibleBits Bool -> Writer InvisibleBits Bool
forall a b.
WriterT InvisibleBits Identity (a -> b)
-> WriterT InvisibleBits Identity a
-> WriterT InvisibleBits Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RnEnv2
-> [TyConBinder] -> [Type] -> [Type] -> Writer InvisibleBits Bool
gos RnEnv2
env [TyConBinder]
bs' [Type]
ts1 [Type]
ts2 }

    gos RnEnv2
_ [TyConBinder]
_ [Type]
_ [Type]
_ = Bool -> Writer InvisibleBits Bool
forall a. a -> WriterT InvisibleBits Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

{- Note [mayLookIdentical]
~~~~~~~~~~~~~~~~~~~~~~~~~~
As described in Note [Showing invisible bits of types in error messages]
in GHC.Tc.Errors.Ppr, the job of 'mayLookIdentical' is to compute whether two
types that are not equal may in fact look identical when pretty-printed to the
user, due to the hiding of explicit kinds, runtime-reps or multiplicities.

'mayLookIdentical' can return:

  - an empty set:
      The types definitely don't look identical, even if we hide all
      RuntimeReps, kinds, multiplicities, etc.

  - a non-empty set of invis_bits:
      The types may look identical to the user, so please don't hide 'invis_bits'
      when pretty-printing them.

Note that 'mayLookIdentical' is conservative: it can sometimes return a non-empty
result when in fact the types might not look identical, even after hiding all the
invisible bits. That's OK: all that happens is that we show a bit of extra
clutter; better that than occasionally displaying very confusing error messages.

To compute which invisible bits should be shown, the main worker function 'go'
walks through the two input types in parallel, accumulating a set of 'InvisBits'
in the Writer monad.

  - If the two types are definitely visibly unequal, 'go' returns 'False'.
  - If the two types might be visibly equal, it returns 'True'.
    Sometimes 'go' can return 'True' even when the types aren't really visibly
    equal, e.g. because of Note [Defaultable tyvars in mayLookIdentical].
    That's OK; all that means is that we will sometimes unnecessarily switch
    on some explicit pretty-printing flags.
  - The 'invis_bits' that go computes in the monad are the invisible bits in
    which the two types are definitely unequal.
    This is implemented by using the 'tell_on_mismatch' on function when we
    look at an invisible bit of the types.

    For example, suppose we have (a %m -> b) vs (a %n -> b):

      * We recursively call 'go' on the multiplicities, which tells us
        that 'm' and 'n' are unequal.
      * We write in the monad that there is a mismatch in a multiplicity.

    Note that, when the inner types differ in yet another invisible component,
    e.g. an invisible kind argument inside a multiplicity:

      (a %(M @k1 t) -> b)   vs   (a %(M @k2 t) -> b)

    then we need to enable the pretty-printing of /both/ multiplicities and
    explicit kinds. This is handled by 'tell_on_mismatch'.

Note [Metavariables in mayLookIdentical]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have a type mismatch, like in the 'PprExplicitKinds' test:

  alpha[tau] :: TYPE (RR @k1)
  b[sk]      :: TYPE (RR @k2)

Of course, 'alpha' and 'b' don't really look identical: they are type variables
with different names. We don't need to display any invisible bits for that to
be apparent to the user.

However, the user might wonder: why didn't 'alpha' unify? In this case, the
reason is that the kinds don't match, so it makes sense to show explicit kinds
to communicate that to the user.

Conclusion: in 'mayLookIdentical', when one of the types is a metavariable and
the kinds don't match, return:

  1. Visibly identical == True (the 'lie')
  2. Parts in which they are invisibly different: the kinds.

Otherwise, if the kinds do match, then set 'visibly identical == False'.

This has the net effect of switching on -fprint-explicit-kinds in the error
message, as desired.

Wrinkle [MetaTv mismatch at top-level only]

  The logic described in the Note only applies for top-level mismatches
  such as

    alpha[tau] ~ b[sk]

  If the mismatch is nested more deeply inside the type, don't bother. This
  is to avoid needlessly cluttering the error message, e.g. in

    T alpha ~ T b

  we shouldn't turn on explicit kinds just because of the 'alpha' vs 'b'
  mismatch. Relevant test case: T8030.

Note [Defaultable tyvars in mayLookIdentical]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are dealing with the following type mismatch in 'mayLookIdentical':

  ty1: forall (r::RuntimeRep). TYPE r -> Type
  ty2:                         Type   -> Type

The type pretty-printer defaults 'RuntimeRep' foralls (see GHC.Iface.Type.hideNonStandardTypes),
which will make the two types identical.

Hence, whenever we see a 'forall' whose binder has kind RuntimeRep, bail out
and say:

  1. May look identical: True.
  2. Parts in which the types are invisibly different: the RuntimeReps.

Hence, we will pass -fprint-explicit-runtime-reps when displaying ty1, which
will avoid a confusing error message.

The same applies for multiplicity variables, e.g.

  ty1: forall (m :: Multiplicity). a %m -> b
  ty2:                             a    -> b

See Note [Showing invisible bits of types in error messages] in GHC.Tc.Errors.Ppr
-}

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
&& Var -> Bool
isDefaultableTyVar Var
tv
isDefaultableTyVar :: TyVar -> Bool
isDefaultableTyVar :: Var -> Bool
isDefaultableTyVar Var
tv =
  Type -> Bool
isLevityTy Type
ki Bool -> Bool -> Bool
|| Type -> Bool
isRuntimeRepTy Type
ki  Bool -> Bool -> Bool
|| Type -> Bool
isMultiplicityTy Type
ki
  where
    ki :: Type
ki = Var -> Type
tyVarKind Var
tv