Make typechecker equality consider visibility in ForAllTys

Previously, can_eq_nc' would equate ForAllTys 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 ArgFlags 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 ForAllTys 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 (closed). 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 (closed).
• 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 (closed).
• 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 (closed).