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

1 files changed, 5 insertions, 5 deletions

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)