Unify result type earlier to improve error messages

Ticket #19364 helpfully points out that we do not currently take
advantage of pushing the result type of an application into the
arguments.  This makes error messages notably less good.

The fix is rather easy: move the result-type unification step earlier.
It's even a bit more efficient; in the the checking case we now
do one less zonk.

See Note [Unify with expected type before typechecking arguments]
in GHC.Tc.Gen.App

This change generally improves error messages, but it made one worse:
typecheck/should_fail/T16204c. That led me to the realisation that
a good error can be replaced by a less-good one, which provoked
me to change GHC.Tc.Solver.Interact.inertsCanDischarge.  It's
explained in the new Note [Combining equalities]

One other refactoring: I discovered that KindEqOrigin didn't need a
Maybe in its type -- a nice simplification.

7 files changed, 46 insertions, 36 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/T12538.stderr b/testsuite/tests/indexed-types/should_compile/T12538.stderr
index 7a26b9c483..7de8f787af 100644
--- a/testsuite/tests/indexed-types/should_compile/T12538.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T12538.stderr
@@ -3,12 +3,12 @@ T12538.hs:37:8: error:
     • Could not deduce: a' ~ Tagged Int a
       from the context: (TagImpl a a', b ~ DF a')
         bound by the instance declaration at T12538.hs:36:10-46
-      Expected: a -> b
-        Actual: a -> DF (Tagged Int a)
+      Expected: Tagged Int a -> b
+        Actual: Tagged Int a -> DF (Tagged Int a)
       ‘a'’ is a rigid type variable bound by
         the instance declaration
         at T12538.hs:36:10-46
-    • In the expression: DF . tag
+    • In the first argument of ‘(.)’, namely ‘DF’
+      In the expression: DF . tag
       In an equation for ‘df’: df = DF . tag
-      In the instance declaration for ‘ToDF a b’
     • Relevant bindings include df :: a -> b (bound at T12538.hs:37:3)
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
index ce087941ea..7968dc3dda 100644
--- a/testsuite/tests/indexed-types/should_fail/T15870.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -1,6 +1,9 @@
 
 T15870.hs:32:34: error:
     • Couldn't match kind ‘k’ with ‘*’
+      When matching kinds
+        b :: *
+        a :: k
       Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
       ‘k’ is a rigid type variable bound by
         a family instance declaration
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 721267e75d..be58f59e05 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,13 +1,26 @@
 
-T2544.hs:19:12: error:
+T2544.hs:19:18: error:
+    • Couldn't match type: IxMap i0
+                     with: IxMap l
+      Expected: IxMap l [Int]
+        Actual: IxMap i0 [Int]
+      NB: ‘IxMap’ is a non-injective type family
+      The type variable ‘i0’ is ambiguous
+    • In the first argument of ‘BiApp’, namely ‘empty’
+      In the expression: BiApp empty empty
+      In an equation for ‘empty’: empty = BiApp empty empty
+    • Relevant bindings include
+        empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
+
+T2544.hs:19:24: error:
     • Couldn't match type: IxMap i1
                      with: IxMap r
-      Expected: IxMap (l :|: r) [Int]
-        Actual: BiApp (IxMap i0) (IxMap i1) [Int]
+      Expected: IxMap r [Int]
+        Actual: IxMap i1 [Int]
       NB: ‘IxMap’ is a non-injective type family
       The type variable ‘i1’ is ambiguous
-    • In the expression: BiApp empty empty
+    • In the second argument of ‘BiApp’, namely ‘empty’
+      In the expression: BiApp empty empty
       In an equation for ‘empty’: empty = BiApp empty empty
-      In the instance declaration for ‘Ix (l :|: r)’
     • Relevant bindings include
         empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index 64fa851258..deaffc82dd 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -1,30 +1,22 @@
 
