Add support for GADTs
Generalized Algebraic Data Types essentially extend standard union types to allow different generic instantiations when defined recursively.
You can see a simple explanation of how they work in haskell here: https://en.wikibooks.org/wiki/Haskell/GADT
They open the door to such fantastic type safe data structures as heterogeneous lists and so can vastly improve type safety within the language.
George Pollard commented
Regarding Don's comment: if matching over GADTs were restricted to occur in the same module, could it be compiled down to a virtual method (with an exported function that invokes it)?
Don Syme commented
A major consideration is that GADTs are difficult to compile to .NET IL efficiently. Specifically, it is not possible to recover an existentially-hidden type variable except via virtual dispatch. For example
type D<T> : C
If we have a C, a GADT implementation may "know" that for certain cases T has certain values, or decomposes in certain ways. But you can't implement this in .NET IL generics - you have to use reflection to recover the value of T and instantiate the branch code with a specific value. Russo and Kennedy had a proposal for what to do about this for C#.
This is a significant blocking factor for adding this to F# - GADT code would need reflection and would be less efficient.
Don Syme commented
There are some relevant commments here too: http://fslang.uservoice.com/forums/245727-f-language/suggestions/6062821-add-dependent-types
Since OCaml has this I don't see why not F#
Radek Micek commented
I don't think that benefits of GADTs outweight how they complicate type system and type inference (you may lose principal-type property).
BTW: you can do heterogeneous lists without GADTs.
BTW 2: you may be interested in Guarded Algebraic Data Types - http://gallium.inria.fr/~fpottier/publis/simonet-pottier-hmg-toplas.pdf