GitLab

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.

1. can_eq_nc' will get to its flattening clause, so both sides get flattened, yielding [D] g c ~ f (b c).
2. can_eq_nc' then decomposes to [D] g ~ f and [D] c ~ b c. We'll continue here with the latter.
3. 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.
4. Then, we go to canEqTyVar. We have c :: d but b c :: e, so we flatten both kinds. We thus get [D] (c |> g1) ~ b c, where g1 :: 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 that e isn't rewritten by flattening because the equality for e 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.