diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils')
-rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 32 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 2 |
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 |