Support pun-free code

[Hithroc]

This proposal introduces -Wpuns and -Wpun-bindings and
introduces namespace-qualified imports and module aliases.

These changes should help the users to write pun-free code to take advantage of
Syntactic Unification Principle described in #378.

Rendered

[goldfirere]

I like the general gist of this proposal. I will have to mull it over for some time to see if I like the details. A few isolated thoughts:

• You mention a Unified namespace in teletype font. But this would just be an internal name within GHC, right? Haskellers will not write this in code anywhere, I think.

• It is possible (through re-exports) for a module to export identifiers in all three (type, data, and unified) namespaces. Is it possible to import only unified-namespace identifiers?

• Why deprecate TH's ''? Perhaps you also want to change the lookup behavior of TH's ' even without -XUnifiedNamepsace? Otherwise, it seems users will have to add quite a bit of code to maintain compatibility with an old usage of ''.

• What's the name of your new module exporting e.g. List? That should be part of this discussion.

• With -XUnifiedNamespace, the renamer looks everywhere. I presume it fails if an identifier is found in more than one namespace, but the proposal should specify this.

• Under "Effect and Interactions" you suggest that ' in types should be deprecated, but this is not in the specification. Was it meant to be?

Thanks for writing this up!

[Hithroc]

You mention a Unified namespace in teletype font. But this would just be an internal name within GHC, right? Haskellers will not write this in code anywhere, I think.

You're right that's an implementation detail. I've updated the proposal so the specification no longer depends on it.

It is possible (through re-exports) for a module to export identifiers in all three (type, data, and unified) namespaces. Is it possible to import only unified-namespace identifiers?

No, you can, and I don't really understand why would that be useful. Perhaps I'm missing something?

Consider this scenario:

module A where

data T = T

{-# LANGUAGE UnifiedNamespace #-}
module B (X(..), module A) where

import A data

data X = MkX

module C where

import B unified

In this case, only X and MkX would be brought into the scope in module C and you'll lose T.

Why deprecate TH's ''? Perhaps you also want to change the lookup behavior of TH's ' even without -XUnifiedNamepsace? Otherwise, it seems users will have to add quite a bit of code to maintain compatibility with an old usage of ''.

Sorry, I forgot to specify this, '' will only be deprecated (or rather disabled) if -XUnifiedNamespace is enabled, because then this syntax would be redundant. I've clarified this in the proposal.

What's the name of your new module exporting e.g. List? That should be part of this discussion.

Good point! Perhaps Prelude.Unified? Other than that I don't think I have any specific suggestions.

With -XUnifiedNamespace, the renamer looks everywhere. I presume it fails if an identifier is found in more than one namespace, but the proposal should specify this.

Indeed! I've clarified this in the proposal.

Under "Effect and Interactions" you suggest that ' in types should be deprecated, but this is not in the specification. Was it meant to be?

Good point, I've moved that part to specification section.

[treeowl]

This is a big change. I think we should be very careful to be sure we get exactly what we want in the end. Personally, I don't see the need to get rid of ' altogether. There's a huge amount of code punning types and constructors. Can't we be more conservative somehow? If not, can you give some more compelling examples showing why this change is forced?

A minor thought: if we have to monkey around with tuples, should we make them a built-in data family?

data family Tuple (ts :: [Type])
data instance Tuple [] = ()
data instance Tuple [a] = Solo a
data instance Tuple [a,b] = (a, b)

That way we won't need to import a tuple module to get a bunch of numbered tuple names.

[isovector]

I'm not at all convinced by this. The motivation as stated is three points:

1. Newcomer confusion. But the the cost and drawbacks of the proposal also cite newcomer confusion, so maybe this won't do much to help the situation.
2. Datakinds/TH having overlapping syntax is admittedly annoying. But I'm not convinced it's annoying enough to warrant a change as big as this!
3. Dependent Haskell. We don't yet have a spec for such a thing, and thus making big changes in its name seems like putting the cart before the horse.

[Hithroc]

@treeowl

This is a big change.

It is a localized change. The code that doesn't use -XUnifiedNamespace extension will not percieve the changes and does not need to change in any way.

I think we should be very careful to be sure we get exactly what we want in the end. Personally, I don't see the need to get rid of ' altogether.

We're only getting rid of ' syntax in -XDataKinds with -XUnifiedNamespace enabled, because then it becomes redundant. And that's a good thing because it can now be used exclusively for Template Haskell.

There's a huge amount of code punning types and constructors. Can't we be more conservative somehow?

That code is unaffected, you only have to worry about it if you have -XUnifiedNamespace enabled and at the same time you're importing code that uses punning. In that case you use the data/type syntax introduced in the proposal.

If not, can you give some more compelling examples showing why this change is forced?

It's forced by the fact that we need to refer to types on term level and to terms on type level. You can see another example below (I've also added it to the proposal).

