Fix typechecking of partial type signatures

Partial type sigs had grown hair.  tcHsParialSigType was
doing lots of unnecessary work, and tcInstSig was cloning it
unnecessarily -- and the result didn't even work: #16728.

This patch cleans it all up, described by TcHsType
  Note [Checking parital type signatures]

I basically just deleted code... but very carefully!

Some refactoring along the way

* Distinguish more explicintly between "anonymous" wildcards "_"
  and "named" wildcards "_a".  I changed the names of a number
  of functions to make this distinction much more apparent.

The patch also revealed that the code in `TcExpr`
that implements the special typing rule for `($)` was wrong.
It called `getRuntimeRep` in a situation where where was no
particular reason to suppose that the thing had kind `TYPE r`.

This caused a crash in typecheck/should_run/T10846.

The fix was easy, and actually simplifies the code in `TcExpr`
quite a bit.  Hooray.

8 files changed, 75 insertions, 4 deletions

diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.hs b/testsuite/tests/partial-sigs/should_compile/T16728.hs
new file mode 100644
index 0000000000..f54f17ef56
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Bug where
+
+import Data.Proxy
+
+f :: forall k (x :: k). Proxy (x :: _)
+f = Proxy
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728.stderr b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
new file mode 100644
index 0000000000..6efdae343e
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728.stderr
@@ -0,0 +1,9 @@
+
+T16728.hs:8:37: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘k’
+      Where: ‘k’ is a rigid type variable bound by
+               the inferred type of f :: Proxy x
+               at T16728.hs:9:1-9
+    • In the kind ‘_’
+      In the first argument of ‘Proxy’, namely ‘(x :: _)’
+      In the type ‘Proxy (x :: _)’
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.hs b/testsuite/tests/partial-sigs/should_compile/T16728a.hs
new file mode 100644
index 0000000000..96d693a192
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE ExplicitForAll, PartialTypeSignatures #-}
+module Bug where
+
+g,h:: forall a. a -> _
+g x = h x
+
+h x = g x
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728a.stderr b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
new file mode 100644
index 0000000000..50785ebc1c
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728a.stderr
@@ -0,0 +1,20 @@
+
+T16728a.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred types of
+                 g :: a -> _
+                 h :: a -> _
+               at T16728a.hs:(5,1)-(7,9)
+    • In the type ‘a -> _’
+      In the type signature: g :: forall a. a -> _
+
+T16728a.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘_’
+      Where: ‘_’ is a rigid type variable bound by
+               the inferred types of
+                 g :: a -> _
+                 h :: a -> _
+               at T16728a.hs:(5,1)-(7,9)
+    • In the type ‘a -> _’
+      In the type signature: h :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.hs b/testsuite/tests/partial-sigs/should_compile/T16728b.hs
new file mode 100644
index 0000000000..db1e564a14
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ExplicitForAll, PartialTypeSignatures #-}
+module Bug where
+
+g,h:: forall a. a -> _
+
+g x = x       -- Instantiates the wildcard to 'a'
+
+h x = True    -- Instantiates the wildcard to Bool
+
diff --git a/testsuite/tests/partial-sigs/should_compile/T16728b.stderr b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
new file mode 100644
index 0000000000..712acfe0b9
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_compile/T16728b.stderr
@@ -0,0 +1,13 @@
+
+T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘Bool’
+    • In the type ‘a -> _’
+      In the type signature: h :: forall a. a -> _
+
+T16728b.hs:4:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
+    • Found type wildcard ‘_’ standing for ‘a’
+      Where: ‘a’ is a rigid type variable bound by
+               the inferred type of g :: a -> a
+               at T16728b.hs:6:1-7
+    • In the type ‘a -> _’
+      In the type signature: g :: forall a. a -> _
diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T
index 56d821eca0..4cb12ed144 100644
--- a/testsuite/tests/partial-sigs/should_compile/all.T
+++ b/testsuite/tests/partial-sigs/should_compile/all.T
@@ -92,3 +92,6 @@ test('T15039c', normal, compile, ['-fprint-equality-relations'])
 test('T15039d', normal, compile,
                 ['-fprint-explicit-kinds -fprint-equality-relations'])
 test('T16334', normal, compile, [''])
+test('T16728', normal, compile, [''])
+test('T16728a', normal, compile, [''])
+test('T16728b', normal, compile, [''])
diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
index 0a07f0590d..24782235ba 100644
--- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr
@@ -1,10 +1,10 @@
 
 T14040a.hs:34:8: error:
-    • Cannot apply expression of type ‘Sing wl0
-                                       -> (forall y. p0 _0 'WeirdNil)
+    • Cannot apply expression of type ‘Sing wl
+                                       -> (forall y. p _2 'WeirdNil)
                                        -> (forall z1 (x :: z1) (xs :: WeirdList (WeirdList z1)).
-                                           Sing x -> Sing xs -> p0 _1 xs -> p0 _2 ('WeirdCons x xs))
-                                       -> p0 _3 wl0’
+                                           Sing x -> Sing xs -> p _0 xs -> p _1 ('WeirdCons x xs))
+                                       -> p _2 wl’
       to a visible type argument ‘(WeirdList z)’
     • In the sixth argument of ‘pWeirdCons’, namely
         ‘(elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)’