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

6 files changed, 120 insertions, 120 deletions

diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 4c9097eacd..433333f21d 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -1,19 +1,19 @@
-
-T3169.hs:13:22: error:
-    • Couldn't match type ‘elt’ with ‘Map 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
-      Expected type: Map a (Map b elt)
-        Actual type: Map (a, 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 }
-    • Relevant bindings include
-        m :: Map (a, b) elt (bound at T3169.hs:12:17)
-        b :: b (bound at T3169.hs:12:13)
-        lookup :: (a, b) -> Map (a, b) elt -> Maybe elt
-          (bound at T3169.hs:12:3)
+

+T3169.hs:13:22: error:

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

+      Expected type: Map a (Map b elt)

+        Actual type: Map (a, 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 }

+    • Relevant bindings include

+        m :: Map (a, b) elt (bound at T3169.hs:12:17)

+        b :: b (bound at T3169.hs:12:13)

+        lookup :: (a, b) -> Map (a, b) elt -> Maybe elt

+          (bound at T3169.hs:12:3)

diff --git a/testsuite/tests/gadt/T7558.stderr b/testsuite/tests/gadt/T7558.stderr
index 6618346452..34ade9778e 100644
--- a/testsuite/tests/gadt/T7558.stderr
+++ b/testsuite/tests/gadt/T7558.stderr
@@ -1,15 +1,15 @@
-
-T7558.hs:8:4: error:
-    • Couldn't match type ‘a’ with ‘Maybe a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          f :: forall a. T a a -> Bool
-        at T7558.hs:7:6
-      Inaccessible code in
-        a pattern with constructor:
-          MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,
-        in an equation for ‘f’
-    • In the pattern: MkT x y
-      In an equation for ‘f’: f (MkT x y) = [x, y] `seq` True
-    • Relevant bindings include
-        f :: T a a -> Bool (bound at T7558.hs:8:1)
+

+T7558.hs:8:4: error:

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

+      ‘a’ is a rigid type variable bound by

+        the type signature for:

+          f :: forall a. T a a -> Bool

+        at T7558.hs:7:1-18

+      Inaccessible code in

+        a pattern with constructor:

+          MkT :: forall a b. a ~ Maybe b => a -> Maybe b -> T a b,

+        in an equation for ‘f’

+    • In the pattern: MkT x y

+      In an equation for ‘f’: f (MkT x y) = [x, y] `seq` True

+    • Relevant bindings include

+        f :: T a a -> Bool (bound at T7558.hs:8:1)

diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 9bcd99cffe..ccd428f106 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -1,19 +1,19 @@
-
-gadt-escape1.hs:19:58: error:
-    • Couldn't match type ‘t’ with ‘ExpGADT Int’
-        ‘t’ is untouchable
-          inside the constraints: t1 ~ Int
-          bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,
-                   in a case alternative
-          at gadt-escape1.hs:19:43-50
-      ‘t’ is a rigid type variable bound by
-        the inferred type of weird1 :: t at gadt-escape1.hs:19:1
-      Possible fix: add a type signature for ‘weird1’
-      Expected type: t
-        Actual type: ExpGADT t1
-    • In the expression: a
-      In a case alternative: Hidden (ExpInt _) a -> a
-      In the expression:
-        case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
-    • Relevant bindings include
-        weird1 :: t (bound at gadt-escape1.hs:19:1)
+

+gadt-escape1.hs:19:58: error:

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

+        ‘t’ is untouchable

+          inside the constraints: t1 ~ Int

+          bound by a pattern with constructor: ExpInt :: Int -> ExpGADT Int,

+                   in a case alternative

+          at gadt-escape1.hs:19:43-50

+      ‘t’ is a rigid type variable bound by

+        the inferred type of weird1 :: t at gadt-escape1.hs:19:1-58

+      Possible fix: add a type signature for ‘weird1’

+      Expected type: t

+        Actual type: ExpGADT t1

+    • In the expression: a

+      In a case alternative: Hidden (ExpInt _) a -> a

+      In the expression:

+        case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }

+    • Relevant bindings include

+        weird1 :: t (bound at gadt-escape1.hs:19:1)

diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index 797fd0ba4d..06b1f9c720 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -1,17 +1,17 @@
-
-gadt13.hs:15:13: error:
-    • Couldn't match expected type ‘t’
-                  with actual type ‘String -> [Char]’
-        ‘t’ is untouchable
-          inside the constraints: t1 ~ Int
-          bound by a pattern with constructor: I :: Int -> Term Int,
-                   in an equation for ‘shw’
-          at gadt13.hs:15:6-8
-      ‘t’ is a rigid type variable bound by
-        the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1
-      Possible fix: add a type signature for ‘shw’
-    • Possible cause: ‘(.)’ is applied to too many arguments
-      In the expression: ("I " ++) . shows t
-      In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
-    • Relevant bindings include
-        shw :: Term t1 -> t (bound at gadt13.hs:15:1)
+

+gadt13.hs:15:13: error:

+    • Couldn't match expected type ‘t’

+                  with actual type ‘String -> [Char]’

+        ‘t’ is untouchable

+          inside the constraints: t1 ~ Int

+          bound by a pattern with constructor: I :: Int -> Term Int,

+                   in an equation for ‘shw’

+          at gadt13.hs:15:6-8

+      ‘t’ is a rigid type variable bound by

+        the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1-30

+      Possible fix: add a type signature for ‘shw’

+    • Possible cause: ‘(.)’ is applied to too many arguments

+      In the expression: ("I " ++) . shows t

+      In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t

+    • Relevant bindings include

+        shw :: Term t1 -> t (bound at gadt13.hs:15:1)

diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 35c8e10363..6e1effa067 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,20 +1,20 @@
-
-gadt7.hs:16:38: error:
-    • Couldn't match expected type ‘t’ with actual type ‘t1’
-        ‘t’ is untouchable
-          inside the constraints: t2 ~ Int
-          bound by a pattern with constructor: K :: T Int,
-                   in a case alternative
-          at gadt7.hs:16:33
-      ‘t’ is a rigid type variable bound by
-        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
-      Possible fix: add a type signature for ‘i1b’
-    • In the expression: y1
-      In a case alternative: K -> y1
-      In the expression: case t1 of { K -> y1 }
-    • Relevant bindings include
-        y1 :: t1 (bound at gadt7.hs:16:16)
-        y :: t1 (bound at gadt7.hs:16:7)
-        i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)
+

+gadt7.hs:16:38: error:

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

+        ‘t’ is untouchable

+          inside the constraints: t2 ~ Int

+          bound by a pattern with constructor: K :: T Int,

+                   in a case alternative

+          at gadt7.hs:16:33

+      ‘t’ is a rigid type variable bound by

+        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1-44

+      ‘t1’ is a rigid type variable bound by

+        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1-44

+      Possible fix: add a type signature for ‘i1b’

+    • In the expression: y1

+      In a case alternative: K -> y1

+      In the expression: case t1 of { K -> y1 }

+    • Relevant bindings include

+        y1 :: t1 (bound at gadt7.hs:16:16)

+        y :: t1 (bound at gadt7.hs:16:7)

+        i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)

diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr
index c79bb72b4c..4c53ff2aa1 100644
--- a/testsuite/tests/gadt/rw.stderr
+++ b/testsuite/tests/gadt/rw.stderr
@@ -1,30 +1,30 @@
-
-rw.hs:14:47: error:
-    • Couldn't match expected type ‘a’ with actual type ‘Int’
-      ‘a’ is a rigid type variable bound by
-        the type signature for:
-          writeInt :: forall a. T a -> IORef a -> IO ()
-        at rw.hs:12:12
-    • In the second argument of ‘writeIORef’, namely ‘(1 :: Int)’
-      In the expression: writeIORef ref (1 :: Int)
-      In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)
-    • Relevant bindings include
-        ref :: IORef a (bound at rw.hs:13:12)
-        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:
-    • Couldn't match type ‘a’ with ‘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:12
-      Expected type: a -> IO ()
-        Actual type: Bool -> IO ()
-    • 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)
-        readBool :: T a -> IORef a -> IO () (bound at rw.hs:17:1)
+

+rw.hs:14:47: error:

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

+      ‘a’ is a rigid type variable bound by

+        the type signature for:

+          writeInt :: forall a. T a -> IORef a -> IO ()

+        at rw.hs:12:1-34

+    • In the second argument of ‘writeIORef’, namely ‘(1 :: Int)’

+      In the expression: writeIORef ref (1 :: Int)

+      In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)

+    • Relevant bindings include

+        ref :: IORef a (bound at rw.hs:13:12)

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

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

+      Expected type: a -> IO ()

+        Actual type: Bool -> IO ()

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

+        readBool :: T a -> IORef a -> IO () (bound at rw.hs:17:1)