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

[plt-amy]

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

[andreasabel]

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]

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]

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