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

Compilation of non-erased module parameters #265

Closed
jespercockx opened this issue Jan 18, 2024 · 2 comments · Fixed by #304
Closed

Compilation of non-erased module parameters #265

jespercockx opened this issue Jan 18, 2024 · 2 comments · Fixed by #304
Assignees
Labels
enhancement New feature or request error-reporting
Milestone

Comments

@jespercockx
Copy link
Member

Currently agda2hs assumes that all non-erased module parameters are types and should be compiled to explicit foralls. For example:

module _ (x : Int) where
  
  foo : Int
  foo = x

{-# COMPILE AGDA2HS foo #-}

is compiled to

foo :: forall x . Int
foo = x

We should either compile the module parameter to a regular function argument, or else throw an error that non-type module parameters are not supported.

@jespercockx jespercockx added enhancement New feature or request error-reporting labels Jan 18, 2024
@jespercockx jespercockx added this to the 1.3 milestone Jan 18, 2024
@flupe flupe self-assigned this Jan 23, 2024
@flupe
Copy link
Contributor

flupe commented Feb 22, 2024

With current master, this compiles to:

foo :: Int
foo x = x

Still bogus, a bit less so. Investigating now.

@jespercockx jespercockx assigned jespercockx and unassigned flupe Mar 22, 2024
@jespercockx jespercockx linked a pull request Mar 22, 2024 that will close this issue
@jespercockx
Copy link
Member Author

This is fixed by #304

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request error-reporting
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants