Even Haskell needs an explicit language extension flag to make this happen (-XDataKinds I believe).
Consider this use case
data Pointer = NullPointer | NonNullPointer Int
And I want a function that only accepts non-null pointers:
dereference :: NonNullPointer -> a
To do that and maintain my Pointer type, I'd have to do something like:
data NonNullPointer = NonNullPointer_ Int
data Pointer = NullPointer | NonNullPointer NonNullPointer
-- ^ The namespace of constructors and types is distinct,
-- so this is fine and is a constructor of Pointer that
-- contains a NonNullPointer, which only
-- has one constructor, NonNullPointer_ (note the _)
I believe -XDataKinds does something like this behind the scenes, but someone better than I should verify. I just use the above technique rather than questionable language extensions.
DataKinds lets you use NullPointer and all the various NotNullPointer values as types, but they are uninhabited. It doesn't (obviously) let you restrict a parameter to values using a particular constructor of a sum type.
