+Note [Kind errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the wanted problem:
+ alpha ~ (# Int, Int #)
+where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
+but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
+simply returns @Nothing@ then that wanted constraint is going to propagate all the way and
+get quantified over in inference mode. That's bad because we do know at this point that the
+constraint is insoluble. Instead, we call 'kindErrorTcS' here, which immediately fails.
+
+The same applies in canonicalization code in case of kind errors in the givens.
+
+However, when we canonicalize givens we only check for compatibility (@compatKind@).
+If there were a kind error in the givens, this means some form of inconsistency or dead code.
+
+When we spontaneously solve wanteds we may have to look through the bindings, hence we
+call zonkTcTypeTcS above. The reason is that maybe xi is @alpha@ where alpha :: ? and
+a previous spontaneous solving has set (alpha := f) with (f :: *). The reason that xi is
+still alpha and not f is becasue the solved constraint may be oriented as (f ~ alpha) instead
+of (alpha ~ f). Then we should be using @xi@s "real" kind, which is * and not ?, when we try
+to detect whether spontaneous solving is possible.
+
+
+Note [Spontaneous solving and kind compatibility]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Note that our canonical constraints insist that only *given* equalities (tv ~ xi)
+or (F xis ~ rhs) require the LHS and the RHS to have exactly the same kinds.
+
+ - We have to require this because:
+ Given equalities can be freely used to rewrite inside
+ other types or constraints.
+ - We do not have to do the same for wanteds because:
+ First, wanted equations (tv ~ xi) where tv is a touchable
+ unification variable may have kinds that do not agree (the
+ kind of xi must be a sub kind of the kind of tv). Second, any
+ potential kind mismatch will result in the constraint not
+ being soluble, which will be reported anyway. This is the
+ reason that @trySpontaneousOneWay@ and @trySpontaneousTwoWay@
+ will perform a kind compatibility check, and only then will
+ they proceed to @solveWithIdentity@.
+
+Caveat:
+ - Givens from higher-rank, such as:
+ type family T b :: * -> * -> *
+ type instance T Bool = (->)
+
+ f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
+ flop = f (...) True
+ Whereas we would be able to apply the type instance, we would not be able to
+ use the given (T Bool ~ (->)) in the body of 'flop'
+
+Note [Loopy Spontaneous Solving]