Note [Skolems in an implication]

GHC/Tc/Types/Constraint.hs:1731 compiler

The skolems in an implication are used:

* When considering floating a constraint outside the implication in
  GHC.Tc.Solver.floatEqualities or GHC.Tc.Solver.approximateImplications
  For this, we can treat ic_skols as a set.

* When checking that a /user-specified/ forall (ic_info = ForAllSkol tvs)
  has its variables in the correct order; see Note [Checking telescopes].
  Only for these implications does ic_skols need to be a list.

Nota bene: Although ic_skols is a list, it is not necessarily
in dependency order:
- In the ic_info=ForAllSkol case, the user might have written them
  in the wrong order
- In the case of a type signature like
      f :: [a] -> [b]
  the renamer gathers the implicit "outer" forall'd variables {a,b}, but
  does not know what order to put them in.  The type checker can sort them
  into dependency order, but only after solving all the kind constraints;
  and to do that it's convenient to create the Implication!

So we accept that ic_skols may be out of order.  Think of it as a set or
(in the case of ic_info=ForAllSkol, a list in user-specified, and possibly
wrong, order.

References 1

Referenced by 2