Opened 5 months ago

Last modified 5 months ago

#8556 new bug

Invalid constructor names are accepted in data declarations

Reported by: dolio Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.6.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets:

Description

Earlier today, someone was asking on #haskell why the constructor name (^) wouldn't work in GADT definitions. My response was that (^) isn't a constructor name, but much to my surprise, GHC accepts such names in a regular data declaration:

data Foo = F | (^^^^) Int Int

This creates a Foo type and value constructor F, but no value constructor (^^^^). However, in 7.6.3, if DataKinds? are enabled, both constructors appear at the type level.

In HEAD, the same definition is accepted, with only F existing at the value level, as before. But at the type level, both F and (^^^^) just generate errors that Foo is not a promotable type. At that point, I think there's no question that the declaration should just be ruled out.

Change History (2)

comment:1 Changed 5 months ago by monoidal

What about data Foo a = F | (^^^^) a a? This is promotable, e.g. Maybe ^^^^ Maybe :: Foo (* -> *). My suggestion is to postpone this till implementing KindsWithoutData?, and then we can forbid data Foo a = F | (^^^^) a a but allow data kind Foo a = F | (^^^^) a a. See also #7725.

comment:2 Changed 5 months ago by monoidal

Here's a simple fix for 7.7 discussed on IRC:

Writing a data declaration which contains at least one operator not starting with : should require -XDataKinds. So if you write data A a = (&) a a you have to enable DataKinds?, since the (&) is available only in the promoted form. After KindsWithoutData? get merged we will forbid it completely by changing the test to unconditional error.

Note: See TracTickets for help on using tickets.