Make equality constraints in kinds invisible

Issues #12102 and #15872 revealed something strange about the way GHC
handles equality constraints in kinds: it treats them as _visible_
arguments! This causes a litany of strange effects, from strange
error messages
(https://gitlab.haskell.org/ghc/ghc/issues/12102#note_169035)
to bizarre `Eq#`-related things leaking through to GHCi output, even
without any special flags enabled.

This patch is an attempt to contain some of this strangeness.
In particular:

* In `TcHsType.etaExpandAlgTyCon`, we propagate through the
  `AnonArgFlag`s of any `Anon` binders. Previously, we were always
  hard-coding them to `VisArg`, which meant that invisible binders
  (like those whose kinds were equality constraint) would mistakenly
  get flagged as visible.
* In `ToIface.toIfaceAppArgsX`, we previously assumed that the
  argument to a `FunTy` always corresponding to a `Required`
  argument. We now dispatch on the `FunTy`'s `AnonArgFlag` and map
  `VisArg` to `Required` and `InvisArg` to `Inferred`. As a
  consequence, the iface pretty-printer correctly recognizes that
  equality coercions are inferred arguments, and as a result,
  only displays them in `-fprint-explicit-kinds` is enabled.
* Speaking of iface pretty-printing, `Anon InvisArg` binders were
  previously being pretty-printed like `T (a :: b ~ c)`, as if they
  were required. This seemed inconsistent with other invisible
  arguments (that are printed like `T @{d}`), so I decided to switch
  this to `T @{a :: b ~ c}`.

Along the way, I also cleaned up a minor inaccuracy in the users'
guide section for constraints in kinds that was spotted in
https://gitlab.haskell.org/ghc/ghc/issues/12102#note_136220.

Fixes #12102 and #15872.

12 files changed, 100 insertions, 16 deletions

diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 4488aef025..298e14e463 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -719,8 +719,9 @@ pprIfaceTyConBinders = sep . map go
       -- See Note [Pretty-printing invisible arguments]
       case vis of
         AnonTCB  VisArg    -> ppr_bndr True
-        AnonTCB  InvisArg  -> ppr_bndr True  -- Rare; just promoted GADT data constructors
-                                             -- Should we print them differently?
+        AnonTCB  InvisArg  -> char '@' <> braces (ppr_bndr False)
+          -- The above case is rare. (See Note [AnonTCB InvisArg] in TyCon.)
+          -- Should we print these differently?
         NamedTCB Required  -> ppr_bndr True
         NamedTCB Specified -> char '@' <> ppr_bndr True
         NamedTCB Inferred  -> char '@' <> braces (ppr_bndr False)
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index aa4e53cfb4..535c1080f2 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -309,8 +309,14 @@ toIfaceAppArgsX fr kind ty_args
         t'  = toIfaceTypeX fr t
         ts' = go (extendTCvSubst env tv t) res ts
 
-    go env (FunTy { ft_res = res }) (t:ts) -- No type-class args in tycon apps
-      = IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
+    go env (FunTy { ft_af = af, ft_res = res }) (t:ts)
+      = IA_Arg (toIfaceTypeX fr t) argf (go env res ts)
+      where
+        argf = case af of
+                 VisArg   -> Required
+                 InvisArg -> Inferred
+                   -- It's rare for a kind to have a constraint argument, but
+                   -- it can happen. See Note [AnonTCB InvisArg] in TyCon.
 
     go env ty ts@(t1:ts1)
       | not (isEmptyTCvSubst env)
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index e0bf2552d3..c58a585356 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -2368,13 +2368,13 @@ etaExpandAlgTyCon tc_bndrs kind
       = case splitPiTy_maybe kind of
           Nothing -> (reverse acc, substTy subst kind)
 
-          Just (Anon _ arg, kind')
+          Just (Anon af arg, kind')
             -> go loc occs' uniqs' subst' (tcb : acc) kind'
             where
               arg'   = substTy subst arg
               tv     = mkTyVar (mkInternalName uniq occ loc) arg'
               subst' = extendTCvInScope subst tv
-              tcb    = Bndr tv (AnonTCB VisArg)
+              tcb    = Bndr tv (AnonTCB af)
               (uniq:uniqs') = uniqs
               (occ:occs')   = occs
 
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index e55cf8b2a3..cdfcf181a5 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -487,14 +487,22 @@ tyConVisibleTyVars tc
   = [ tv | Bndr tv vis <- tyConBinders tc
          , isVisibleTcbVis vis ]
 
-{- Note [AnonTCB InivsArg]
+{- Note [AnonTCB InvisArg]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's pretty rare to have an (AnonTCB InvisArg) binder.  The
-only way it can occur is in a PromotedDataCon whose
-kind has an equality constraint:
-  'MkT :: forall a b. (a~b) => blah
-See Note [Constraints in kinds] in TyCoRep, and
-Note [Promoted data constructors] in this module.
+only way it can occur is through equality constraints in kinds. These
+can arise in one of two ways:
+
+* In a PromotedDataCon whose kind has an equality constraint:
+
+    'MkT :: forall a b. (a~b) => blah
+
+  See Note [Constraints in kinds] in TyCoRep, and
+  Note [Promoted data constructors] in this module.
+* In a data type whose kind has an equality constraint, as in the
+  following example from #12102:
+
+    data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type
 
 When mapping an (AnonTCB InvisArg) to an ArgFlag, in
 tyConBndrVisArgFlag, we use "Inferred" to mean "the user cannot
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 781a10691e..c86f30d00b 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -9395,7 +9395,8 @@ Here is an example of a constrained kind: ::
 The declarations above are accepted. However, if we add ``MkOther :: T Int``,
 we get an error that the equality constraint is not satisfied; ``Int`` is
 not a type literal. Note that explicitly quantifying with ``forall a`` is
-not necessary here.
+necessary in order for ``T`` to typecheck
+(see :ref:`complete-kind-signatures`).
 
 The kind ``Type``
 -----------------
@@ -10351,13 +10352,13 @@ function that can *never* be called, such as this one: ::
       f :: (Int ~ Bool) => a -> a
 
 Sometimes :extension:`AllowAmbiguousTypes` does not mix well with :extension:`RankNTypes`.
-For example: :: 
+For example: ::
       foo :: forall r. (forall i. (KnownNat i) => r) -> r
       foo f = f @1
 
       boo :: forall j. (KnownNat j) => Int
       boo = ....
-          
+
       h :: Int
       h = foo boo
 
@@ -10367,7 +10368,7 @@ the type variables `j` and `i`.
 Unlike the previous examples, it is not currently possible
 to resolve the ambiguity manually by using :extension:`TypeApplications`.
 
-       
+
 .. note::
     *A historical note.* GHC used to impose some more restrictive and less
     principled conditions on type signatures. For type
diff --git a/testsuite/tests/ghci/scripts/T15872.hs b/testsuite/tests/ghci/scripts/T15872.hs
new file mode 100644
index 0000000000..0f53a327b6
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15872.hs
@@ -0,0 +1,12 @@
+{-# Language RankNTypes #-}
+{-# Language DataKinds  #-}
+{-# Language PolyKinds  #-}
+{-# Language GADTs      #-}
+module T15872 where
+
+import Data.Kind
+
+data WHICH = OP | OPOP
+
+data Fun :: forall (a :: WHICH). a ~ OP => Type -> Type -> Type where
+  MkFun :: (a -> b) -> Fun a b
diff --git a/testsuite/tests/ghci/scripts/T15872.script b/testsuite/tests/ghci/scripts/T15872.script
new file mode 100644
index 0000000000..9a60bbd5f8
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15872.script
@@ -0,0 +1,10 @@
+:l T15872
+
+:t MkFun
+:k Fun
+:i Fun
+
+:set -fprint-explicit-kinds
+:t MkFun
+:k Fun
+:i Fun
diff --git a/testsuite/tests/ghci/scripts/T15872.stdout b/testsuite/tests/ghci/scripts/T15872.stdout
new file mode 100644
index 0000000000..623631162a
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15872.stdout
@@ -0,0 +1,16 @@
+MkFun :: (a -> b) -> Fun a b
+Fun :: (a ~ 'OP) => * -> * -> *
+data Fun b c where
+  MkFun :: (b -> c) -> Fun b c
+  	-- Defined at T15872.hs:11:1
+MkFun
+  :: (a -> b) -> Fun @'OP @{'GHC.Types.Eq# @WHICH @'OP @'OP <>} a b
+Fun :: ((a :: WHICH) ~ ('OP :: WHICH)) => * -> * -> *
+type role Fun nominal nominal representational representational
+data Fun @(a :: WHICH)
+         @{a1 :: (a :: WHICH) ~ ('OP :: WHICH)}
+         b
+         c where
+  MkFun :: (b -> c)
+           -> Fun @'OP @{'GHC.Types.Eq# @WHICH @'OP @'OP <>} b c
+  	-- Defined at T15872.hs:11:1
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index c2d9d9fc6e..53b4f26cb6 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -287,6 +287,7 @@ test('T15325', normal, ghci_script, ['T15325.script'])
 test('T15591', normal, ghci_script, ['T15591.script'])
 test('T15743b', normal, ghci_script, ['T15743b.script'])
 test('T15827', normal, ghci_script, ['T15827.script'])
+test('T15872', normal, ghci_script, ['T15872.script'])
 test('T15898', normal, ghci_script, ['T15898.script'])
 test('T15941', normal, ghci_script, ['T15941.script'])
 test('T16030', normal, ghci_script, ['T16030.script'])
diff --git a/testsuite/tests/typecheck/should_fail/T12102b.hs b/testsuite/tests/typecheck/should_fail/T12102b.hs
new file mode 100644
index 0000000000..8478059c8f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12102b.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+module T12102b where
+
+import Data.Kind
+import GHC.TypeLits
+
+type family IsTypeLit a where
+  IsTypeLit Nat    = 'True
+  IsTypeLit Symbol = 'True
+  IsTypeLit a      = 'False
+
+data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
+  MkNat    :: T 42
+  MkSymbol :: T "Don't panic!"
+
+deriving instance Show (T a)
diff --git a/testsuite/tests/typecheck/should_fail/T12102b.stderr b/testsuite/tests/typecheck/should_fail/T12102b.stderr
new file mode 100644
index 0000000000..d93b7fda9c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12102b.stderr
@@ -0,0 +1,7 @@
+
+T12102b.hs:21:25: error:
+    • Couldn't match expected kind ‘'True’
+                  with actual kind ‘IsTypeLit a0’
+      The type variable ‘a0’ is ambiguous
+    • In the first argument of ‘Show’, namely ‘(T a)’
+      In the stand-alone deriving instance for ‘Show (T a)’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index d155ca0e8c..fec3a3ae67 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -411,6 +411,7 @@ test('T12083a', normal, compile_fail, [''])
 test('T12083b', normal, compile_fail, [''])
 test('T11974b', normal, compile_fail, [''])
 test('T12102', normal, compile, [''])
+test('T12102b', normal, compile_fail, [''])
 test('T12151', normal, compile_fail, [''])
 test('T7437', normal, compile_fail, [''])
 test('T12177', normal, compile_fail, [''])