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
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?