Lawvere theories

While you can write the Infinity with undecidable instances, I’m pretty sure that using it anywhere in your code will throw the type checker into an infinite loop. One comment I recall, which showed how data families can be used to the same effect as my Stuck said

That’s a good reminder that pattern matching on types is never total.

Sorry, I’m on my phone so this comment might be a bit unreadable.