-T2664.hs:31:9: error:
-    • Could not deduce: Dual a ~ Dual b
+T2664.hs:31:52: error:
+    • Could not deduce: b ~ a arising from a use of ‘newPChan’
       from the context: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b))
         bound by the type signature for:
                    newPChan :: forall c.
                                ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
                                IO (PChan (a :*: b), PChan c)
         at T2664.hs:23:5-12
-      Expected: IO (PChan (a :*: b), PChan c)
-        Actual: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
-      NB: ‘Dual’ is a non-injective type family
-    • In a stmt of a 'do' block:
-        return
-          (O $ takeMVar v, 
-           E (pchoose Right v newPChan) (pchoose Left v newPChan))
+      ‘b’ is a rigid type variable bound by
+        the instance declaration
+        at T2664.hs:22:10-52
+      ‘a’ is a rigid type variable bound by
+        the instance declaration
+        at T2664.hs:22:10-52
+    • In the third argument of ‘pchoose’, namely ‘newPChan’
+      In the first argument of ‘E’, namely ‘(pchoose Right v newPChan)’
       In the expression:
-        do v <- newEmptyMVar
-           return
-             (O $ takeMVar v, 
-              E (pchoose Right v newPChan) (pchoose Left v newPChan))
-      In an equation for ‘newPChan’:
-          newPChan
-            = do v <- newEmptyMVar
-                 return
-                   (O $ takeMVar v, 
-                    E (pchoose Right v newPChan) (pchoose Left v newPChan))
+        E (pchoose Right v newPChan) (pchoose Left v newPChan)
     • Relevant bindings include
         v :: MVar (Either (PChan a) (PChan b)) (bound at T2664.hs:24:9)
         newPChan :: IO (PChan (a :*: b), PChan c) (bound at T2664.hs:23:5)
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index c921445d2e..69df514c0f 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,16 +1,17 @@
 
-T4272.hs:15:19: error:
-    • Couldn't match expected type ‘TermFamily a a’
-                  with actual type ‘a’
+T4272.hs:15:26: error:
+    • Couldn't match type ‘a’ with ‘TermFamily a a’
+      Expected: TermFamily a (TermFamily a a)
+        Actual: TermFamily a a
       ‘a’ is a rigid type variable bound by
         the type signature for:
           laws :: forall a b. TermLike a => TermFamily a a -> b
         at T4272.hs:14:1-53
-    • In the second argument of ‘prune’, namely
+    • In the first argument of ‘terms’, namely
+        ‘(undefined :: TermFamily a a)’
+      In the second argument of ‘prune’, namely
         ‘(terms (undefined :: TermFamily a a))’
       In the expression: prune t (terms (undefined :: TermFamily a a))
-      In an equation for ‘laws’:
-          laws t = prune t (terms (undefined :: TermFamily a a))
     • Relevant bindings include
         t :: TermFamily a a (bound at T4272.hs:15:6)
         laws :: TermFamily a a -> b (bound at T4272.hs:15:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index 5dcce91edb..c7f230654e 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -3,7 +3,8 @@ T5439.hs:82:33: error:
     • Couldn't match expected type: Attempt (HElemOf rs)
                   with actual type: Attempt (HHead (HDrop n0 l0))
                                     -> Attempt (HElemOf l0)
-    • In the second argument of ‘($)’, namely
+    • Probable cause: ‘($)’ is applied to too few arguments
+      In the second argument of ‘($)’, namely
         ‘inj $ Failure (e :: SomeException)’
       In a stmt of a 'do' block:
         c <- complete ev $ inj $ Failure (e :: SomeException)
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 04acdc653d..e2f7597b93 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -2,7 +2,7 @@
 T9662.hs:49:8: error:
     • Couldn't match type ‘n’ with ‘Int’
       Expected: Exp (((sh :. k) :. m) :. n)
-                -> Exp (((sh :. k) :. m) :. n)
+                -> Exp (((sh :. m) :. n) :. k)
         Actual: Exp
                   (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
                 -> Exp