This problem is extremely open-ended. It reflects the kind of question you may need to answer if you ever design a language.

Consider our typing rules for datatypes. A datatype declaration defines a new type (such as nlist), and each constructor (eg, cons) creates a value of that type. As a result, however, selectors (such as first) cannot statically determine whether or not they have been given the correct variant (there are two variants of lists, for instance) of the datatype, and must rely on a check from the run-time system.

Your boss, who thinks he has a better idea of how to design a type system (your colleagues always do, and so do your students) thinks you've made a poor decision. He says that if you instead create a new type for each variant, you can give a very precise type for the selector — thus turning the dynamic check into a static one, thereby increasing the effectiveness of the type system. (You ask him what to do about the new type declared in the datatype declaration — should the programmer no longer declare it? Should they declare two or three new types when defining lists? He hasn't of course thought this issue out in that much depth — that's your problem — so he just murmurs and asks you to do at least a little work in return for the brainwave he's just handed you.)

Write at most a page (of reasonably-sized text) exploring this question. Can we build an effective type system out of this idea? If so, how, and if not, why not? If so, why hasn't someone already done this? If not, can we turn this germ of an idea into something that actually works? Have you seen any languages that do something like this?