Improve error message for misplaced quote inside promoted qualified type

The program

{-# 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 type-natural, which also defines the promoted constructor 'Z.

{-# 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 useRankNTypes, I get the same error message. It's a bit strange for GHC suggest adding an extension that is already enabled.

changed weight to 5

added Tbug Trac import parser labels

changed the description

It's 'Foo.Z not Foo.'Z. Foo.Z is the name here; there is no "type beginning with a tick", that is just syntax to disambiguate namespaces. (Think like (Map.!), etc.)

Good point about the RankNTypes error message though.

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)

changed title from Allow Qualified Promoted Types to Improve error message for misplaced quote inside promoted qualified type

Trac metadata

Trac field	Value
Type	Bug → FeatureRequest
Related	→ #3155 (closed)

added Tfeature request label and removed Tbug label

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

Yes, I think the lexer makes more sense. Although it doesn't quite make sense to me, presumably there's a good reason for making 'Foo.Z the right thing. If that's the case, then I think I'd rather see a lexer warning that have it lex correctly.

Trac metadata

Trac field	Value
TypeOfFailure	ValidProgramRejected → IncorrectWarning

added Tbug label

added Pnormal label