A minor thought: if we have to monkey around with tuples, should we make them a built-in data family?

That is a nice suggestion! Unfortunately, you can't partially apply Tuple like this, you'd need a type-level lambda for that:

-- You can do this with Tuple2
F (Tuple2 a)
-- but not with Tuple
F (Tuple [a, ?])
F (\b -> Tuple [a,b])

@isovector

Newcomer confusion. But the cost and drawbacks of the proposal also cite newcomer confusion, so maybe this won't do much to help the situation.

It is true that newcomer confusion is mentioned in both motivation and drawbacks, but I believe the introduction of the new type/data syntax will cause less confusion than punning does, because a newcomer can just look up the syntax to clear things up.

Datakinds/TH having overlapping syntax is admittedly annoying. But I'm not convinced it's annoying enough to warrant a change as big as this!

What should be the meaning of 'Nothing in types? Is it a Template Haskell name or a promoted data constructor? We need the same answer as in terms if we want to unify term/type parsers for visible forall or Dependent Haskell.

Dependent Haskell. We don't yet have a spec for such a thing, and thus making big changes in its name seems like putting the cart before the horse.

We do have a Richard Eisengberg's paper Dependent Types in Haskell: Theory and Practice which pretty much describes the end goal that we're currently moving towards.

This is also be useful in cases other than Dependent Haskell, for example with visible dependent quantification. Here's a closer to the real world example with sizeOf from Foreign.Storable.

sizeOf :: Storable a => a -> Int

-- To use it we have to do this:
sizeOf (undefined :: MyType)

Here's an example of hasktorch using this pattern.

With -XUnifiedNamespace and visible dependent quantification we could just have this instead:

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

sizeOf MyType

Of course, there's an option to use @ syntax like this:

sizeOf :: forall a. Storable a => Int

sizeOf @MyType

But the problem here is that the argument here is not required and if you forget to put it there GHC will try to infer it which will lead to errors like "could not deduce" which do not directly hint to what the problem is and how to fix it.

I've updated the proposal with this example.

Furthermore, other dependently typed languages like Agda and Idris use pretty much this approach: they have a single namespace for everything.

[Hithroc]

Well, there has been no comments in a while, so I guess it's time to submit! @nomeata

[yav]

Since most modules define both types and data, wouldn't this extension double the number of imports required? I mean this for the imports that are explicitly annotated with a namespace.

Also, it seems that this extension is conflicting with itself---to define the module that renames the types, you'd have to turn off this extension correct?

I am extremely unconvinced by the motivation:

1. It seems fairly important for a Haskell programmer to understand the difference between [5] and [Int], and I think we have little evidence that this is confusing for anyone. On the contrary, I suspect that mixing up the terms and type namespaces would lead to confusion for everyone, not just beginners.
2. The back tick is indeed a wart, but this is entirely due to design choices related to how data promotion works. As @isovector points out, this proposal looks like a very big change for a very small gain in that respect. Also, it seems that most of the uses of the back tick are not really needed, so perhaps there are other designs to work around this issue.
3. Perhaps it would be convenient to have functions that have type arguments that must be provided at each call site. This seem quite unrelated to Dependent Haskell or namespaces, at least in my mind. It is not clear to me why the current notation of @T wouldn't work for this use case---I think the visual queue that we are passing a type rather than a value is quite informative. You say that using @T somehow allows the type to be omitted, but it seems to me that this is all about how the function that is being called is declared, and not with how we pass arguments to it. For example, I could easily imagine having some sort of type quantifier, which requires explicit instantiations. This seems like a completely separate proposal though.

