Haskell has two namespaces: one for types, one for terms.
Here is a definition of the identity function that uses distinct names for the type variable and the term variable:
id :: forall a. a -> a id = \x -> x
Here is a version that reuses the same name for both variables:
id :: forall a. a -> a id = \a -> a
The reason we can give two variables the same name is that each lives in its own namespace. There is no shadowing here.
A similar situation arises when it comes to constructors. Here is the unit type that uses distinct names for the type constructor and the data constructor:
data Unit = U
Here is a version that reuses the same name for both constructors:
data Unit = Unit
Haskell uses this style of punning in its standard library and built-in types:
data [a] =  | a : [a] data (a, b) = (a, b) data () = () data Proxy a = Proxy newtype Identity a = Identity a
You might find it elegant or convenient, but it has caused me nothing but pain for several reasons:
. For someone new to programming, the last thing they need is having to distinguish between the meaning of
(a,b)depending on whether the thing is to the left or to the right of
Proxythe type constructor or
Proxythe data constructor, same goes for
Identityand other types. In this post I employed color to convey this information (blue for types, orange for terms).
-XDataKindsrequires ticks to disambiguate the namespace, for example
'. This is both unpleasant to read and confusing to many a syntax highlighter.
-XDataKindsare in conflict with Template Haskell syntax for identifier quotation, which is bad news for type-level Template Haskell. There is no way to refer to a type constructor in terms, which is bad news for Dependent Haskell.
Using distinct names for type constructors and data constructors is not that difficult:
data List a =  | a : List a data Pair a b = (a, b) data Unit = () data Proxy a = P newtype Identity a = Id a
However, it is probably too late to consider this.
We would be better off if Haskell did not have this style of punning in the first place. Designers of new programming languages, my plea to you: learn from this mistake and resist the temptation of meaningless overloading!