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

Derivation fails when record update is used as a data index #178

Open
buzden opened this issue Aug 13, 2024 · 0 comments
Open

Derivation fails when record update is used as a data index #178

buzden opened this issue Aug 13, 2024 · 0 comments
Labels
issue: compilation error When compilation error raises because of the library part: derivation Related to automated derivation of generators status: confirmed bug Something isn't working

Comments

@buzden
Copy link
Owner

buzden commented Aug 13, 2024

Consider the following example:

record X where
  constructor MkX
  field : Nat

data Y : X -> Type where
  Start : Y r
  Next : Y ({field $= S} r) -> Y r

genY : Fuel -> (x : X) -> Gen MaybeEmpty $ Y x
genY = deriveGen

I'd expect this derivation to succeed, but it fails with

While processing right hand side of genY.
Error during reflection:
While processing right hand side of $resolved13352,<Deriving.DepTyCheck.Gen.Y>[0].
While processing right hand side of $resolved13352,<Deriving.DepTyCheck.Gen.Y>[0],<<Deriving.DepTyCheck.Gen.Next>>.
Deriving.DepTyCheck.Gen.case block in $resolved13323 is not accessible in this context.

I suspect coding of field update syntax through some case block does this, maybe we need to workaround it somehow on the library side.

@buzden buzden added status: confirmed bug Something isn't working part: derivation Related to automated derivation of generators issue: compilation error When compilation error raises because of the library labels Aug 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
issue: compilation error When compilation error raises because of the library part: derivation Related to automated derivation of generators status: confirmed bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant