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.

40 files changed, 215 insertions, 233 deletions

diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 3a5fc99fb3..5770e03c70 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -1,20 +1,17 @@
 
-T3169.hs:13:13: error:
+T3169.hs:13:22: error:
     • Couldn't match type ‘elt’ with ‘Map b elt’
-      Expected: Maybe (Map b elt)
-        Actual: Maybe elt
+      Expected: Map a (Map b elt)
+        Actual: Map (a, b) elt
       ‘elt’ is a rigid type variable bound by
         the type signature for:
           lookup :: forall elt. (a, b) -> Map (a, b) elt -> Maybe elt
         at T3169.hs:12:3-8
-    • In the expression: lookup a m :: Maybe (Map b elt)
+    • In the second argument of ‘lookup’, namely ‘m’
+      In the expression: lookup a m :: Maybe (Map b elt)
       In the expression:
         case lookup a m :: Maybe (Map b elt) of {
           Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
-      In an equation for ‘lookup’:
-          lookup (a, b) (m :: Map (a, b) elt)
-            = case lookup a m :: Maybe (Map b elt) of {
-                Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
     • Relevant bindings include
         m :: Map (a, b) elt (bound at T3169.hs:12:17)
         b :: b (bound at T3169.hs:12:13)
diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr
index fe6ba1edee..c4221368fd 100644
--- a/testsuite/tests/gadt/rw.stderr
+++ b/testsuite/tests/gadt/rw.stderr
@@ -13,17 +13,17 @@ rw.hs:14:47: error:
         v :: T a (bound at rw.hs:13:10)
         writeInt :: T a -> IORef a -> IO () (bound at rw.hs:13:1)
 
-rw.hs:19:43: error:
+rw.hs:19:51: error:
     • Couldn't match type ‘a’ with ‘Bool’
-      Expected: a -> IO ()
-        Actual: Bool -> IO ()
+      Expected: a -> Bool
+        Actual: Bool -> Bool
       ‘a’ is a rigid type variable bound by
         the type signature for:
           readBool :: forall a. T a -> IORef a -> IO ()
         at rw.hs:16:1-34
-    • In the second argument of ‘(>>=)’, namely ‘(print . not)’
+    • In the second argument of ‘(.)’, namely ‘not’
+      In the second argument of ‘(>>=)’, namely ‘(print . not)’
       In the expression: readIORef ref >>= (print . not)
-      In a case alternative: ~(Lb x) -> readIORef ref >>= (print . not)
     • Relevant bindings include
         ref :: IORef a (bound at rw.hs:17:12)
         v :: T a (bound at rw.hs:17:10)
diff --git a/testsuite/tests/ghci.debugger/scripts/T14628.stderr b/testsuite/tests/ghci.debugger/scripts/T14628.stderr
index fbce771874..0eb90fde1f 100644
--- a/testsuite/tests/ghci.debugger/scripts/T14628.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/T14628.stderr
@@ -1,9 +1,9 @@
 
-<interactive>:4:7: error:
+<interactive>:4:17: error:
     • Couldn't match type ‘m’ with ‘(,) a0’
-      Expected: (a0, ((), Int))
-        Actual: m ((), Int)
+      Expected: StateT Int ((,) a0) ()
+        Actual: StateT Int m ()
       ‘m’ is an interactive-debugger skolem
-    • In the second argument of ‘($)’, namely ‘runStateT _result 0’
+    • In the first argument of ‘runStateT’, namely ‘_result’
+      In the second argument of ‘($)’, namely ‘runStateT _result 0’
       In the expression: snd $ runStateT _result 0
-      In an equation for ‘it’: it = snd $ runStateT _result 0
diff --git a/testsuite/tests/ghci/scripts/T10508.stderr b/testsuite/tests/ghci/scripts/T10508.stderr
index f7931e48e2..8cbcb2936d 100644
--- a/testsuite/tests/ghci/scripts/T10508.stderr
+++ b/testsuite/tests/ghci/scripts/T10508.stderr
@@ -1,13 +1,10 @@
 
-<interactive>:1:8: error:
+<interactive>:1:15: error:
     • Couldn't match type: a0 -> a0
                      with: [Char]
-      Expected: IO Prelude.String
-        Actual: IO (a0 -> a0)
-    • In the expression: return id
+      Expected: Prelude.String
+        Actual: a0 -> a0
+    • Probable cause: ‘id’ is applied to too few arguments
+      In the first argument of ‘return’, namely ‘id’
+      In the expression: return id
       In the second argument of ‘(.)’, namely ‘(\ _ -> return id)’
-      In the expression:
-          (.)
-            (GHC.GHCi.ghciStepIO :: IO Prelude.String -> IO Prelude.String)
-            (\ _ -> return id) ::
-            Prelude.String -> IO Prelude.String
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
diff --git a/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr b/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
index 26c895ef3c..4a2d167327 100644
--- a/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
@@ -1,5 +1,6 @@
 
-Forall1Bad.hs:9:8: error:
+Forall1Bad.hs:9:13: error:
     • Couldn't match expected type ‘Char’ with actual type ‘Bool’
-    • In the expression: fall True
+    • In the first argument of ‘fall’, namely ‘True’
+      In the expression: fall True
       In an equation for ‘test’: test = fall True
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
index e366651f7d..17ffbc1595 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
@@ -22,14 +22,14 @@ NamedWildcardExplicitForall.hs:13:26: error:
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature: baz :: forall _a. _a -> _b -> (_a, _b)
 
-NamedWildcardExplicitForall.hs:14:16: error:
-    • Couldn't match expected type ‘Bool’ with actual type ‘_a’
+NamedWildcardExplicitForall.hs:14:12: error:
+    • Couldn't match expected type ‘_a’ with actual type ‘Bool’
       ‘_a’ is a rigid type variable bound by
         the inferred type of baz :: _a -> Bool -> (_a, Bool)
         at NamedWildcardExplicitForall.hs:13:15-16
-    • In the first argument of ‘not’, namely ‘x’
-      In the expression: not x
+    • In the expression: not x
       In the expression: (not x, not y)
+      In an equation for ‘baz’: baz x y = (not x, not y)
     • Relevant bindings include
         x :: _a (bound at NamedWildcardExplicitForall.hs:14:5)
         baz :: _a -> Bool -> (_a, Bool)
diff --git a/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr b/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
index e4c368c6e1..a1a1295b12 100644
--- a/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
@@ -1,9 +1,10 @@
 
-PatBind3.hs:6:12: error:
+PatBind3.hs:6:17: error:
     • Couldn't match type ‘(Bool, w)’ with ‘Char’
-      Expected: Maybe ((Bool, w) -> Char)
-        Actual: Maybe ((Bool, w) -> (Bool, w))
-    • In the expression: Just id
+      Expected: (Bool, w) -> Char
+        Actual: (Bool, w) -> (Bool, w)
+    • In the first argument of ‘Just’, namely ‘id’
+      In the expression: Just id
       In a pattern binding: Just foo = Just id
     • Relevant bindings include
         foo :: (Bool, w) -> Char (bound at PatBind3.hs:6:6)
diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr
index 82398e15a7..9418f15a71 100644
--- a/testsuite/tests/patsyn/should_fail/T15695.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15695.stderr
@@ -33,12 +33,13 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
         from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
           (bound at T15695.hs:39:1)
 
-T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)]
+T15695.hs:40:33: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type: a0 : as0
                      with: '[]
