Use IfaceAppArgs to store an IfaceAppTy's arguments

Summary:
Currently, an `IfaceAppTy` has no way to tell whether its
argument is visible or not, so it simply treats all arguments as
visible, leading to #15330. We already have a solution for this
problem in the form of the `IfaceTcArgs` data structure, used by
`IfaceTyConApp` to represent the arguments to a type constructor.
Therefore, it makes sense to reuse this machinery for `IfaceAppTy`,
so this patch does just that.

This patch:

1. Renames `IfaceTcArgs` to `IfaceAppArgs` to reflect its more
   general purpose.
2. Changes the second field of `IfaceAppTy` from `IfaceType` to
   `IfaceAppArgs`, and propagates the necessary changes through. In
   particular, pretty-printing an `IfaceAppTy` now goes through the
   `IfaceAppArgs` pretty-printer, which correctly displays arguments
   as visible or not for free, fixing #15330.
3. Changes `toIfaceTypeX` and related functions so that when
   converting an `AppTy` to an `IfaceAppTy`, it flattens as many
   argument `AppTy`s as possible, and then converts those arguments
   into an `IfaceAppArgs` list, using the kind of the function
   `Type` as a guide. (Doing so minimizes the number of times we need
   to call `typeKind`, which is more expensive that finding the kind
   of a `TyCon`.)

Test Plan: make test TEST=T15330

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15330

Differential Revision: https://phabricator.haskell.org/D4938

6 files changed, 47 insertions, 21 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T14369.stderr b/testsuite/tests/indexed-types/should_fail/T14369.stderr
index 4cac995464..96e55d2f1e 100644
--- a/testsuite/tests/indexed-types/should_fail/T14369.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T14369.stderr
@@ -1,9 +1,9 @@
 
 T14369.hs:27:5: error:
     • Couldn't match type ‘Demote a’ with ‘Demote a1’
-      Expected type: Sing (x a) -> Maybe (Demote a1)
-        Actual type: Sing (x a) -> Demote (Maybe a)
+      Expected type: Sing x -> Maybe (Demote a1)
+        Actual type: Sing x -> Demote (Maybe a)
     • In the expression: fromSing
       In an equation for ‘f’: f = fromSing
     • Relevant bindings include
-        f :: Sing (x a) -> Maybe (Demote a1) (bound at T14369.hs:27:1)
+        f :: Sing x -> Maybe (Demote a1) (bound at T14369.hs:27:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index b9318940fd..20a0fa51ca 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,13 +1,10 @@
 
 T14040a.hs:34:8: error:
     • Cannot apply expression of type ‘Sing wl
-                                       -> (forall y. p k0 w0 'WeirdNil)
+                                       -> (forall y. p w0 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                                           Sing x
-                                           -> Sing xs
-                                           -> p (WeirdList k1) w1 xs
-                                           -> p k1 w2 ('WeirdCons x xs))
-                                       -> p k2 w3 wl’
+                                           Sing x -> Sing xs -> p w1 xs -> p w2 ('WeirdCons x xs))
+                                       -> p w3 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’
diff --git a/testsuite/tests/typecheck/should_fail/T14350.stderr b/testsuite/tests/typecheck/should_fail/T14350.stderr
index 258518e9be..cbf67b405f 100644
--- a/testsuite/tests/typecheck/should_fail/T14350.stderr
+++ b/testsuite/tests/typecheck/should_fail/T14350.stderr
@@ -1,19 +1,18 @@
 
 T14350.hs:59:15: error:
     • Couldn't match expected type ‘Proxy a2
-                                    -> Apply (Apply (c x3) 'Proxy) (Apply (g x3) 'Proxy)’
-                  with actual type ‘Sing (f x y @@ t0)’
+                                    -> Apply (Apply c 'Proxy) (Apply g 'Proxy)’
+                  with actual type ‘Sing (f @@ t0)’
     • The function ‘applySing’ is applied to three arguments,
-      but its type ‘Sing (f x y) -> Sing t0 -> Sing (f x y @@ t0)’
-      has only two
+      but its type ‘Sing f -> Sing t0 -> Sing (f @@ t0)’ has only two
       In the expression: applySing f Proxy Proxy
       In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
     • Relevant bindings include
         x :: Sing x3 (bound at T14350.hs:59:11)
-        g :: Sing (g x2) (bound at T14350.hs:59:9)
-        f :: Sing (f x1 y) (bound at T14350.hs:59:7)
-        dcomp :: Sing (f x1 y)
-                 -> Sing (g x2) -> Sing x3 -> (c x3 @@ 'Proxy) @@ (g x3 @@ 'Proxy)
+        g :: Sing g (bound at T14350.hs:59:9)
+        f :: Sing f (bound at T14350.hs:59:7)
+        dcomp :: Sing f
+                 -> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
           (bound at T14350.hs:59:1)
 
 T14350.hs:59:27: error:
@@ -24,8 +23,8 @@ T14350.hs:59:27: error:
       In an equation for ‘dcomp’: dcomp f g x = applySing f Proxy Proxy
     • Relevant bindings include
         x :: Sing x3 (bound at T14350.hs:59:11)
-        g :: Sing (g x2) (bound at T14350.hs:59:9)
-        f :: Sing (f x1 y) (bound at T14350.hs:59:7)
-        dcomp :: Sing (f x1 y)
-                 -> Sing (g x2) -> Sing x3 -> (c x3 @@ 'Proxy) @@ (g x3 @@ 'Proxy)
+        g :: Sing g (bound at T14350.hs:59:9)
+        f :: Sing f (bound at T14350.hs:59:7)
+        dcomp :: Sing f
+                 -> Sing g -> Sing x3 -> (c @@ 'Proxy) @@ (g @@ 'Proxy)
           (bound at T14350.hs:59:1)
diff --git a/testsuite/tests/typecheck/should_fail/T15330.hs b/testsuite/tests/typecheck/should_fail/T15330.hs
new file mode 100644
index 0000000000..0041806244
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15330.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T15330 where
+
+import Data.Kind
+import Data.Proxy
+
+data T :: forall a. a -> Type
+
+f1 :: Proxy (T True)
+f1 = "foo"
+
+f2 :: forall (t :: forall a. a -> Type).
+      Proxy (t True)
+f2 = "foo"
diff --git a/testsuite/tests/typecheck/should_fail/T15330.stderr b/testsuite/tests/typecheck/should_fail/T15330.stderr
new file mode 100644
index 0000000000..cef80452a1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T15330.stderr
@@ -0,0 +1,14 @@
+
+T15330.hs:11:6: error:
+    • Couldn't match expected type ‘Proxy (T 'True)’
+                  with actual type ‘[Char]’
+    • In the expression: "foo"
+      In an equation for ‘f1’: f1 = "foo"
+
+T15330.hs:15:6: error:
+    • Couldn't match expected type ‘Proxy (t 'True)’
+                  with actual type ‘[Char]’
+    • In the expression: "foo"
+      In an equation for ‘f2’: f2 = "foo"
+    • Relevant bindings include
+        f2 :: Proxy (t 'True) (bound at T15330.hs:15:1)
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 6a0012700f..b357b55d57 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -474,3 +474,4 @@ test('T14884', normal, compile_fail, [''])
 test('T14904a', normal, compile_fail, [''])
 test('T14904b', normal, compile_fail, [''])
 test('T15067', normal, compile_fail, [''])
+test('T15330', normal, compile_fail, [''])