That's a problem with the domain itself. Type system examples can be two of: short, concrete, well-motivated. Short concrete examples don't have time for motiva

That's a problem with the domain itself. Type system examples can be two of: short, concrete, well-motivated. Short concrete examples don't have time for motivation; concrete well-motivated examples require lots of text (or else are unreadable); and short well-motivated examples are forced to be highly abstract. There's no substitute for actually encountering a real-world problem which makes you want/need type-level programming. The article makes the sensible choice of not trying to invent one for you. I don't think it should be bemoaned for that.