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

Strange error when using direct DPair instead of (... ** ...) syntax of a derived generator return type #153

Open
buzden opened this issue May 6, 2024 · 0 comments
Labels
derive: entry Issue on the derivation function facing to the end-user issue: bad message When library reports some problem badly 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 status: workarounded Problem per se is not solved but workaround exists or implemented

Comments

@buzden
Copy link
Owner

buzden commented May 6, 2024

I had a definitions and a derived generator

data NameIsNew : (funs : Funs) -> (vars : Vars) -> UniqNames funs vars -> String -> Type

genNewName : Fuel -> (Fuel -> Gen MaybeEmpty String) =>
             (funs : Funs) -> (vars : Vars) -> (names : UniqNames funs vars) ->
             Gen MaybeEmpty (s ** NameIsNew funs vars names s)

and all worked, but once I change the return type to be in form of

             Gen MaybeEmpty $ DPair String $ NameIsNew funs vars names

derivation suddenly crashes with

Error: While processing right hand side of genNewName. Error during reflection: Target type's argument must be a variable name

with non-var expression being String.

Suddenly, replacing the return type with

             Gen MaybeEmpty $ DPair String $ \x => NameIsNew funs vars names x

helps with this.

@buzden buzden added status: confirmed bug Something isn't working part: derivation Related to automated derivation of generators issue: bad message When library reports some problem badly issue: compilation error When compilation error raises because of the library derive: entry Issue on the derivation function facing to the end-user status: workarounded Problem per se is not solved but workaround exists or implemented labels May 6, 2024
@buzden buzden changed the title Strange error when using direct DPair instread of (... ** ...) syntax of a derived generator return type Strange error when using direct DPair instead of (... ** ...) syntax of a derived generator return type May 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
derive: entry Issue on the derivation function facing to the end-user issue: bad message When library reports some problem badly 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 status: workarounded Problem per se is not solved but workaround exists or implemented
Projects
None yet
Development

No branches or pull requests

1 participant