Improve typechecking of let-bindings

This major commit was initially triggered by #11339, but it spiraled
into a major review of the way in which type signatures for bindings
are handled, especially partial type signatures.  On the way I fixed a
number of other bugs, namely
   #12069
   #12033
   #11700
   #11339
   #11670

The main change is that I completely reorganised the way in which type
signatures in bindings are handled. The new story is in TcSigs
Note [Overview of type signatures].  Some specific:

* Changes in the data types for signatures in TcRnTypes:
  TcIdSigInfo and new TcIdSigInst

* New module TcSigs deals with typechecking type signatures
  and pragmas. It contains code mostly moved from TcBinds,
  which is already too big

* HsTypes: I swapped the nesting of HsWildCardBndrs
  and HsImplicitBndsrs, so that the wildcards are on the
  oustide not the insidde in a LHsSigWcType.  This is just
  a matter of convenient, nothing deep.

There are a host of other changes as knock-on effects, and
it all took FAR longer than I anticipated :-).  But it is
a significant improvement, I think.

Lots of error messages changed slightly, some just variants but
some modest improvements.

New tests

* typecheck/should_compile
    * SigTyVars: a scoped-tyvar test
    * ExPat, ExPatFail: existential pattern bindings
    * T12069
    * T11700
    * T11339

* partial-sigs/should_compile
    * T12033
    * T11339a
    * T11670

One thing to check:

* Small change to output from ghc-api/landmines.
  Need to check with Alan Zimmerman

14 files changed, 321 insertions, 307 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
index bbbe0fbc58..eadcfc6953 100644
--- a/testsuite/tests/indexed-types/should_compile/Simple14.stderr
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -1,18 +1,17 @@
-
-Simple14.hs:8:8: error:
-    • Couldn't match type ‘z0’ with ‘z’
-        ‘z0’ is untouchable
-          inside the constraints: x ~ y
-          bound by the type signature for:
-                     eqE :: x ~ y => EQ_ z0 z0
-          at Simple14.hs:8:8-39
-      ‘z’ is a rigid type variable bound by
-        the type signature for:
-          eqE :: forall x y z p. EQ_ x y -> (x ~ y => EQ_ z z) -> p
-        at Simple14.hs:8:8
-      Expected type: EQ_ z0 z0
-        Actual type: EQ_ z z
-    • In the ambiguity check for ‘eqE’
-      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-      In the type signature:
-        eqE :: EQ_ x y -> (x ~ y => EQ_ z z) -> p
+

+Simple14.hs:8:8: error:

+    • Couldn't match type ‘z0’ with ‘z’

+        ‘z0’ is untouchable

+          inside the constraints: x ~ y

+          bound by the type signature for:

+                     eqE :: x ~ y => EQ_ z0 z0

+          at Simple14.hs:8:8-39

+      ‘z’ is a rigid type variable bound by

+        the type signature for:

+          eqE :: forall x y z p. EQ_ x y -> (x ~ y => EQ_ z z) -> p

+        at Simple14.hs:8:8-39

+      Expected type: EQ_ z0 z0

+        Actual type: EQ_ z z

+    • In the ambiguity check for ‘eqE’

+      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

+      In the type signature: eqE :: EQ_ x y -> (x ~ y => EQ_ z z) -> p

diff --git a/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr b/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
index 5a0892ed31..f8689f9b8d 100644
--- a/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
+++ b/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
@@ -1,17 +1,17 @@
-
-GADTwrong1.hs:12:21: error:
-    • Couldn't match expected type ‘b’ with actual type ‘c’
-      ‘c’ is a rigid type variable bound by
-        a pattern with constructor: T :: forall c. c -> T (Const c),
-        in a case alternative
-        at GADTwrong1.hs:12:14
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          coerce :: forall a b. a -> b
-        at GADTwrong1.hs:10:20
-    • In the expression: y
-      In a case alternative: T y -> y
-      In the expression: case T x :: T (Const b) of { T y -> y }
-    • Relevant bindings include
-        y :: c (bound at GADTwrong1.hs:12:16)
-        coerce :: a -> b (bound at GADTwrong1.hs:11:1)
+

+GADTwrong1.hs:12:21: error:

+    • Couldn't match expected type ‘b’ with actual type ‘c’

