[Joker_vD]

The academic term for such types is "singleton types". They allow for some quite mind-blowing possibilities as you've shown.