Make typechecker equality consider visibility in ForAllTys

Previously, `can_eq_nc'` would equate `ForAllTy`s regardless of their
`ArgFlag`, including `forall i -> i -> Type` and `forall i. i -> Type`! To fix
this, `can_eq_nc'` now uses the `sameVis` function to first check if the
`ArgFlag`s are equal modulo specificity. I have also updated `tcEqType`'s
implementation to match this behavior. For more explanation on the "modulo
specificity" part, see the new `Note [ForAllTy and typechecker equality]`
in `GHC.Tc.Solver.Canonical`.

While I was in town, I fixed some related documentation issues:

* I added `Note [Typechecker equality]` to `GHC.Tc.Utils.TcType` to describe
  what exactly distinguishes `can_eq_nc'` and `tcEqType` (which implement
  typechecker equality) from `eqType` (which implements definitional equality,
  which does not care about the `ArgFlags` of `ForAllTy`s at all).
* The User's Guide had some outdated prose on the specified/inferred
  distinction being different for types and kinds, a holdover from #15079. This
  is no longer the case on today's GHC, so I removed this prose, added some new
  prose to take its place, and added a regression test for the programs in
  #15079.
* The User's Guide had some _more_ outdated prose on inferred type variables
  not being allowed in `default` type signatures for class methods, which is no
  longer true as of the resolution of #18432.
* The related `Note [Deferred Unification]` was being referenced as
  `Note [Deferred unification]` elsewhere, which made it harder to `grep`
  for. I decided to change the name of the Note to `Deferred unification`
  for consistency with the capitalization style used for most other Notes.

Fixes #18863.

1 files changed, 28 insertions, 4 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