Fix #19682 by breaking cycles in Deriveds

This commit expands the old Note [Type variable cycles in Givens] to apply
as well to Deriveds. See the Note for details and examples. This fixes a
regression introduced by my earlier commit that killed off the flattener in
favor of the rewriter.

A few other things happened along the way:

* unifyTest was renamed to touchabilityTest, because that's what it does.

* isInsolubleOccursCheck was folded into checkTypeEq, which does much of the
  same work. To get this to work out, though, we need to keep more careful
  track of what errors we spot in checkTypeEq, and so CheckTyEqResult has
  become rather more glorious.

* A redundant Note or two was eliminated.

* Kill off occCheckForErrors; due to Note [Rewriting synonyms], the
  extra occCheckExpand here is always redundant.

* Store blocked equalities separately from other inerts; less stuff
  to look through when kicking out.

Close #19682.

test case: typecheck/should_compile/T19682{,b}

1 files changed, 7 insertions, 5 deletions

diff --git a/testsuite/tests/dependent/should_fail/T15859a.stderr b/testsuite/tests/dependent/should_fail/T15859a.stderr
index 1fdac765f2..491733c7b9 100644
--- a/testsuite/tests/dependent/should_fail/T15859a.stderr
+++ b/testsuite/tests/dependent/should_fail/T15859a.stderr
@@ -1,6 +1,8 @@
 
-T15859a.hs:19:5: error:
-    • Cannot apply expression of type ‘KindOf A’
-      to a visible type argument ‘Int’
-    • In the expression: (undefined :: KindOf A) @Int
-      In an equation for ‘a’: a = (undefined :: KindOf A) @Int
+T15859a.hs:19:26: error:
+    • Expected kind ‘k0’, but ‘A’ has kind ‘forall k -> k -> *’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall k -> k -> *
+    • In the first argument of ‘KindOf’, namely ‘A’
+      In an expression type signature: KindOf A
+      In the expression: undefined :: KindOf A