Opened 2 years ago

Last modified 23 months ago

#11310 new bug

Surprising accepted constructor for GADT instance of data family

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.3
Keywords: TypeFamilies, GADTs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

-- Accepted:
data family Foo (x :: *) :: * -> *
data instance Foo Int Char where
  Foo :: Foo Int Char

-- Not accepted
data Bar Char where
  Bar :: Bar Char

It seems the second example, using a simple GADT, is syntactically barred from having a specific type constructor in its "head". That syntactic restriction is relaxed, however, for all arguments of the data instance, even though I'd expect it only for the first argument.

Change History (3)

comment:1 Changed 2 years ago by goldfire

This is a documentation bug more than an implementation bug (or perhaps a design bug).

In contrast to type families, data family results must always have kind *. And the variables in a data family declaration have no scope anyway (ignoring TypeInType stuff), so a user may usefully say

data family DF1 :: * -> Nat -> *

as equivalent to

data family DF2 x (y :: Nat)

Because type families may have higher-kinded results (that is, result kinds with arrows), type families have to distinguish between proper arguments and components of the result.

Do you have an improvement to suggest, in either the design or documentation? I admit this inconsistency is quite surprising, but I don't have a better approach in mind.

comment:2 Changed 23 months ago by thomie

Keywords: TypeFamilies added

comment:3 Changed 23 months ago by thomie

Keywords: GADTs added
Note: See TracTickets for help on using tickets.