Namespace collision detection for promoted types

In the following example

{-# 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.

changed weight to 5

added Tfeature request Trac import labels

But what if you mean the datatype S and not the promoted constructor? If you report an ambiguity error, we would need a way to disambiguate the other way as well, and we currently cannot.

I guess the kind error you're getting now could in addition include a hint that there's an ambiguity, though, something like

Foo.hs:12:8:
    ‘S’ is applied to too many type arguments
    In the type signature for ‘foo’: foo :: S n -> S n
    (Hint: did you mean the promoted constructor 'S?)

changed the description

@kosimus I see your point. I think your suggestion would certainly be an improvement over the current error. It could use the existing phrasing of Perhaps you meant the promoted constructor 'S (imported from MODULE) or Perhaps you meant the promoted constructor 'S (defined at Foo::5:16)

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.

It seems there are a couple of options:

1. Solve this problem by making DataKinds ~~always~~ only promote to 'S, and ~~never~~ not to S. I'm sure this was long-debated when DataKinds was introduced, and is therefore unlikely to happen.
2. Add a very mild message anytime there is a type error about a type that shares a name with a promoted constructor, something like "Be aware that S could refer to the constructor promoted from blah"

Either one is an improvement over the current black-holing of promoted types when a non-promoted type is in scope. However, only the first resolves strange behavior where the type of a function can change *without* error by adding an import:

{-# LANGUAGE DataKinds #-}
module Foo where

import GHC.Generics

data MyNat = S

foo :: S -> Int
foo = 3

Without the import, foo has the type Foo.'S -> Int. After the import, foo has the type GHC.Generics.S -> Int, and both versions compile. Also, see #9784 for a related possible parse bug.

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.

@rwbarton -fwarn-implicit-promoted-constructors is an interesting suggestion. Just to be clear, I'm imagining that such an option would result in a warning whenever S is written but it refers to the same type as a 'S promoted constructor.

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.

I'm ok with -fwarn-unticked-promoted-constructors if someone wants to add (and document) it.

Simon

added newcomer label

assigned to @trac-carlostome

Thanks, carlostome, for adopting this ticket. Let me know if I can be of any help -- eir@cis.upenn.edu, and on IRC.

I added this warning flag and updated the documentation according to it. The new flag is documented as follows:

---

-fwarn-unticked-promoted-constructors:

Warn if a promoted data constructor is used without a tick preceding it's name.

For example:

    data Nat = Succ Nat | Zero

    data Vec n s where
      Nil  :: Vec Zero a
      Cons :: a -> Vec n a -> Vec (Succ n) a

This program will raise two warnings because Zero and Succ are not written as 'Zero and 'Succ.

This warning is off by default.

---

If anybody thinks this can be explained better, all suggestions are welcomed!

Trac metadata

Trac field	Value
Test case	→ T9778
Differential revisions	→ D534

mentioned in commit 87160c1a

closed

changed milestone to %7.10.1

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Pnormal label