-      Expected: NS (NP NA) '[ '[ 'VO]]
-        Actual: NS (NP NA) ('[ 'VO] : a0 : as0)
-    • In the expression: There (Here undefined)
+      Expected: NS (NP NA) '[]
+        Actual: NS (NP NA) (a0 : as0)
+    • In the first argument of ‘There’, namely ‘(Here undefined)’
+      In the expression: There (Here undefined)
       In an equation for ‘from'’:
           from' (ASSO (Right b)) = There (Here undefined)
     • Relevant bindings include
diff --git a/testsuite/tests/th/T10945.stderr b/testsuite/tests/th/T10945.stderr
index 1c7a0f238d..fe71a2f50c 100644
--- a/testsuite/tests/th/T10945.stderr
+++ b/testsuite/tests/th/T10945.stderr
@@ -1,10 +1,17 @@
 
-T10945.hs:7:4: error:
+T10945.hs:7:11: error:
     • Couldn't match type: [Dec]
                      with: Q [Dec]
-      Expected: Code Q DecsQ
-        Actual: Code Q [Dec]
-    • In the expression:
+      Expected: DecsQ
+        Actual: [Dec]
+    • In the first argument of ‘return’, namely
+        ‘[SigD
+            (mkName "m")
+            (ForallT
+               [PlainTV (mkName "a") SpecifiedSpec] []
+               (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
+          FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]’
+      In the expression:
         return
           [SigD
              (mkName "m")
@@ -20,11 +27,3 @@ T10945.hs:7:4: error:
                    [PlainTV (mkName "a") SpecifiedSpec] []
                    (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
               FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]])
-      In the expression:
-        $$(return
-             [SigD
-                (mkName "m")
-                (ForallT
-                   [PlainTV (mkName "a") SpecifiedSpec] []
-                   (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
-              FunD (mkName "m") [Clause ... (NormalB (VarE (mkName "x"))) []]])
diff --git a/testsuite/tests/typecheck/should_compile/FD2.stderr b/testsuite/tests/typecheck/should_compile/FD2.stderr
index 323d10f06d..a5462aa94e 100644
--- a/testsuite/tests/typecheck/should_compile/FD2.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD2.stderr
@@ -1,6 +1,6 @@
 
-FD2.hs:26:36: error:
-    • Couldn't match expected type ‘e’ with actual type ‘e1’
+FD2.hs:26:34: error:
+    • Couldn't match expected type ‘e1’ with actual type ‘e’
       ‘e1’ is a rigid type variable bound by
         the type signature for:
           mf :: forall e1. Elem a e1 => e1 -> Maybe e1 -> Maybe e1
@@ -9,9 +9,9 @@ FD2.hs:26:36: error:
         the type signature for:
           foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e
         at FD2.hs:21:13-47
-    • In the first argument of ‘f’, namely ‘x’
-      In the first argument of ‘Just’, namely ‘(f x y)’
+    • In the first argument of ‘Just’, namely ‘(f x y)’
       In the expression: Just (f x y)
+      In an equation for ‘mf’: mf x (Just y) = Just (f x y)
     • Relevant bindings include
         y :: e1 (bound at FD2.hs:26:23)
         x :: e1 (bound at FD2.hs:26:15)
diff --git a/testsuite/tests/typecheck/should_compile/T15368.stderr b/testsuite/tests/typecheck/should_compile/T15368.stderr
index 33b0407730..5760692c75 100644
--- a/testsuite/tests/typecheck/should_compile/T15368.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15368.stderr
@@ -14,14 +14,15 @@ T15368.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
     • Relevant bindings include
         trigger :: a -> b -> (F a b, F b a) (bound at T15368.hs:11:1)
 
-T15368.hs:11:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
+T15368.hs:11:30: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type: F b0 a0
                      with: F b a
-      Expected: (F a b, F b a)
-        Actual: (F a b, F b0 a0)
+      Expected: (F a0 b0, F b a)
+        Actual: (F a0 b0, F b0 a0)
       NB: ‘F’ is a non-injective type family
       The type variables ‘b0’, ‘a0’ are ambiguous
-    • In the expression: _ `transitive` trigger _ _
+    • In the second argument of ‘transitive’, namely ‘trigger _ _’
+      In the expression: _ `transitive` trigger _ _
       In an equation for ‘trigger’:
           trigger _ _ = _ `transitive` trigger _ _
     • Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/T15370.stderr b/testsuite/tests/typecheck/should_compile/T15370.stderr
index f359155dbd..798cfc9f8a 100644
--- a/testsuite/tests/typecheck/should_compile/T15370.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15370.stderr
@@ -20,19 +20,15 @@ T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
     • Couldn't match type ‘S r’ with ‘()’
       Expected: ()
         Actual: S r
-    • In the expression: no + _
+    • In the first argument of ‘(+)’, namely ‘no’
+      In the expression: no + _
       In a case alternative: Refl -> no + _
-      In the expression: case mkRefl @x @y of { Refl -> no + _ }
     • Relevant bindings include
         no :: S r (bound at T15370.hs:18:7)
         right :: S r -> () (bound at T15370.hs:18:1)
 
 T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: S r
-      Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
-               the type signature for:
-                 right :: forall x y (r :: Either x y). S r -> ()
-               at T15370.hs:(16,1)-(17,18)
+    • Found hole: _ :: ()
     • In the second argument of ‘(+)’, namely ‘_’
       In the expression: no + _
       In a case alternative: Refl -> no + _
@@ -40,3 +36,8 @@ T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
         no :: S r (bound at T15370.hs:18:7)
         right :: S r -> () (bound at T15370.hs:18:1)
       Constraints include y ~ x (from T15370.hs:20:5-8)
+      Valid hole fits include
+        () :: ()
+        mempty :: forall a. Monoid a => a
+        maxBound :: forall a. Bounded a => a
+        minBound :: forall a. Bounded a => a
diff --git a/testsuite/tests/typecheck/should_compile/T2494.stderr b/testsuite/tests/typecheck/should_compile/T2494.stderr
index 8e427c5ac8..d7c96aeeaa 100644
--- a/testsuite/tests/typecheck/should_compile/T2494.stderr
+++ b/testsuite/tests/typecheck/should_compile/T2494.stderr
@@ -21,7 +21,7 @@ T2494.hs:15:14: error:
 
 T2494.hs:15:30: error:
     • Couldn't match type ‘b’ with ‘a’
-      Expected: Maybe (m b) -> Maybe (m a)
+      Expected: Maybe (m a) -> Maybe (m a)
         Actual: Maybe (m b) -> Maybe (m b)
       ‘b’ is a rigid type variable bound by
         the RULE "foo/foo"
diff --git a/testsuite/tests/typecheck/should_fail/T12648.stderr b/testsuite/tests/typecheck/should_fail/T12648.stderr
index f13b6c1cd0..6f12341c06 100644
--- a/testsuite/tests/typecheck/should_fail/T12648.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12648.stderr
@@ -1,17 +1,13 @@
 
-T12648.hs:76:2: error:
-    • Couldn't match type ‘a’ with ‘()’
-      Expected: m a
-        Actual: m ()
+T12648.hs:76:9: error:
+    • Couldn't match expected type ‘a’ with actual type ‘()’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           f :: forall (m :: * -> *) a. MonadBaseUnlift m IO => m a
         at T12648.hs:71:1-34
-    • In a stmt of a 'do' block: return ()
+    • In the first argument of ‘return’, namely ‘()’
+      In a stmt of a 'do' block: return ()
       In the expression:
         do _ <- askUnliftBase
            return ()
-      In an equation for ‘f’:
-          f = do _ <- askUnliftBase
-                 return ()
     • Relevant bindings include f :: m a (bound at T12648.hs:72:1)
diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr
index bd4aceed9e..ceb5f69c66 100644
--- a/testsuite/tests/typecheck/should_fail/T1899.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1899.stderr
@@ -1,15 +1,15 @@
 
-T1899.hs:15:36: error:
-    • Couldn't match type ‘a’ with ‘Proposition a0’
-      Expected: [Proposition a0]
-        Actual: [a]
+T1899.hs:15:26: error:
+    • Couldn't match expected type ‘a’
+                  with actual type ‘Proposition a0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           transRHS :: forall a. [a] -> Int -> Constraint a
         at T1899.hs:9:2-39
-    • In the first argument of ‘Auxiliary’, namely ‘varSet’
-      In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
+    • In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
       In the expression: Prop (Auxiliary varSet)
+      In the expression:
+        [Prop (Auxiliary varSet), Prop (Auxiliary varSet)]
     • Relevant bindings include
         varSet :: [a] (bound at T1899.hs:10:11)
         transRHS :: [a] -> Int -> Constraint a (bound at T1899.hs:10:2)
diff --git a/testsuite/tests/typecheck/should_fail/T19364.hs b/testsuite/tests/typecheck/should_fail/T19364.hs
new file mode 100644
index 0000000000..6b7259c6ee
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19364.hs
@@ -0,0 +1,12 @@
+module T19364 where
+
+type Foo = Bool
+type Bar = String
+
+data Pair a b = Pair a b
+
+baz :: Pair Foo Bar
+baz = Pair "yes" "no"
+
+-- The whole point about this test is the quality
+-- of the error message in baz: see #19364
diff --git a/testsuite/tests/typecheck/should_fail/T19364.stderr b/testsuite/tests/typecheck/should_fail/T19364.stderr
new file mode 100644
index 0000000000..ffd5ad2bf7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19364.stderr
@@ -0,0 +1,8 @@
+
+T19364.hs:9:12: error:
+    • Couldn't match type ‘[Char]’ with ‘Bool’
+      Expected: Foo
+        Actual: String
+    • In the first argument of ‘Pair’, namely ‘"yes"’
+      In the expression: Pair "yes" "no"
+      In an equation for ‘baz’: baz = Pair "yes" "no"
diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr
index f7980d2734..748ec505f3 100644
--- a/testsuite/tests/typecheck/should_fail/T2688.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2688.stderr
@@ -1,5 +1,5 @@
 
-T2688.hs:8:14: error:
+T2688.hs:8:22: error:
     • Couldn't match expected type ‘v’ with actual type ‘s’
       ‘s’ is a rigid type variable bound by
         the class declaration for ‘VectorSpace’
@@ -7,8 +7,9 @@ T2688.hs:8:14: error:
       ‘v’ is a rigid type variable bound by
         the class declaration for ‘VectorSpace’
         at T2688.hs:5:19
-    • In the expression: v *^ (1 / s)
-      In an equation for ‘^/’: v ^/ s = v *^ (1 / s)
+    • In the second argument of ‘(/)’, namely ‘s’
+      In the second argument of ‘(*^)’, namely ‘(1 / s)’
+      In the expression: v *^ (1 / s)
     • Relevant bindings include
         s :: s (bound at T2688.hs:8:10)
         v :: v (bound at T2688.hs:8:5)
diff --git a/testsuite/tests/typecheck/should_fail/T3613.stderr b/testsuite/tests/typecheck/should_fail/T3613.stderr
index 8183ff981e..cff3344597 100644
--- a/testsuite/tests/typecheck/should_fail/T3613.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3613.stderr
@@ -1,12 +1,11 @@
 
 T3613.hs:14:20: error:
     • Couldn't match type ‘IO’ with ‘Maybe’
-      Expected: Maybe b
-        Actual: IO b
-    • In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
+      Expected: Maybe ()
+        Actual: IO ()
+    • In the first argument of ‘(>>)’, namely ‘bar’
+      In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
       In the expression: fooThen (bar >> undefined)
-      In the expression:
-        let fooThen m = foo >> m in fooThen (bar >> undefined)
 
 T3613.hs:17:24: error:
     • Couldn't match type ‘IO’ with ‘Maybe’
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index f71fd5d501..69ff276479 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,12 +1,13 @@
 
-T3950.hs:15:8: error:
+T3950.hs:15:13: error:
     • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
         w :: (* -> * -> *) -> *
         Sealed :: (* -> *) -> *
-      Expected: Maybe (w (Id p))
-        Actual: Maybe (Sealed (Id p0 x0))
-    • In the expression: Just rp'
+      Expected: w (Id p)
+        Actual: Sealed (Id p0 x0)
+    • In the first argument of ‘Just’, namely ‘rp'’
+      In the expression: Just rp'
       In an equation for ‘rp’:
           rp _
             = Just rp'
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
index 3b203968f0..52d57c01e6 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
@@ -1,7 +1,6 @@
 
-T6018failclosed2.hs:17:14:
-    Couldn't match expected type ‘Bar a0’ with actual type ‘Char’
-    The type variable ‘a0’ is ambiguous
-    In the first argument of ‘bar’, namely ‘'c'’
-    In the expression: bar 'c'
-    In an equation for ‘barapp’: barapp = bar 'c'
+T6018failclosed2.hs:17:10: error:
+    • Couldn't match expected type ‘Char’ with actual type ‘Bar a0’
+      The type variable ‘a0’ is ambiguous
+    • In the expression: bar 'c'
+      In an equation for ‘barapp’: barapp = bar 'c'
diff --git a/testsuite/tests/typecheck/should_fail/T8450.stderr b/testsuite/tests/typecheck/should_fail/T8450.stderr
index 9ac0d63643..8ba84a76f1 100644
--- a/testsuite/tests/typecheck/should_fail/T8450.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8450.stderr
@@ -1,15 +1,11 @@
 
-T8450.hs:8:19: error:
-    • Couldn't match type ‘a’ with ‘Bool’
-      Expected: Either Bool ()
-        Actual: Either a ()
+T8450.hs:8:7: error:
+    • Couldn't match expected type ‘a’ with actual type ‘()’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           run :: forall a. a
         at T8450.hs:7:1-18
-    • In the second argument of ‘($)’, namely
-        ‘(undefined :: Either a ())’
-      In the expression: runEffect $ (undefined :: Either a ())
+    • In the expression: runEffect $ (undefined :: Either a ())
       In an equation for ‘run’:
           run = runEffect $ (undefined :: Either a ())
     • Relevant bindings include run :: a (bound at T8450.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr
index b3752e4279..2a6c0ac16c 100644
--- a/testsuite/tests/typecheck/should_fail/T9260.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9260.stderr
@@ -1,7 +1,8 @@
 
-T9260.hs:12:8: error:
-    • Couldn't match type ‘2’ with ‘1’
-      Expected: Fin 1
-        Actual: Fin ((0 + 1) + 1)
-    • In the expression: Fsucc Fzero
+T9260.hs:12:14: error:
+    • Couldn't match type ‘1’ with ‘0’
+      Expected: Fin 0
+        Actual: Fin (0 + 1)
+    • In the first argument of ‘Fsucc’, namely ‘Fzero’
+      In the expression: Fsucc Fzero
       In an equation for ‘test’: test = Fsucc Fzero
diff --git a/testsuite/tests/typecheck/should_fail/T9774.stderr b/testsuite/tests/typecheck/should_fail/T9774.stderr
index da75c339b8..2381e3ce75 100644
--- a/testsuite/tests/typecheck/should_fail/T9774.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9774.stderr
@@ -1,8 +1,8 @@
 
-T9774.hs:5:17: error:
+T9774.hs:5:29: error:
     • Couldn't match type ‘Char’ with ‘[Char]’
       Expected: String
         Actual: Char
-    • In the first argument of ‘putStrLn’, namely ‘(assert True 'a')’
+    • In the second argument of ‘assert’, namely ‘'a'’
+      In the first argument of ‘putStrLn’, namely ‘(assert True 'a')’
       In the expression: putStrLn (assert True 'a')
-      In an equation for ‘foo’: foo = putStrLn (assert True 'a')
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 07eafc65b5..4768b19263 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -616,3 +616,4 @@ test('T12178a', normal, compile_fail, [''])
 test('T18869', normal, compile_fail, [''])
 test('T19142', normal, compile_fail, [''])
 test('T19346', normal, compile_fail, ['-fprint-typechecker-elaboration'])
+test('T19364', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail065.stderr b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
index 9be21918cb..81746cd200 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail065.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
@@ -1,8 +1,6 @@
 
-tcfail065.hs:29:18: error:
-    • Couldn't match type ‘x1’ with ‘x’
-      Expected: X x
-        Actual: X x1
+tcfail065.hs:29:20: error:
+    • Couldn't match expected type ‘x’ with actual type ‘x1’
       ‘x1’ is a rigid type variable bound by
         the type signature for:
           setX :: forall x1. x1 -> X x -> X x
@@ -10,9 +8,9 @@ tcfail065.hs:29:18: error:
       ‘x’ is a rigid type variable bound by
         the instance declaration
         at tcfail065.hs:28:10-19
-    • In the expression: X x
+    • In the first argument of ‘X’, namely ‘x’
+      In the expression: X x
       In an equation for ‘setX’: setX x (X _) = X x
-      In the instance declaration for ‘HasX (X x)’
     • Relevant bindings include
         x :: x1 (bound at tcfail065.hs:29:8)
         setX :: x1 -> X x -> X x (bound at tcfail065.hs:29:3)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
index c7b7630e04..7266e76823 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
@@ -22,10 +22,10 @@ tcfail068.hs:14:9: error:
         itgen :: (Int, Int) -> a -> IndTree s a
           (bound at tcfail068.hs:12:1)
 
-tcfail068.hs:19:9: error:
+tcfail068.hs:19:21: error:
     • Couldn't match type ‘s1’ with ‘s’
-      Expected: GHC.ST.ST s1 (IndTree s a)
-        Actual: GHC.ST.ST s (IndTree s a)
+      Expected: STArray s1 (Int, Int) a
+        Actual: IndTree s a
       ‘s1’ is a rigid type variable bound by
         a type expected by the context:
           forall s1. GHC.ST.ST s1 (IndTree s a)
@@ -36,18 +36,11 @@ tcfail068.hs:19:9: error:
                    Constructed a =>
                    (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
         at tcfail068.hs:16:1-75
-    • In the first argument of ‘runST’, namely
+    • In the first argument of ‘readSTArray’, namely ‘arr’
+      In the first argument of ‘(>>=)’, namely ‘readSTArray arr i’
+      In the first argument of ‘runST’, namely
         ‘(readSTArray arr i
             >>= \ val -> writeSTArray arr i (f val) >> return arr)’
-      In the expression:
-        runST
-          (readSTArray arr i
-             >>= \ val -> writeSTArray arr i (f val) >> return arr)
-      In an equation for ‘itiap’:
-          itiap i f arr
-            = runST
-                (readSTArray arr i
-                   >>= \ val -> writeSTArray arr i (f val) >> return arr)
     • Relevant bindings include
         arr :: IndTree s a (bound at tcfail068.hs:17:11)
         itiap :: (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
diff --git a/testsuite/tests/typecheck/should_fail/tcfail103.stderr b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
index 84c9c8b0b6..0a7a386f9e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail103.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
@@ -1,8 +1,8 @@
 
-tcfail103.hs:15:13: error:
+tcfail103.hs:15:23: error:
     • Couldn't match type ‘s’ with ‘t’
-      Expected: ST s Int
-        Actual: ST t Int
+      Expected: STRef s Int
+        Actual: STRef t Int
       ‘s’ is a rigid type variable bound by
         the type signature for:
           g :: forall s. ST s Int
@@ -11,13 +11,9 @@ tcfail103.hs:15:13: error:
         the type signature for:
           f :: forall t. ST t Int
         at tcfail103.hs:10:1-12
-    • In the expression: readSTRef v
+    • In the first argument of ‘readSTRef’, namely ‘v’
+      In the expression: readSTRef v
       In an equation for ‘g’: g = readSTRef v
-      In the expression:
-        do v <- newSTRef 5
-           let g :: ST s Int
-               g = readSTRef v
-           g
     • Relevant bindings include
         g :: ST s Int (bound at tcfail103.hs:15:9)
         v :: STRef t Int (bound at tcfail103.hs:12:5)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail131.stderr b/testsuite/tests/typecheck/should_fail/tcfail131.stderr
index 04fa000204..25f3f427ed 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail131.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail131.stderr
@@ -1,12 +1,11 @@
 
-tcfail131.hs:7:11: error:
-    • Couldn't match expected type ‘Integer’ with actual type ‘b’
+tcfail131.hs:7:9: error:
+    • Couldn't match expected type ‘b’ with actual type ‘Integer’
       ‘b’ is a rigid type variable bound by
         the type signature for:
           g :: forall b. Num b => b -> b
         at tcfail131.hs:6:3-22
-    • In the first argument of ‘f’, namely ‘x’
-      In the expression: f x x
+    • In the expression: f x x
       In an equation for ‘g’: g x = f x x
     • Relevant bindings include
         x :: b (bound at tcfail131.hs:7:5)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail153.stderr b/testsuite/tests/typecheck/should_fail/tcfail153.stderr
index 4faca8f037..0d38db4385 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail153.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail153.stderr
@@ -1,12 +1,13 @@
 
-tcfail153.hs:6:9: error:
-    • Couldn't match expected type ‘Bool’ with actual type ‘a’
+tcfail153.hs:6:7: error:
+    • Couldn't match type ‘a’ with ‘Bool’
+      Expected: [a]
+        Actual: [Bool]
       ‘a’ is a rigid type variable bound by
         the type signature for:
           f :: forall a. a -> [a]
         at tcfail153.hs:5:1-13
-    • In the first argument of ‘g’, namely ‘x’
-      In the expression: g x
+    • In the expression: g x
       In an equation for ‘f’:
           f x
             = g x
diff --git a/testsuite/tests/typecheck/should_fail/tcfail179.stderr b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
index a0c124590f..963ab0ba78 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail179.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
@@ -1,8 +1,6 @@
 
-tcfail179.hs:14:41: error:
-    • Couldn't match type ‘x’ with ‘s’
-      Expected: x -> s
-        Actual: x -> x
+tcfail179.hs:14:39: error:
+    • Couldn't match expected type ‘s’ with actual type ‘x’
       ‘x’ is a rigid type variable bound by
         a pattern with constructor:
           T :: forall s x. (s -> (x -> s) -> (x, s, Int)) -> T s,
@@ -12,11 +10,11 @@ tcfail179.hs:14:41: error:
         the type signature for:
           run :: forall s. T s -> Int
         at tcfail179.hs:12:1-17
-    • In the second argument of ‘g’, namely ‘id’
+    • In the first argument of ‘g’, namely ‘x’
       In the expression: g x id
       In a pattern binding: (x, _, b) = g x id
     • Relevant bindings include
-        x :: s (bound at tcfail179.hs:14:26)
+        x :: x (bound at tcfail179.hs:14:26)
         g :: s -> (x -> s) -> (x, s, Int) (bound at tcfail179.hs:14:16)
         ts :: T s (bound at tcfail179.hs:13:5)
         run :: T s -> Int (bound at tcfail179.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index dd1385fc90..023772c775 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,17 +1,15 @@
 
-tcfail201.hs:17:56: error:
-    • Couldn't match type ‘a’ with ‘HsDoc id0’
-      Expected: c a
-        Actual: c (HsDoc id0)
+tcfail201.hs:17:58: error:
+    • Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           gfoldl' :: forall (c :: * -> *) a.
                      (forall a1 b. c (a1 -> b) -> a1 -> c b)
                      -> (forall g. g -> c g) -> a -> c a
         at tcfail201.hs:15:1-85
-    • In the expression: z DocEmpty
+    • In the first argument of ‘z’, namely ‘DocEmpty’
+      In the expression: z DocEmpty
       In a case alternative: DocEmpty -> z DocEmpty
-      In the expression: case hsDoc of { DocEmpty -> z DocEmpty }
     • Relevant bindings include
         hsDoc :: a (bound at tcfail201.hs:16:13)
         gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
diff --git a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
index c2ff69c9ef..a4b6cc0b74 100644
--- a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
+++ b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
@@ -1,50 +1,27 @@
 
-CaretDiagnostics1.hs:(5,3)-(7,16): error:
+CaretDiagnostics1.hs:7:8-15: error:
     • Couldn't match expected type ‘IO a0’ with actual type ‘Int’
-    • In a stmt of a 'do' block:
+    • In the second argument of ‘(+)’, namely ‘(3 :: Int)’
+      In a stmt of a 'do' block:
         10000000000000000000000000000000000000 + 2 + (3 :: Int)
       In the expression:
         do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
            pure ("this is not an IO" + ())
-      In an equation for ‘main’:
-          main
-            = do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
-                 pure ("this is not an IO" + ())
-            where
-                _ = case id of { "γηξ" -> () '0' }
   |
-5 |   10000000000000000000000000000000000000 +
-  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
+7 |       (3 :: Int)
+  |        ^^^^^^^^
 
-CaretDiagnostics1.hs:8:3-45: error:
+CaretDiagnostics1.hs:8:9-27: error:
     • Couldn't match type ‘[Char]’ with ‘()’
-      Expected: IO ()
-        Actual: IO String
-    • In a stmt of a 'do' block: pure ("this is not an IO" + ())
-      In the expression:
-        do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
-           pure ("this is not an IO" + ())
-      In an equation for ‘main’:
-          main
-            = do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
-                 pure ("this is not an IO" + ())
-            where
-                _ = case id of { "γηξ" -> () '0' }
-  |
-8 |   pure ("this is not an IO" + (            ))
-  |   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-CaretDiagnostics1.hs:8:31-44: error:
-    • Couldn't match type ‘()’ with ‘[Char]’
-      Expected: String
-        Actual: ()
-    • In the second argument of ‘(+)’, namely ‘()’
+      Expected: ()
+        Actual: String
+    • In the first argument of ‘(+)’, namely ‘"this is not an IO"’
       In the first argument of ‘pure’, namely
         ‘("this is not an IO" + ())’
       In a stmt of a 'do' block: pure ("this is not an IO" + ())
   |
 8 |   pure ("this is not an IO" + (            ))
-  |                               ^^^^^^^^^^^^^^
+  |         ^^^^^^^^^^^^^^^^^^^
 
 CaretDiagnostics1.hs:13:7-11: error:
     • Couldn't match type: a1 -> a1