summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Utils
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Utils')
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs32
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs2
2 files changed, 29 insertions, 5 deletions
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 412fc5aa43..83256c9c8c 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -1506,9 +1506,8 @@ tcEqKind :: HasDebugCallStack => TcKind -> TcKind -> Bool
tcEqKind = tcEqType
tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool
--- tcEqType is a proper implements the same Note [Non-trivial definitional
--- equality] (in GHC.Core.TyCo.Rep) as `eqType`, but Type.eqType believes (* ==
--- Constraint), and that is NOT what we want in the type checker!
+-- ^ tcEqType implements typechecker equality, as described in
+-- @Note [Typechecker equality vs definitional equality]@.
tcEqType ty1 ty2
= tc_eq_type False False ki1 ki2
&& tc_eq_type False False ty1 ty2
@@ -1557,7 +1556,9 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
go env (ForAllTy (Bndr tv1 vis1) ty1)
(ForAllTy (Bndr tv2 vis2) ty2)
- = vis1 == vis2
+ = vis1 `sameVis` vis2
+ -- See Note [ForAllTy and typechecker equality] in
+ -- GHC.Tc.Solver.Canonical for why we use `sameVis` here
&& (vis_only || go env (varType tv1) (varType tv2))
&& go (rnBndr2 env tv1 tv2) ty1 ty2
@@ -1622,6 +1623,29 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
get_args _ _ = False
eqFunTy _ _ _ _ _ = False
+{- Note [Typechecker equality vs definitional equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC has two notions of equality over Core types:
+
+* 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 (in GHC.Tc.Utils.TcType).
+ GHC.Tc.Solver.Canonical.canEqNC also respects typechecker equality.
+
+Typechecker equality implies 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:
+
+* Unlike definitional equality, which equates Type and Constraint, typechecker
+ treats them as distinct types. See Note [Kind Constraint and kind Type] in
+ GHC.Core.Type.
+* Unlike definitional equality, which does not care about the ArgFlag of a
+ ForAllTy, typechecker equality treats Required type variable binders as
+ distinct from Invisible type variable binders.
+ See Note [ForAllTy and typechecker equality] in GHC.Tc.Solver.Canonical.
+-}
+
{- *********************************************************************
* *
Predicate types
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index c1202f02d7..d704bcbf8f 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1321,7 +1321,7 @@ We expand synonyms during unification, but:
This is particularly helpful when checking (* ~ *), because * is
now a type synonym.
-Note [Deferred Unification]
+Note [Deferred unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically,
and yet its consistency is undetermined. Previously, there was no way to still