Fix #13819 by refactoring TypeEqOrigin.uo_thing

The uo_thing field of TypeEqOrigin is used to track the
"thing" (either term or type) that has the type (kind) stored
in the TypeEqOrigin fields. Previously, this was sometimes a
proper Core Type, which needed zonking and tidying. Now, it
is only HsSyn: much simpler, and the error messages now use
the user-written syntax.

But this aspect of uo_thing didn't cause #13819; it was the
sibling field uo_arity that did. uo_arity stored the number
of arguments of uo_thing, useful when reporting something
like "should have written 2 fewer arguments". We wouldn't want
to say that if the thing didn't have two arguments. However,
in practice, GHC was getting this wrong, and this message
didn't seem all that helpful. Furthermore, the calculation
of the number of arguments is what caused #13819 to fall over.
This patch just removes uo_arity. In my opinion, the change
to error messages is a nudge in the right direction.

Test case: typecheck/should_fail/T13819

24 files changed, 74 insertions, 77 deletions

diff --git a/testsuite/tests/indexed-types/should_fail/T12867.stderr b/testsuite/tests/indexed-types/should_fail/T12867.stderr
index 40e566b3ec..2115e43541 100644
--- a/testsuite/tests/indexed-types/should_fail/T12867.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T12867.stderr
@@ -1,7 +1,6 @@
 
 T12867.hs:7:21: error:
-    • Expecting one fewer arguments to ‘TestM’
-      Expected kind ‘k0 -> *’, but ‘TestM’ has kind ‘*’
+    • Expected kind ‘k0 -> *’, but ‘TestM’ has kind ‘*’
     • In the first argument of ‘Eq’, namely ‘(TestM a)’
       In the type ‘(Eq (TestM a))’
       In the type declaration for ‘Test2’
diff --git a/testsuite/tests/polykinds/T12593.stderr b/testsuite/tests/polykinds/T12593.stderr
index 0a1b83ad9e..4dda0cddd5 100644
--- a/testsuite/tests/polykinds/T12593.stderr
+++ b/testsuite/tests/polykinds/T12593.stderr
@@ -1,7 +1,6 @@
 
 T12593.hs:11:16: error:
-    • Expecting two fewer arguments to ‘Free k k4 k5 p’
-      Expected kind ‘k0 -> k1 -> *’, but ‘Free k k4 k5 p’ has kind ‘*’
+    • Expected kind ‘k0 -> k1 -> *’, but ‘Free k k1 k2 p’ has kind ‘*’
     • In the type signature:
         run :: k2 q =>
                Free k k1 k2 p a b
@@ -20,9 +19,9 @@ T12593.hs:12:31: error:
                -> (forall (c :: k) (d :: k1). p c d -> q c d) -> q a b
 
 T12593.hs:12:40: error:
-    • Expecting two more arguments to ‘k4’
+    • Expecting two more arguments to ‘k1’
       Expected a type, but
-      ‘k4’ has kind
+      ‘k1’ has kind
       ‘((k0 -> k1 -> *) -> Constraint) -> (k2 -> k3 -> *) -> *’
     • In the kind ‘k1’
       In the type signature:
diff --git a/testsuite/tests/polykinds/T6039.stderr b/testsuite/tests/polykinds/T6039.stderr
index 4c31bb4aa4..048efd538f 100644
--- a/testsuite/tests/polykinds/T6039.stderr
+++ b/testsuite/tests/polykinds/T6039.stderr
@@ -1,5 +1,4 @@
 
 T6039.hs:5:14: error:
-    • Expecting one fewer arguments to ‘j’
-      Expected kind ‘* -> *’, but ‘j’ has kind ‘*’
+    • Expected kind ‘* -> *’, but ‘j’ has kind ‘*’
     • In the kind ‘j k’
