Refactor the typechecker to use ExpTypes.

The idea here is described in [wiki:Typechecker]. Briefly,
this refactor keeps solid track of "synthesis" mode vs
"checking" in GHC's bidirectional type-checking algorithm.
When in synthesis mode, the expected type is just an IORef
to write to.

In addition, this patch does a significant reworking of
RebindableSyntax, allowing much more freedom in the types
of the rebindable operators. For example, we can now have
`negate :: Int -> Bool` and
`(>>=) :: m a -> (forall x. a x -> m b) -> m b`. The magic
is in tcSyntaxOp.

This addresses tickets #11397, #11452, and #11458.

Tests:
  typecheck/should_compile/{RebindHR,RebindNegate,T11397,T11458}
  th/T11452

3 files changed, 23 insertions, 23 deletions

diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 215426ed15..9bcd99cffe 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 ‘r’ with ‘ExpGADT Int’
-        ‘r’ is untouchable
-          inside the constraints: t ~ Int
+    • 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
-      ‘r’ is a rigid type variable bound by
-        the inferred type of weird1 :: r at gadt-escape1.hs:19:1
+      ‘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: r
-        Actual type: ExpGADT t
+      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 :: r (bound at gadt-escape1.hs:19:1)
+        weird1 :: t (bound at gadt-escape1.hs:19:1)
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index 57ee3fdc92..bc14bf1c51 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 ‘r’
+    • Couldn't match expected type ‘t1’
                   with actual type ‘String -> [Char]’
-        ‘r’ is untouchable
+        ‘t1’ is untouchable
           inside the constraints: t ~ Int
           bound by a pattern with constructor: I :: Int -> Term Int,
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
-      ‘r’ is a rigid type variable bound by
-        the inferred type of shw :: Term t -> r at gadt13.hs:15:1
+      ‘t1’ is a rigid type variable bound by
+        the inferred type of shw :: Term t -> t1 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 t -> r (bound at gadt13.hs:15:1)
+        shw :: Term t -> t1 (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 93b8c70c1f..8219bee032 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 ‘r’ with actual type ‘r1’
-        ‘r’ is untouchable
-          inside the constraints: t ~ Int
+    • Couldn't match expected type ‘t2’ with actual type ‘t’
+        ‘t2’ is untouchable
+          inside the constraints: t1 ~ Int
           bound by a pattern with constructor: K :: T Int,
                    in a case alternative
           at gadt7.hs:16:33
-      ‘r’ is a rigid type variable bound by
-        the inferred type of i1b :: T t -> r1 -> r at gadt7.hs:16:1
-      ‘r1’ is a rigid type variable bound by
-        the inferred type of i1b :: T t -> r1 -> r at gadt7.hs:16:1
+      ‘t2’ is a rigid type variable bound by
+        the inferred type of i1b :: T t1 -> t -> t2 at gadt7.hs:16:1
+      ‘t’ is a rigid type variable bound by
+        the inferred type of i1b :: T t1 -> t -> t2 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 :: r1 (bound at gadt7.hs:16:16)
-        y :: r1 (bound at gadt7.hs:16:7)
-        i1b :: T t -> r1 -> r (bound at gadt7.hs:16:1)
+        y1 :: t (bound at gadt7.hs:16:16)
+        y :: t (bound at gadt7.hs:16:7)
+        i1b :: T t1 -> t -> t2 (bound at gadt7.hs:16:1)