[GHC] #9784: Allow Qualified Promoted Types

[GHC]

#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