Allow full constraint solving under a for-all (Trac #5595)

The main idea is that when we unify
    forall a. t1  ~  forall a. t2
we get constraints from unifying t1~t2 that mention a.
We are producing a coercion witnessing the equivalence of
the for-alls, and inside *that* coercion we need bindings
for the solved constraints arising from t1~t2.

We didn't have way to do this before.  The big change is
that here's a new type TcEvidence.TcCoercion, which is
much like Coercion.Coercion except that there's a slot
for TcEvBinds in it.

This has a wave of follow-on changes. Not deep but broad.

* New module TcEvidence, which now contains the HsWrapper
  TcEvBinds, EvTerm etc types that used to be in HsBinds

* The typechecker works exclusively in terms of TcCoercion.

* The desugarer converts TcCoercion to Coercion

* The main payload is in TcUnify.unifySigmaTy. This is the
  function that had a gross hack before, but is now beautiful.

* LCoercion is gone!  Hooray.

Many many fiddly changes in conssequence.  But it's nice.

1 files changed, 1 insertions, 0 deletions

diff --git a/compiler/rename/RnBinds.lhs b/compiler/rename/RnBinds.lhs
index 51cd09fb07..0da8070438 100644
--- a/compiler/rename/RnBinds.lhs
+++ b/compiler/rename/RnBinds.lhs
@@ -35,6 +35,7 @@ import {-# SOURCE #-} RnExpr( rnLExpr, rnStmts )
 import HsSyn
 import RnHsSyn
 import TcRnMonad
+import TcEvidence     ( emptyTcEvBinds )
 import RnTypes        ( rnIPName, rnHsSigType, rnLHsType, checkPrecMatch )
 import RnPat
 import RnEnv