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

Support derivation for types with implicit parameters in the type signature #72

Open
buzden opened this issue May 30, 2023 · 1 comment
Labels
derive: core Something in between single type generator and its constructors derive: entry Issue on the derivation function facing to the end-user derive: infrastructure Issue around derivation, but not directly in 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: feature request Request for new functionality or improvement

Comments

@buzden
Copy link
Owner

buzden commented May 30, 2023

Implicit arguments were always supported at the derivation task and in constructors of derived types, but as a curious case, were never supported in the types themselves, which is unfortunate.

@buzden buzden added status: confirmed bug Something isn't working part: derivation Related to automated derivation of generators status: feature request Request for new functionality or improvement issue: compilation error When compilation error raises because of the library derive: core Something in between single type generator and its constructors derive: infrastructure Issue around derivation, but not directly in derive: entry Issue on the derivation function facing to the end-user labels May 30, 2023
@buzden
Copy link
Owner Author

buzden commented Dec 20, 2023

As an example of such type, one can consider

data X : Vect n a -> Fin n -> a -> Type where
  Here : X (x::xs) FZ x
  There : X xs n y -> X (x::xs) (FS n) y

Here we have n and a to be an implicit type arguments in the type signature of X

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
derive: core Something in between single type generator and its constructors derive: entry Issue on the derivation function facing to the end-user derive: infrastructure Issue around derivation, but not directly in 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: feature request Request for new functionality or improvement
Projects
None yet
Development

No branches or pull requests

1 participant