It seems that one motivation is that DataKinds is “bad” in some way,
namely in that term constructors are available in types. So if we
accept this proposal, does that mean we agree with that assessment,
what are we going to do about it? Is there a better way of referring to
term constructors that we could work to wards to that works for
everyone? Or are we going to have multiple future Haskell dialects, one
with strict separation between terms and types, one with some things
also on the type level (basic literals, but no tuples or user-defined
constructors), and a third one that’s the full story?
DataKinds is indeed a "bad" extension because it introduces ambiguity to name resolution.
There are two ways to avoid this issue:
1. Keep namespaces separate and double down on using punned constructor names.
2. Merge terms and types, discouraging punned constructor names.
Each approach could indeed lead to a "dialect" of sorts.
* The (accepted and recently implemented) TypeData extension moves us in the direction of option (1), and I imagine the proposed TypeLevelLiterals would be often used in conjunction with TypeData. This carves out a limited, conservative language subset for type-level programming.
* At the same time, #270 "Support pun-free code" moves us in the direction of option (2), and I expect it to be the better option when it comes to fully fledged dependently-typed programming envisioned by #378.
If I had to choose, I'd go with option (2). I don't see myself using TypeData, nor TypeLevelLiterals for that matter. But I am of a "let a thousand flowers bloom" persuasion, hence my recommendation to accept.
- Vlad