Orient TyVar/TyVar equalities with deepest on the left

Trac #15009 showed that, for Given TyVar/TyVar equalities, we really
want to orient them with the deepest-bound skolem on the left. As it
happens, we also want to do the same for Wanteds, but for a different
reason (more likely to be touchable).  Either way, deepest wins:
see TcUnify Note [Deeper level on the left].

This observation led me to some significant changes:

* A SkolemTv already had a TcLevel, but the level wasn't really being
  used.   Now it is!

* I updated added invariant (SkolInf) to TcType
  Note [TcLevel and untouchable type variables], documenting that
  the level number of all the ic_skols should be the same as the
  ic_tclvl of the implication

* FlatSkolTvs and FlatMetaTvs previously had a dummy level-number of
  zero, which messed the scheme up.   Now they get a level number the
  same way as all other TcTyVars, instead of being a special case.

* To make sure that FlatSkolTvs and FlatMetaTvs are untouchable (which
  was previously done via their magic zero level) isTouchableMetaTyVar
  just tests for those two cases.

* TcUnify.swapOverTyVars is the crucial orientation function; see the
  new Note [TyVar/TyVar orientation].  I completely rewrote this function,
  and it's now much much easier to understand.

I ended up doing some related refactoring, of course

* I noticed that tcImplicitTKBndrsX and tcExplicitTKBndrsX were doing
  a lot of useless work in the case where there are no skolems; I
  added a fast-patch

* Elminate the un-used tcExplicitTKBndrsSig; and thereby get rid of
  the higher-order parameter to tcExpliciTKBndrsX.

* Replace TcHsType.emitTvImplication with TcUnify.checkTvConstraints,
  by analogy with TcUnify.checkConstraints.

* Inline TcUnify.buildImplication into its only call-site in
  TcUnify.checkConstraints

* TcS.buildImplication becomes TcS.CheckConstraintsTcS, with a
  simpler API

* Now that we have NoEvBindsVar we have no need of termEvidenceAllowed;
  nuke the latter, adding Note [No evidence bindings] to TcEvidence.

2 files changed, 21 insertions, 0 deletions

diff --git a/testsuite/tests/gadt/T15009.hs b/testsuite/tests/gadt/T15009.hs
new file mode 100644
index 0000000000..58e17af864
--- /dev/null
+++ b/testsuite/tests/gadt/T15009.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs #-}
+
+module T15009 where
+
+-- T2 is an ordinary H98 data type,
+-- and f2 should typecheck with no problem
+data T2 a where
+  MkT2 :: a -> T2 a
+
+f2 (MkT2 x) = not x
+
+-- T1 is a GADT, but the equality is really just a 'let'
+-- so f1 should also typecheck no problem
+data T1 a where
+  MkT1 :: b ~ a => b -> T1 a
+
+f1 (MkT1 x) = not x
+
+
+
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 4c8eb806a7..321d67e9e8 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -117,3 +117,4 @@ test('T12468', normal, compile_fail, [''])
 test('T14320', normal, compile, [''])
 test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret'])
 test('T14808', normal, compile, [''])
+test('T15009', normal, compile, [''])