-Note [Loopy spontaneous solving]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider the original wanted:
- wanted : Maybe (E alpha) ~ alpha
-where E is a type family, such that E (T x) = x. After canonicalization,
-as a result of flattening, we will get:
- given : E alpha ~ fsk
- wanted : alpha ~ Maybe fsk
-where (fsk := E alpha, on the side). Now, if we spontaneously *solve*
-(alpha := Maybe fsk) we are in trouble! Instead, we should refrain from solving
-it and keep it as wanted. In inference mode we'll end up quantifying over
- (alpha ~ Maybe (E alpha))
-Hence, 'solveWithIdentity' performs a small occurs check before
-actually solving. But this occurs check *must look through* flatten
-skolems.
+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 @CantSolve@ 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 'recKindErrorTcS' here, which will fail later on.
+
+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.
+
+You may think that when we spontaneously solve wanteds we may have to look through the
+bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
+@alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
+But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
+so this situation can't happen.
+
+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'
+