Fix impredicativity (again)

This patch fixes Trac #12616.

Dignosis.  In TcUnify.tc_sub_type_ds we were going to some trouble to
support co- and contra-variance even for impredicative types.  With
-XImpredicativeTYpes, this allowed a unification variable to be
unified with a polytype (probably wrongly) and that caused later
trouble in the constraint solver, where -XImpredicativeTypes was /not/
on.  In effect, -XImpredicativeTypes can't be switched on locally.

Why did we want ImpredicativeTypes locally?  Because the program
generated by GND for a higher-rank method involved impredicative
instantation of 'coerce':
      op = coerce op   -- where op has a higher rank type
See Note [Newtype-deriving instances] in TcGenDeriv.

Cure.

1.  It is ghastly to rely on ImpredicativeTypes (a 100% flaky
    feature) to instantiate coerce polymorphically.  Happily we
    now have Visible Type Application, so I've used that instead
    which should be solid and reliable.

2.  I deleted the code in tc_sub_type_ds that allows the constraint
    solver to "look through" a unification variable to find a
    polytype.  That used to be essential in the days of ReturnTv,
    but it's utterly unreliable and should be consigned to the dustbin
    of history.  (We have ExpType now for the essential uses.)

Tests involving ImpredicativeTypes are affected, but I'm not worried
about them... it's advertised as a feature you can't rely on, and
I want to reform it outright.

1 files changed, 74 insertions, 4 deletions

diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr
index 89c82c4f9a..5cda3a1e97 100644
--- a/testsuite/tests/typecheck/should_compile/tc211.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc211.stderr
@@ -1,9 +1,79 @@
 
-tc211.hs:73:9: error:
-    • Couldn't match type ‘forall a2. a2 -> a2’ with ‘a1 -> a1’
+tc211.hs:20:8: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘a1 -> a1’
+    • In the expression:
+          (:) ::
+            (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a]
+      In the expression:
+        ((:) ::
+           (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
+          (head foo) foo
+      In an equation for ‘bar’:
+          bar
+            = ((:) ::
+                 (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a])
+                (head foo) foo
+
+tc211.hs:25:8: error:
+    • Couldn't match type ‘a3 -> a3’ with ‘forall a. a -> a’
+      Expected type: [forall a. a -> a]
+        Actual type: [a3 -> a3]
+    • In the expression: (head foo) : (tail foo)
+      In an equation for ‘barr’: barr = (head foo) : (tail foo)
+
+tc211.hs:25:20: error:
+    • Couldn't match type ‘forall a. a -> a’ with ‘a3 -> a3’
+      Expected type: [a3 -> a3]
+        Actual type: [forall a. a -> a]
+    • In the second argument of ‘(:)’, namely ‘(tail foo)’
+      In the expression: (head foo) : (tail foo)
+      In an equation for ‘barr’: barr = (head foo) : (tail foo)
+
+tc211.hs:62:18: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘a0 -> a0’
+    • In the expression:
+          Cons ::
+            (forall a. a -> a)
+            -> List (forall a. a -> a) -> List (forall a. a -> a)
+      In an equation for ‘cons’:
+          cons
+            = Cons ::
+                (forall a. a -> a)
+                -> List (forall a. a -> a) -> List (forall a. a -> a)
+      In the expression:
+        let
+          cons
+            = Cons ::
+                (forall a. a -> a)
+                -> List (forall a. a -> a) -> List (forall a. a -> a)
+        in cons (\ x -> x) Nil
+
+tc211.hs:68:8: error:
+    • Couldn't match expected type ‘forall a. a -> a’
+                  with actual type ‘a2 -> a2’
+    • In the expression:
+          Cons ::
+            (forall a. a -> a)
+            -> List (forall a. a -> a) -> List (forall a. a -> a)
+      In the expression:
+        (Cons ::
+           (forall a. a -> a)
+           -> List (forall a. a -> a) -> List (forall a. a -> a))
+          (\ x -> x) Nil
+      In an equation for ‘xs2’:
+          xs2
+            = (Cons ::
+                 (forall a. a -> a)
+                 -> List (forall a. a -> a) -> List (forall a. a -> a))
+                (\ x -> x) Nil
+
+tc211.hs:76:9: error:
+    • Couldn't match type ‘forall a5. a5 -> a5’ with ‘a4 -> a4’
       Expected type: List (forall a. a -> a)
-                     -> (forall a. a -> a) -> a1 -> a1
-        Actual type: List (a1 -> a1) -> (a1 -> a1) -> a1 -> a1
+                     -> (forall a. a -> a) -> a4 -> a4
+        Actual type: List (a4 -> a4) -> (a4 -> a4) -> a4 -> a4
     • In the expression:
           foo2 ::
             List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a)