Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Error with promotion fields for sum types #180

Closed
odr opened this issue Mar 3, 2017 · 1 comment
Closed

Error with promotion fields for sum types #180

odr opened this issue Mar 3, 2017 · 1 comment

Comments

@odr
Copy link

odr commented Mar 3, 2017

When I write

promote [d|
  data X = X1 {y :: Symbol} | X2 {y :: Symbol}
  z (X1 x) = x
  z (X2 x) = x
  |]

I expect that Y and Z are similar. But now definition for Y is wrong:

:i Y
type family Y (a0 :: X) :: Symbol
  where [(field0 :: Symbol)] Y ('X2 field0) = field0
:i Z
type family Z (a0 :: X) :: Symbol
  where
    [(x0 :: Symbol)] Z ('X1 x0) = x0
    [(x0 :: Symbol)] Z ('X2 x0) = x0

That is on stack lts-8.0

@goldfirere
Copy link
Owner

Well-spotted. Yes, it seems that singletons doesn't consider the possibility that a record selector is used in multiple different constructors. I'm happy to review a PR before then, but I'm afraid you can't expect a fix before summertime. During this semester, time is extraordinarily precious!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants