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

The GHC backend generates incorrect code for Agda code that uses reflection #5421

Closed
nad opened this issue May 31, 2021 · 2 comments
Closed
Assignees
Labels
backend: ghc Haskell code generation backend ("MAlonzo") reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
Milestone

Comments

@nad
Copy link
Contributor

nad commented May 31, 2021

If you compile the following code using the GHC backend and run the resulting binary, then the result is a crash:

open import Agda.Builtin.IO
open import Agda.Builtin.Reflection
open import Agda.Builtin.Strict
open import Agda.Builtin.String
open import Agda.Builtin.Unit

postulate
  putStrLn : String  IO ⊤

{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# COMPILE GHC putStrLn = Data.Text.IO.putStrLn #-}

main : IO ⊤
main = primForce (bindTC {A = Set} {B = Set}) λ _  putStrLn "Success"
Bug: MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Reflection.bindTC
CallStack (from HasCallStack):
  error, called at ./MAlonzo/Code/Agda/Builtin/Reflection.hs:178:5 in main:MAlonzo.Code.Agda.Builtin.Reflection

I acknowledge that the code above is not idiomatic, but I don't think that the GHC backend should generate code that crashes in this way.

@nad nad added type: bug Issues and pull requests about actual bugs backend: ghc Haskell code generation backend ("MAlonzo") reflection Elaborator reflection, macros, tactic arguments labels May 31, 2021
@nad nad added this to the icebox milestone May 31, 2021
@nad nad self-assigned this May 31, 2021
nad added a commit that referenced this issue May 31, 2021
nad added a commit that referenced this issue Jun 2, 2021
nad added a commit that referenced this issue Jun 2, 2021
@nad nad modified the milestones: icebox, 2.6.3 Jun 3, 2021
@nad nad closed this as completed in ef2d3d0 Jun 7, 2021
@asr
Copy link
Member

asr commented Jun 7, 2021

What about of cherry-picking the fix into release-2.6.2?

@nad
Copy link
Contributor Author

nad commented Jun 8, 2021

I have no strong opinion on this.

@andreasabel andreasabel modified the milestones: 2.6.3, 2.6.2.1 Aug 18, 2021
@andreasabel andreasabel mentioned this issue Aug 25, 2021
5 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend: ghc Haskell code generation backend ("MAlonzo") reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
Projects
None yet
Development

No branches or pull requests

3 participants