diff --git a/testsuite/tests/polykinds/T7278.stderr b/testsuite/tests/polykinds/T7278.stderr
index 676be2cb0f..265e27892b 100644
--- a/testsuite/tests/polykinds/T7278.stderr
+++ b/testsuite/tests/polykinds/T7278.stderr
@@ -1,6 +1,5 @@
 
 T7278.hs:9:43: error:
-    • Expecting two fewer arguments to ‘t’
-      Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’
+    • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’
     • In the type signature:
         f :: (C (t :: k) (TF t)) => TF t p1 p0 -> t p1 p0
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 00c9c6328e..6249bf7b62 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -1,6 +1,6 @@
 
 T8616.hs:8:29: error:
-    • Expected a type, but ‘Any’ has kind ‘k’
+    • Expected a type, but ‘(Any :: k)’ has kind ‘k’
     • In an expression type signature: (Any :: k)
       In the expression: undefined :: (Any :: k)
       In an equation for ‘withSomeSing’:
diff --git a/testsuite/tests/polykinds/T9200b.stderr b/testsuite/tests/polykinds/T9200b.stderr
index 22f9df73f1..7c3cb65bd0 100644
--- a/testsuite/tests/polykinds/T9200b.stderr
+++ b/testsuite/tests/polykinds/T9200b.stderr
@@ -1,5 +1,5 @@
 
 T9200b.hs:8:5: error:
-    Expected kind ‘k’, but ‘'True’ has kind ‘Bool’
-    In the first argument of ‘F’, namely ‘True’
-    In the type family declaration for ‘F’
+    • Expected kind ‘k’, but ‘True’ has kind ‘Bool’
+    • In the first argument of ‘F’, namely ‘True’
+      In the type family declaration for ‘F’
diff --git a/testsuite/tests/rename/should_fail/rnfail026.stderr b/testsuite/tests/rename/should_fail/rnfail026.stderr
index dc6ee9691a..8bd80b1b58 100644
--- a/testsuite/tests/rename/should_fail/rnfail026.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail026.stderr
@@ -1,7 +1,6 @@
 
 rnfail026.hs:16:27: error:
-    • Expecting one fewer arguments to ‘Set a’
-      Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
+    • Expected kind ‘* -> *’, but ‘Set a’ has kind ‘*’
     • In the first argument of ‘Monad’, namely
         ‘(forall a. Eq a => Set a)’
       In the instance declaration for ‘Monad (forall a. Eq a => Set a)’
diff --git a/testsuite/tests/th/T3177a.stderr b/testsuite/tests/th/T3177a.stderr
index e2e8cadbdc..d68be6d1fc 100644
--- a/testsuite/tests/th/T3177a.stderr
+++ b/testsuite/tests/th/T3177a.stderr
@@ -1,10 +1,8 @@
 
 T3177a.hs:8:8: error:
-    • Expecting one fewer arguments to ‘Int’
-      Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the type signature: f :: (Int Int)
 
 T3177a.hs:11:6: error:
-    • Expecting one fewer arguments to ‘Int’
-      Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the type signature: g :: Int Int
diff --git a/testsuite/tests/typecheck/should_fail/T11356.stderr b/testsuite/tests/typecheck/should_fail/T11356.stderr
index aa1db97c62..e0224022a2 100644
--- a/testsuite/tests/typecheck/should_fail/T11356.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11356.stderr
@@ -1,5 +1,4 @@
 
 T11356.hs:3:7: error:
-    • Expecting one fewer arguments to ‘T p’
-      Expected kind ‘k0 -> Constraint’, but ‘T p’ has kind ‘Constraint’
+    • Expected kind ‘k0 -> Constraint’, but ‘T p’ has kind ‘Constraint’
     • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_fail/T11672.stderr b/testsuite/tests/typecheck/should_fail/T11672.stderr
index d08acba037..16eb31042f 100644
--- a/testsuite/tests/typecheck/should_fail/T11672.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11672.stderr
@@ -1,6 +1,6 @@
 
 T11672.hs:9:10: error:
