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

Private bindings in imported modules defeat check for binding of primIdFace/primIdPath #6022

Closed
plt-amy opened this issue Aug 14, 2022 · 3 comments · Fixed by #6152
Closed

Private bindings in imported modules defeat check for binding of primIdFace/primIdPath #6022

plt-amy opened this issue Aug 14, 2022 · 3 comments · Fixed by #6152
Assignees
@andreasabel
Labels
builtin Enhancements to the builtin modules and builtin definitions cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp dead-code Concerning the dead-code removal optimization internal-error Concerning internal errors of Agda modules Issues relating to the module system scope Issues relating to scope checking type: bug Issues and pull requests about actual bugs
Milestone
2.6.3

Comments

@plt-amy
Copy link
Member

plt-amy commented Aug 14, 2022

Suppose you have a module

{-# OPTIONS --cubical #-}
module test5 where

open import Agda.Primitive.Cubical renaming
  (primINeg to ~_; primIMax to _∨_; primIMin to _∧_;
  primHComp to hcomp; primTransp to transp; primComp to comp;
  itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path

{-# BUILTIN ID      Id   #-}
{-# BUILTIN REFLID  refl #-}

private primitive
  primDepIMin : _
  primIdFace : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → I
  primIdPath : ∀ {ℓ} {A : Set ℓ} {x y : A} → Id x y → x ≡ y
  primConId : ∀ {ℓ} {A : Set ℓ} {x y : A} → I → x ≡ y → Id x y

and a module

{-# OPTIONS --cubical #-}
module test4 where

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive.Cubical renaming (primTransp to transp)

open import test5

module _ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) where
  q : Id x y
  q = transp (λ i → Id x (p i)) i0 refl

  r = {! q !}

Normalizing q results in fireworks:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Monad/Signature.hs:733:32 in Agda-2.6.3-inplace:Agda.TypeChecking.Monad.Signature

this shouldn't even type check — there is no binding for primIdFace/primIdPath in scope, which are necessary for transport in the cubical identity types, but the primitives have been bound, so we don't get the expected error message
@plt-amy plt-amy added type: bug Issues and pull requests about actual bugs modules Issues relating to the module system cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp internal-error Concerning internal errors of Agda labels Aug 14, 2022
@plt-amy plt-amy added this to the 2.6.3 milestone Aug 14, 2022
@plt-amy plt-amy self-assigned this Aug 14, 2022
@plt-amy plt-amy changed the title Private bindings in exported modules defeat check for binding of primIdFace/primIdPath Private bindings in imported modules defeat check for binding of primIdFace/primIdPath Aug 14, 2022
@andreasabel andreasabel assigned andreasabel and unassigned plt-amy Sep 30, 2022
@andreasabel
Copy link
Member

andreasabel commented Sep 30, 2022 •
edited
Loading

I can trigger this internal error non-interactively by:

...
module _ {ℓ} {A : Set ℓ} {x y : A} (p : x ≡ y) where

  q : Id x y
  q = transp (λ i → Id x (p i)) i0 refl

  q' : Id x y
  q' = transp (λ i → Id x (p i)) i0 refl

  test : q ≡ q'
  test i = {!!}

The information given by {-# OPTIONS -v impossible:100 #-} is:

Unbound name: Issue6022Import.primConId[0,36]@ModuleNameHash 715247100494519651

@andreasabel andreasabel added scope Issues relating to scope checking builtin Enhancements to the builtin modules and builtin definitions labels Sep 30, 2022
@andreasabel
Copy link
Member

I tried to reproduce this for other primitives:

module Issue6022.Char where

open import Agda.Builtin.Nat

postulate Char : Set
{-# BUILTIN CHAR Char #-}

private primitive
  primCharToNat : Char → Nat
  primNatToChar : Nat → Char

roundtrip : Char → Char
roundtrip c = primNatToChar (primCharToNat c)
module Issue6022 where

open import Agda.Builtin.Equality
open import Issue6022.Char

test : ∀{c} → roundtrip c ≡ c
test = refl

This gives a normal error:

Issue6022.Char.primNatToChar (Issue6022.Char.primCharToNat c) != c of type Char
when checking that the expression refl has type roundtrip c ≡ c

Probably, in this case the deadcode analysis does not kick in, because roundtrip explicitly mentions the two primitives. There is no such explicit mention in the OP.

@andreasabel andreasabel added the dead-code Concerning the dead-code removal optimization label Sep 30, 2022
@andreasabel
Copy link
Member

Excluding primitive definitions from dead-code elimination fixes the problem.

andreasabel added a commit that referenced this issue Sep 30, 2022
@andreasabel
Fix #6022 crudely: do not subject primitives to dead-code removal
8a69947 
Some cubical primitives are used internally even if declared
privately, so removing them from the interface leads to crashes in
client modules.
@andreasabel andreasabel mentioned this issue Sep 30, 2022
Merged
andreasabel added a commit that referenced this issue Sep 30, 2022
@andreasabel
Fix #6022 crudely: do not subject primitives to dead-code removal
657fce0 
Some cubical primitives are used internally even if declared
privately, so removing them from the interface leads to crashes in
client modules.
andreasabel added a commit that referenced this issue Sep 30, 2022
@andreasabel
Fix #6022 crudely: do not subject primitives to dead-code removal
495d35e 
Some cubical primitives are used internally even if declared
privately, so removing them from the interface leads to crashes in
client modules.
andreasabel added a commit that referenced this issue Sep 30, 2022
@andreasabel
Fix #6022 crudely: do not subject primitives to dead-code removal
7183739 
Some cubical primitives are used internally even if declared
privately, so removing them from the interface leads to crashes in
client modules.
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
builtin Enhancements to the builtin modules and builtin definitions cubical Cubical Agda paraphernalia: Paths, Glue, partial elements, hcomp, transp dead-code Concerning the dead-code removal optimization internal-error Concerning internal errors of Agda modules Issues relating to the module system scope Issues relating to scope checking 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.

Fix #6022 crudely: do not subject primitives to dead-code removal agda/agda
2 participants
@andreasabel @plt-amy