Tc gets in an Infinite `Loop`

[fxdpntthm]

type family Loop where
   Loop = [Loop]

qqqq :: Loop -> Int
qqqq _ = 3

type checker loops while elaborating of type signature of qqqq.

[jgbm]

It sure does.

This is essentially the pay-off of the discussion at the bottom of page 8 of constrained type families:

We can add the instance

instance Loopy ⇒ Loopy where
   type Loop = [Loop]

but it is clear that the Loopy constraint cannot be satisfied. Thus, any attempt to use this Loop equation must be guarded by an unsatisfiable Loopy constraint, and so cannot compromise type safety.

If you were to add that instance, then instance solving could (hypothetically) diverge—as it would attempt to solve Loopy using the instance Loopy ⇒ Loopy forever. With our implementation, we're accomplishing the same thing.

This is kinda what I mean when I say that we have all the pain of CTF, but none of the payoff. We expect Loop to be unusuable in our system, and indeed it is.........

[fxdpntthm]

I see, I changed the definition for it to be an associated type:

class Loopy where 
  type Loop

instance Loopy where
  type Loop = [Loop]

also diverges and so does

instance Loopy => Loopy where
  type Loop = [Loop]