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.

4 files changed, 39 insertions, 0 deletions

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'])