Improve error recovery in the typechecker

Issue #16418 showed that we were carrying on too eagerly after a bogus
type signature was identified (a bad telescope in fact), leading to a
subsequent crash.

This led me in to a maze of twisty little passages in the typechecker's
error recovery, and I ended up doing some refactoring in TcRnMonad.
Some specfifics

* TcRnMonad.try_m is now called attemptM.

* I switched the order of the result pair in tryTc,
  to make it consistent with other similar functions.

* The actual exception used in the Tc monad is irrelevant so,
  to avoid polluting type signatures, I made tcTryM, a simple
  wrapper around tryM, and used it.

The more important changes are in

* TcSimplify.captureTopConstraints, where we should have been calling
  simplifyTop rather than reportUnsolved, so that levity defaulting
  takes place properly.

* TcUnify.emitResidualTvConstraint, where we need to set the correct
  status for a new implication constraint.  (Previously we ended up
  with an Insoluble constraint wrapped in an Unsolved implication,
  which meant that insolubleWC gave the wrong answer.

13 files changed, 63 insertions, 36 deletions

diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.hs b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
index e33fdf110e..73f69676e7 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.hs
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.hs
@@ -3,12 +3,9 @@
 module BadTelescope2 where
 
 import Data.Kind
-import Data.Proxy
 
 data SameKind :: k -> k -> *
 
 foo :: forall a k (b :: k). SameKind a b
 foo = undefined
 
-bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
-bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index a8c4b689ae..3637dece24 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -1,13 +1,6 @@
 
-BadTelescope2.hs:10:8: error:
+BadTelescope2.hs:9:8: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
     • In the type signature: foo :: forall a k (b :: k). SameKind a b
-
-BadTelescope2.hs:13:81: error:
-    • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
-    • In the second argument of ‘SameKind’, namely ‘d’
-      In the type signature:
-        bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
-               Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.hs b/testsuite/tests/dependent/should_fail/BadTelescope5.hs
new file mode 100644
index 0000000000..ce2368bbbe
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope5.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds, PolyKinds, ExplicitForAll #-}
+
+module BadTelescope5 where
+
+import Data.Kind
+import Data.Proxy
+
+data SameKind :: k -> k -> *
+
+bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). Proxy c -> SameKind b d
+bar = undefined
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
new file mode 100644
index 0000000000..da79678d5b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr
@@ -0,0 +1,7 @@
+
+BadTelescope5.hs:10:81: error:
+    • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’
+    • In the second argument of ‘SameKind’, namely ‘d’
+      In the type signature:
+        bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a).
+               Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/T15743c.stderr b/testsuite/tests/dependent/should_fail/T15743c.stderr
index 8e3ad5077f..4cb1c0c959 100644
--- a/testsuite/tests/dependent/should_fail/T15743c.stderr
+++ b/testsuite/tests/dependent/should_fail/T15743c.stderr
@@ -13,3 +13,18 @@ T15743c.hs:10:1: error:
         (b :: Proxy d)
         (x :: SimilarKind a b)
     • In the data type declaration for ‘T’
+
+T15743c.hs:11:1: error:
+    • The kind of ‘T2’ is ill-scoped
+        Inferred kind: T2 :: forall (d :: k).
+                             forall k (c :: k) (a :: Proxy c) (b :: Proxy d) ->
+                             SimilarKind a b -> *
+      NB: Specified variables (namely: (d :: k)) always come first
+      Perhaps try this order instead:
+        k
+        (d :: k)
+        (c :: k)
+        (a :: Proxy c)
+        (b :: Proxy d)
+        (x :: SimilarKind a b)
+    • In the data type declaration for ‘T2’
diff --git a/testsuite/tests/dependent/should_fail/T16418.hs b/testsuite/tests/dependent/should_fail/T16418.hs
new file mode 100644
index 0000000000..8097e3cbf3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16418.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module T16418 where
+
+import Data.Kind
+
+data SameKind :: forall k. k -> k -> Type
+
+f :: forall a k (b :: k). SameKind a b -> ()
+f = g
+  where
+    g :: SameKind a b -> ()
+    g _ = ()
diff --git a/testsuite/tests/dependent/should_fail/T16418.stderr b/testsuite/tests/dependent/should_fail/T16418.stderr
new file mode 100644
index 0000000000..fa2263abd3
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T16418.stderr
@@ -0,0 +1,7 @@
+
+T16418.hs:9:6: error:
+    • These kind and type variables: a k (b :: k)
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k) (b :: k)
+    • In the type signature:
+        f :: forall a k (b :: k). SameKind a b -> ()
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 1f75a85716..1e6ab40b09 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -4,9 +4,10 @@ test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
 test('BadTelescope3', normal, compile_fail, [''])
