A collection of type-inference refactorings.

This patch does a raft of useful tidy-ups in the type checker.
I've been meaning to do this for some time, and finally made
time to do it en route to ICFP.

1. Modify TcType.ExpType to make a distinct data type,
   InferResult for the Infer case, and consequential
   refactoring.

2. Define a new function TcUnify.fillInferResult, to fill in
   an InferResult. It uses TcMType.promoteTcType to promote
   the type to the level of the InferResult.
   See TcMType Note [Promoting a type]
   This refactoring is in preparation for an improvement
   to typechecking pattern bindings, coming next.

   I flirted with an elaborate scheme to give better
   higher rank inference, but it was just too complicated.
   See TcMType Note [Promotion and higher rank types]

3. Add to InferResult a new field ir_inst :: Bool to say
   whether or not the type used to fill in the
   InferResult should be deeply instantiated.  See
   TcUnify Note [Deep instantiation of InferResult].

4. Add a TcLevel to SkolemTvs. This will be useful generally

    - it's a fast way to see if the type
      variable escapes when floating (not used yet)

    - it provides a good consistency check when updating a
      unification variable (TcMType.writeMetaTyVarRef, the
      level_check_ok check)

   I originally had another reason (related to the flirting
   in (2), but I left it in because it seems like a step in
   the right direction.

5. Reduce and simplify the plethora of uExpType,
   tcSubType and related functions in TcUnify.  It was
   such an opaque mess and it's still not great, but it's
   better.

6. Simplify the uo_expected field of TypeEqOrigin.  Richard
   had generatlised it to a ExpType, but it was almost always
   a Check type.  Now it's back to being a plain TcType which
   is much, much easier.

7. Improve error messages by refraining from skolemisation when
   it's clear that there's an error: see
   TcUnify Note [Don't skolemise unnecessarily]

8. Type.isPiTy and isForAllTy seem to be missing a coreView check,
   so I added it

9. Kill off tcs_used_tcvs.  Its purpose is to track the
   givens used by wanted constraints.  For dictionaries etc
   we do that via the free vars of the /bindings/ in the
   implication constraint ic_binds.  But for coercions we
   just do update-in-place in the type, rather than
   generating a binding.  So we need something analogous to
   bindings, to track what coercions we have added.

   That was the purpose of tcs_used_tcvs.  But it only
   worked for a /single/ iteration, whereas we may have
   multiple iterations of solving an implication.  Look
   at (the old) 'setImplicationStatus'.  If the constraint
   is unsolved, it just drops the used_tvs on the floor.
   If it becomes solved next time round, we'll pick up
   coercions used in that round, but ignore ones used in
   the first round.

   There was an outright bug.  Result = (potentialy) bogus
   unused-constraint errors.  Constructing a case where this
   actually happens seems quite trick so I did not do so.

   Solution: expand EvBindsVar to include the (free vars of
   the) coercions, so that the coercions are tracked in
   essentially the same way as the bindings.

   This turned out to be much simpler.  Less code, more
   correct.

10. Make the ic_binds field in an implication have type
      ic_binds :: EvBindsVar
    instead of (as previously)
       ic_binds :: Maybe EvBindsVar
    This is notably simpler, and faster to use -- less
    testing of the Maybe.  But in the occaional situation
    where we don't have anywhere to put the bindings, the
    belt-and-braces error check is lost.  So I put it back
    as an ASSERT in 'setImplicationStatus' (see the use of
    'termEvidenceAllowed')

All these changes led to quite bit of error message wibbling

3 files changed, 22 insertions, 22 deletions

diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index 056d451a09..41322f9cbc 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
+    • Couldn't match type ‘p’ with ‘ExpGADT Int’
+        ‘p’ is untouchable
+          inside the constraints: t ~ 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
+      ‘p’ is a rigid type variable bound by
+        the inferred type of weird1 :: p at gadt-escape1.hs:19:1-58
       Possible fix: add a type signature for ‘weird1’
-      Expected type: t
-        Actual type: ExpGADT t1
+      Expected type: p
+        Actual type: ExpGADT t
     • 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)
+        weird1 :: p (bound at gadt-escape1.hs:19:1)
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index e304430b51..6673ff68b0 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’
+    • Couldn't match expected type ‘p’
                   with actual type ‘String -> [Char]’
-        ‘t’ is untouchable
+        ‘p’ is untouchable
           inside the constraints: a ~ 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 a -> t at gadt13.hs:15:1-30
+      ‘p’ is a rigid type variable bound by
+        the inferred type of shw :: Term a -> p 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 a -> t (bound at gadt13.hs:15:1)
+        shw :: Term a -> p (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index e66226eaea..f75e8c5bff 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
+    • Couldn't match expected type ‘p’ with actual type ‘p1’
+        ‘p1’ is untouchable
           inside the constraints: a ~ 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 a -> t1 -> t at gadt7.hs:16:1-44
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of i1b :: T a -> t1 -> t at gadt7.hs:16:1-44
+      ‘p1’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p at gadt7.hs:16:1-44
+      ‘p’ is a rigid type variable bound by
+        the inferred type of i1b :: T a -> p1 -> p 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 a -> t1 -> t (bound at gadt7.hs:16:1)
+        y1 :: p1 (bound at gadt7.hs:16:16)
+        y :: p1 (bound at gadt7.hs:16:7)
+        i1b :: T a -> p1 -> p (bound at gadt7.hs:16:1)