-    • Couldn't match kind ‘Symbol’ with ‘*’
+    • Couldn't match kind ‘*’ with ‘Symbol’
       When matching types
         a0 :: Symbol
         Int -> Bool :: *
@@ -10,12 +10,3 @@ T11672.hs:9:10: error:
         ‘(Proxy :: Proxy (Int -> Bool))’
       In the expression: f (Proxy :: Proxy (Int -> Bool))
       In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))
-
-T11672.hs:9:10: error:
-    • Couldn't match type ‘*’ with ‘Symbol’
-      Expected type: Proxy a0
-        Actual type: Proxy (Int -> Bool)
-    • In the first argument of ‘f’, namely
-        ‘(Proxy :: Proxy (Int -> Bool))’
-      In the expression: f (Proxy :: Proxy (Int -> Bool))
-      In an equation for ‘f’: f _ = f (Proxy :: Proxy (Int -> Bool))
diff --git a/testsuite/tests/typecheck/should_fail/T12785b.stderr b/testsuite/tests/typecheck/should_fail/T12785b.stderr
index 1b1d1bc569..b8e572d6e2 100644
--- a/testsuite/tests/typecheck/should_fail/T12785b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12785b.stderr
@@ -8,6 +8,12 @@ T12785b.hs:29:63: error:
                              a -> HTree n (HTree ('S n) a) -> HTree ('S n) a,
                  in an equation for ‘nest’
         at T12785b.hs:29:7-51
+      ‘s’ is a rigid type variable bound by
+        a pattern with constructor:
+          Hide :: forall a (n :: Peano) (f :: a -> *) (s :: HTree n a).
+                  STree n a f s -> Hidden n f,
+        in an equation for ‘nest’
+        at T12785b.hs:29:7-12
     • In the second argument of ‘($)’, namely ‘a `SBranchX` tr’
       In the expression: Hide $ a `SBranchX` tr
       In an equation for ‘nest’:
diff --git a/testsuite/tests/typecheck/should_fail/T13819.hs b/testsuite/tests/typecheck/should_fail/T13819.hs
new file mode 100644
index 0000000000..5244ddc840
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13819.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DeriveFunctor, TypeApplications #-}
+
+module T13819 where
+
+import Data.Coerce
+import Control.Applicative
+
+newtype A a = A (IO a)
+  deriving Functor
+
+instance Applicative A where
+  pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
+
+instance Monad A where
diff --git a/testsuite/tests/typecheck/should_fail/T13819.stderr b/testsuite/tests/typecheck/should_fail/T13819.stderr
new file mode 100644
index 0000000000..ab818f399b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13819.stderr
@@ -0,0 +1,18 @@
+
+T13819.hs:12:10: error:
+    • Couldn't match type ‘w0 -> A w0’ with ‘A a’
+      Expected type: a -> A a
+        Actual type: (w1 -> WrappedMonad A w2) (w0 -> A w0)
+    • In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
+      In an equation for ‘pure’:
+          pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
+      In the instance declaration for ‘Applicative A’
+    • Relevant bindings include
+        pure :: a -> A a (bound at T13819.hs:12:3)
+
+T13819.hs:12:17: error:
+    • Expected kind ‘* -> *’, but ‘_ -> WrappedMonad A _’ has kind ‘*’
+    • In the type ‘(_ -> WrappedMonad A _)’
+      In the expression: pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
+      In an equation for ‘pure’:
+          pure = pure @(_ -> WrappedMonad A _) @(_ -> A _) pure
diff --git a/testsuite/tests/typecheck/should_fail/T2994.stderr b/testsuite/tests/typecheck/should_fail/T2994.stderr
index 4777e486e6..7f20acf5aa 100644
--- a/testsuite/tests/typecheck/should_fail/T2994.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2994.stderr
@@ -18,7 +18,6 @@ T2994.hs:13:23: error:
       In the instance declaration for ‘MonadReader (Reader' r)’
 
 T2994.hs:15:10: error:
-    • Expecting one fewer arguments to ‘MonadReader r r’
-      Expected kind ‘(* -> *) -> Constraint’,
+    • Expected kind ‘(* -> *) -> Constraint’,
         but ‘MonadReader r r’ has kind ‘Constraint’
     • In the instance declaration for ‘MonadReader r r (Reader' r)’
diff --git a/testsuite/tests/typecheck/should_fail/T3540.stderr b/testsuite/tests/typecheck/should_fail/T3540.stderr
index 1723e86bbe..0fdb88b313 100644
--- a/testsuite/tests/typecheck/should_fail/T3540.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3540.stderr
@@ -12,7 +12,7 @@ T3540.hs:10:13: error:
     • In the type signature: thing2 :: (a ~ Int) -> Int
 
 T3540.hs:13:12: error:
-    • Expected a type, but ‘?dude::Int’ has kind ‘Constraint’
+    • Expected a type, but ‘?dude :: Int’ has kind ‘Constraint’
     • In the type signature: thing3 :: (?dude :: Int) -> Int
 
 T3540.hs:16:11: error:
diff --git a/testsuite/tests/typecheck/should_fail/T4875.stderr b/testsuite/tests/typecheck/should_fail/T4875.stderr
index 782b0969d5..48808e319c 100644
--- a/testsuite/tests/typecheck/should_fail/T4875.stderr
+++ b/testsuite/tests/typecheck/should_fail/T4875.stderr
@@ -1,7 +1,5 @@
 
 T4875.hs:27:24: error:
-    • Expecting one fewer arguments to ‘r’
-      Expected kind ‘* -> *’, but ‘r’ has kind ‘*’
-    • In the type signature:
-        multiplicities :: r c -> [c]
+    • Expected kind ‘* -> *’, but ‘r’ has kind ‘*’
+    • In the type signature: multiplicities :: r c -> [c]
       In the class declaration for ‘Morphic’
diff --git a/testsuite/tests/typecheck/should_fail/T7609.stderr b/testsuite/tests/typecheck/should_fail/T7609.stderr
index 24339311b8..32bc980fe9 100644
--- a/testsuite/tests/typecheck/should_fail/T7609.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7609.stderr
@@ -2,16 +2,13 @@
 T7609.hs:7:16: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        f :: (a `X` a, Maybe)
+    • In the type signature: f :: (a `X` a, Maybe)
 
 T7609.hs:10:7: error:
-    • Expected a constraint, but ‘X a a’ has kind ‘*’
-    • In the type signature:
-        g :: (a `X` a) => Maybe
+    • Expected a constraint, but ‘a `X` a’ has kind ‘*’
+    • In the type signature: g :: (a `X` a) => Maybe
 
 T7609.hs:10:19: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        g :: (a `X` a) => Maybe
+    • In the type signature: g :: (a `X` a) => Maybe
diff --git a/testsuite/tests/typecheck/should_fail/T7778.stderr b/testsuite/tests/typecheck/should_fail/T7778.stderr
index 2db22e95ff..a0f10fcd92 100644
--- a/testsuite/tests/typecheck/should_fail/T7778.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7778.stderr
@@ -1,12 +1,10 @@
 
 T7778.hs:3:7: error:
-    • Expecting one fewer arguments to ‘Num Int => Num’
-      Expected kind ‘* -> Constraint’, but ‘Num Int => Num’ has kind ‘*’
-    • In the type signature:
-        v :: ((Num Int => Num) ()) => ()
+    • Expected kind ‘* -> Constraint’,
+        but ‘Num Int => Num’ has kind ‘*’
+    • In the type signature: v :: ((Num Int => Num) ()) => ()
 
 T7778.hs:3:19: error:
     • Expecting one more argument to ‘Num’
       Expected a type, but ‘Num’ has kind ‘* -> Constraint’
-    • In the type signature:
-        v :: ((Num Int => Num) ()) => ()
+    • In the type signature: v :: ((Num Int => Num) ()) => ()
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 4a1d74877b..58ae57f53e 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -450,4 +450,5 @@ test('T13530', normal, compile_fail, [''])
 test('T12373', normal, compile_fail, [''])
 test('T13610', normal, compile_fail, [''])
 test('T11672', normal, compile_fail, [''])
+test('T13819', normal, compile_fail, [''])
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail070.stderr b/testsuite/tests/typecheck/should_fail/tcfail070.stderr
index 0219626375..3f7bc90d8a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail070.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail070.stderr
@@ -1,6 +1,5 @@
 
 tcfail070.hs:15:15: error:
-    • Expecting one fewer arguments to ‘[Int]’
-      Expected kind ‘* -> k0’, but ‘[Int]’ has kind ‘*’
+    • Expected kind ‘* -> k0’, but ‘[Int]’ has kind ‘*’
     • In the type ‘([Int] Bool)’
       In the type declaration for ‘State’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail078.stderr b/testsuite/tests/typecheck/should_fail/tcfail078.stderr
index 8a94f7c4e4..014d589bf6 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail078.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail078.stderr
@@ -1,6 +1,4 @@
 
 tcfail078.hs:5:6: error:
-    • Expecting one fewer arguments to ‘Integer’
-      Expected kind ‘* -> Constraint’, but ‘Integer’ has kind ‘*’
-    • In the type signature:
-        f :: Integer i => i
+    • Expected kind ‘* -> Constraint’, but ‘Integer’ has kind ‘*’
+    • In the type signature: f :: Integer i => i
diff --git a/testsuite/tests/typecheck/should_fail/tcfail113.stderr b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
index 410ce3daac..fbdffa5ab9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail113.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail113.stderr
@@ -2,17 +2,13 @@
 tcfail113.hs:12:7: error:
     • Expecting one more argument to ‘Maybe’
       Expected a type, but ‘Maybe’ has kind ‘* -> *’
-    • In the type signature:
-        f :: [Maybe]
+    • In the type signature: f :: [Maybe]
 
 tcfail113.hs:15:8: error:
     • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
     • In the first argument of ‘T’, namely ‘Int’
-      In the type signature:
-        g :: T Int
+      In the type signature: g :: T Int
 
 tcfail113.hs:18:6: error:
-    • Expecting one fewer arguments to ‘Int’
-      Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
-    • In the type signature:
-        h :: Int Int
+    • Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’
+    • In the type signature: h :: Int Int
diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
index ad512e102e..7089810e7c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
@@ -7,12 +7,3 @@ tcfail123.hs:11:9: error:
     • In the first argument of ‘f’, namely ‘3#’
       In the expression: f 3#
       In an equation for ‘h’: h v = f 3#
-
-tcfail123.hs:11:9: error:
-    • Couldn't match a lifted type with an unlifted type
-      When matching types
-        p0 :: *
-        GHC.Prim.Int# :: TYPE 'GHC.Types.IntRep
-    • In the first argument of ‘f’, namely ‘3#’
-      In the expression: f 3#
-      In an equation for ‘h’: h v = f 3#
diff --git a/testsuite/tests/typecheck/should_fail/tcfail132.stderr b/testsuite/tests/typecheck/should_fail/tcfail132.stderr
index 3f8f226468..2e0a13c844 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail132.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail132.stderr
@@ -1,7 +1,6 @@
 
 tcfail132.hs:17:37: error:
-    • Expecting one fewer arguments to ‘Object f' f t’
-      Expected kind ‘* -> * -> * -> *’,
+    • Expected kind ‘* -> * -> * -> *’,
         but ‘Object f' f t’ has kind ‘* -> * -> *’
     • In the first argument of ‘T’, namely ‘(Object f' f t)’
       In the type ‘T (Object f' f t) (DUnit t)’