Loop in the constraint solver around variables free in kinds
Spun off from the bowels of #17323 (#17323 (comment 243178), #17323 (comment 243577), #17323 (comment 244748)), but I think orthogonal to that ticket. No need to read that ticket to understand this one.
Here is a simple form of the potential problem (due to @simonpj):
Inert set: [G] b ~ a Work item: [G] (a :: *) ~ (c :: b -> *) (d :: b)
I think GHC will add that work item to the inert set, despite the fact that it seems loopy.
And in this example, I think we'll actually get a loop:
a :: e b :: d -> e c :: d d :: Type e :: Type f :: e -> Type g :: d -> Type inert set: [D] a ~ b c [D] e ~ g c [G] g1 :: d ~ f a -- just having `a` here would violate K3a of Note [Extending the inert equalities] work item: [D] e ~ f a
Let's see what happens.
can_eq_nc'will get to its flattening clause, so both sides get flattened, yielding
[D] g c ~ f (b c).
can_eq_nc'then decomposes to
[D] g ~ fand
[D] c ~ b c. We'll continue here with the latter.
- On the new work item
[D] c ~ b c,
can_eq_nc'will get to its flattening clause, so both sides get flattened, causing no change.
- Then, we go to
canEqTyVar. We have
c :: dbut
b c :: e, so we flatten both kinds. We thus get
[D] (c |> g1) ~ b c, where
g1 :: d ~ f acomes from flattening. We then emit
[D] f a ~ e. The first is irreducible, but the second brings us right back where we started. (Note that
eisn't rewritten by flattening because the equality for
eis a Derived, which cannot be used to rewrite a kind.)
This comment below shows
f8 which shows an actual loop from this case. Plus: the other examples there show cases where simply re-ordering the constraints in a type changes the accept/reject behaviour; this is Bad.