search

IaFP / ghc

A slightly more Glorious Haskell Compiler
Other
2 stars 0 forks source link

Support Partial Data Families #8

Closed ahubers closed 2 years ago

ahubers commented 2 years ago

Manual

fxdpntthm commented 2 years ago 
data family DF a :: *             -- (0)
data family DF [a] = DF1 (BST a)  -- (1)
data family DF (T a) = DF2 [a]    -- (2)

The interesting case is when we have (1) BST a is partial. We have two options:

data family DF [a] = BST @ a => DF1 (BST a)  -- (a)

or

data family BST @ a => DF [a] = DF1 (BST a) -- (b)

The syntax for first one is supported, the syntax for the second declaration is not. Syntax is supported if the rep constructor is not a GADT. As a short term goal, we would expect the user to provide the signature as in (a) As a long term goal, we would want to support the syntax in (b)