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.

4 files changed, 85 insertions, 3 deletions

diff --git a/testsuite/tests/polykinds/T12444.hs b/testsuite/tests/polykinds/T12444.hs
new file mode 100644
index 0000000000..746c6448ef
--- /dev/null
+++ b/testsuite/tests/polykinds/T12444.hs
@@ -0,0 +1,65 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T12444 where
+
+data Nat = Zero | Succ Nat
+
+data SNat (n :: Nat) where
+  SZero :: SNat Zero
+  SSucc :: SNat n -> SNat (Succ n)
+
+type family (:+:) (a :: Nat) (b :: Nat) :: Nat where
+  m :+: Zero = m
+  m :+: (Succ n) = Succ (m :+: n)
+
+foo :: SNat (Succ c) -> SNat b -> SNat (Succ (c :+: b))
+foo _ x = x
+
+
+{-
+sadd :: ((Succ n1 :+: n) ~ Succ (n1 :+: n), (Succ n1) ~ m)
+     => SNat m -> SNat n -> SNat (m :+: n)
+sadd SZero n = n
+-}
+
+{- [G]  a ~ Succ c
+        Succ c + b ~ Succ (c+b)
+        a ~ Zero
+
+-->
+        Zero ~ Succ c            TyEq
+        fsk1 ~ Succ fsk2         TyEq
+        fsk1 ~ (Succ c) + b      FunEq
+        fsk2 ~ c+b               FunEq
+----
+[W] b ~ a+b  --->   b ~ Succ (c+b)
+
+
+Derived
+       a ~ Succ c
+       fsk1 ~ Succ fsk2
+       b ~ Succ fsk2
+
+work   (Succ c) + b ~ fsk1
+       c+b ~ fsk2
+
+
+-}
+
+{-
+
+[G] a ~ [b]
+--> Derived shadow [D] a ~ [b]
+    When adding this to the model
+    don't kick out a derived shadow again!
+
+[G] (a ~ b)  --> sc   a ~~ b, a ~# b
+  Silly to then kick out (a~b) and (a~~b)
+  and rewrite them to (a~a) and (a~~a)
+
+Insoluble constraint does not halt solving;
+indeed derived version stays. somehow
+-}
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)
diff --git a/testsuite/tests/polykinds/T9222.stderr b/testsuite/tests/polykinds/T9222.stderr
index df97578029..dc1b92c202 100644
--- a/testsuite/tests/polykinds/T9222.stderr
+++ b/testsuite/tests/polykinds/T9222.stderr
@@ -1,12 +1,12 @@
 
 T9222.hs:13:3: error:
-    • Couldn't match type ‘b0’ with ‘b’
-        ‘b0’ is untouchable
+    • Couldn't match type ‘c0’ with ‘c’
+        ‘c0’ is untouchable
           inside the constraints: a ~ '(b0, c0)
           bound by the type of the constructor ‘Want’:
                      a ~ '(b0, c0) => Proxy b0
           at T9222.hs:13:3
-      ‘b’ is a rigid type variable bound by
+      ‘c’ is a rigid type variable bound by
         the type of the constructor ‘Want’:
           forall i1 j1 (a :: (i1, j1)) (b :: i1) (c :: j1).
           (a ~ '(b, c) => Proxy b) -> Want a
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 6ec2a439e6..0e0d66a676 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -154,3 +154,4 @@ test('T12055a', normal, compile_fail, [''])
 test('T12593', normal, compile_fail, [''])
 test('T12668', normal, compile, [''])
 test('T12718', normal, compile, [''])
+test('T12444', normal, compile_fail, [''])