+      ‘c’ is a rigid type variable bound by

+        a pattern with constructor: T :: forall c. c -> T (Const c),

+        in a case alternative

+        at GADTwrong1.hs:12:14-16

+      ‘b’ is a rigid type variable bound by

+        the type signature for:

+          coerce :: forall a b. a -> b

+        at GADTwrong1.hs:10:1-29

+    • In the expression: y

+      In a case alternative: T y -> y

+      In the expression: case T x :: T (Const b) of { T y -> y }

+    • Relevant bindings include

+        y :: c (bound at GADTwrong1.hs:12:16)

+        coerce :: a -> b (bound at GADTwrong1.hs:11:1)

diff --git a/testsuite/tests/indexed-types/should_fail/Overlap6.stderr b/testsuite/tests/indexed-types/should_fail/Overlap6.stderr
index 6ffcda02ce..406ac9d3b6 100644
--- a/testsuite/tests/indexed-types/should_fail/Overlap6.stderr
+++ b/testsuite/tests/indexed-types/should_fail/Overlap6.stderr
@@ -1,14 +1,14 @@
-
-Overlap6.hs:15:7: error:
-    • Couldn't match type ‘x’ with ‘And x 'True’
-      ‘x’ is a rigid type variable bound by
-        the type signature for:
-          g :: forall (x :: Bool). Proxy x -> Proxy (And x 'True)
-        at Overlap6.hs:14:6
-      Expected type: Proxy (And x 'True)
-        Actual type: Proxy x
-    • In the expression: x
-      In an equation for ‘g’: g x = x
-    • Relevant bindings include
-        x :: Proxy x (bound at Overlap6.hs:15:3)
-        g :: Proxy x -> Proxy (And x 'True) (bound at Overlap6.hs:15:1)
+

+Overlap6.hs:15:7: error:

+    • Couldn't match type ‘x’ with ‘And x 'True’

+      ‘x’ is a rigid type variable bound by

+        the type signature for:

+          g :: forall (x :: Bool). Proxy x -> Proxy (And x 'True)

+        at Overlap6.hs:14:1-34

+      Expected type: Proxy (And x 'True)

+        Actual type: Proxy x

+    • In the expression: x

+      In an equation for ‘g’: g x = x

+    • Relevant bindings include

+        x :: Proxy x (bound at Overlap6.hs:15:3)

+        g :: Proxy x -> Proxy (And x 'True) (bound at Overlap6.hs:15:1)

diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
index 4b9c3657db..539628c6eb 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
@@ -1,13 +1,13 @@
-
-SimpleFail5a.hs:31:11: error:
-    • Couldn't match type ‘a’ with ‘Int’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          bar3wrong :: forall a. S3 a -> a
-        at SimpleFail5a.hs:30:14
-      Expected type: S3 a
-        Actual type: S3 Int
-    • In the pattern: D3Int
-      In an equation for ‘bar3wrong’: bar3wrong D3Int = 1
-    • Relevant bindings include
-        bar3wrong :: S3 a -> a (bound at SimpleFail5a.hs:31:1)
+

+SimpleFail5a.hs:31:11: error:

+    • Couldn't match type ‘a’ with ‘Int’

+      ‘a’ is a rigid type variable bound by

+        the type signature for:

+          bar3wrong :: forall a. S3 a -> a

+        at SimpleFail5a.hs:30:1-22

+      Expected type: S3 a

+        Actual type: S3 Int

+    • In the pattern: D3Int

+      In an equation for ‘bar3wrong’: bar3wrong D3Int = 1

+    • Relevant bindings include

+        bar3wrong :: S3 a -> a (bound at SimpleFail5a.hs:31:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index 3a84f18272..1409f1f44c 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -1,19 +1,19 @@
-
-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 :: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
-                               IO (PChan (a :*: b), PChan c)
-        at T2664.hs:23:5-12
-      ‘b’ is a rigid type variable bound by
-        the instance declaration at T2664.hs:22:10
-      ‘a’ is a rigid type variable bound by
-        the instance declaration at T2664.hs:22:10
-    • In the third argument of ‘pchoose’, namely ‘newPChan’
-      In the first argument of ‘E’, namely ‘(pchoose Right v newPChan)’
-      In the expression:
-        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)
+

+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 :: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>

+                               IO (PChan (a :*: b), PChan c)

+        at T2664.hs:23:5-12

+      ‘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:

+        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/T3330a.hs b/testsuite/tests/indexed-types/should_fail/T3330a.hs
index 55bf067238..b14a7d0858 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330a.hs
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.hs
@@ -30,12 +30,13 @@ children p x = execWriter (hmapM p collect x)
 Hence ix0 := ix
       r0  := r
       f0  := PF s
-      phi0 := s2 ix2
+      phi0 := (->) s2 ix2
       m0 := Writer [AnyF s]
       a0 : = f0 r'0 ix0
 
-  (forall ixx. (s2 ix2 ixx -> r ixx -> Writer [AnyF s] (r'0 ixx) ~ s ix))
-  s2 ix2 ix0 ~ s2 ix2 -> r2 ix2 -> Writer [AnyF s2] (r2 ix2)
+  (forall ixx. ((->) (s2 ix2 -> ixx) (r ixx -> Writer [AnyF s] (r'0 ixx)) ~ s ix))
+
+  s2 ix2 ix0 ~ (->) (s2 ix2) (r2 ix2 -> Writer [AnyF s2] (r2 ix2))
 
 -}
 
diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.stderr b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
index 0950875229..ffda424227 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
@@ -1,37 +1,37 @@
-
-T3330a.hs:19:34: error:
-    • Couldn't match type ‘ix’
-                     with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’
-      ‘ix’ is a rigid type variable bound by
-        the type signature for:
-          children :: forall (s :: * -> *) ix (r :: * -> *).
-                      s ix -> PF s r ix -> [AnyF s]
-        at T3330a.hs:18:13
-      Expected type: (s0 ix0 -> ix1)
-                     -> r ix1 -> Writer [AnyF s] (r'0 ix1)
-        Actual type: s ix
-    • In the first argument of ‘hmapM’, namely ‘p’
-      In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
-      In the expression: execWriter (hmapM p collect x)
-    • Relevant bindings include
-        x :: PF s r ix (bound at T3330a.hs:19:12)
-        p :: s ix (bound at T3330a.hs:19:10)
-        children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1)
-
-T3330a.hs:19:44: error:
-    • Couldn't match type ‘ix’
-                     with ‘r0 ix0 -> Writer [AnyF s0] (r0 ix0)’
-      ‘ix’ is a rigid type variable bound by
-        the type signature for:
-          children :: forall (s :: * -> *) ix (r :: * -> *).
-                      s ix -> PF s r ix -> [AnyF s]
-        at T3330a.hs:18:13
-      Expected type: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0))
-        Actual type: PF s r ix
-    • In the third argument of ‘hmapM’, namely ‘x’
-      In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’
-      In the expression: execWriter (hmapM p collect x)
-    • Relevant bindings include
-        x :: PF s r ix (bound at T3330a.hs:19:12)
-        p :: s ix (bound at T3330a.hs:19:10)
-        children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1)
+

+T3330a.hs:19:34: error:

+    • Couldn't match type ‘ix’

+                     with ‘r ix1 -> Writer [AnyF s] (r'0 ix1)’

+      ‘ix’ is a rigid type variable bound by

+        the type signature for:

+          children :: forall (s :: * -> *) ix (r :: * -> *).

+                      s ix -> PF s r ix -> [AnyF s]

+        at T3330a.hs:18:1-43

+      Expected type: (s0 ix0 -> ix1)

+                     -> r ix1 -> Writer [AnyF s] (r'0 ix1)

+        Actual type: s ix

+    • In the first argument of ‘hmapM’, namely ‘p’

+      In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’

+      In the expression: execWriter (hmapM p collect x)

+    • Relevant bindings include

+        x :: PF s r ix (bound at T3330a.hs:19:12)

+        p :: s ix (bound at T3330a.hs:19:10)

+        children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1)

+

+T3330a.hs:19:44: error:

+    • Couldn't match type ‘ix’

+                     with ‘r0 ix0 -> Writer [AnyF s0] (r0 ix0)’

+      ‘ix’ is a rigid type variable bound by

+        the type signature for:

+          children :: forall (s :: * -> *) ix (r :: * -> *).

+                      s ix -> PF s r ix -> [AnyF s]

+        at T3330a.hs:18:1-43

+      Expected type: PF s r (r0 ix0 -> Writer [AnyF s0] (r0 ix0))

+        Actual type: PF s r ix

+    • In the third argument of ‘hmapM’, namely ‘x’

+      In the first argument of ‘execWriter’, namely ‘(hmapM p collect x)’

+      In the expression: execWriter (hmapM p collect x)

+    • Relevant bindings include

+        x :: PF s r ix (bound at T3330a.hs:19:12)

+        p :: s ix (bound at T3330a.hs:19:10)

+        children :: s ix -> PF s r ix -> [AnyF s] (bound at T3330a.hs:19:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T3440.stderr b/testsuite/tests/indexed-types/should_fail/T3440.stderr
index 8289d144c2..84eb475b23 100644
--- a/testsuite/tests/indexed-types/should_fail/T3440.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3440.stderr
@@ -1,24 +1,24 @@
-
-T3440.hs:11:22: error:
-    • Could not deduce: a1 ~ a
-      from the context: Fam a ~ Fam a1
-        bound by a pattern with constructor:
-                   GADT :: forall a. a -> Fam a -> GADT (Fam a),
-                 in an equation for ‘unwrap’
-        at T3440.hs:11:9-16
-      ‘a1’ is a rigid type variable bound by
-        a pattern with constructor:
-          GADT :: forall a. a -> Fam a -> GADT (Fam a),
-        in an equation for ‘unwrap’
-        at T3440.hs:11:9
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          unwrap :: forall a. GADT (Fam a) -> (a, Fam a)
-        at T3440.hs:10:11
-    • In the expression: x
-      In the expression: (x, y)
-      In an equation for ‘unwrap’: unwrap (GADT x y) = (x, y)
-    • Relevant bindings include
-        y :: Fam a1 (bound at T3440.hs:11:16)
-        x :: a1 (bound at T3440.hs:11:14)
-        unwrap :: GADT (Fam a) -> (a, Fam a) (bound at T3440.hs:11:1)
+

+T3440.hs:11:22: error:

+    • Could not deduce: a1 ~ a

+      from the context: Fam a ~ Fam a1

+        bound by a pattern with constructor:

+                   GADT :: forall a. a -> Fam a -> GADT (Fam a),

+                 in an equation for ‘unwrap’

+        at T3440.hs:11:9-16

+      ‘a1’ is a rigid type variable bound by

+        a pattern with constructor:

+          GADT :: forall a. a -> Fam a -> GADT (Fam a),

+        in an equation for ‘unwrap’

+        at T3440.hs:11:9-16

+      ‘a’ is a rigid type variable bound by

+        the type signature for:

+          unwrap :: forall a. GADT (Fam a) -> (a, Fam a)

+        at T3440.hs:10:1-36

+    • In the expression: x

+      In the expression: (x, y)

+      In an equation for ‘unwrap’: unwrap (GADT x y) = (x, y)

+    • Relevant bindings include

+        y :: Fam a1 (bound at T3440.hs:11:16)

+        x :: a1 (bound at T3440.hs:11:14)

+        unwrap :: GADT (Fam a) -> (a, Fam a) (bound at T3440.hs:11:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.stderr b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
index d226122614..3ce9158bdc 100644
--- a/testsuite/tests/indexed-types/should_fail/T4093a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
@@ -1,16 +1,16 @@
-
-T4093a.hs:8:8: error:
-    • Could not deduce: e ~ ()
-      from the context: Foo e ~ Maybe e
-        bound by the type signature for:
-                   hang :: Foo e ~ Maybe e => Foo e
-        at T4093a.hs:7:1-34
-      ‘e’ is a rigid type variable bound by
-        the type signature for:
-          hang :: forall e. Foo e ~ Maybe e => Foo e
-        at T4093a.hs:7:9
-      Expected type: Foo e
-        Actual type: Maybe ()
-    • In the expression: Just ()
-      In an equation for ‘hang’: hang = Just ()
-    • Relevant bindings include hang :: Foo e (bound at T4093a.hs:8:1)
+

+T4093a.hs:8:8: error:

+    • Could not deduce: e ~ ()

+      from the context: Foo e ~ Maybe e

+        bound by the type signature for:

+                   hang :: Foo e ~ Maybe e => Foo e

+        at T4093a.hs:7:1-34

+      ‘e’ is a rigid type variable bound by

+        the type signature for:

+          hang :: forall e. Foo e ~ Maybe e => Foo e

+        at T4093a.hs:7:1-34

+      Expected type: Foo e

+        Actual type: Maybe ()

+    • In the expression: Just ()

+      In an equation for ‘hang’: hang = Just ()

+    • Relevant bindings include hang :: Foo e (bound at T4093a.hs:8:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T4093b.stderr b/testsuite/tests/indexed-types/should_fail/T4093b.stderr
index 0950de8c66..92530d58bf 100644
--- a/testsuite/tests/indexed-types/should_fail/T4093b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4093b.stderr
@@ -1,42 +1,42 @@
-
-T4093b.hs:31:13: error:
-    • Could not deduce: e ~ C
-      from the context: (EitherCO e (A C O n) (A O O n) ~ A e O n,
-                         EitherCO x (A C C n) (A C O n) ~ A C x n)
-        bound by the type signature for:
-                   blockToNodeList :: (EitherCO e (A C O n) (A O O n) ~ A e O n,
-                                       EitherCO x (A C C n) (A C O n) ~ A C x n) =>
-                                      Block n e x -> A e x n
-        at T4093b.hs:(19,1)-(22,26)
-      ‘e’ is a rigid type variable bound by
-        the type signature for:
-          blockToNodeList :: forall (n :: * -> * -> *) e x.
-                             (EitherCO e (A C O n) (A O O n) ~ A e O n,
-                              EitherCO x (A C C n) (A C O n) ~ A C x n) =>
-                             Block n e x -> A e x n
-        at T4093b.hs:20:12
-      Expected type: EitherCO e (A C O n) (A O O n)
-        Actual type: (MaybeC C (n C O), MaybeC O (n O C))
-    • In the expression: (JustC n, NothingC)
-      In an equation for ‘f’: f n _ = (JustC n, NothingC)
-      In an equation for ‘blockToNodeList’:
-          blockToNodeList b
-            = foldBlockNodesF (f, l) b z
-            where
-                z ::
-                  EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))
-                z = undefined
-                f ::
-                  n C O
-                  -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
-                f n _ = (JustC n, NothingC)
-                ....
-    • Relevant bindings include
-        f :: n C O
-             -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
-          (bound at T4093b.hs:31:5)
-        l :: n O C
-             -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C C n) (A O C n)
-          (bound at T4093b.hs:34:5)
-        b :: Block n e x (bound at T4093b.hs:25:17)
-        blockToNodeList :: Block n e x -> A e x n (bound at T4093b.hs:25:1)
+

+T4093b.hs:31:13: error:

+    • Could not deduce: e ~ C

+      from the context: (EitherCO e (A C O n) (A O O n) ~ A e O n,

+                         EitherCO x (A C C n) (A C O n) ~ A C x n)

+        bound by the type signature for:

+                   blockToNodeList :: (EitherCO e (A C O n) (A O O n) ~ A e O n,

+                                       EitherCO x (A C C n) (A C O n) ~ A C x n) =>

+                                      Block n e x -> A e x n

+        at T4093b.hs:(19,1)-(22,26)

+      ‘e’ is a rigid type variable bound by

+        the type signature for:

+          blockToNodeList :: forall (n :: * -> * -> *) e x.

+                             (EitherCO e (A C O n) (A O O n) ~ A e O n,

+                              EitherCO x (A C C n) (A C O n) ~ A C x n) =>

+                             Block n e x -> A e x n

+        at T4093b.hs:(19,1)-(22,26)

+      Expected type: EitherCO e (A C O n) (A O O n)

+        Actual type: (MaybeC C (n C O), MaybeC O (n O C))

+    • In the expression: (JustC n, NothingC)

+      In an equation for ‘f’: f n _ = (JustC n, NothingC)

+      In an equation for ‘blockToNodeList’:

+          blockToNodeList b

+            = foldBlockNodesF (f, l) b z

+            where

+                z ::

+                  EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))

+                z = undefined

+                f ::

+                  n C O

+                  -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)

+                f n _ = (JustC n, NothingC)

+                ....

+    • Relevant bindings include

+        f :: n C O

+             -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)

+          (bound at T4093b.hs:31:5)

+        l :: n O C

+             -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C C n) (A O C n)

+          (bound at T4093b.hs:34:5)

+        b :: Block n e x (bound at T4093b.hs:25:17)

+        blockToNodeList :: Block n e x -> A e x n (bound at T4093b.hs:25:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr
index c932530e5a..7fe8c704b9 100644
--- a/testsuite/tests/indexed-types/should_fail/T4174.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr
@@ -1,16 +1,16 @@
-
-T4174.hs:42:12: error:
-    • Couldn't match type ‘b’ with ‘RtsSpinLock’
-      ‘b’ is a rigid type variable bound by
-        the type signature for:
-          testcase :: forall (m :: * -> *) minor n t p a b.
-                      Monad m =>
-                      m (Field (Way (GHC6'8 minor) n t p) a b)
-        at T4174.hs:41:13
-      Expected type: m (Field (Way (GHC6'8 minor) n t p) a b)
-        Actual type: m (Field (WayOf m) SmStep RtsSpinLock)
-    • In the expression: sync_large_objects
-      In an equation for ‘testcase’: testcase = sync_large_objects
-    • Relevant bindings include
-        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
-          (bound at T4174.hs:42:1)
+

+T4174.hs:42:12: error:

+    • Couldn't match type ‘b’ with ‘RtsSpinLock’

+      ‘b’ is a rigid type variable bound by

+        the type signature for:

+          testcase :: forall (m :: * -> *) minor n t p a b.

+                      Monad m =>

+                      m (Field (Way (GHC6'8 minor) n t p) a b)

+        at T4174.hs:41:1-63

+      Expected type: m (Field (Way (GHC6'8 minor) n t p) a b)

+        Actual type: m (Field (WayOf m) SmStep RtsSpinLock)

+    • In the expression: sync_large_objects

+      In an equation for ‘testcase’: testcase = sync_large_objects

+    • Relevant bindings include

+        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)

+          (bound at T4174.hs:42:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index a3b750a459..49a6e9f6c9 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,17 +1,17 @@
-
-T4272.hs:15:26: error:
-    • Couldn't match type ‘a’ with ‘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:16
-      Expected type: TermFamily a (TermFamily a a)
-        Actual type: TermFamily a a
-    • 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))
-    • Relevant bindings include
-        t :: TermFamily a a (bound at T4272.hs:15:6)
-        laws :: TermFamily a a -> b (bound at T4272.hs:15:1)
+

+T4272.hs:15:26: error:

+    • Couldn't match type ‘a’ with ‘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

+      Expected type: TermFamily a (TermFamily a a)

+        Actual type: TermFamily a a

+    • 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))

+    • 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/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr
index a58b69e7e7..79230e1555 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7786.stderr
@@ -1,36 +1,50 @@
-
-T7786.hs:86:22: error:
-    • Couldn't match type ‘xxx’ with ‘'Empty’
-      Inaccessible code in
-        a pattern with constructor: Nil :: forall a. Sing 'Empty,
-        in a pattern binding in
-             'do' block
-    • In the pattern: Nil
-      In the pattern: Nil :: Sing xxx
-      In a stmt of a 'do' block:
-        Nil :: Sing xxx <- return
-                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
-
-T7786.hs:86:49: error:
-    • Couldn't match type ‘xxx’
-                     with ‘Intersect (BuriedUnder sub k 'Empty) inv’
-      Expected type: Sing xxx
-        Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv)
-    • In the first argument of ‘return’, namely
-        ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’
-      In a stmt of a 'do' block:
-        Nil :: Sing xxx <- return
-                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
-      In the expression:
-        do { Nil :: Sing xxx <- return
-                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
-             return $ Sub db k sub }
-    • Relevant bindings include
-        sub :: Database sub (bound at T7786.hs:86:13)
-        k :: Sing k (bound at T7786.hs:86:11)
-        db :: Database inv (bound at T7786.hs:86:8)
-        addSub :: Database inv
-                  -> Sing k
-                  -> Database sub
-                  -> Maybe (Database (BuriedUnder sub k inv))
-          (bound at T7786.hs:86:1)
+

+T7786.hs:86:49: error:

+    • Couldn't match type ‘xxx’

+                     with ‘Intersect (BuriedUnder sub k 'Empty) inv’

+      Expected type: Sing xxx

+        Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv)

+    • In the first argument of ‘return’, namely

+        ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’

+      In a stmt of a 'do' block:

+        Nil :: Sing xxx <- return

+                             (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)

+      In the expression:

+        do { Nil :: Sing xxx <- return

+                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);

+             return $ Sub db k sub }

+    • Relevant bindings include

+        sub :: Database sub (bound at T7786.hs:86:13)

+        k :: Sing k (bound at T7786.hs:86:11)

+        db :: Database inv (bound at T7786.hs:86:8)

+        addSub :: Database inv

+                  -> Sing k

+                  -> Database sub

+                  -> Maybe (Database (BuriedUnder sub k inv))

+          (bound at T7786.hs:86:1)

+

+T7786.hs:90:31: error:

+    • Could not deduce: Intersect (BuriedUnder sub k 'Empty) inv

+                        ~

+                        'Empty

+        arising from a use of ‘Sub’

+      from the context: xxx ~ 'Empty

+        bound by a pattern with constructor: Nil :: forall a. Sing 'Empty,

+                 in a pattern binding in

+                      'do' block

+        at T7786.hs:86:22-24

+    • In the second argument of ‘($)’, namely ‘Sub db k sub’

+      In a stmt of a 'do' block: return $ Sub db k sub

+      In the expression:

+        do { Nil :: Sing xxx <- return

+                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);

+             return $ Sub db k sub }

+    • Relevant bindings include

+        sub :: Database sub (bound at T7786.hs:86:13)

+        k :: Sing k (bound at T7786.hs:86:11)

+        db :: Database inv (bound at T7786.hs:86:8)

+        addSub :: Database inv

+                  -> Sing k

+                  -> Database sub

+                  -> Maybe (Database (BuriedUnder sub k inv))

+          (bound at T7786.hs:86:1)

diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 04ba4f4dba..403f769dfd 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,35 +1,35 @@
-
-T9662.hs:47:8: error:
-    • Couldn't match type ‘n’ with ‘Int’
-      ‘n’ is a rigid type variable bound by
-        the type signature for:
-          test :: forall sh k m n.
-                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
-        at T9662.hs:44:9
-      Expected type: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. m) :. n) :. k)
-        Actual type: Exp
-                       (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-                     -> Exp
-                          (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
-    • In the first argument of ‘backpermute’, namely
-        ‘(modify
-            (atom :. atom :. atom :. atom)
-            (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’
-      In the expression:
-        backpermute
-          (modify
-             (atom :. atom :. atom :. atom)
-             (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
-          id
-      In an equation for ‘test’:
-          test
-            = backpermute
-                (modify
-                   (atom :. atom :. atom :. atom)
-                   (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))
-                id
-    • Relevant bindings include
-        test :: Shape (((sh :. k) :. m) :. n)
-                -> Shape (((sh :. m) :. n) :. k)
-          (bound at T9662.hs:45:1)
+

+T9662.hs:47:8: error:

+    • Couldn't match type ‘n’ with ‘Int’

+      ‘n’ is a rigid type variable bound by

+        the type signature for:

+          test :: forall sh k m n.

+                  Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)

+        at T9662.hs:44:1-50

+      Expected type: Exp (((sh :. m) :. n) :. k)

+                     -> Exp (((sh :. m) :. n) :. k)

+        Actual type: Exp

+                       (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))

+                     -> Exp

+                          (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))

+    • In the first argument of ‘backpermute’, namely

+        ‘(modify

+            (atom :. atom :. atom :. atom)

+            (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’

+      In the expression:

+        backpermute

+          (modify

+             (atom :. atom :. atom :. atom)

+             (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))

+          id

+      In an equation for ‘test’:

+          test

+            = backpermute

+                (modify

+                   (atom :. atom :. atom :. atom)

+                   (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))

+                id

+    • Relevant bindings include

+        test :: Shape (((sh :. k) :. m) :. n)

+                -> Shape (((sh :. m) :. n) :. k)

+          (bound at T9662.hs:45:1)