[Git][ghc/ghc][wip/T24725] Faster type equality
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed Jun 19 10:52:02 UTC 2024
Simon Peyton Jones pushed to branch wip/T24725 at Glasgow Haskell Compiler / GHC
Commits:
0eb7cf7e by Simon Peyton Jones at 2024-06-19T11:50:41+01:00
Faster type equality
This MR speeds up type equality, triggered by perf regressions that
showed up when fixing #24725 by parameterising type equality over
whether to ignore multiplicity.
The changes are:
* Do not use `nonDetCmpType` for type /equality/. Instead use a specialised
type-equality function, which we have always had!
`nonDetCmpType` remains, but I did not invest effort in refactoring
or optimising it.
* Type equality is parameterised by
- whether to expand synonyms
- whether to respect multiplicities
- whether it has a RnEnv2 environment
In this MR I systematically specialise it for static values of these
parameters. Much more direct and predictable than before. See
Note [Specialising type equality]
* We want to avoid comparing kinds if possible. I refactored how this
happens, at least for `eqType`.
See Note [Casts and coercions in type comparison]
* To make Lint fast, we want to avoid allocating a thunk for <msg> in
ensureEqTypes ty1 ty2 <msg>
because the test almost always succeeds, and <msg> isn't needed.
See Note [INLINE ensureEqTys]
Metric Decrease:
T13386
T5030
- - - - -
5 changed files:
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Multiplicity.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Utils/TcType.hs
Changes:
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -53,7 +53,7 @@ import GHC.Core.Predicate( isCoVarType )
import GHC.Core.Multiplicity
import GHC.Core.UsageEnv
import GHC.Core.TyCo.Rep -- checks validity of types/coercions
-import GHC.Core.TyCo.Compare ( eqType, eqTypeOpt, defaultCmpTypeOpt, CmpTypeOpt (..), eqForAllVis )
+import GHC.Core.TyCo.Compare ( eqType, eqTypes, eqTypeIgnoringMultiplicity, eqForAllVis )
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
@@ -2807,7 +2807,7 @@ lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches
extra_checks
| isNewTyCon tc
- = do { CoAxBranch { cab_tvs = tvs
+ = do { CoAxBranch { cab_tvs = ax_tvs
, cab_eta_tvs = eta_tvs
, cab_cvs = cvs
, cab_roles = roles
@@ -2815,14 +2815,10 @@ lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches
<- case branch_list of
[branch] -> return branch
_ -> failWithL (text "multi-branch axiom with newtype")
- ; let ax_lhs = mkInfForAllTys tvs $
- mkTyConApp tc lhs_tys
- nt_tvs = takeList tvs (tyConTyVars tc)
- -- axiom may be eta-reduced: Note [Newtype eta] in GHC.Core.TyCon
- nt_lhs = mkInfForAllTys nt_tvs $
- mkTyConApp tc (mkTyVarTys nt_tvs)
- -- See Note [Newtype eta] in GHC.Core.TyCon
- ; lintL (ax_lhs `eqType` nt_lhs)
+
+ -- The LHS of the axiom is (N lhs_tys)
+ -- We expect it to be (N ax_tvs)
+ ; lintL (mkTyVarTys ax_tvs `eqTypes` lhs_tys)
(text "Newtype axiom LHS does not match newtype definition")
; lintL (null cvs)
(text "Newtype axiom binds coercion variables")
@@ -2831,7 +2827,7 @@ lint_axiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches
(text "Newtype axiom has eta-tvs")
; lintL (ax_role == Representational)
(text "Newtype axiom role not representational")
- ; lintL (roles `equalLength` tvs)
+ ; lintL (roles `equalLength` ax_tvs)
(text "Newtype axiom roles list is the wrong length." $$
text "roles:" <+> sep (map ppr roles))
; lintL (roles == takeList roles (tyConRoles tc))
@@ -3101,17 +3097,14 @@ Note [Linting linearity]
Lint ignores linearity unless `-dlinear-core-lint` is set. For why, see below.
But first, "ignore linearity" specifically means two things. When ignoring linearity:
-* In `ensureEqTypes`, use `eqTypeOpt` with instructions to ignore multiplicities in FunTy.
+* In `ensureEqTypes`, use `eqTypeIgnoringMultiplicity`
* In `ensureSubMult`, do nothing
-The behaviour of functions such as eqTypeOpt which may or may not ignore
-linearity is governed by a flag of type GHC.Core.Multiplicity.MultiplicityFlag.
-
-But why make `-dcore-lint` ignore linearity? Because
-optimisation passes are not (yet) guaranteed to maintain linearity. They should
-do so semantically (GHC is careful not to duplicate computation) but it is much
-harder to ensure that the statically-checkable constraints of Linear Core are
-maintained. The current Linear Core is described in the wiki at:
+But why make `-dcore-lint` ignore linearity? Because optimisation passes are
+not (yet) guaranteed to maintain linearity. They should do so semantically (GHC
+is careful not to duplicate computation) but it is much harder to ensure that
+the statically-checkable constraints of Linear Core are maintained. The current
+Linear Core is described in the wiki at:
https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation.
Here are some examples of how the optimiser can break linearity checking. Other
@@ -3495,17 +3488,25 @@ ensureEqTys :: LintedType -> LintedType -> SDoc -> LintM ()
-- check ty2 is subtype of ty1 (ie, has same structure but usage
-- annotations need only be consistent, not equal)
-- Assumes ty1,ty2 are have already had the substitution applied
-ensureEqTys ty1 ty2 msg = do
- flags <- getLintFlags
- -- When `-dlinear-core-lint` is off, then consider `a -> b` and `a %1 -> b` to
- -- be equal. See Note [Linting linearity].
- lintL (eqTypeOpt (opt flags) ty1 ty2) msg
- where
- opt flags =
- if lf_check_linearity flags then
- defaultCmpTypeOpt { cmp_multiplicity_in_funty = RespectMultiplicities }
- else
- defaultCmpTypeOpt { cmp_multiplicity_in_funty = IgnoreMultiplicities }
+{-# INLINE ensureEqTys #-} -- See Note [INLINE ensureEqTys]
+ensureEqTys ty1 ty2 msg
+ = do { flags <- getLintFlags
+ ; lintL (eq_type flags ty1 ty2) msg }
+
+eq_type :: LintFlags -> Type -> Type -> Bool
+-- When `-dlinear-core-lint` is off, then consider `a -> b` and `a %1 -> b` to
+-- be equal. See Note [Linting linearity].
+eq_type flags ty1 ty2 | lf_check_linearity flags = eqType ty1 ty2
+ | otherwise = eqTypeIgnoringMultiplicity ty1 ty2
+
+{- Note [INLNE ensureEqTys]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+To make Lint fast, we want to avoid allocating a thunk for <msg> in
+ ensureEqTypes ty1 ty2 <msg>
+because the test almost always succeeds, and <msg> isn't needed.
+So we INLINE `ensureEqTys`. This actually make a difference of
+1-2% when compiling programs with -dcore-lint.
+-}
ensureSubUsage :: Usage -> Mult -> SDoc -> LintM ()
ensureSubUsage Bottom _ _ = return ()
=====================================
compiler/GHC/Core/Multiplicity.hs
=====================================
@@ -31,7 +31,8 @@ module GHC.Core.Multiplicity
, submult
, mapScaledType
, pprArrowWithMultiplicity
- , MultiplicityFlag(..)) where
+ , MultiplicityFlag(..)
+ ) where
import GHC.Prelude
=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -7,16 +7,17 @@
-- | Type equality and comparison
module GHC.Core.TyCo.Compare (
- -- * Type comparison
- eqType, eqTypeOpt, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
- nonDetCmpTypesX, nonDetCmpTc,
+ -- * Type equality
+ eqType, eqTypeIgnoringMultiplicity, eqTypeX, eqTypes,
eqVarBndrs,
- CmpTypeOpt (..), defaultCmpTypeOpt,
pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck,
tcEqTyConApps,
mayLookIdentical,
+ -- * Type comparison
+ nonDetCmpType,
+
-- * Visiblity comparision
eqForAllVis, cmpForAllVis
@@ -30,10 +31,12 @@ import GHC.Core.Type( typeKind, coreView, tcSplitAppTyNoView_maybe, splitAppTyNo
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCon
+import GHC.Core.Multiplicity( MultiplicityFlag(..) )
import GHC.Types.Var
import GHC.Types.Unique
import GHC.Types.Var.Env
+import GHC.Types.Var.Set
import GHC.Utils.Outputable
import GHC.Utils.Misc
@@ -42,7 +45,6 @@ import GHC.Utils.Panic
import GHC.Base (reallyUnsafePtrEquality#)
import qualified Data.Semigroup as S
-import GHC.Core.Multiplicity
{- GHC.Core.TyCo.Compare overview
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -54,7 +56,8 @@ so it currently sits "on top of" GHC.Core.Type.
{- *********************************************************************
* *
- Type equality
+ Type equality
+ We don't use (==) from class Eq, that we know where it happens
* *
********************************************************************* -}
@@ -74,6 +77,75 @@ that needs to be updated.
* 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 involved
+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.
+
+Now the kind of `s1` and `s2` must be equal; and hence the kind of `s2` and `t2`
+must be equal (the kind of T could be (forall k. k -> ...), but `k` will be
+instantiate with `s1` and `t1` resp, which are equal. And so on.
+
+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.
+
+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.
+
Note [Type comparisons using object pointer comparisons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Quite often we substitute the type from a definition site into
@@ -83,6 +155,19 @@ 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%.
+
+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
-}
@@ -90,21 +175,12 @@ tcEqKind :: HasDebugCallStack => Kind -> Kind -> Bool
tcEqKind = tcEqType
tcEqType :: HasDebugCallStack => Type -> Type -> Bool
--- ^ tcEqType implements typechecker equality
--- It behaves just like eqType, but is implemented
--- differently (for now)
-tcEqType ty1 ty2
- = tcEqTypeNoSyns ki1 ki2
- && tcEqTypeNoSyns ty1 ty2
- where
- ki1 = typeKind ty1
- ki2 = typeKind ty2
+tcEqType = 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 ty1 ty2
- = tcEqTypeNoSyns ty1 ty2
+tcEqTypeNoKindCheck = eqTypeNoKindCheck
-- | Check whether two TyConApps are the same; if the number of arguments
-- are different, just checks the common prefix of arguments.
@@ -116,175 +192,221 @@ tcEqTyConApps tc1 args1 tc2 args2
-- 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.
--}
-
-mayLookIdentical :: Type -> Type -> Bool
--- | Returns True if the /visible/ part of the types
--- might look equal, even if they are really unequal (in the invisible bits)
---
--- This function is very similar to tc_eq_type but it is much more
--- heuristic. Notably, it is always safe to return True, even with types
--- that might (in truth) be unequal -- this affects error messages only
--- (Originally there were one function with an extra flag, but the result
--- was hard to understand.)
-mayLookIdentical orig_ty1 orig_ty2
- = go orig_env orig_ty1 orig_ty2
- where
- orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
+-- | Type equality on lists of types, looking through type synonyms
+eqTypes :: [Type] -> [Type] -> Bool
+eqTypes [] [] = True
+eqTypes (t1:ts1) (t2:ts2) = eqType t1 t2 && eqTypes ts1 ts2
+eqTypes _ _ = False
- go :: RnEnv2 -> Type -> Type -> Bool
- -- See Note [Comparing nullary type synonyms]
- go _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
+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 env [] []
+ = Just env
+eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
+ | eqTypeX env (varType tv1) (varType tv2)
+ = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
+eqVarBndrs _ _ _= Nothing
- go env t1 t2 | Just t1' <- coreView t1 = go env t1' t2
- go env t1 t2 | Just t2' <- coreView t2 = go env t1 t2'
+initRnEnv :: Type -> Type -> RnEnv2
+initRnEnv ta tb = mkRnEnv2 $ mkInScopeSet $
+ tyCoVarsOfType ta `unionVarSet` tyCoVarsOfType tb
- go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
- go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
- go env (CastTy t1 _) t2 = go env t1 t2
- go env t1 (CastTy t2 _) = go env t1 t2
- go _ (CoercionTy {}) (CoercionTy {}) = True
+eqTypeNoKindCheck :: Type -> Type -> Bool
+eqTypeNoKindCheck ty1 ty2 = eq_type_expand_respect ty1 ty2
- go env (ForAllTy (Bndr tv1 vis1) ty1)
- (ForAllTy (Bndr tv2 vis2) ty2)
- = vis1 `eqForAllVis` vis2 -- See Note [ForAllTy and type equality]
- && go (rnBndr2 env tv1 tv2) ty1 ty2
- -- Visible stuff only: ignore kinds of binders
+-- | Type equality comparing both visible and invisible arguments,
+-- expanding synonyms and respecting multiplicities.
+eqType :: HasCallStack => Type -> Type -> Bool
+eqType ta tb = fullEq eq_type_expand_respect ta tb
- -- If we have (forall (r::RunTimeRep). ty1 ~ blah) then respond
- -- with True. Reason: the type pretty-printer defaults RuntimeRep
- -- foralls (see Ghc.Iface.Type.hideNonStandardTypes). That can make,
- -- say (forall r. TYPE r -> Type) into (Type -> Type), so it looks the
- -- same as a very different type (#24553). By responding True, we
- -- tell GHC (see calls of mayLookIdentical) to display without defaulting.
- -- See Note [Showing invisible bits of types in error messages]
- -- in GHC.Tc.Errors.Ppr
- go _ (ForAllTy b _) _ | isDefaultableBndr b = True
- go _ _ (ForAllTy b _) | isDefaultableBndr b = True
+-- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
+eqTypeX :: HasCallStack => RnEnv2 -> Type -> Type -> Bool
+eqTypeX env ta tb = fullEq (eq_type_expand_respect_x env) ta tb
- go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
- = go env arg1 arg2 && go env res1 res2 && go env w1 w2
- -- Visible stuff only: ignore agg kinds
+eqTypeIgnoringMultiplicity :: Type -> Type -> Bool
+-- See Note [Respecting multiplicity when comparing types]
+eqTypeIgnoringMultiplicity ta tb = fullEq eq_type_expand_ignore ta tb
- -- See Note [Equality on AppTys] in GHC.Core.Type
- go env (AppTy s1 t1) ty2
- | Just (s2, t2) <- tcSplitAppTyNoView_maybe ty2
- = go env s1 s2 && go env t1 t2
- go env ty1 (AppTy s2 t2)
- | Just (s1, t1) <- tcSplitAppTyNoView_maybe ty1
- = go env s1 s2 && go env t1 t2
+-- | 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 ta tb = eq_type_keep_respect ta tb
- go env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
- = tc1 == tc2 && gos env (tyConBinders tc1) ts1 ts2
+{- 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:
- go _ _ _ = False
+* The main workhorse is `inline_generic_eq_type_x`. It is /non-recursive/
+ and is marked INLINE.
- gos :: RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
- gos _ _ [] [] = True
- gos env bs (t1:ts1) (t2:ts2)
- | (invisible, bs') <- case bs of
- [] -> (False, [])
- (b:bs) -> (isInvisibleTyConBinder b, bs)
- = (invisible || go env t1 t2) && gos env bs' ts1 ts2
+* `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.
- gos _ _ _ _ = False
+* `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.
--- | Type equality comparing both visible and invisible arguments and expanding
--- type synonyms.
-tcEqTypeNoSyns :: Type -> Type -> Bool
-tcEqTypeNoSyns ta tb = tc_eq_type False ta tb
+* 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.
--- | 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 ty1 ty2 = tc_eq_type True ty1 ty2
+See #19226.
+-}
--- | Real worker for 'tcEqType'. No kind check!
-tc_eq_type :: Bool -- ^ True <=> do not expand type synonyms
- -> Type -> Type
- -> Bool
--- Flags False, False is the usual setting for tc_eq_type
+-- | 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 = inline_generic_eq_type_x ExpandSynonyms RespectMultiplicities Nothing
+eq_type_expand_respect_x env = inline_generic_eq_type_x ExpandSynonyms RespectMultiplicities (Just env)
+eq_type_expand_ignore = inline_generic_eq_type_x ExpandSynonyms IgnoreMultiplicities Nothing
+eq_type_expand_ignore_x env = inline_generic_eq_type_x ExpandSynonyms IgnoreMultiplicities (Just env)
+eq_type_keep_respect = inline_generic_eq_type_x KeepSynonyms RespectMultiplicities Nothing
+eq_type_keep_respect_x env = inline_generic_eq_type_x KeepSynonyms RespectMultiplicities (Just 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 = inline_generic_eq_type_x
-- See Note [Computing equality on types] in Type
-{-# INLINE tc_eq_type #-} -- See Note [Specialising tc_eq_type].
-tc_eq_type keep_syns orig_ty1 orig_ty2
- = go orig_env orig_ty1 orig_ty2
+
+{-# INLINE inline_generic_eq_type_x #-}
+inline_generic_eq_type_x syn_flag mult_flag mb_env
+ = inline_go -- This is the only call of inline_go
where
- orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
+ -------------------
+ go = generic_eq_type_x syn_flag mult_flag mb_env
- go :: RnEnv2 -> Type -> Type -> Bool
- -- See Note [Comparing nullary type synonyms]
- go _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
+ -------------------
+ inline_go !t1 !t2 | 1# <- reallyUnsafePtrEquality# t1 t2 = True
+ -- See Note [Type comparisons using object pointer comparisons]
- go env t1 t2 | not keep_syns, Just t1' <- coreView t1 = go env t1' t2
- go env t1 t2 | not keep_syns, Just t2' <- coreView t2 = go env t1 t2'
+ inline_go (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
+ -- See Note [Comparing nullary type synonyms]
- go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
- go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
- go env (CastTy t1 _) t2 = go env t1 t2
- go env t1 (CastTy t2 _) = go env t1 t2
- go _ (CoercionTy {}) (CoercionTy {}) = True
+ inline_go t1 t2 | ExpandSynonyms <- syn_flag, Just t1' <- coreView t1 = go t1' t2
+ inline_go t1 t2 | ExpandSynonyms <- syn_flag, Just t2' <- coreView t2 = go t1 t2'
- go env (ForAllTy (Bndr tv1 vis1) ty1)
- (ForAllTy (Bndr tv2 vis2) ty2)
- = vis1 `eqForAllVis` vis2 -- See Note [ForAllTy and type equality]
- && go env (varType tv1) (varType tv2)
- && go (rnBndr2 env tv1 tv2) ty1 ty2
+ inline_go (TyVarTy tv1) (TyVarTy tv2)
+ = case mb_env of
+ Nothing -> tv1 == tv2
+ Just env -> rnOccL env tv1 == rnOccR env tv2
+
+ inline_go (LitTy lit1) (LitTy lit2) = lit1 == lit2
+ inline_go (CastTy t1 _) t2 = go t1 t2 -- Ignore casts
+ inline_go t1 (CastTy t2 _) = go t1 t2 -- Ignore casts
+ inline_go (CoercionTy {}) (CoercionTy {}) = 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
- go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
- = go env (typeKind arg1) (typeKind arg2) &&
- go env (typeKind res1) (typeKind res2) &&
- go env arg1 arg2 && go env res1 res2 && go env w1 w2
+ inline_go (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
+ = fullEq go arg1 arg2
+ && fullEq go res1 res2
+ && (case mult_flag of
+ RespectMultiplicities -> go w1 w2
+ IgnoreMultiplicities -> True)
-- See Note [Equality on AppTys] in GHC.Core.Type
- go env (AppTy s1 t1) ty2
+ inline_go (AppTy s1 t1) ty2
| Just (s2, t2) <- tcSplitAppTyNoView_maybe ty2
- = go env s1 s2 && go env t1 t2
- go env ty1 (AppTy s2 t2)
+ = go s1 s2 && go t1 t2
+ inline_go ty1 (AppTy s2 t2)
| Just (s1, t1) <- tcSplitAppTyNoView_maybe ty1
- = go env s1 s2 && go env t1 t2
-
- go env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
- = tc1 == tc2 && gos env ts1 ts2
-
- go _ _ _ = False
-
- gos _ [] [] = True
- gos env (t1:ts1) (t2:ts2) = go env t1 t2 && gos env ts1 ts2
- gos _ _ _ = False
+ = go s1 s2 && go t1 t2
+
+ inline_go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ | tc1 == tc2 = gos ts1 ts2
+ | otherwise = False
+ where
+ gos [] [] = True
+ gos (t1:ts1) (t2:ts2) = go t1 t2 && gos ts1 ts2
+ gos _ _ = False
+
+ inline_go ty1@(ForAllTy (Bndr tv1 vis1) body1)
+ ty2@(ForAllTy (Bndr tv2 vis2) body2)
+ = case mb_env of
+ Nothing -> generic_eq_type_x syn_flag mult_flag
+ (Just (initRnEnv ty1 ty2)) ty1 ty2
+ Just env
+ | vis1 `eqForAllVis` vis2 -- See Note [ForAllTy and type equality]
+ -> go (varType tv1) (varType tv2) -- Always do kind-check
+ && generic_eq_type_x syn_flag mult_flag
+ (Just (rnBndr2 env tv1 tv2)) body1 body2
+ | otherwise
+ -> False
+
+ inline_go _ _ = 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 eq ty1 ty2
+ = case eq ty1 ty2 of
+ False -> False
+ True | hasCasts ty1 || hasCasts ty2
+ -> eq (typeKind ty1) (typeKind ty2)
+ | otherwise
+ -> True
+
+hasCasts :: Type -> Bool
+-- Fast, does not look deep, does not allocate
+hasCasts (CastTy {}) = True
+hasCasts (CoercionTy {}) = True
+hasCasts (AppTy t1 t2) = hasCasts t1 || hasCasts t2
+hasCasts (ForAllTy _ ty) = hasCasts ty
+hasCasts _ = False -- TyVarTy, TyConApp, FunTy, LitTy
-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 (Bndr tv vis)
- = isInvisibleForAllTyFlag vis && is_defaultable (tyVarKind tv)
- where
- is_defaultable ki = isLevityTy ki || isRuntimeRepTy ki || isMultiplicityTy ki
+{- *********************************************************************
+* *
+ Comparing ForAllTyFlags
+* *
+********************************************************************* -}
-- | Do these denote the same level of visibility? 'Required'
-- arguments are visible, others are not. So this function
@@ -444,94 +566,13 @@ is more finer-grained than definitional equality in two places:
************************************************************************
* *
Comparison for types
- (We don't use instances so that we know where it happens)
+
+ Not so heavily used, less carefully optimised
* *
************************************************************************
-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 t1 t2 = isEqual $ nonDetCmpType t1 t2
- -- It's OK to use nonDetCmpType here and eqType is deterministic,
- -- nonDetCmpType does equality deterministically
-
-eqTypeOpt :: CmpTypeOpt -> Type -> Type -> Bool
-eqTypeOpt opt t1 t2 = isEqual $ nonDetCmpTypeOpt opt t1 t2
-
--- | Compare types with respect to a (presumably) non-empty 'RnEnv2'.
-eqTypeX :: RnEnv2 -> Type -> Type -> Bool
-eqTypeX env t1 t2 = isEqual $ nonDetCmpTypeX defaultCmpTypeOpt env t1 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 tys1 tys2 = isEqual $ nonDetCmpTypes tys1 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 env [] []
- = Just env
-eqVarBndrs env (tv1:tvs1) (tv2:tvs2)
- | eqTypeX env (varType tv1) (varType tv2)
- = eqVarBndrs (rnBndr2 env tv1 tv2) tvs1 tvs2
-eqVarBndrs _ _ _= Nothing
-
-- Now here comes the real worker
-{-
Note [nonDetCmpType nondeterminism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
@@ -541,27 +582,20 @@ comparing type variables is nondeterministic, note the call to nonDetCmpVar in
nonDetCmpTypeX.
See Note [Unique Determinism] for more details.
-}
-nonDetCmpType :: Type -> Type -> Ordering
-nonDetCmpType = nonDetCmpTypeOpt defaultCmpTypeOpt
-nonDetCmpTypeOpt :: CmpTypeOpt -> Type -> Type -> Ordering
-nonDetCmpTypeOpt _ !t1 !t2
+nonDetCmpType :: Type -> Type -> Ordering
+{-# INLINE nonDetCmpType #-}
+nonDetCmpType !t1 !t2
-- See Note [Type comparisons using object pointer comparisons]
| 1# <- reallyUnsafePtrEquality# t1 t2
= EQ
-nonDetCmpTypeOpt _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2
+nonDetCmpType (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2
= EQ
-nonDetCmpTypeOpt opt t1 t2
+nonDetCmpType t1 t2
-- we know k1 and k2 have the same kind, because they both have kind *.
- = nonDetCmpTypeX opt rn_env t1 t2
+ = nonDetCmpTypeX rn_env t1 t2
where
rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes [t1, t2]))
-{-# INLINE nonDetCmpType #-}
-
-nonDetCmpTypes :: [Type] -> [Type] -> Ordering
-nonDetCmpTypes ts1 ts2 = nonDetCmpTypesX rn_env ts1 ts2
- where
- rn_env = mkRnEnv2 (mkInScopeSet (tyCoVarsOfTypes (ts1 ++ ts2)))
-- | An ordering relation between two 'Type's (known below as @t1 :: k1@
-- and @t2 :: k2@)
@@ -573,10 +607,11 @@ data TypeOrdering = TLT -- ^ @t1 < t2@
| TGT -- ^ @t1 > t2@
deriving (Eq, Ord, Enum, Bounded)
-nonDetCmpTypeX :: CmpTypeOpt -> RnEnv2 -> Type -> Type -> Ordering -- Main workhorse
+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 opt env orig_t1 orig_t2 =
+ -- Always respects multiplicities, unlike eqType
+nonDetCmpTypeX env orig_t1 orig_t2 =
case go env orig_t1 orig_t2 of
-- If there are casts then we also need to do a comparison of
-- the kinds of the types being compared
@@ -635,13 +670,9 @@ nonDetCmpTypeX opt env orig_t1 orig_t2 =
go env (FunTy _ w1 s1 t1) (FunTy _ w2 s2 t2)
-- NB: nonDepCmpTypeX does the kind check requested by
-- Note [Equality on FunTys] in GHC.Core.TyCo.Rep
- = liftOrdering (nonDetCmpTypeX opt env s1 s2 S.<> nonDetCmpTypeX opt env t1 t2)
- `thenCmpTy` cmp_mults
+ = liftOrdering (nonDetCmpTypeX env s1 s2 S.<> nonDetCmpTypeX env t1 t2)
+ `thenCmpTy` go env w1 w2
-- Comparing multiplicities last because the test is usually true
- where
- cmp_mults = case cmp_multiplicity_in_funty opt of
- RespectMultiplicities -> go env w1 w2
- IgnoreMultiplicities -> TEQ
go env (TyConApp tc1 tys1) (TyConApp tc2 tys2)
= liftOrdering (tc1 `nonDetCmpTc` tc2) `thenCmpTy` gos env tys1 tys2
@@ -672,36 +703,6 @@ nonDetCmpTypeX opt env orig_t1 orig_t2 =
gos _ _ [] = TGT
gos env (ty1:tys1) (ty2:tys2) = go env ty1 ty2 `thenCmpTy` gos env tys1 tys2
-{- 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
-* `CmpTypeOpt` 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
--}
-data CmpTypeOpt = CmpTypeOpt
- { -- Whether to consider `a -> b` and `a %1 -> b` distinct or equal. Default:
- -- RespectMultiplicities. See Note [Respecting multiplicity when comparing types].
- cmp_multiplicity_in_funty :: MultiplicityFlag
- }
-
-defaultCmpTypeOpt :: CmpTypeOpt
-defaultCmpTypeOpt = CmpTypeOpt
- { cmp_multiplicity_in_funty = RespectMultiplicities }
-
--------------
-nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering
-nonDetCmpTypesX _ [] [] = EQ
-nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX defaultCmpTypeOpt env t1 t2 S.<>
- nonDetCmpTypesX env tys1 tys2
-nonDetCmpTypesX _ [] _ = LT
-nonDetCmpTypesX _ _ [] = GT
-------------
-- | Compare two 'TyCon's.
@@ -714,4 +715,91 @@ nonDetCmpTc tc1 tc2
u2 = tyConUnique tc2
+{- *********************************************************************
+* *
+ mayLookIdentical
+* *
+********************************************************************* -}
+
+mayLookIdentical :: Type -> Type -> Bool
+-- | Returns True if the /visible/ part of the types
+-- might look equal, even if they are really unequal (in the invisible bits)
+--
+-- This function is very similar to tc_eq_type but it is much more
+-- heuristic. Notably, it is always safe to return True, even with types
+-- that might (in truth) be unequal -- this affects error messages only
+-- (Originally there were one function with an extra flag, but the result
+-- was hard to understand.)
+mayLookIdentical orig_ty1 orig_ty2
+ = go orig_env orig_ty1 orig_ty2
+ where
+ orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
+
+ go :: RnEnv2 -> Type -> Type -> Bool
+ -- See Note [Comparing nullary type synonyms]
+ go _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
+
+ go env t1 t2 | Just t1' <- coreView t1 = go env t1' t2
+ go env t1 t2 | Just t2' <- coreView t2 = go env t1 t2'
+
+ go env (TyVarTy tv1) (TyVarTy tv2) = rnOccL env tv1 == rnOccR env tv2
+ go _ (LitTy lit1) (LitTy lit2) = lit1 == lit2
+ go env (CastTy t1 _) t2 = go env t1 t2
+ go env t1 (CastTy t2 _) = go env t1 t2
+ go _ (CoercionTy {}) (CoercionTy {}) = True
+
+ go env (ForAllTy (Bndr tv1 vis1) ty1)
+ (ForAllTy (Bndr tv2 vis2) ty2)
+ = vis1 `eqForAllVis` vis2 -- See Note [ForAllTy and type equality]
+ && go (rnBndr2 env tv1 tv2) ty1 ty2
+ -- Visible stuff only: ignore kinds of binders
+
+ -- If we have (forall (r::RunTimeRep). ty1 ~ blah) then respond
+ -- with True. Reason: the type pretty-printer defaults RuntimeRep
+ -- foralls (see Ghc.Iface.Type.hideNonStandardTypes). That can make,
+ -- say (forall r. TYPE r -> Type) into (Type -> Type), so it looks the
+ -- same as a very different type (#24553). By responding True, we
+ -- tell GHC (see calls of mayLookIdentical) to display without defaulting.
+ -- See Note [Showing invisible bits of types in error messages]
+ -- in GHC.Tc.Errors.Ppr
+ go _ (ForAllTy b _) _ | isDefaultableBndr b = True
+ go _ _ (ForAllTy b _) | isDefaultableBndr b = True
+
+ go env (FunTy _ w1 arg1 res1) (FunTy _ w2 arg2 res2)
+ = go env arg1 arg2 && go env res1 res2 && go env w1 w2
+ -- Visible stuff only: ignore agg kinds
+
+ -- See Note [Equality on AppTys] in GHC.Core.Type
+ go env (AppTy s1 t1) ty2
+ | Just (s2, t2) <- tcSplitAppTyNoView_maybe ty2
+ = go env s1 s2 && go env t1 t2
+ go env ty1 (AppTy s2 t2)
+ | Just (s1, t1) <- tcSplitAppTyNoView_maybe ty1
+ = go env s1 s2 && go env t1 t2
+
+ go env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ = tc1 == tc2 && gos env (tyConBinders tc1) ts1 ts2
+
+ go _ _ _ = False
+
+ gos :: RnEnv2 -> [TyConBinder] -> [Type] -> [Type] -> Bool
+ gos _ _ [] [] = True
+ gos env bs (t1:ts1) (t2:ts2)
+ | (invisible, bs') <- case bs of
+ [] -> (False, [])
+ (b:bs) -> (isInvisibleTyConBinder b, bs)
+ = (invisible || go env t1 t2) && gos env bs' ts1 ts2
+
+ gos _ _ _ _ = False
+
+
+isDefaultableBndr :: ForAllTyBinder -> Bool
+-- This function should line up with the defaulting done
+-- by GHC.Iface.Type.defaultIfaceTyVarsOfKind
+-- See Note [Showing invisible bits of types in error messages]
+-- in GHC.Tc.Errors.Ppr
+isDefaultableBndr (Bndr tv vis)
+ = isInvisibleForAllTyFlag vis && is_defaultable (tyVarKind tv)
+ where
+ is_defaultable ki = isLevityTy ki || isRuntimeRepTy ki || isMultiplicityTy ki
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -350,14 +350,24 @@ This kind instantiation only happens in TyConApp currently.
Note [Non-trivial definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Is Int |> <*> the same as Int? YES! In order to reduce headaches,
-we decide that any reflexive casts in types are just ignored.
-(Indeed they must be. See Note [Respecting definitional equality].)
-More generally, the `eqType` function, which defines Core's type equality
-relation, ignores casts and coercion arguments, as long as the
-two types have the same kind. This allows us to be a little sloppier
-in keeping track of coercions, which is a good thing. It also means
-that eqType does not depend on eqCoercion, which is also a good thing.
+Is ((Monad |> co1) Int |> co2) equal to (Monad Int)?
+Assume
+ co1 :: (Type->Type) ~ (Type->Wombat)
+ co2 :: Wombat ~ Type
+Well, yes. The casts are just getting in the way.
+See also Note [Respecting definitional equality].
+
+So we do this:
+
+(EQTYPE)
+ The `eqType` function, which defines Core's type equality relation,
+ - /ignores/ casts, and
+ - /ignores/ coercion arguments
+ - /provided/ two types have the same kind
+
+This allows us to be a little sloppier in keeping track of coercions, which is a
+good thing. It also means that eqType does not depend on eqCoercion, which is
+also a good thing.
Why is this sensible? That is, why is something different than α-equivalence
appropriate for the implementation of eqType?
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -96,7 +96,7 @@ module GHC.Tc.Utils.TcType (
-- Re-exported from GHC.Core.TyCo.Compare
-- mainly just for back-compat reasons
- eqType, eqTypes, nonDetCmpType, nonDetCmpTypes, eqTypeX,
+ eqType, eqTypes, nonDetCmpType, eqTypeX,
pickyEqType, tcEqType, tcEqKind, tcEqTypeNoKindCheck, mayLookIdentical,
tcEqTyConApps, eqForAllVis, eqVarBndrs,
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0eb7cf7eee1dc2159b8d5d8ce3108a076d548c4b
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0eb7cf7eee1dc2159b8d5d8ce3108a076d548c4b
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240619/a2f4a061/attachment-0001.html>
More information about the ghc-commits
mailing list