#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Description changed by crockeea: Old description:

In the following example {{{#!hs {-# LANGUAGE DataKinds #-}

module Foo where

data Nat = Z | S Nat

data S

foo :: S n -> S n foo = id }}}

GHC displays the error

{{{ Foo.hs:12:8: ‘S’ is applied to too many type arguments In the type signature for ‘foo’: foo :: S n -> S n Failed, modules loaded: none. }}} Although it's clear in my example where the problem is, this example was distilled from a case where I imported module1 with type `S` defined and module2 with the promoted type `S`, which is what I was trying to use. Can we get namespace collision detection instead? Something like:

{{{ Foo.hs:9:15 Ambiguous occurence ‘S’ It could refer to either Foo.S defined at Foo.hs:7:1 or to the promoted constructor S defined at Foo.hs:5:16 Use 'S to refer to the promoted constructor. }}}

New description: In the following example {{{#!hs {-# LANGUAGE DataKinds #-} module Foo where data Nat = Z | S Nat data S foo :: S n -> S n foo = id }}} GHC displays the error {{{ Foo.hs:12:8: ‘S’ is applied to too many type arguments In the type signature for ‘foo’: foo :: S n -> S n Failed, modules loaded: none. }}} Of course this code compiles without the definition of `data S`. Without namespace collision detection, it is easy to have working code, and then import a module which breaks the code. For example, I made this request after I imported Module1 with type `S` defined and Module2 with the promoted type `S`, which is what I was trying to use. Can we get namespace collision detection instead? I'm proposing something like: {{{ Foo.hs:9:15 Ambiguous occurence ‘S’ It could refer to either Foo.S defined at Foo.hs:7:1 or to Foo.'S promoted from the constructor defined at Foo.hs:5:16 or to `Bar.'S` promoted from the constructor defined at Bar.hs:line#:char# or to ... Use 'S to refer to promoted constructors. }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Kosmikus is right. Moreover, it's very common to say {{{ data T = T Int f :: T -> T f (T x) = T (x+1) }}} where the type and the data constructor deliberately share a name. That has to work. So in general terms, Kosmikus's suggestion of a hint is probably the way to go. However in this example, the hint is positively misleading. You say that "This code compiles without the definition of `data S`" but that's not true: {{{ T9778.hs:9:8: Expected a type, but ‘S n’ has kind ‘Nat’ In the type signature for ‘foo’: foo :: S n -> S n }}} So suggesting to use the data constructor instead is not helpful. I suppose if you had {{{ foo :: Proxy (S n) -> Proxy (S n) }}} ''then'' the hint would make sense. But now thing are getting quite complicated! I'm concerned that we might make matters worse instead of better. Suggestions welcome. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): Well, DataKinds does always promote to `'S`. It just also promotes to `S`. But you could avoid ever using the un-`'`ed form of a promoted constructor; that's up to you. Are you asking for a `-fwarn-implicit- promoted-constructors`? That should probably not be the default, as the currently common style is not to write `'True` and `'False` everywhere. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): I could rally behind calling `-fwarn-unticked-promoted-constructors` the solution to this problem. I'm -0.5 on including text in any error message about `S` the possibility that the user means `'S` -- just seems like noise to me. Note that I've changed the name of the warning flag, as `implicit` conjures up the wrong associations for me. It's interesting to note that I frequently use ticks everywhere in presentations about !DataKinds stuff. (I leave off the ticks in my own code, though.) I think requiring the ticks makes for a better reader experience for folks who are not deep into this. I also think that the ticks should be allowed (but not required) in kinds. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: newcomer Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by jstolarek): * keywords: => newcomer -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: carlostome Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: newcomer Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Thanks, carlostome, for adopting this ticket. Let me know if I can be of any help -- `eir@cis.upenn.edu`, and on IRC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: carlostome Type: feature | Status: patch request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: newcomer Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: None/Unknown | Test Case: T9778 | Blocking: | Differential Revisions: Phab:D534 | -------------------------------------+------------------------------------- Changes (by carlostome): * status: new => patch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9778: Namespace collision detection for promoted types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: carlostome Type: feature request | Status: closed Priority: normal | Milestone: 7.10.1 Component: Compiler | Version: 7.8.3 Resolution: fixed | Keywords: newcomer Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: T9778 Related Tickets: | Blocking: | Differential Revisions: Phab:D534 -------------------------------------+------------------------------------- Changes (by thoughtpolice): * status: patch => closed * resolution: => fixed * milestone: => 7.10.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9778#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler