8000 Warn about opaque `unquoteDecl`/`unquoteDef` · Issue #6959 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Warn about opaque unquoteDecl/unquoteDef #6959

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
Closed
nad opened this issue Nov 7, 2023 · 0 comments · Fixed by #6971
Closed

Warn about opaque unquoteDecl/unquoteDef #6959

nad opened this issue Nov 7, 2023 · 0 comments · Fixed by #6971
Assignees
@plt-amy
Labels
opaque Issues about `opaque` definitions type: bug Issues and pull requests about actual bugs
Milestone
2.6.4.1

Comments

@nad
Copy link
Contributor
nad commented Nov 7, 2023

Agda does not complain about the following code, but c′ and c″ are not opaque:

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection

data D : Set where
  c : D

opaque

  unquoteDecl c′ =
     bindTC
       (declareDef
          (arg (arg-info visible (modality relevant quantity-ω)) c′)
          (def (quote D) [])) λ _ →
     defineFun c′ (clause [] [] (con (quote c) []) ∷ [])

  c″ : D
  unquoteDef c″ =
    defineFun c″ (clause [] [] (con (quote c) []) ∷ [])

_ : c ≡ c′
_ = refl

_ : c ≡ c″
_ = refl

The following code suggests that the idea is that these definitions should be opaque:

agda/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

Lines 2161 to 2164 in 4b23885

interestingOpaqueDecl A.FunDef{} = True
interestingOpaqueDecl A.UnquoteDecl{} = True
interestingOpaqueDecl A.UnquoteDef{} = True
interestingOpaqueDecl A.Primitive{} = True

@nad nad added type: bug Issues and pull requests about actual bugs opaque Issues about `opaque` definitions labels Nov 7, 2023
@nad nad added this to the 2.6.5 milestone Nov 7, 2023
@plt-amy plt-amy mentioned this issue Nov 9, 2023
Merged
plt-amy added a commit that referenced this issue Nov 9, 2023
@plt-amy
fix #6959: Keep ambient opacity in unquoted defs
186d780
plt-amy added a commit that referenced this issue Nov 9, 2023
@plt-amy
fix #6959: Keep ambient opacity in unquoted defs
93f7e3a
plt-amy added a commit that referenced this issue Nov 9, 2023
@plt-amy
fix #6959: Keep ambient opacity in unquoted defs
a712999
@plt-amy plt-amy mentioned this issue Nov 9, 2023
Merged
@andreasabel andreasabel modified the milestones: 2.6.5, 2.6.4.1 Nov 9, 2023
plt-amy added a commit that referenced this issue Nov 9, 2023
@plt-amy
Bugfixes for opaque definitions (#6971)
ce76d14 
* fix #6958: Primitives can not be opaque

* #6958: Add a test case

* fix #6745: Keep track of copies when making them

* fix #6959: Keep ambient opacity in unquoted defs

* fixup: manually disambiguate defOpaque field name
@andreasabel andreasabel changed the title Warn about opaque unquoteDecl/unquoteDef? Warn about opaque unquoteDecl/unquoteDef Nov 15, 2023
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
@plt-amy @JobPetrovcic
Bugfixes for opaque definitions (agda#6971)
aba413a 
* fix agda#6958: Primitives can not be opaque

* agda#6958: Add a test case

* fix agda#6745: Keep track of copies when making them

* fix agda#6959: Keep ambient opacity in unquoted defs

* fixup: manually disambiguate defOpaque field name
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@plt-amy plt-amy

Labels
opaque Issues about `opaque` definitions type: bug Issues and pull requests about actual bugs
Projects
None yet
Milestone
2.6.4.1
Development

Successfully merging a pull request may close this issue.

Bugfixes for opaque definitions agda/agda
3 participants
@nad @andreasabel @plt-amy
0