Given f :: forall a -> t, while x in f x is a type, it is parsed and renamed as a term, and then reinterpreted as a type

Seeing as, apparently, the only difference between forall a . and forall a -> is visibility, would it make sense to change f @x, given f :: forall a . t, to use this same parsing as term/reinterpreting as type procedure for x? It seems like this should improve consistency and reduce future maintenance burden (one process instead of two for type applications), while not being too much additional work to implement.

And some bikeshedding - while, in principle, I prefer the capitalization of -XVisibleForall, it is inconsistent with the already existing -XExplicitForAll.

Seeing as, apparently, the only difference between forall a . and forall a -> is visibility, would it make sense to change f @x, given f :: forall a . t, to use this same parsing as term/reinterpreting as type procedure for x?

Sounds reasonable, but this would be a breaking change. Consider:

data T = T

x = f @T

Which T is referenced here? Today it's the type constructor, but with updated rules it would be the data constructor.

The proposal says:

• Allow forall a -> blah in types, as proposed.
• For functions with such a type, require an explicit type argument

One way to meet "require an explicit type argument" is to write applications as f type, thus f Int or f (Mabybe Int). An obvious alterantive is to signal those type arugments, with their change of syntax and namespace, explicitly, thus f @Int or f !Int or something. It's worth pointing out that this is a possible choice and discussing the tradeoffs.

It's worth noting that, as proposed,

