Improve kind generalisation, error messages

This patch does two things:

* It refactors GHC.Tc.Errors a bit.  In debugging Quick Look I was
  forced to look in detail at error messages, and ended up doing a bit
  of refactoring, esp in mkTyVarEqErr'.  It's still quite a mess, but
  a bit better, I think.

* It makes a significant improvement to the kind checking of type and
  class declarations. Specifically, we now ensure that if kind
  checking fails with an unsolved constraint, all the skolems are in
  scope.  That wasn't the case before, which led to some obscure error
  messages; and occasional failures with "no skolem info" (eg #16245).

Both of these, and the main Quick Look patch itself, affect a /lot/ of
error messages, as you can see from the number of files changed.  I've
checked them all; I think they are as good or better than before.

Smaller things

* I documented the various instances of VarBndr better.
  See Note [The VarBndr tyep and its uses] in GHC.Types.Var

* Renamed GHC.Tc.Solver.simpl_top to simplifyTopWanteds

* A bit of refactoring in bindExplicitTKTele, to avoid the
  footwork with Either.  Simpler now.

* Move promoteTyVar from GHC.Tc.Solver to GHC.Tc.Utils.TcMType

Fixes #16245 (comment 211369), memorialised as
  typecheck/polykinds/T16245a
Also fixes the three bugs in #18640

1 files changed, 27 insertions, 4 deletions

diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 96bff3d261..f50cab2bb7 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -1816,10 +1816,33 @@ Here 'p' is out of scope, so we get an insoluble Hole constraint. But
 the visible type application fails in the monad (throws an exception).
 We must not discard the out-of-scope error.
 
-So we /retain the insoluble constraints/ if there is an exception.
-Hence:
-  - insolublesOnly in tryCaptureConstraints
-  - emitConstraints in the Left case of captureConstraints
+It's distressingly delicate though:
+
+* If we discard too /many/ constraints we may fail to report the error
+  that led us to interrupte the constraint gathering process.
+
+  One particular example "variable out of scope" Hole constraints. For
+  example (#12529):
+   f = p @ Int
+  Here 'p' is out of scope, so we get an insoluble Hole constraint. But
+  the visible type application fails in the monad (throws an exception).
+  We must not discard the out-of-scope error.
+
+  Also GHC.Tc.Solver.emitFlatConstraints may fail having emitted some
+  constraints with skolem-escape problems.
+
+* If we discard too /few/ constraints, we may get the misleading
+  class constraints mentioned above.  But we may /also/ end up taking
+  constraints built at some inner level, and emitting them at some
+  outer level, and then breaking the TcLevel invariants
+  See Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType
+
+So dropMisleading has a horridly ad-hoc structure.  It keeps only
+/insoluble/ flat constraints (which are unlikely to very visibly trip
+up on the TcLevel invariant, but all /implication/ constraints (except
+the class constraints inside them).  The implication constraints are
+OK because they set the ambient level before attempting to solve any
+inner constraints.  Ugh! I hate this. But it seems to work.
 
 However note that freshly-generated constraints like (Int ~ Bool), or
 ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as