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

2 files changed, 15 insertions, 14 deletions

diff --git a/testsuite/tests/rebindable/rebindable6.hs b/testsuite/tests/rebindable/rebindable6.hs
index ec975e7f37..3ec03477d2 100644
--- a/testsuite/tests/rebindable/rebindable6.hs
+++ b/testsuite/tests/rebindable/rebindable6.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module Main where
 	{
@@ -88,7 +89,7 @@ module Main where
 		negate :: a;
 		};
 
-	instance HasNegate (a -> a) where
+	instance (b ~ (a -> a)) => HasNegate b where
 		{
 		negate a = a; -- don't actually negate
 		};
@@ -98,7 +99,7 @@ module Main where
 		(-) :: a;
 		};
 
-	instance HasMinus (a -> a -> a) where
+	instance (b ~ (a -> a -> a)) => HasMinus b where
 		{
 		(-) x y = y; -- changed function
 		};
diff --git a/testsuite/tests/rebindable/rebindable6.stderr b/testsuite/tests/rebindable/rebindable6.stderr
index 0497c9fc61..8d2ea09928 100644
--- a/testsuite/tests/rebindable/rebindable6.stderr
+++ b/testsuite/tests/rebindable/rebindable6.stderr
@@ -1,18 +1,18 @@
 
-rebindable6.hs:109:17: error:
+rebindable6.hs:110:17: error:
     • Ambiguous type variable ‘t0’ arising from a do statement
       prevents the constraint ‘(HasSeq
                                   (IO a -> t0 -> IO b))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
       Relevant bindings include
-        g :: IO (Maybe b) (bound at rebindable6.hs:107:19)
-        f :: IO a (bound at rebindable6.hs:107:17)
+        g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
+        f :: IO a (bound at rebindable6.hs:108:17)
         test_do :: IO a -> IO (Maybe b) -> IO b
-          (bound at rebindable6.hs:107:9)
+          (bound at rebindable6.hs:108:9)
       Probable fix: use a type annotation to specify what ‘t0’ should be.
       These potential instance exist:
         instance HasSeq (IO a -> IO b -> IO b)
-          -- Defined at rebindable6.hs:55:18
+          -- Defined at rebindable6.hs:56:18
     • In a stmt of a 'do' block: f
       In the expression:
         do { f;
@@ -24,7 +24,7 @@ rebindable6.hs:109:17: error:
                    Just (b :: b) <- g;
                    return b }
 
-rebindable6.hs:110:17: error:
+rebindable6.hs:111:17: error:
     • Ambiguous type variable ‘t1’ arising from a do statement
                                    with the failable pattern ‘Just (b :: b)’
       prevents the constraint ‘(HasFail
@@ -33,7 +33,7 @@ rebindable6.hs:110:17: error:
       Probable fix: use a type annotation to specify what ‘t1’ should be.
       These potential instance exist:
         instance HasFail (String -> IO a)
-          -- Defined at rebindable6.hs:60:18
+          -- Defined at rebindable6.hs:61:18
     • In a stmt of a 'do' block: Just (b :: b) <- g
       In the expression:
         do { f;
@@ -45,18 +45,18 @@ rebindable6.hs:110:17: error:
                    Just (b :: b) <- g;
                    return b }
 
-rebindable6.hs:111:17: error:
+rebindable6.hs:112:17: error:
     • Ambiguous type variable ‘t1’ arising from a use of ‘return’
       prevents the constraint ‘(HasReturn (b -> t1))’ from being solved.
         (maybe you haven't applied a function to enough arguments?)
       Relevant bindings include
-        b :: b (bound at rebindable6.hs:110:23)
-        g :: IO (Maybe b) (bound at rebindable6.hs:107:19)
+        b :: b (bound at rebindable6.hs:111:23)
+        g :: IO (Maybe b) (bound at rebindable6.hs:108:19)
         test_do :: IO a -> IO (Maybe b) -> IO b
-          (bound at rebindable6.hs:107:9)
+          (bound at rebindable6.hs:108:9)
       Probable fix: use a type annotation to specify what ‘t1’ should be.
       These potential instance exist:
-        instance HasReturn (a -> IO a) -- Defined at rebindable6.hs:45:18
+        instance HasReturn (a -> IO a) -- Defined at rebindable6.hs:46:18
     • In a stmt of a 'do' block: return b
       In the expression:
         do { f;