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 ~ f
and[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 havec :: d
butb c :: e
, so we flatten both kinds. We thus get[D] (c |> g1) ~ b c
, whereg1 :: d ~ f a
comes from flattening. We then emit[D] f a ~ e
. The first is irreducible, but the second brings us right back where we started. (Note thate
isn't rewritten by flattening because the equality fore
is 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.