#9784: Allow Qualified Promoted Types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Parser) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Description changed by crockeea: Old description:

The program

{{{#!hs {-# LANGUAGE DataKinds #-} module Foo where import Data.Proxy

data MyNat = Z | S MyNat

bar :: Proxy Foo.'Z -> Int bar _ = 0 }}} fails with the error {{{ Foo.hs:7:17: Illegal symbol '.' in type Perhaps you intended to use RankNTypes or a similar language extension to enable explicit-forall syntax: forall <tvs>. <type> Failed, modules loaded: none. }}}

I believe the program above should compile without error. In the example above, I could make the code compile with my intended meanign using `Z`, `'Z`, or even `Foo.Z` in place of `Foo.'Z`, all of which refer to `Foo.'Z`. However, if there is also a vanilla type `Z` in scope and another promoted constructor `'Z` in scope, I have no way to disambiguate the reference to `'Z` in `bar`: - `Z` and `Foo.Z` refer to the vanilla type - `'Z` could be from the promoted `MyNat` constructor, or from the other module

Concretely, I could import `Data.Type.Natural` from [https://hackage.haskell.org/package/type-natural type-natural], which also defines the promoted constructor `'Z`.

{{{#!hs {-# LANGUAGE DataKinds #-} module Foo where import Data.Proxy import Data.Type.Natural

data MyNat = Z | S MyNat

bar :: Proxy Foo.'Z -> Int bar _ = 0 }}}

In this case, there is no way for me to indicate that `bar` has the type `Foo.'Z -> Int`

As a side note, if I do as the error suggests and use`RankNTypes`, I get the same error message. It's a bit strange for GHC suggest adding an extension that is already enabled.

New description: The program {{{#!hs {-# LANGUAGE DataKinds #-} module Foo where import Data.Proxy data MyNat = Z | S MyNat bar :: Proxy Foo.'Z -> Int bar _ = 0 }}} fails with the error {{{ Foo.hs:7:17: Illegal symbol '.' in type Perhaps you intended to use RankNTypes or a similar language extension to enable explicit-forall syntax: forall <tvs>. <type> Failed, modules loaded: none. }}} I believe the program above should compile without error. In the example above, I could make the code compile with my intended meanign using `Z`, `'Z`, or even `Foo.Z` in place of `Foo.'Z`, all of which refer to `Foo.'Z`. However, if there is also a vanilla type `Z` in scope and another promoted constructor `'Z` in scope, I have no way to disambiguate the reference to `'Z` in `bar`: - `Z` and `Foo.Z` refer to the vanilla type - `'Z` could be from the promoted `MyNat` constructor, or from the other module Concretely, I could import `Data.Type.Natural` from [https://hackage.haskell.org/package/type-natural type-natural], which also defines the promoted constructor `'Z`. {{{#!hs {-# LANGUAGE DataKinds #-} module Foo where import Data.Proxy import Data.Type.Natural data MyNat = Z | S MyNat bar :: Proxy Foo.'Z -> Int bar _ = 0 }}} In this case, there is no way for me to indicate that `bar` has the type `Foo.'Z -> Int`. Although a user cannot define the a type beginning with a tick, they are perfectly valid types to refer to. I suspect the parser is failing to make this distinction, at least in the context of name qualification. As a side note, if I do as the error suggests and use`RankNTypes`, I get the same error message. It's a bit strange for GHC suggest adding an extension that is already enabled. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9784#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9784: Allow Qualified Promoted Types -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Parser) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by crockeea): Interesting. Instead of suggesting `RankNTypes`, perhaps the error should explain this syntax. If there's a promoted variable in scope (or maybe even if there isn't a promoted variable in scope) `parse error on Foo.'Z (perhaps you meant 'Foo.Z)` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9784#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9784: Improve error message for misplaced quote inside promoted qualified type -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature | Status: new request | Milestone: Priority: normal | Version: 7.8.3 Component: Compiler | Keywords: (Parser) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: #3155 Type of failure: GHC | rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Good idea, but not so clear how to implement it. Your text tokenises as {{{ bar :: Rpoxy Foo . 'Z -> Int }}} and the parse error happens on the "." before the parse has even seen the `'Z`. I suppose the lexer could see `Foo.'Z` and warn that it looks suspicious. Or even lex it as if you had written `'Foo.Z`? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9784#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9784: Improve error message for misplaced quote inside promoted qualified type -------------------------------------+------------------------------------- Reporter: crockeea | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Parser) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Incorrect | Unknown/Multiple warning at compile-time | Test Case: Blocked By: | Blocking: Related Tickets: #3155 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * failure: GHC rejects valid program => Incorrect warning at compile-time -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9784#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler