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

Pragmas and scopes #3077

Open
nad opened this issue May 23, 2018 · 2 comments
Open

Pragmas and scopes #3077

nad opened this issue May 23, 2018 · 2 comments
Labels
pragma scope Issues relating to scope checking status: info-needed More information is needed from the bug reporter to confirm the issue.
Milestone
icebox

Comments

@nad
Copy link
Contributor

nad commented May 23, 2018

The polarity pragma can only be given in the same scope as the name which it is applied to. The following code triggers a warning:

module _ where

module M where

  postulate F : Set → Set

open M

{-# POLARITY F + #-}

Warning:

The following names are not declared in the same scope as their
polarity pragmas (they could for instance be out of scope, imported
from another module, or declared in a super module): F

I think other pragmas should be restricted in the same way. The following code is currently accepted:

{-# OPTIONS --rewriting #-}

module _ where

open import Agda.Builtin.Equality

{-# BUILTIN REWRITE _≡_ #-}

module M (_ : Set₁) where

  data D : Set where
    c : D

  A : c ≡ c
  A = refl

  record R : Set where
    coinductive

open M Set

{-# NOINLINE A #-}
{-# INLINE A #-}
{-# REWRITE A #-}
{-# STATIC A #-}
{-# INJECTIVE A #-}
{-# DISPLAY A = c #-}
{-# ETA R #-}
{-# WARNING_ON_USAGE R "..." #-}
{-# COMPILE GHC D = data D (D) #-}

{-# FOREIGN GHC data D = D #-}

I did not test all FFI pragmas, perhaps more can be added to the list.
@nad nad added type: bug Issues and pull requests about actual bugs scope Issues relating to scope checking pragma labels May 23, 2018
@nad nad added this to the 2.5.5 milestone May 23, 2018
@nad
Copy link
Contributor Author

nad commented May 23, 2018 

{-# NOINLINE A #-}
{-# INLINE A #-}

I think this should be ruled out even if the pragmas are given in the correct scope.

@andreasabel
Copy link
Member

andreasabel commented May 23, 2018 •
edited
Loading

{-# REWRITE A #-} is allowed on purpose and it makes sense to attempt to add a rewrite rule for the instance of A generated by the module application in the open statement.
Similar arguments apply to INJECTIVE and DISPLAY.
Maybe also STATIC.

@andreasabel andreasabel added status: info-needed More information is needed from the bug reporter to confirm the issue. and removed type: bug Issues and pull requests about actual bugs labels May 23, 2018
@jespercockx jespercockx modified the milestones: 2.6.0, 2.6.1 Nov 14, 2018
@jespercockx jespercockx modified the milestones: 2.6.1, icebox Oct 8, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
pragma scope Issues relating to scope checking status: info-needed More information is needed from the bug reporter to confirm the issue.
Projects
None yet
Milestone
icebox
Development

No branches or pull requests
3 participants
@nad @andreasabel @jespercockx