+test('BadTelescope4', normal, compile_fail, [''])
+test('BadTelescope5', normal, compile_fail, [''])
 test('PromotedClass', normal, compile_fail, [''])
 test('SelfDep', normal, compile_fail, [''])
-test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
@@ -55,3 +56,4 @@ test('T16326_Fail12', normal, compile_fail, [''])
 test('T16391b', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('T16344', normal, compile_fail, [''])
 test('T16344a', normal, compile_fail, [''])
+test('T16418', normal, compile_fail, [''])
diff --git a/testsuite/tests/patsyn/should_fail/T9161-1.hs b/testsuite/tests/patsyn/should_fail/T9161-1.hs
index c14eb542cc..32a6f9d6aa 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-1.hs
+++ b/testsuite/tests/patsyn/should_fail/T9161-1.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DataKinds #-}
 
+module Bug where
+
 pattern PATTERN = ()
 
 wrongLift :: PATTERN
diff --git a/testsuite/tests/patsyn/should_fail/T9161-1.stderr b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
index fff6efe286..39faffdaa8 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-1.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-1.stderr
@@ -1,5 +1,5 @@
 
-T9161-1.hs:6:14: error:
+T9161-1.hs:8:14: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
         (pattern synonyms cannot be promoted)
     • In the type signature: wrongLift :: PATTERN
diff --git a/testsuite/tests/patsyn/should_fail/T9161-2.hs b/testsuite/tests/patsyn/should_fail/T9161-2.hs
index 941d23e35f..ccdfa1ff05 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-2.hs
+++ b/testsuite/tests/patsyn/should_fail/T9161-2.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
 
+module Bug where
+
 pattern PATTERN = ()
 
 data Proxy (tag :: k) (a :: *)
diff --git a/testsuite/tests/patsyn/should_fail/T9161-2.stderr b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
index cc429313aa..71f7cbe257 100644
--- a/testsuite/tests/patsyn/should_fail/T9161-2.stderr
+++ b/testsuite/tests/patsyn/should_fail/T9161-2.stderr
@@ -1,5 +1,5 @@
 
-T9161-2.hs:8:20: error:
+T9161-2.hs:10:20: error:
     • Pattern synonym ‘PATTERN’ cannot be used here
         (pattern synonyms cannot be promoted)
     • In the first argument of ‘Proxy’, namely ‘PATTERN’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail212.stderr b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
index ad5985e63a..011a3772ef 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail212.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail212.stderr
@@ -16,25 +16,3 @@ tcfail212.hs:13:7: error:
 tcfail212.hs:13:13: error:
     • Expecting a lifted type, but ‘Int#’ is unlifted
     • In the type signature: g :: (Int#, Int#)
-
-tcfail212.hs:14:6: error:
-    • Couldn't match a lifted type with an unlifted type
-      When matching types
-        a :: *
-        Int# :: TYPE 'IntRep
-    • In the expression: 1#
-      In the expression: (1#, 2#)
-      In an equation for ‘g’: g = (1#, 2#)
-    • Relevant bindings include
-        g :: (a, b) (bound at tcfail212.hs:14:1)
-
-tcfail212.hs:14:10: error:
-    • Couldn't match a lifted type with an unlifted type
-      When matching types
-        b :: *
-        Int# :: TYPE 'IntRep
-    • In the expression: 2#
-      In the expression: (1#, 2#)
-      In an equation for ‘g’: g = (1#, 2#)
-    • Relevant bindings include
-        g :: (a, b) (bound at tcfail212.hs:14:1)