Another major constraint-solver refactoring

This patch takes further my refactoring of the constraint
solver, which I've been doing over the last couple of months
in consultation with Richard.

It fixes a number of tricky bugs that made the constraint
solver actually go into a loop, including

  Trac #12526
  Trac #12444
  Trac #12538

The main changes are these

* Flatten unification variables (fmvs/fuvs) appear on the LHS
  of a tvar/tyvar equality; thus
           fmv ~ alpha
  and not
           alpha ~ fmv

  See Note [Put flatten unification variables on the left]
  in TcUnify.  This is implemented by TcUnify.swapOverTyVars.

* Don't reduce a "loopy" CFunEqCan where the fsk appears on
  the LHS:
      F t1 .. tn ~ fsk
  where 'fsk' is free in t1..tn.
  See Note [FunEq occurs-check principle] in TcInteract

  This neatly stops some infinite loops that people reported;
  and it allows us to delete some crufty code in reduce_top_fun_eq.
  And it appears to be no loss whatsoever.

  As well as fixing loops, ContextStack2 and T5837 both terminate
  when they didn't before.

* Previously we generated "derived shadow" constraints from
  Wanteds, but we could (and sometimes did; Trac #xxxx) repeatedly
  generate a derived shadow from the same Wanted.

  A big change in this patch is to have two kinds of Wanteds:
     [WD] behaves like a pair of a Wanted and a Derived
     [W]  behaves like a Wanted only
  See CtFlavour and ShadowInfo in TcRnTypes, and the ctev_nosh
  field of a Wanted.

  This turned out to be a lot simpler.  A [WD] gets split into a
  [W] and a [D] in TcSMonad.maybeEmitShaodow.

  See TcSMonad Note [The improvement story and derived shadows]

* Rather than have a separate inert_model in the InertCans, I've
  put the derived equalities back into inert_eqs.  We weren't
  gaining anything from a separate field.

* Previously we had a mode for the constraint solver in which it
  would more aggressively solve Derived constraints; it was used
  for simplifying the context of a 'deriving' clause, or a 'default'
  delcaration, for example.

  But the complexity wasn't worth it; now I just make proper Wanted
  constraints.  See TcMType.cloneWC

* Don't generate injectivity improvement for Givens; see
  Note [No FunEq improvement for Givens] in TcInteract

* solveSimpleWanteds leaves the insolubles in-place rather than
  returning them.  Simpler.

I also did lots of work on comments, including fixing Trac #12821.

1 files changed, 16 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T12444.stderr b/testsuite/tests/polykinds/T12444.stderr
new file mode 100644
index 0000000000..0ebd2986cf
--- /dev/null
+++ b/testsuite/tests/polykinds/T12444.stderr
@@ -0,0 +1,16 @@
+
+T12444.hs:19:11: error:
+    • Couldn't match type ‘b’ with ‘'Succ (c :+: b)’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          foo :: forall (c :: Nat) (b :: Nat).
+                 SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
+        at T12444.hs:18:1-55
+      Expected type: SNat ('Succ (c :+: b))
+        Actual type: SNat b
+    • In the expression: x
+      In an equation for ‘foo’: foo _ x = x
+    • Relevant bindings include
+        x :: SNat b (bound at T12444.hs:19:7)
+        foo :: SNat ('Succ c) -> SNat b -> SNat ('Succ (c :+: b))
+          (bound at T12444.hs:19:1)