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.

14 files changed, 224 insertions, 28 deletions

diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 87b943f790..1e8fcda0ca 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -485,6 +485,12 @@ Another helpful principle with eqType is this:
 This principle also tells us that eqType must relate only types with the
 same kinds.
 
+Besides eqType, another equality relation that upholds the (EQ) property above
+is /typechecker equality/, which is implemented as
+GHC.Tc.Utils.TcType.tcEqType. See
+Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType for
+what the difference between eqType and tcEqType is.
+
 Note [Respecting definitional equality]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Note [Non-trivial definitional equality] introduces the property (EQ).
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 68b73b589b..8ae7812c07 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -2236,7 +2236,7 @@ eqVarBndrs _ _ _= Nothing
 
 {-
 Note [nonDetCmpType nondeterminism]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 nonDetCmpType is implemented in terms of nonDetCmpTypeX. nonDetCmpTypeX
 uses nonDetCmpTc which compares TyCons by their Unique value. Using Uniques for
 ordering leads to nondeterminism. We hit the same problem in the TyVarTy case,
@@ -2926,7 +2926,7 @@ splitVisVarsOfTypes = foldMap splitVisVarsOfType
 ************************************************************************
 
 Note [Kind Constraint and kind Type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The kind Constraint is the kind of classes and other type constraints.
 The special thing about types of kind Constraint is that
  * They are displayed with double arrow:
@@ -2945,6 +2945,18 @@ generates an axiom witnessing
 so on the left we have Constraint, and on the right we have Type.
 See #7451.
 
+Because we treat Constraint/Type differently during and after type inference,
+GHC has two notions of equality that differ in whether they equate
+Constraint/Type or not:
+
+* GHC.Tc.Utils.TcType.tcEqType implements typechecker equality (see
+  Note [Typechecker equality vs definitional equality] in GHC.Tc.Utils.TcType),
+  which treats Constraint and Type as distinct. This is used during type
+  inference. See #11715 for issues that arise from this.
+* GHC.Core.TyCo.Rep.eqType implements definitional equality (see
+  Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep), which treats
+  Constraint and Type as equal. This is used after type inference.
+
 Bottom line: although 'Type' and 'Constraint' are distinct TyCons, with
 distinct uniques, they are treated as equal at all times except
 during type inference.
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 8cf326bac0..924996edfd 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -1035,7 +1035,9 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
   = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
 
 can_eq_nc' _flat _rdr_env _envs ev eq_rel
-           s1@(ForAllTy {}) _ s2@(ForAllTy {}) _
+           s1@(ForAllTy (Bndr _ vis1) _) _
+           s2@(ForAllTy (Bndr _ vis2) _) _
+  | vis1 `sameVis` vis2 -- Note [ForAllTy and typechecker equality]
   = can_eq_nc_forall ev eq_rel s1 s2
 
 -- See Note [Canonicalising type applications] about why we require flat types
@@ -1071,6 +1073,63 @@ If we have an unsolved equality like
 that is not necessarily insoluble!  Maybe 'a' will turn out to be a newtype.
 So we want to make it a potentially-soluble Irred not an insoluble one.
 Missing this point is what caused #15431
+
+Note [ForAllTy and typechecker equality]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Should GHC type-check the following program (adapted from #15740)?
+
+  {-# LANGUAGE PolyKinds, ... #-}
+  data D a
+  type family F :: forall k. k -> Type
+  type instance F = D
+
+Due to the way F is declared, any instance of F must have a right-hand side
+whose kind is equal to `forall k. k -> Type`. The kind of D is
+`forall {k}. k -> Type`, which is very close, but technically uses distinct
+Core:
+
+  -----------------------------------------------------------
+  | Source Haskell    | Core                                |
+  -----------------------------------------------------------
+  | forall  k.  <...> | ForAllTy (Bndr k Specified) (<...>) |
+  | forall {k}. <...> | ForAllTy (Bndr k Inferred)  (<...>) |
+  -----------------------------------------------------------
+
+We could deem these kinds to be unequal, but that would imply rejecting
+programs like the one above. Whether a kind variable binder ends up being
+specified or inferred can be somewhat subtle, however, especially for kinds
+that aren't explicitly written out in the source code (like in D above).
+For now, we decide to not make the specified/inferred status of an invisible
+type variable binder affect GHC's notion of typechecker equality
+(see Note [Typechecker equality vs definitional equality] in
+GHC.Tc.Utils.TcType). That is, we have the following:
+
+  --------------------------------------------------
+  | Type 1            | Type 2            | Equal? |
+  --------------------|-----------------------------
+  | forall k. <...>   | forall k. <...>   | Yes    |
+  |                   | forall {k}. <...> | Yes    |
+  |                   | forall k -> <...> | No     |
+  --------------------------------------------------
+  | forall {k}. <...> | forall k. <...>   | Yes    |
+  |                   | forall {k}. <...> | Yes    |
+  |                   | forall k -> <...> | No     |
+  --------------------------------------------------
+  | forall k -> <...> | forall k. <...>   | No     |
+  |                   | forall {k}. <...> | No     |
+  |                   | forall k -> <...> | Yes    |
+  --------------------------------------------------
+
+We implement this nuance by using the GHC.Types.Var.sameVis function in
+GHC.Tc.Solver.Canonical.canEqNC and GHC.Tc.Utils.TcType.tcEqType, which
+respect typechecker equality. sameVis puts both forms of invisible type
+variable binders into the same equivalence class.
+
+Note that we do /not/ use sameVis in GHC.Core.Type.eqType, which implements
+/definitional/ equality, a slighty more coarse-grained notion of equality
+(see Note [Non-trivial definitional equality] in GHC.Core.TyCo.Rep) that does
+not consider the ArgFlag of ForAllTys at all. That is, eqType would equate all
+of forall k. <...>, forall {k}. <...>, and forall k -> <...>.
 -}
 
 ---------------------------------
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
diff --git a/docs/users_guide/exts/poly_kinds.rst b/docs/users_guide/exts/poly_kinds.rst
index 58800d47cb..3cd9540a26 100644
--- a/docs/users_guide/exts/poly_kinds.rst
+++ b/docs/users_guide/exts/poly_kinds.rst
@@ -769,24 +769,6 @@ In this redefinition, we give an explicit kind for ``(:~~:)``, deferring the cho
 of ``k2`` until after the first argument (``a``) has been given. With this declaration
 for ``(:~~:)``, the instance for ``HTestEquality`` is accepted.
 
-Another difference between higher-rank kinds and types can be found in their
-treatment of inferred and user-specified type variables. Consider the following
-program: ::
-
-  newtype Foo (f :: forall k. k -> Type) = MkFoo (f Int)
-  data Proxy a = Proxy
-
-  foo :: Foo Proxy
-  foo = MkFoo Proxy
-
-The kind of ``Foo``'s parameter is ``forall k. k -> Type``, but the kind of
-``Proxy`` is ``forall {k}. k -> Type``, where ``{k}`` denotes that the kind
-variable ``k`` is to be inferred, not specified by the user. (See
-:ref:`visible-type-application` for more discussion on the inferred-specified
-distinction). GHC does not consider ``forall k. k -> Type`` and
-``forall {k}. k -> Type`` to be equal at the kind level, and thus rejects
-``Foo Proxy`` as ill-kinded.
-
 The kind ``Type``
 -----------------
 
diff --git a/docs/users_guide/exts/type_applications.rst b/docs/users_guide/exts/type_applications.rst
index c175008617..d86b4854ae 100644
--- a/docs/users_guide/exts/type_applications.rst
+++ b/docs/users_guide/exts/type_applications.rst
@@ -246,8 +246,7 @@ The braces are *not* allowed in the following places:
   explicitly applied. Making them inferred (and thus not appliable) would be
   conflicting.
 
-- In default type signatures for class methods, in SPECIALISE pragmas or in
-  instance declaration heads, e.g.::
+- In SPECIALISE pragmas or in instance declaration heads, e.g.::
 
     instance forall {a}. Eq (Maybe a) where ...
 
@@ -256,3 +255,22 @@ The braces are *not* allowed in the following places:
   could play a role.
 
 - On the left-hand sides of type declarations, such as classes, data types, etc.
+
+Note that while specified and inferred type variables have different properties
+vis-à-vis visible type application, they do not otherwise affect GHC's notion
+of equality over types. For example, given the following definitions: ::
+
+  id1 :: forall a. a -> a
+  id1 x = x
+
+  id2 :: forall {a}. a -> a
+  id2 x = x
+
+  app1 :: (forall a. a -> a) -> b -> b
+  app1 g x = g x
+
+  app2 :: (forall {a}. a -> a) -> b -> b
+  app2 g x = g x
+
+GHC will deem all of ``app1 id1``, ``app1 id2``, ``app2 id1``, and ``app2 id2``
+to be well typed.
diff --git a/testsuite/tests/saks/should_fail/T18863a.hs b/testsuite/tests/saks/should_fail/T18863a.hs
new file mode 100644
index 0000000000..3e7e95047e
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/T18863a.hs
@@ -0,0 +1,9 @@
+{-# Language PolyKinds                #-}
+{-# Language RankNTypes               #-}
+{-# Language StandaloneKindSignatures #-}
+module T18863a where
+
+import Data.Kind
+
+type IDa :: forall i -> i -> Type
+data IDa :: forall i.   i -> Type
diff --git a/testsuite/tests/saks/should_fail/T18863a.stderr b/testsuite/tests/saks/should_fail/T18863a.stderr
new file mode 100644
index 0000000000..8a9de6da6e
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/T18863a.stderr
@@ -0,0 +1,5 @@
+
+T18863a.hs:9:1: error:
+    • Couldn't match expected kind: forall i. i -> *
+                  with actual kind: forall i -> i -> *
+    • In the data type declaration for ‘IDa’
diff --git a/testsuite/tests/saks/should_fail/T18863b.hs b/testsuite/tests/saks/should_fail/T18863b.hs
new file mode 100644
index 0000000000..63f7bb34a9
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/T18863b.hs
@@ -0,0 +1,9 @@
+{-# Language PolyKinds                #-}
+{-# Language RankNTypes               #-}
+{-# Language StandaloneKindSignatures #-}
+module T18863b where
+
+import Data.Kind
+
+type IDb :: forall i.   i -> Type
+data IDb :: forall i -> i -> Type
diff --git a/testsuite/tests/saks/should_fail/T18863b.stderr b/testsuite/tests/saks/should_fail/T18863b.stderr
new file mode 100644
index 0000000000..d1453044c1
--- /dev/null
+++ b/testsuite/tests/saks/should_fail/T18863b.stderr
@@ -0,0 +1,5 @@
+
+T18863b.hs:9:1: error:
+    • Couldn't match expected kind: forall i -> i -> *
+                  with actual kind: i -> *
+    • In the data type declaration for ‘IDb’
diff --git a/testsuite/tests/saks/should_fail/all.T b/testsuite/tests/saks/should_fail/all.T
index d2722fb9c4..7e2194a21f 100644
--- a/testsuite/tests/saks/should_fail/all.T
+++ b/testsuite/tests/saks/should_fail/all.T
@@ -31,3 +31,5 @@ test('T16725', normal, compile_fail, [''])
 test('T16826', normal, compile_fail, [''])
 test('T16756b', normal, compile_fail, [''])
 test('T16758', normal, compile_fail, [''])
+test('T18863a', normal, compile_fail, [''])
+test('T18863b', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_compile/T15079.hs b/testsuite/tests/typecheck/should_compile/T15079.hs
new file mode 100644
index 0000000000..62115182af
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T15079.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T15079 where
+
+import           Data.Kind
+import qualified Data.Type.Equality as Eq
+import           Data.Void
+import           GHC.Exts (Any)
+
+infixl 4 :==
+-- | Heterogeneous Leibnizian equality.
+newtype (a :: j) :== (b :: k)
+  = HRefl { hsubst :: forall (c :: forall (i :: Type). i -> Type). c a -> c b }
+
+-----
+
+newtype Coerce a = Coerce { uncoerce :: Starify a }
+type family Starify (a :: k) :: Type where
+  Starify (a :: Type) = a
+  Starify _           = Void
+
+coerce :: a :== b -> a -> b
+coerce f = uncoerce . hsubst f . Coerce
+
+-----
+
+newtype Flay :: (forall (i :: Type). i -> i -> Type)
+             -> forall (j :: Type). j -> forall (k :: Type). k -> Type where
+  Flay :: forall (p :: forall (i :: Type). i -> i -> Type)
+                 (j :: Type) (k :: Type) (a :: j) (b :: k).
+          { unflay :: p a (MassageKind j b) } -> Flay p a b
+
+type family MassageKind (j :: Type) (a :: k) :: j where
+  MassageKind j (a :: j) = a
+  MassageKind _ _        = Any
+
+fromLeibniz :: forall a b. a :== b -> a Eq.:~: b
+fromLeibniz f = unflay $ hsubst f $ Flay Eq.Refl
+
+-----
+
+newtype Foo (f :: forall (a :: Type). a -> Type) = MkFoo (f Int)
+data InferredProxy a = MkInferredProxy
+
+foo :: Foo InferredProxy
+foo = MkFoo MkInferredProxy
+
+-----
+
+id1 :: forall a. a -> a
+id1 x = x
+
+id2 :: forall {a}. a -> a
+id2 x = x
+
+app1 :: (forall a. a -> a) -> b -> b
+app1 g x = g x
+
+app2 :: (forall {a}. a -> a) -> b -> b
+app2 g x = g x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 953f2489c7..060d179400 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -627,6 +627,7 @@ test('SplitWD', normal, compile, [''])
 #       (2) Build the program twice: once with -dynamic, and then
 #           with -prof using -osuf to set a different object file suffix.
 test('T14441', omit_ways(['profasm']), compile, [''])
+test('T15079', normal, compile, [''])
 test('T15050', normal, compile, [''])
 test('T14735', normal, compile, [''])
 test('T15180', normal, compile, [''])