As a user I usually need to know whether I'm looking at a type or a term in the code. For doing renaming in your head, it makes a difference whether you're looking at a type or a term: the namespaces are different.
Is it reasonable for that to apply to visible type application too? That is, are we assuming that the user knows they're looking at a type, or are we assuming that the user "shouldn't need to care", or something else?
> Syntactic Unification Principle (SUP). In the absence of punning, there is
no difference between type-syntax and term-syntax.
Here, "punning" means having the same identifier in scope in both terms and types. Forgetting about the possibility of punning, users shouldn't care about whether they're writing a term or a type. All syntax will have equivalent meanings in the two environments. The *only* challenge is around namespacing -- and the LSP says that, in a term, names should correspond to term-level entities.
What could we do if we were allowed to treat types differently? Well, we already do various bits of magic in T2T. But we could also use different name resolution rules. That doesn't necessarily mean we have to defer renaming until during type checking: we could resolve each name twice, once for the term context and once for the type context, and then pick one of these later when we apply the T2T mapping. (earlier Vlad objected to this idea on the grounds that it might introduce spurious recursive dependencies, though).
We *could* do this, yes, but it's in violation of the LSP (and, perhaps, the SUP). Of course, we wrote the LSP and can choose to break it, but, like Simon PJ, I think the ability to resolve names in the absence of type-checking is very valuable to readers of code.
--------------
One development on the GitHub tracker that may be of interest:
@AntC2 proposes a migration trick to allow functions to migrate from today's world to a world with this new feature. The key example is sizeOf. Today, we have
> sizeOf :: Storable a => a -> Int
where the argument to sizeOf is always unevaluated and ignored. The proposal under consideration would allow this to change to
> sizeOf' :: forall a -> Storable a => Int
(NB: do not get distracted by the movement of the constraint, which will be invisible at usage sites) The problem is that we would have to make sizeOf' a new function, likely exported from a new library, in order not to clash. This is annoying. So @AntC2 proposes (in my paraphrasing, which @AntC2 has agreed with):
* With -XNoRequiredTypeArguments, if a function f takes a required type argument of kind Type, then instead you can pass an arbitrary expression. f is called with the type of that expression; the expression is never evaluated.