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.

Sign up for GitHub

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

Jump to bottom

Internal error when compiling program with quoted metavariable #5754

Closed
jespercockx opened this issue Jan 25, 2022 · 1 comment · Fixed by #6326
Closed

Internal error when compiling program with quoted metavariable #5754

jespercockx opened this issue Jan 25, 2022 · 1 comment · Fixed by #6326
Labels
backend: ghc Haskell code generation backend ("MAlonzo") bugfix-sprint-candidate internal-error Concerning internal errors of Agda reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
Milestone
2.6.3

Comments

@jespercockx
Copy link
Member

jespercockx commented Jan 25, 2022 •
edited by andreasabel
Loading

(forked off from the discussion at #5731)

open import Agda.Builtin.IO
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)
open import Agda.Builtin.String
open import Agda.Builtin.Unit

macro
  getMeta : Term → TC ⊤
  getMeta hole@(meta m _) = quoteTC m >>= unify hole
  getMeta _ = typeError []

myMeta : Meta
myMeta = getMeta

postulate putStrLn : String → IO ⊤
{-# FOREIGN GHC import qualified Data.Text as T #-}

main : IO ⊤
main = putStrLn (primShowMeta myMeta)

Trying to compile this with the GHC backend this produces an internal error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/Compiler/MAlonzo/Compiler.hs:1097:18 in Agda-2.6.3-2GgStRv6exQAe2hnultIdP:Agda.Compiler.MAlonzo.Compiler

P.S. (Andreas): Error is thrown here:

agda/src/full/Agda/Compiler/MAlonzo/Compiler.hs

Line 1110 in 5f074ff

LitMeta{} -> __IMPOSSIBLE__

@jespercockx jespercockx added type: bug Issues and pull requests about actual bugs backend: ghc Haskell code generation backend ("MAlonzo") reflection Elaborator reflection, macros, tactic arguments internal-error Concerning internal errors of Agda labels Jan 25, 2022
@jespercockx jespercockx added this to the 2.6.3 milestone Jan 25, 2022
@jespercockx jespercockx mentioned this issue Aug 31, 2022
Closed
@andreasabel andreasabel modified the milestones: 2.6.3, later Aug 31, 2022
fredrikNordvallForsberg added a commit that referenced this issue Nov 14, 2022
@fredrikNordvallForsberg
[ fix #5754 ] properly compile Meta (GHC and JS)
4a4b842
Merged
@andreasabel
Copy link
Member

Consider for 2.6.3.

@andreasabel andreasabel modified the milestones: later, 2.6.3 Nov 14, 2022
andreasabel pushed a commit that referenced this issue Nov 19, 2022
@fredrikNordvallForsberg
Proper compilation of Metas (GHC and JS) (#6326)
03070c0 
Fixes #5754. Investigated together with @felixwellen at AIM XXXI.
andreasabel pushed a commit that referenced this issue Nov 19, 2022
@fredrikNordvallForsberg @andreasabel
Proper compilation of Metas (GHC and JS) (#6326)
0e5fa29 
Fixes #5754. Investigated together with @felixwellen at AIM XXXI.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
backend: ghc Haskell code generation backend ("MAlonzo") bugfix-sprint-candidate internal-error Concerning internal errors of Agda reflection Elaborator reflection, macros, tactic arguments type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.3
Development

Successfully merging a pull request may close this issue.

Proper compilation of Metas (GHC and JS) agda/agda
2 participants
@andreasabel @jespercockx