So, overall, I am not convinced that we'd be gaining much here, and the cost seems quite high. Am I missing something?

[int-index]

Since most modules define both types and data, wouldn't this extension double the number of imports required? I mean this for the imports that are explicitly annotated with a namespace.

Yes, although such imports would be needed only for disambiguation purposes. For example, import Control.Monad.Reader would require no duplication, as the identifiers it exports (MonadReader, ask, local, etc) occur only in one of the namespaces.

Also, it seems that this extension is conflicting with itself---to define the module that renames the types, you'd have to turn off this extension correct?

That module would be a compatibility shim. Of course it'd be nice to live in a world where we're dealing with List instead of [], and Tuple2 instead of (,) in the first place, but insofar as we are not, we need a backwards compatibility story. It is therefore an intrinsic property of this compatibility module that it needs to be dealing with syntax/identifiers with the extension disabled. I don't see how it makes the extension "conflicting with itself".

It seems fairly important for a Haskell programmer to understand the difference between [5] and [Int], and I think we have little evidence that this is confusing for anyone.

Indeed, it is crucial to understand the difference between [5] and [Int], and the identical notation is an obstacle to achieving this understanding. [5] :: List Int would reflect the reality more directly. As to evidence, it is overwhelming in my teaching experience, and we have more anecdotal evidence from a Reddit discussion:

• I have been teaching Haskell to bachelors for half a decade. I could not agree more with this post.

• I have taught Haskell to students for some years. There is some truth to this.

• The overloading of names in [] is particularly troublesome, in my experience too.

I believe this one is a no brainer for anyone who actually tried to explain Haskell to beginners.

On the contrary, I suspect that mixing up the terms and type namespaces would lead to confusion for everyone, not just beginners.

Dependently typed programming implies the use of types and terms together, we already can refer to the term namespace in types with DataKinds enabled. Therefore, I don't follow how we're "mixing up" these namespaces: it is just a fact of life that in dependently-typed code, we need to use entities from both namespaces alongside each other.

The back tick is indeed a wart, but this is entirely due to design choices related to how data promotion works.

And this proposal offers an alternative way that data promotion could work, a way that doesn't require promotion quote syntax. Hence, accepting this proposal means we get rid of the aforementioned wart.

As @isovector points out, this proposal looks like a very big change for a very small gain in that respect.

What makes this change "big", how do you quantify its size? It doesn't break any code whatsoever because it's opt-in, and modules that don't enable the extension can seamlessly use the modules that do.

Therefore, for users who opt-in, the impact of this proposal (big or not) is desired, and for users who don't opt-in, the impact is zero.

As to the gain of this proposal, it is quite clear to me that the gain is immense, as it solves one of the fundamental challenges towards dependently typed programming in Haskell – the namespace problem.

Also, it seems that most of the uses of the back tick are not really needed, so perhaps there are other designs to work around this issue.

It is not enough to say that there are alternative designs, one must name them. So far, I can name three:

• explicit namespace specifiers (type.X, data.X), as proposed in Namespace specifiers #214. It has the disadvantage of verbosity (no one wants to write type.Either type.Int type.Bool)
• promotion quote overloading, such that 'T "flips" the namespace – this has two disadvantages:
  1. we're still stuck with the quote syntax which conflicts with Template Haskell
  2. it is highly context-dependent, so one must keep track of the current ambient namespace to understand the meaning of '
• namespace-qualified imports, which are proposed here

Perhaps it would be convenient to have functions that have type arguments that must be provided at each call site. This seem quite unrelated to Dependent Haskell or namespaces, at least in my mind.

It is quite related to both Dependent Haskell and namespaces. The landmark feature of Dependent Haskell is the foreach x -> quantifier: the quantifier that introduces a dependently-typed function (a pi-type). The difference between foreach x -> and forall x -> is relevance (as described in the thesis), and as long as we're discussing syntax and namespaces rather than runtime behavior and the ability to pattern-match on this data, we do not need to take relevance into account and might as well be discussing forall x ->. In turn, the difference between forall x -> and forall x. is the visibility: that is, whether the visibility override, written as @, is needed to provide the argument.