• one can parse expressions without knowing whether an argument is a type or a term, because the syntax of types and terms is united in big union.
• But one cannot rename an expression. For example

  f :: forall a. blah
  f a = g a
  

  In the argument to g, am I referring to f's value parameter a, or to the type variable a bound by the forall? We can't tell until we know the type of g`. That's a problem for the renamer.
• In the typechecker we finally know the types, so we can "reinterpret" the argument as a type if necessary.

we all agree that the term/type unification is The Right Thing.

I am open to that as a future possiblity but, as you know, I am not ready to commit to it. I'd like to accept or reject this propsoal on its own merits.

It's worth pointing out that this is a possible choice and discussing the tradeoffs.

I added this as an alternative and explained why I don't think it's a good one.

In the typechecker we finally know the types, so we can "reinterpret" the argument as a type if necessary.

To be clear, reinterpretation as proposed does not change how the names were resolved. That is, if a was referring to a term-level variable, it continues to do so, and ends up as a type error.

I am open to that as a future possiblity but, as you know, I am not ready to commit to it. I'd like to accept or reject this propsoal on its own merits.

This proposal is a step towards a destination, and if we disagree about the destination, I'm not sure we should invest time and effort into making this step. That is, I don't believe this proposal has a good power-to-weight ratio if we look at it in isolation. Looking at the motivation section, we have:

1. Language consistency (symmetry between terms and types)
2. Ability to design better APIs (good error messages, no proxy types, no ambiguous types)
3. Prepare the compiler internals for further work on dependent types

But:

Point 3 refers to pi-types, which will require term/type unification either way. Point 1 is about symmetry between terms and types, which means little if we do not seek to unify them. Point 2 alone is not sufficient to make this proposal worthwhile (in my opinion).

When VisibleForAll is in effect, lift the restriction that the forall a -> quantifier cannot be used in terms.

I just want to be careful about language here. forall a -> cannot, in this proposal, be used in terms. It can be used in types of terms. This happens in several places.

It is sad that the renaming of a visible dependent argument is different than that of a specified dependent argument. Maybe it is inevitable, but it's sad. If we imagine dependent Haskell, it will be a wart on the language. If we end up accepting this proposal as currently written, I would welcome a separate proposal (or maybe a rider on this one) that we add a warning to -Wcompat whenever a visible type application uses a name in scope at the term level, and then to move the warning to -W, and then switch the renaming, all in due course.

However, since we rename this as a term, we retain the fixities of term-level operators.

This doesn't seem right. Consider an argument x + y. If + is in scope as a term, then we can't reinterpret, as explained elsewhere. Otherwise, + must be in scope as a type and the phrase "fixities of term-level operators" does not make sense.

Do we need to make forall a keyword in terms? It seems possible to live without this, making forall a keyword only in types. If a forall is used in a visible dependent argument, we can just reinterpret the syntax.

Maybe it's s good idea to make forall a keyword everywhere, but I want to establish whether or not it's an essential part of this proposal.

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing.

This section is almost worthy of its own proposal. With my GHC-committee hat on (leaving my Dependent-Types hat to the side), I'm very dubious of this. And I don't see it as essential here.

I understand that the proposal process is onerous, and I'm sympathetic to attempts to short-circuit it. Indeed, I support the suggestion you have here (as long as the changes are non-breaking -- fixing Symbol will be a breaking change, for example). But I still say it shouldn't be tied to this particular proposal.

Nice example.

I do not see a need for a new extension here. We have too many extensions! Just hook into ExplicitForAll. I expect others may disagree on this point.

We don't have a unified type/term parser yet, do we? This proposal is designed assuming that these parsers are mergeable. That may be true, but I don't yet have evidence of it. Is this simply impossible because of forall? (I doubt that.) I'm worried that, after we accept this proposal, we'll realize we have to make a subtle syntactic change in order to merge the parsers, and then we'll either have to retract this proposal or make some breaking change to the language.

On the other hand, it would seem a waste of effort to merge these parsers without the acceptance of this proposal, unless it served to reduce complexity in the parser and improve error messages.

I'm unsurprisingly in favor, in general.

It is worth noting that making forall a keyword at the term level by default will break a sizable chunk of code in the wild. A quick Hackage search reveals 53 top-level functions on Hackage named forall. (Ironically, one of those packages is Idris.)

I just want to be careful about language here. forall a -> cannot, in this proposal, be used in terms. It can be used in types of terms. This happens in several places.

Yes, "forall in terms" isn't quite right, I changed the language to "in types of terms".

It is sad that the renaming of a visible dependent argument is different than that of a specified dependent argument. Maybe it is inevitable, but it's sad. If we imagine dependent Haskell, it will be a wart on the language.

This is resolved by #270, no? With -Werror=punning, name resolution is the same in terms and types.

This doesn't seem right. Consider an argument x + y. If + is in scope as a term, then we can't reinterpret, as explained elsewhere. Otherwise, + must be in scope as a type and the phrase "fixities of term-level operators" does not make sense.

Right, I removed the part about fixities.

Maybe it's s good idea to make forall a keyword everywhere, but I want to establish whether or not it's an essential part of this proposal.

Assume we do not make forall a keyword and attempt reinterpretation. We parse x = f (forall a. a) as the . operator, and forall a as its LHS.

Before we get to type-checking (where reinterpretation should happen), we do name resolution. We end up trying to resolve . as an operator (which may fail), forall as an identifier (which may fail), and a as a variable (which is no longer bound). Not good.

The real question is not whether to make forall a keyword in terms, but whether to make it a keyword in terms only when ExplicitForAll is in effect. Implementation-wise, it would be easy to do it as long as that was what we did in types too. That is:

• it is easy to make forall a keyword only under -XExplicitForAll (as was the case before Make forall a keyword in types #193)
• it is easy to make forall a keyword, always (as is proposed here)
• it is not so easy to make forall a keyword in types always, and in terms only under -XExplicitForAll

Not to say that it's impossible, but it would require some fancy footwork. Every discrepancy between terms and types is a burden.

Indeed, I support the suggestion you have here (as long as the changes are non-breaking -- fixing Symbol will be a breaking change, for example).

I added "non-breaking" to clarify the intent.

But I still say it shouldn't be tied to this particular proposal.

The thought process behind this is that by introducing this reinterpretation business, we add a bit of ugly complexity, but at least we plan to get rid of it down the line. If we don't agree that we should be moving away from reinterpretation of terms as types, and towards unification of terms with types, then maybe we shouldn't be adding reinterpretation in the first place. It's scaffolding, not the final product.

I do not see a need for a new extension here.

I disagree, but not strongly. Added to alternatives, happy to do whatever the committee decides about this.

This proposal is designed assuming that these parsers are mergeable. That may be true, but I don't yet have evidence of it.

I'm happy to do go ahead and merge them, but before I do this, let's agree first that this is even a thing we want to do!

I'm worried that, after we accept this proposal, we'll realize we have to make a subtle syntactic change in order to merge the parsers, and then we'll either have to retract this proposal or make some breaking change to the language.

Sure, then we'll do either of these things:

• Retract this proposal
• Go through another proposal process for the required breaking changes

I only expect that we first agree that this is the direction we all want to go in, and so far @simonpj indicated that this is not necessarily the case.

A quick Hackage search reveals 53 top-level functions on Hackage named forall. (Ironically, one of those packages is Idris.)

The search query doesn't seem right to me, as the results include identifiers such as pforall, _forall, check_exists_forall, can_eq_nc_forall, ppr_forall, fresh_forall, etc. The actual amount should be smaller than 53, and even then, there will be a three-release (1.5 years) migration period.

we all agree that the term/type unification is The Right Thing.

No. Do not use the first person there. I think you mean the elite and increasingly exclusive brethren at GHC HQ want to unify terms/types. Fine. Suggest you stop calling the resulting language 'Haskell'.

@AntC2

elite and increasingly exclusive brethren at GHC HQ

I'll point out that both Simon and I have balked at the bit of the proposal you're criticizing here. I personally do think this is a good direction of travel, but I wouldn't presume to say that others do, too.

@int-index

Before we get to type-checking (where reinterpretation should happen), we do name resolution. We end up trying to resolve . as an operator (which may fail), forall as an identifier (which may fail), and a as a variable (which is no longer bound). Not good.

I'll point out that name lookup failures do not stop the compilation pipeline. They don't even induce warnings or errors! (It's trying to give them a type that produces the errors.) So I still claim that this is possible. Maybe not preferable, but possible.

[Difference between name lookup in required arguments and specified arguments] is resolved by #270, no?

Not quite. While -Werror=punning does make the problem go away, nowhere do we have a plan to put -Wpunning even in -W, much less make it a hard error. One might argue that anyone using dependent Haskell is well-advised to do so, but it would still be a strangeness in the language.

@goldfirere I'll point out that both Simon and I have balked at the bit of the proposal you're criticizing here.

Thank you Richard, I apologise my intemperate language was a (visceral) reaction against @int-index's high-handed presumption. If there's some merit to unifying types/terms, Vladislav needs to carry everybody with him by persuading and demonstrating how it supports better programming (for some value of 'better').

We've always had unified syntax for type construction and data construction; and somewhat similar for pattern matching (if we allow class and TF instances as type-level patterns). That doesn't persuade me we have or need unified semantics; because ...

GHC Haskell (even more than Hugs Haskell) is a multi-module compiled language. There's a phase distinction between the semantics at compile time (type inference) vs execution time. Needing to support multi-module (where the compiler can't know what other modules this might get imported into) puts a hard block on what can happen when.

I think it's important users of Haskell understand that distinction. Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction.

To @AntC2,

No. Do not use the first person there. I think you mean the elite and increasingly exclusive brethren at GHC HQ want to unify terms/types.

In this particular sentence, "we" refers to everyone involved in the discussion. I see that you disagree – alright, then it's up to me to improve the Motivation section until that phrase, "we all agree that the term/type unification is The Right Thing", becomes true.

Note how it is prefixed by "by accepting this proposal". Let's not accept it until we reach consensus.

Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction.

I'm afraid this argument went over my head. There are other multi-module compiled languages, which are dependently typed and use the same language for types and terms. Could you demonstrate how this distinction grins through the abstraction in those languages, using the one most familiar to you? (I'll make the effort to understand the example whatever language you pick, but I'm most familiar with Agda/Coq/Idris)

To @goldfirere,

I'll point out that name lookup failures do not stop the compilation pipeline. They don't even induce warnings or errors! (It's trying to give them a type that produces the errors.) So I still claim that this is possible. Maybe not preferable, but possible.

That's something I didn't realize. I think there are other ways this hack may fail. For example:

infix 9 %
x = f (forall a. T a % G x)

This results in an error before the type checker:

    Precedence parsing error
        cannot mix ‘.’ [infixr 9] and ‘%’ [infix 9] in the same infix expression

In general, I'm very wary of reinterpreting syntactic constructs. Parsing forall a. t with . as an infix operator is exactly the sort of thing that sets off an alarm in my head. Another one was parsing bang patterns f !x = ... as infix operators, which led to #1087 and #17162. Fixing this required the proposal #229, which I'm still implementing (there's a prototype, !1664).

So, why would we add new faulty code like this, while firefighting its consequences in other places? The reason reinterpretation as described in this proposal isn't that bad is that there are direct equivalences between the reinterpreted constructs:

1. HsLit becomes HsTyLit
2. HsVar becomes HsTyVar
3. HsApp becomes HsTyApp
4. OpApp becomes HsOpTy

... and so on. The reinterpretation of terms as types is direct. My hope is that in the end, we can fully unify them, removing the need even for a direct reinterpretation. On the other hand, parsing forall a. t as OpApp and then reinterpreting it as HsForAllTy rather than HsOpTy is just the sort of thing that can't end well.

While -Werror=punning does make the problem go away, nowhere do we have a plan to put -Wpunning even in -W, much less make it a hard error. One might argue that anyone using dependent Haskell is well-advised to do so, but it would still be a strangeness in the language.

What if -XVisibleForAll implies -Werror=punning, would that work?

Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction.

There are other multi-module compiled languages, which are dependently typed ...

There you go again making a high-handed presumption (in fact much the same presumption) that Haskell must become a dependently-typed language. It's a lot less than clear how we get there from a language whose typing theory was originally based on Damas-Hindley-Milner. It's an open research question whether such a migration is possible without breaking too much. My guess is it's hard; and that you might end up with a language that is 'based on Haskell' but is not Haskell.

You need to not only improve the Motivation section here, but the Motivation for each step along the journey. There's currently no roadmap. Section 4 Meta is not a roadmap, it reads more like handing over the hen-house to the fox. (This is my favourite language you're messing with. Already the fluffy chicks I first knew have become cantankerous broilers.)

Could you demonstrate how this distinction grins through

It's already grinning through in a small way. With promoted DataKinds there's occasionally ambiguity within types as to whether some name (eg Bool) denotes a type or a promoted type-of-type, thus needing the ' prefix. Haskell was not originally designed for Dependent typing; it was designed with separate namespaces for type-level vs term-level (and no namespace for type-of-type level). So with no risk of ambiguity, punning type names as term names is ubiquitous. So within the syntax for terms there's always clear syntactic demarcation that types appear only to the right of :: (or within the scope of @). That syntactic demarcation is a valuable analogue of the phase distinction. In

ghci> rgb "red"
ghci> Foo Foo Bar Bar

(And of course real-life terms will be more complex) I'm seeing "red", Foo, Bar as term-level. You're ushering me into a world of fear, uncertainty and doubt for any term: which are the types, which are the terms? If the first Foo is a data constructor, the second could be a type, the Bars could also be one of each.

To understand the semantics I need to bear in mind: terms are evaluated left-to-right by Beta-reduction; types are solved Outside-In by unification. (Yes that's a gross simplification.)

[languages that] use the same language for types and terms.

Those languages designed from the ground up for Dependent Typing: do they support punning type-names as term-level names; and punning term-level literals as types?

the abstraction in those languages, using the one most familiar to you? (I'll make the effort to understand the example whatever language you pick, but I'm most familiar with Agda/Coq/Idris)

Coq is a theorem-prover not comparable to Haskell; Agda/Idris are as much theorem-provers/proof assistants as programming languages. I don't see any of them as achieving the industrial-strength optimised object code that Haskell achieves.

And thank you for the invitation, but no I'm not going to enter into some language war. As @simonpj already said "I'd like to accept or reject this propsoal on its own merits." The argument you're making implicitly 'This proposal moves Haskell closer to Coq/Agda/Idris' does not give any merits.

(@int-index you might want to edit the PR name and description to "in types of terms" as well?)

2. Ability to design better APIs (good error messages, no proxy types, no ambiguous types)
   Point 2 alone is not sufficient to make this proposal worthwhile (in my opinion).

I want to add that point 2 is enough for me to consider this proposal useful and worthy to be implemented. It opens a possibility to improve the UX of Haskell users which I value a lot (and I think we all should care about improving Haskell UX for beginners, but that's just my opinion). Haskell has a reputation for being non-beginner-friendly and with this feature, developers can implement better libraries. Below I'm going to provide a few examples from production usage of Haskell where I can find this feature useful.

1. Better show. Sometimes I use show to format custom values. And sometimes people silently update their dependencies and my code breaks (which also can sometimes be quite painful to debug if maintainers don't update CHANGELOG properly and don't write proper migration guides). So in some cases, I want to require explicit type annotations. The following function solves this problem:

   show :: forall a -> Show a => a -> String

2. Sometimes I call length on various containers data types. And sometimes I refactor code changing types from [a] to Maybe [a] or [a] to (Int, a). Since length works for any Foldable, the code after such refactoring still compiles, but it contains an invisible error that can lead to some serious hard-to-find bugs later (we had this happening, and we spent 2 days to find this bug). I agree that this is a general problem with such polymorphic code and with Foldable the proposed solution doesn't work if you change [a] to [[a]]. However, the solution might not be perfect it's is still extremely useful.

   length :: forall a. forall f -> Foldable f => f a -> Int

3. In our code, we have the Id newtype with a phantom type parameter. And we also have castId function that changes this tag. It would be much nicer to be able to force users of this function to specify type argument of result to make code more readable and not break it accidentally when you change Id User to Id Admin.

   newtype Id a = Id { unId :: UUID }
   
   type AnyId = Id ()
   
   castId :: forall from . forall to -> Id from -> Id to

4. We're using proto-lens library by Goole which implements Protocol Buffers data type and codecs generation in Haskell. In this library you need to use a polymorphic variable defMessage :: Message a => a to construct data types. However, we want to specify the type argument of this defMessage explicitly not to break code accidentally and make the refactoring easier and improve code readability. So we want the following functions:

   defMessage :: forall a -> Message a => a

As you can see from my examples, I often want to be able to force users to specify the type of argument explicitly. It's often useful that with forall x. type is inferred automatically for you, but sometimes you want to the specify the type explicitly. I believe that it's possible to solve this problem differently, with some external tools or enforcing guidelines (which is fragile) or some ad-hoc mechanism for this specific case. But at least the solution with visible forall in terms seems sane and elegant enough for this problem.

@goldfirere

Not quite. While -Werror=punning does make the problem go away, nowhere do we have a plan to put -Wpunning even in -W, much less make it a hard error. One might argue that anyone using dependent Haskell is well-advised to do so, but it would still be a strangeness in the language.

I think this is good enough. I am fine with people using multiple namespaces thinking of @arg as a "type thing", and plain arg as a "term thing". The beauty of @ being just about visibility and orthogonal to everything else is the same beauty as using the same parser and namespace for both types and terms. If the user isn't drawn to the aesthetics of one of those, they probably aren't drawn to the other, either.

As to the eventual goals discussion, I think it's important to remember that these are ghc-proposals not haskell-proposals. I am fine rebranding "Dependent Haskell" as, I dunno, "Alonzo", if we agree that GHC should support both and they should freely interoperate type safely.

Now, when this proposal says

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing

We should understand not as

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing for Haskell.

but as:

Hence, by accepting this proposal, we all agree that the term/type unification is The Right Thing for GHC's core, in order to support future language research for Haskell or other interoperable languages.

I think that's hard to argue against. The people working on GHC which to research these things. This proposal is inarguably a good step in service of that goal. Haskell 98 remains Haskell 98. What's the problem?

@chshersh improve the UX of Haskell users which I value a lot (and I think we all should care about improving Haskell UX for beginners, but that's just my opinion). Haskell has a reputation for being non-beginner-friendly

Yes where I'm coming from is the UX. For beginners we used to offer an easier experience, with the mind-twisting bits hidden away behind extensions.

Then I'm very puzzled by @chshersh's comment. Haskell 98, and even including common extensions such as MPTCs is user friendly. What has made GHC Haskell non-beginner-friendly is that it's increasingly difficult to hide the mind-twisting bits. I see this proposal as one more twist.

and with this feature, developers can implement better libraries.

Well yes maybe (for some value of 'better'). The examples you give of better libraries: do you expect beginners to use them, with explicit type application? And without some syntactic marking that types are appearing in terms? That seems to me the opposite of beginner-friendly. To remind, the story we give to beginners is:

1. Recommend giving signatures for your functions, as machine checked documentation and sanity check over both the equations for those functions and the usage sites. Having done that ...
2. The power of type inference (Hindley-Milner) means you can write higher-order functions and partial applications and use library-supplied highly abstract combinators, without having to hand-thread the types through them.
3. That is, beginners rarely need type annotations in terms nor explicit type applications.

Unfortunately GHC is currently failing at point 1. If you write a dodgy signature (which beginners are very prone to), GHC rather than saying that's probably not what you meant, recommends you switch on AllowAmbiguousTypes; then you slide down a few rabbit-holes and find you need ExplicitApplication -- i.e. at point 3 where beginners should not be. Absolutely not beginner-friendly when the problem was the original signature. There's a proposal to avoid that -- motivated precisely by the large amount of beginner-confusion.

@Ericson2314 the term/type unification is The Right Thing for GHC's core,

I have no view on that. Remember GHC's core is not Haskell, and has always had explicit type application; that's compulsory explicit-type-application-everywhere. Remember that GHC core is type-checked; but has no type improvement/type inference mechanisms. That's OK as an intermediate language whose type applications are generated mechanically. Nobody writes core by hand do they? That would be like bit-aligning and byte/word-aligning data layouts by hand.

For some features from core, it has been useful to expose them in surface Haskell. Compulsory explicit-type-application-everywhere is not one of those features. I (for one) don't expect beginners to look at core; I don't expect they'll know that core has explicit type application; I do position Haskell for beginners as a High Level Language which to a large extent looks after the types for itself. If you enjoy burdening your code with type-management, C is a fine language.

@AntC2 With all due respect, please knock it off. Virtually nothing you've written on this thread pertains to this specific proposal. It's all general grousing about the direction of GHC.

Let's be clear: I've been to many talks by Richard and others on the work being done to bring dependent types to haskell. Invariably, the first question, to significant applause, is "how soon can we get it?" So yes, there is great demand for this, and there are many proposals pertaining to it.

If you don't like that direction -- go find a better venue to convince people otherwise. Write to a mailing list, write a blog post. Complain on reddit.

But derailing specific proposals over your complaints about a general direction that many people, with much support, are working towards -- that's not appropriate, and I wish you would stop.

To @glaebhoerl,

you might want to edit the PR name and description to "in types of terms" as well?

Yes, thank you. Fixed it.

To @chshersh,

Thank you for all the examples. I'm not sure what would be a good way to incorporate them into the proposal, as it is a matter of judgement whether to use visible or invisible forall there. After all, there are no ambiguous variables in those examples.

But it's still valuable to see these examples in the discussion, and to know that visible forall could be used to improve APIs, even if the improvement is subjective.

To @AntC2,

There you go again making a high-handed presumption (in fact much the same presumption) that Haskell must become a dependently-typed language.

I'm rather of the opinion that Haskell should provide an option of dependent typing, as I find it immensely useful, but it's up to the programmer whether to make use of dependent types.

What has made GHC Haskell non-beginner-friendly is that it's increasingly difficult to hide the mind-twisting bits. I see this proposal as one more twist.

The proposed change is hidden behind an extension, VisibleForAll. Haskell2010 remains as is. Same goes for the extended clause about term/type unification: it would not affect the standard language.

With promoted DataKinds there's occasionally ambiguity within types as to whether some name (eg Bool) denotes a type or a promoted type-of-type, thus needing the ' prefix. Haskell was not originally designed for Dependent typing; it was designed with separate namespaces for type-level vs term-level (and no namespace for type-of-type level). So with no risk of ambiguity, punning type names as term names is ubiquitous.

Let's put dependent types aside for the moment.

As far as I understand your arguments, you care a lot about making Haskell beginner-friendly (so do I). But then, the consistent thing would be to become a proponent of term/type unification and getting rid of punning. In my teaching experience, it's difficult for beginners to keep track of the current context, and to realize that [a] may mean either a singleton list with the element a, or the type of lists where each element has type a.

So, even without dependent types, using a single language for terms and types, and eschewing punning, would be a win.

1. Recommend giving signatures for your functions, as machine checked documentation and sanity check over both the equations for those functions and the usage sites.
   Unfortunately GHC is currently failing at point 1.

With all the extensions that were added to GHC, the inference is not any worse as long as you do not enable them. So I don't think that GHC is failing here, its inference engine is a blazing success.

I do position Haskell for beginners as a High Level Language which to a large extent looks after the types for itself. If you enjoy burdening your code with type-management, C is a fine language.

I'm afraid there are differences between C and Haskell other than the amount of required type annotations.

And thank you for the invitation, but no I'm not going to enter into some language war.

This was not an invitation for a language war, but an attempt to understand your point of view on the matter. As far as I can tell, the argument goes like this:

1. Haskell is a multi-module compiled language
2. In such a language, there is a phase distinction between terms and types
3. Therefore, any attempt to unify terms/types is a leaky abstraction

I don't believe we can jump from (2) to (3), and the existence of other multi-module compiled languages with dependent types is evidence that I used to back up the claim that, in fact, term/type unification is a very reasonable thing to have in a multi-module compiled language such as Haskell.

But of course I'm always considering the possibility that I'm wrong, so I asked you to compromise my evidence, so that I could change my view and we'd end up on the same page.

The goal of this argument is to arrive at the consensus, is it not?

Just to reiterate, I think the following holds true:

1. I care about industrial applications of dependent types, but you do not. (That's fine!)
2. We both care about beginner experience with Haskell. (Very good, we agree here)
3. You believe term/type unification and dependent types would be detrimental to beginners' experience (I disagree, but it doesn't matter because...)
4. The proposed features are to be hidden behind extension flags, and GHC continues to support the Haskell dialect that you cherish (lacking dependent types).

Or, as @Ericson2314 puts it:

This proposal is inarguably a good step in service of that goal. Haskell 98 remains Haskell 98. What's the problem?

Finally, to @gbaz,

With all due respect, please knock it off. <...> If you don't like that direction -- go find a better venue to convince people otherwise.

I appreciate the fervor of your comment, but I think this venue is perfectly fine. We are discussing an addition to Haskell, and, furthermore, a new policy about future additions!

I like to believe that @AntC2 argues in good faith, trying to do the best for Haskell. Except we don't quite agree on what would be best.

It is true that Haskell 2010 is a different spot in the design space than Dependent Haskell. It has name punning, it has better inference at the expense of other features.

@AntC2 enjoys this spot in the design space and tries to protect it from the invasive changes, motivated by dependent types, that threaten it. And it's a noble thing to do that. I like Haskell 2010 as well.

But! I don't believe we are threatening it. The reason Dependent Haskell isn't a new language but an extension of Haskell is that it's designed to have perfect interoperability with Haskell 2010. GHC will continue to implement Haskell 2010, and the new features are to be hidden behind extension flags as appropriate.

I would much prefer that @AntC2 and the dependent types crowd (of which I'm a vocal member) would realize that we don't need to be at odds with each other. And we should not exclude anyone from the conversation.

I often want to be able to force users to specify the type of argument explicitly

Regarding the proposal as it stands (rather than as a pathway to something more ambitious), this ability to specify a compulsory type argument looks like the main benefit. And I agree that it is a benefit, and it's one that is quite independent of the full-spectrum dependency issue. The question is: how much does this benefit cost.

The main cost is resolving the syntactic and name-space difference between types and terms. On obvious way of resolving that is via a syntactic marker. We already have one, namely @. So we could use @ for those compulsory type arguments too. This would be simple to explain, and require none of this re-interpretation. But it would occasionally be inconvenient. For example, if f :: forall k. forall (a:k) -> blah, then you could not write f @Int; you'd have to write f @_ @Int. Or change the type of f to f :: forall {k}. forall (a:k) -> blah.

@simonpj I added this as another alternative. Unsurprisingly, I'm not enamored with it either, as the primary motivation for me is to blur the distinction between terms and types, not to make it stand out with a syntactic marker.

@int-index I would to add to that alternative that even without of dependent types we may want want invisible relevant non-dependent quantification (that is to say, @ for terms). Now using one sigal for visibility and namespacing bights us even harder--no terms are in scope!

I hate to be negative, but I personally would rather do away with this proposal than to require the @ sign for required arguments. You might -- just barely -- be able to convince me to use some other syntactic marker, but requiring @ seems a step in the wrong direction.

I personally would rather do away with this proposal than to require the @ sign for required arguments

OK. Would you like to say why it seems like a step in the wrong direction?

Would you like to say why it seems like a step in the wrong direction?

It moves us away from uniformity. Let's even pretend for a moment that I'm not trying to actually merge the term-level and type-level.

Right now, we can say this:

type VDQ :: forall k1. forall k2 -> k1 -> k2 -> Type
data VDQ k2 a b

type VDQIntTrue = VDQ @Type Bool Int True
type VDQCharFalse = VDQ Bool Char False

If we were to require the @ in terms, the term-level equivalent would be

vid :: forall a. forall b -> a -> b -> ()
vid _ _ _ = ()

ex1 = vid @Int @Bool 3 True
ex2 = vid @_ @Bool 'x' False

These look different! Why different syntaxes for the same idea?

Worse, imagine a data constructor:

data Silly a b where
  Mk :: forall a. forall b -> a -> b -> Silly a b

Now we have this oddity:

type Different1 = Mk @Nat Bool 3 True
type Different2 = Mk Bool "hi" False
different3 = Mk @Int @Bool 3 True
different4 = Mk @_ @Bool "hi" False

Here, the right-hand sides should be the same, but they have to be different.

Today, we have non-uniformity by omission: we have no visible forall in types of terms. But with your proposed @ on required dependent arguments, we would have active non-uniformity, which seems worse as it paints us into a corner that's difficult to escape from. At least non-uniformity by omission can, in theory, be fixed uniformly, later.

If I wanted to define a sizeOf method would there be any way to control for the way a is quantified.

type  Storable :: Type -> Constraint
class Storable a where
  sizeOf :: Int

The default type of sizeOf would be an invisible quantifier

sizeOf :: forall a. Storable a => Int

but if I wanted a visible quantifier, is my only hope to define a new function?

sizeOf :: forall a -> Storable a => Int

but if I wanted a visible quantifier, is my only hope to define a new function?

Yes. But improvements have been wondered about. See #236, for example.

While not strictly necessary for the proposal, I think it would be valuable to point out that the TypeApplications+AllowAmbigousTypes workaround fails for higher-order functions. I imagine you intend to allow useful functions with types like

nicerReify :: forall a r. a -> (forall (s :: *) -> Reifies s a => r) -> r

@treeowl Higher-order usage is also addressed by TypeAbstractions in #448.

@int-index I have a question about how this interacts with #448.

After presenting the new the syntax rule to allow @x and @_ for invisible forall in lambda expressions, #448 says

Note that this does not subsume the new grammar for constructor patterns, which allow types, not just variables.

In #23704 you say "GHC Proposals #281 and #402 allow the use of visible forall in data constructors.".

Does/should this proposal allow types (rather than just variables and wildcards) in constructor patterns for visible forall as well? If so, does there need to be a pattern to type mapping (P2T?) as well?

Update: I just saw that the proposal states

We could, but we do not relax this requirement even when the type is statically known:

data T a where
 Typed :: forall a -> a -> T a

g :: T Int -> ...
g (Typed Int x) = ...   -- Reasonable, but no.

so I retract my question, sorry for the noise

so I retract my question

@JakobBruenker Actually, I want to answer that question. Yes, we need a pattern-to-type-pattern mapping, the issue for it is #23739. We need it even if we don't relax the restriction you cited because it will affect error messages. Furthermore, I believe the restriction was added only because we didn't know how to handle higher-kinded variables (#18986). We figured it out, so the restriction can be lifted. In fact, I now believe it must be lifted because it creates a bad inconsistency.

Let's say we have

data TInvis a where
 TypedInvis :: forall a. a -> TInvis a

g :: TInvis Int -> ...
g (TypedInvis @Int x) = ...

The restriction means that I can't change forall a. to forall a ->, which is hard to justify. The easy solution is to simply remove the restriction from the proposal. It doesn't serve its original purpose.

That makes sense! Thanks for the explanation

@int-index I have one more question:

The proposal contains the typing rule:

G |- sigma[a := rho];                 pis  ~>  Theta; phis; rho_r
------------------------------------------------------------------  ITVDQ
G |- (forall a -> sigma); (type rho), pis  ~>  Theta; phis; rho_r

It requires that the argument that's passed is a rho type. Yet the typing rule for visible type applications from the quick look paper,

merely requires the argument be a σ-type, so allows foralls, and indeed with -XImpredicativeTypes, this is accepted:

ghci> id @(forall a . a) undefined
*** Exception: Prelude.undefined

What is the reason for not allowing them for required type arguments?

I have a version of GHC HEAD from July which also allows

ghci> id' :: forall a -> a -> a; id' (type _) = id
ghci> id' (type (forall a . a)) undefined
*** Exception: Prelude.undefined

This seems to suggest that the implementation does allow any σ-type?

@JakobBruenker Good question. I don't quite remember why I used rho there, it must've been a mistake.

easy to fix, as part of #626