As soon as we're dealing with visible arguments, by definition we're not using the visibility override @, so we face the namespace issue. If one can write f @Int, then one must also be able to write f Int, so we're referencing the type namespace in terms, just like we can already reference the data namespace in types with DataKinds.

I think the visual queue that we are passing a type rather than a value is quite informative.

This makes the assumption that we make a distinction between terms and types, whereas the entire premise of this proposal is that we're moving towards a future where we do not make such a distinction. Types are values of type Type.

---

So, overall, I am not convinced that we'd be gaining much here, and the cost seems quite high. Am I missing something?

Hopefully, I was able to clear a few things up. The proposal has close to zero costs, as it's entirely opt-in and has no impact on non-users. Its implementation is not difficult either. It is of huge importance for the dependently-typed programming movement as it resolves the namespace problem.

[Ericson2314]

How do exports from a -XUnifiedNamespace module work, especially when implemented by a -XNoUnifiedNamespace module?

[int-index]

Entities defined in a module with -XUnifiedNamespace are accessible in all contexts. Assume we have a module that defines this:

{-# LANGUAGE UnifiedNamespace #-} 
module U where

data T = MkT

Now both T and MkT are accessible in both types and terms, in any module:

-- {-# LANGUAGE NoUnifiedNamespace #-}
module X where

import U

type S1 = T    -- ok
type S2 = MkT  -- ok

s1 = T    -- currently, a type error, but not a namespace error
s2 = MkT  -- ok

[Ericson2314]

Great, though I think the proposal should call that out explicitly?

I agree that that this proposal doesn't does seem lightweight to me. It's certainly simpler than the disambiguate one that came before. The costs are born by

1. The user code not GHC
2. Only the user code using the extension, not the other user code

I don't see who gets hurt in this scenario.

[int-index]

Great, though I think the proposal should call that out explicitly?

@Hithroc Would you mind extending the proposal to make this more clear?

I agree that that this proposal doesn't seem lightweight to me.

The user code that uses the extension:

• Gets the ability to refer to types in terms and to terms in types
• Loses the ability to use punning
• May need to write more imports than usual for disambiguation

I do share the feeling that this is not a small change because it would lead to very different naming conventions. Haskellers (including myself) are very used to punning, but now instead of writing data Foo = Foo we'll be writing data Foo = MkFoo in modules with the extension. Having to write a few more imports may be somewhat taxing as well.

Of course it's not a small syntactic change like, say, #87 or #190, but it's not exactly heavyweight either?

[Ericson2314]

@int-index Sorry! I meant it does seem lightweight. I had "doesn't seem heavyweight" before or something 😂

[Ericson2314]

Hehe in terms of ecosystem effects, I wouldn't say it's like GPL vs MIT; both multiple namespaces and unified namespace work better when all the other code uses the same scheme, so unified namespace will have the worse hand for a while.

[Ericson2314]

Oh, and regular namespaces should have some way to get the additional import syntax, so they can "confine" a unified namespace module's exports to one namespace too. That should give the old-style modules maximal flexibility for dealing with the new style

[simonpj]

Let me just note that this proposal introduces a "fork" in the language, in the sense decribed by Simon Marlow in his email earlier this month. He says

A "fork" is the thing I think we should strive to avoid. What is a fork?

• It fails the test "Is this extension something that most people would
  be happy to enable, even if they don't want to use it?"

• It fails the test "Do we think there's a reasonable chance this
  extension will make it into a future language standard?"

  The idea is that unless we can see a path to a point where everyone has the extension turned on, we're left with different groups of people using incompatible dialects of the language. A similar problem arises with extensions that are mutually incompatible.

Unlike, say, RankNTypes, this unified namespace hting fails the first test -- it's not something everyone is going to be happy to enable even if they don't use it.

That leaves the second test. We might conclude that this is the right direction of travel, and I can see its advantages. But I doubt we are ready to say "yes, this is what future Haskell will be like, and we'll be deprecating the two-namespace version in due course".

That's not to say that we should never accept a fork-like proposal -- there are judgements everywhere. But an alternative would to park this one until the need becomes more proximate; that is, until we want accept a dependent Haskell proposal that really needs it.

[int-index]

park this one until the need becomes more proximate; that is, until we want accept a dependent Haskell proposal that really needs it.

Visible forall in terms alone would need a solution to the namespace problem:

f :: forall (x :: Type) -> ...

a = f Int

I'm counting on either this proposal or an alternative to solve this issue before I (or a collaborator) formally propose visible forall in terms, but I assumed that it was the general consensus that this is a problem that needs solving (as described in https://gitlab.haskell.org/ghc/ghc/wikis/dependent-haskell#parsingnamespace-resolution).

I encouraged @Hithroc to make a separate proposal for this namespace problem, but it could also be bundled with the visible forall in terms where the pay-off is immediate rather than laying the ground for future work.

[Ericson2314]

Maybe we can have both proposals up at once, with the dependency made clear? I think the connection is simple enough that it shouldn't feel like a split conversation.

[goldfirere]

@yav:

On the contrary, I suspect that mixing up the terms and type namespaces would lead to confusion for everyone, not just beginners.

My experience with teaching Haskell suggests that different names for types and terms would be a net benefit. It's certainly not a primary challenge in teaching Haskell, but I've found it to be consistent. Others' experiences may differ, and I have no real data to offer on the matter.

For example, I could easily imagine having some sort of type quantifier, which requires explicit instantiations. This seems like a completely separate proposal though.

That would be a separate proposal, but it depends on either this one or some other solution to the namespace problem. If I f T x in my code, do I mean the type T or the term T? Without some new approach to namespacing, the only way to tell is to look up the type of f, but now we're in very deep water, with type-directed name resolution, anathema to type inference.

@int-index:

we have more anecdotal evidence from a Reddit discussion:

That discussion has points on both sides of this issue. I think it's helpful background, but I don't find the discussion moves the needle here much.

I believe this one is a no brainer for anyone who actually tried to explain Haskell to beginners.

I think it's fair to say that everyone has their own experiences here. My experience agrees with yours.

in dependently-typed code, we need to use entities from both namespaces alongside each other.

In other words, this proposal or something similar is a necessary prerequisite for dependent types, in my opinion.

for users who don't opt-in, the impact is zero.

I disagree fairly strongly here. All users are affected, because libraries will start to program in this new style. Everyone will eventually have to be aware of this extension.

It is of huge importance for the dependently-typed programming movement as it resolves the namespace problem.

If I wasn't clear on this point before, I would like to amplify the sentence above. This really is of huge importance to dependent types, and I don't have a better solution than this one.

@simonpj:

Let me just note that this proposal introduces a "fork" in the language

I agree. And that is worrisome. I'll also explicitly agree with Simon's text, that this extension is not for everyone today, but could conceivably work its way into a future standard.

An interesting counterpart to forking is #214, which does not fork the language, but is otherwise quite unsatisfying. I honestly don't know what's best here.

@Ericson2314:

Maybe we can have both proposals up at once, with the dependency made clear?

I think this is a fine idea. I personally wouldn't bundle this with the visible-dependent-quantification-in-terms proposal, but we could usefully debate both at the same time.

[JakobBruenker]

@goldfirere @yav

If I f T x in my code, do I mean the type T or the term T?

@yav seems to be suggesting that we use f @T x for both visible and invisible application, using @ as signifier of a type in term namespace rather than as a signifier of visibility overriding, judging by

Perhaps it would be convenient to have functions that have type arguments that must be provided at each call site. [...] It is not clear to me why the current notation of @T wouldn't work for this use case---I think the visual queue that we are passing a type rather than a value is quite informative.

Though presumably this would also imply part of a solution to the namespace problem, that solution probably being something like ' being used to signify terms in types and @ being used to signify types in terms.

Personally I like the unified namespace approach more for all the reasons that have already been brought up in this discussion, and also because being able to call both id :: forall a -> a -> a and id :: forall a . a -> a as id @Bool True strikes me as somewhat confusing.

edit: I just realized, it might be worth mentioning how this will interact with the accepted but (as far as I can tell) not yet implemented #65.

[int-index]

Let me just note that this proposal introduces a "fork" in the language, in the sense decribed by Simon Marlow in his email earlier this month.

@simonpj and I briefly discussed this proposal elsewhere, and if I understood correctly, the fork-like nature of this proposal is the biggest obstacle to its acceptance.

A possible alternative is to make punning a warning instead of an error. That is:

{-# OPTIONS -Wpunning #-}

data T = T

In fact, adding this warning would not even need a proposal, as it's not a new language extension. And the users could make punning an error using the existing -Werror= feature:

{-# OPTIONS -Werror=punning #-}

Whether to enable this warning and whether to make it an error is a matter of style rather than language design. And the part of this proposal about ambiguity and teaching beginners can be addressed with the warning, so with that out of the way, we are free to discuss what we actually need for visible forall in terms.

---

Surprisingly, the part that's needed for forall x -> is not fork-like. Today, we have the following namespace lookup rules:

• in terms, look in the data namespace
• in types, look in the type namespace and fall back to the data namespace

We could extend these rules to:

• in terms, look in the data namespace and fall bock to the type namespace
• in types, look in the type namespace and fall back to the data namespace

This would mean that the following program would work fine:

f :: forall (a :: Type) -> ...

x = f (Either Int Bool)

There are no data constructors Either, Int, or Bool, so the renamer would fall back to the type namespace. What about an ambiguity?

data T = T
x = f T

In this case, GHC would select the term-level T, as we are in a term context. This would have two disadvantages:

• Bad error messages if what I had in mind was the type-level T. This is resolved by using -Wpunning.
• No ability to refer to the type-level T. Short of introducing namespace specifiers, there are at least two workarounds:
  1. Rename the type-level T:

     data TT = T
     x = f TT
     

  2. Make a synonym for the type-level T:

     data T = T
     type TT = T
     x = f TT
     

So, while there are disadvantages, they can be addressed. As to the advantages:

• The proposal becomes no longer fork-like!

I would prefer to see the proposal accepted in its current form (punning as an error), but it's true that this would have the (possibly unwanted) implication that we are moving away from punning:

We might conclude that this is the right direction of travel, and I can see its advantages. But I doubt we are ready to say "yes, this is what future Haskell will be like, and we'll be deprecating the two-namespace version in due course".

On the other hand, punning as a warning is unopinionated and does not have such implications. And it would unblock visible forall in terms. What do others think?

[goldfirere]

I'm opposed to using @ as a namespace specifier. It should be a visibility override. That is, writing @ allows a call site to supply a specified argument -- that's it. Why? Because I want the call sites of id1 :: forall a. a -> a and id2 :: forall a -> a -> a to look different, as @int-index suggests.

I like the idea of -Wpunning. Its existence is a subtle indicator that punning should be reserved for bad jokes, and not in code. (Note that many languages allow punning -- for example, C, C++, and Java -- but I've never seen it intentionally used outside of Haskell.) It definitely shouldn't be in -W. I would argue (but not hard) against putting it in -Wall. Maybe in -Wcompat.

Separately, we could still retain the import X.Y.Z type as X syntax. That, by itself, is not at all fork-like. Then, if a non-punner imports a punning module and wishes to use visible dependent quantification, they can do so without worrying about ambiguity.

Actually, there's a wonderful balance here. I offer this counter-proposal:

• Extend -XExplicitNamespaces with the new behavior described in the original proposal for import declarations, allowing for selecting either the type or data namespaces.

• Extend the namespace lookup in terms to also consult the type-level namespace.

• Deprecate (in due course) the ' namespace-selector in types.

• Deprecate (in due course) the '' Template Haskell type-quote mechanism.

• Introduce -Wpunning.

• Introduce the compatibility shim as described in this original proposal. I propose calling it Data.Type.

Those points should address the needs in this ticket and be scalable to dependent types (and fairly ergonomic in the future). This counter-proposal is not fork-like!

I would actually like to go further, adopting some of my thoughts from #214:

• Introduce data as the namespace name for the data-level namespace.

• Use data in fixity declarations (replacing value, see the relevant proposal), ANN pragmas, and import/export lists (this last one would replace the current pattern).

This "further" could reasonably be a separate proposal, but life is short.

What do we think?

[jvanbruegge]

I do support the proposal, but I am also not happy about forking the language. So this is most likely a unpopular opinion, but I would suggest to add a deprecation plan for punning with a long overall timespan, similar how -XStarIsType was handled. So start with making it optional and then emit a warning with -Wall and continue to enable the extension by default

EDIT: This also means that the Prelude and base would at some point remove all usages of punning

[goldfirere]

As a committee member with sometimes a short memory, I'm surprised by the last comment here. Why was this rejected? There are a bunch of comments above that sound like "here's just a few more cleanup things we need before merging", after which a rejection seems quite dispiriting. In any case, there hasn't been visible action here over the past week -- I do hope this hasn't started withering!

[Hithroc]

Chris asked me how do I feel about removing the part about ExplicitNamespaces from my proposal and consider that separately, since the part about warnings is, as far as I understand, good to go, but there is some problem with specification of ExplicitNamespaces.

However, I had to disagree that this is the way to go. This proposal does not make sense without the changes to ExplicitNamespaces. Without type/data qualified imports this proposal introduces warnings that, in certain scenarios, have no workaround, short of disabling them (such as when a library the user is using uses punning). So if making some clarifications to ExplicitNamespaces is absolutely necessary, then that would have to be done first, before any other part of the proposal is accepted.

[adamgundry]

I argued against acceptance of the proposal as-is on the basis laid out here: https://mail.haskell.org/pipermail/ghc-steering-committee/2022-December/003059.html. My main concerns are about the changes to ExplicitNamespaces and PatternSynonyms, which need to be clearly motivated and precisely specified.

@Hithroc to be clear, I'm very grateful for all your work on this, and I hope to see this proposal accepted in some form. I'm sorry that this process can be drawn out and difficult, and hope this doesn't feel too demotivating. Language specification is a tricky task!

This proposal does not make sense without the changes to ExplicitNamespaces. Without type/data qualified imports this proposal introduces warnings that, in certain scenarios, have no workaround, short of disabling them (such as when a library the user is using uses punning). So if making some clarifications to ExplicitNamespaces is absolutely necessary, then that would have to be done first, before any other part of the proposal is accepted.

Splitting out the extension changes into a separate proposal seems like a good idea to me, as it will allow quicker progress on the warning parts, and more space to focus on the extension changes explicitly. Given that these warnings will not be enabled by default, I don't see it as a big problem to have one proposal that introduces them (even if some warnings cannot be avoided when importing a punned type) and then a follow-up proposal that is motivated by allowing the warnings to be avoided. I would be happy to help with drafting such a split if that would be useful?

That said, if you prefer to keep everything together in a single proposal and incorporate detailed motivation, specification and examples for the changes to extensions, I don't think a split is essential.

[nomeata]

An alternative to splitting the proposal would be, to me, to introduce a new NamespacedImports instead of getting this entangled with our unrelated concerns about ExplicitNamespaces (e.g. whether the latter should be part of the next GHC20xx, or should get a general overhaul). Eventually, they’ll all become on by default anyways, so this is, in a way, a temporary measure anyways.

Then I think this proposal can stay as one.

[goldfirere]

I agree with @nomeata. A topic that came up at work recently was bundling, in that it can be easy to think that two objectives/tasks/goals/whatever are required to be addressed together, when really they are separable. I fear there has been some unnecessary bundling here, where we've somehow decided that the specification of an existing -XExplicitNamespaces feature has to be cleaned up before we can have new warnings about puns. I watched the history happen and understand how we got here, but we can still step back and see where we can unbundle. And, if we have a new extension name, we can unbundle here. If we want to be extra careful, we can go even further than @nomeata's suggestion and call the new extension Unstable_NamespacedImports to loudly say that the definition of the extension is subject to change. Hopefully, we can even clean it up before it's released! But if we fail to do so, then we still have some protection if we later decide to change its meaning.

Once we make a new extension here, then I see no remaining blockers. And then it would be great to clean up -XExplicitNamespaces, but that can be addressed as a separate task.

[adamgundry]

I personally think using a different extension name would be no bad thing, though I am aware there are differing opinions about how much change to existing extensions is warranted, so I wouldn't consider it a blocker either way. The point is that, regardless of whether we are changing existing extensions or introducing new ones, those changes need to be clearly specified! 😄

[cdornan]

I agree with @adamgundry whose analysis of the issues here has been outstanding. I am very busy with other business right now but (as I told @Hithroc) I have scheduled the start of Feb (w/b 2023-02-06) to return to this.

[Hithroc]

Decoupling the changes to imports in this proposal from ExplicitNamespaces would indeed solve the problem. But I don't believe that's a clean solution? ExplicitNamespaces seems like the perfect fit for the changes here and having two similar, yet different extensions does not sound ideal.

Unstable_NamespacedImports could be a way to move forward for this proposal, perhaps until ExplicitNamespaces is fixed and Unstable_NamespacedImports could be removed in favor of it.

[nomeata]

having two similar, yet different extensions does not sound ideal.

True. But not necessarily better than one extension meaning widely different things in different versions of GHC, and also not necessarily better than tying this change to an extension that some expect to be redone in the future.

Especially if one sees extensions as merely a stepping stone towards a future language edition where the new feature is simply part of the language, then having one more is only a temporary nuisance for early adopters, and can also help form the future language more selectively (e.g. include the present change, but a revised ExplicitNamespaces variant).

[adamgundry]

I'm working with @Hithroc and @cdornan on a new proposal text, essentially derived from this one and the previous work in this area, that will tidy up ExplicitNamespaces and introduce namespaced imports with a full specification.

I think ultimately the question of one extension or two isn't very important, because I don't think we should use "let's add a new extension" as a way to avoid nailing down the interaction with ExplicitNamespaces.

[cdornan]

As @adamgundry said, we have a proposal in the works — it will aims to fix ExplicitNameSpaces while covering the mechanisms proposed here. I would expect its exact final form to be a function of the priorities that emerge from the associated discussion — let's see.

[adamgundry]

For reference, the new proposal for the ExplicitNamespaces changes is now available at #581.

@Hithroc Now that it's out, how would you feel about amending the present proposal to focus on the new warnings? (I'm happy to help if you'd like, but you're the proposer of this one so I wanted to give you the option first!)

[Hithroc]

Thanks @adamgundry!
I will update the proposal sometime this week.

[cdornan]

@Hithroc clearly there is not a rush on this — hopefully this is all moving forward again.

[int-index]

@Hithroc #581 was just accepted and it adds namespace-specified imports to the language. It means that this proposal can focus on -Wpuns and -Wpun-bindings. The sections related to "namespace qualified imports" and -Wpattern-namespace-qualified can be dropped.

[Hithroc]

Awesome. I'll get the proposal updated over the weekend.

[cdornan]

@Hithroc Just a quick checkin — are you still OK to make these revisions?

[AntC2]

Am I allowed to ask a quick q here? I'm puzzled by 3.2.6 -Wpun-bindings, example #1, second part:

f :: t -> ()
f @a = \a -> ()

the code is fine, ..., the a is shadowed instead [no Wpun-bindings]

(Not what I'd call "fine".) If I try to make use of the @-bound a (daft example, merely for illustration)

f @a = \a -> const () $ bar (undefined :: a)

That'll actually use the \-bound a as a type(?) Ok that'll likely give a type error, but I'd expect a friendly compiler(/linter?) to warn me that's probably not what I meant.

(Asking because the consequences of the consequences of #608 are getting tangled.)

Edit: perhaps a more critical illustration

f @a = \(a :: a) -> ()
             ^^ not the @-bound a

[adamgundry]

Thanks @Hithroc for your work on this proposal. I'm unassigning it as sadly @cdornan is no longer with us.

It appears that previous discussion on this proposal petered out, so I'll mark it as dormant. The main thing it needs is revision as described in #270 (comment), and there's a recent open question in #270 (comment). If anyone would like to pick this up, please feel free to shout.