Cubical Agda: Unquote anonymous copattern involving path

[ecavallo]

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Cubical.Path 
open import Agda.Builtin.Reflection

record A : Set₀ where
  constructor mk
  field
    out : ⊤

test : PathP (λ _ → A) (mk tt) (mk tt)
test = λ where i .A.out → tt

macro
  mac : Term → Term → TC _
  mac t _ =
    bindTC (normalise t) λ norm →
    bindTC (unquoteTC norm) λ _ →
    returnTC _

b = mac test

raises

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Unquote.hs:442

No issue if the type of test is replaced with I → A.

[gallais]

Is it the copattern or the PathP? I tried to remove the
--cubical dependency and I am not getting the internal error:

open import Agda.Builtin.Sigma
open import Agda.Builtin.Reflection

id : Σ Set₁ (λ A → A)
id = λ where
  .fst → Set → Set
  .snd → λ x → x

macro
  mac : Term → Term → TC _
  mac t _ =
    bindTC (normalise t) λ norm →
    bindTC {A = Σ Set₁ (λ A → A)} (unquoteTC norm) λ _ →
    returnTC _

b = mac id

[ecavallo]

Removing the record but leaving the PathP also eliminates the internal error:

{-# OPTIONS --cubical #-}

open import Agda.Builtin.Unit
open import Agda.Builtin.List
open import Agda.Builtin.Cubical.Path 
open import Agda.Builtin.Reflection

test : PathP (λ _ → ⊤) tt tt
test = λ where i → tt

macro
  mac : Term → Term → TC _
  mac t _ =
    bindTC (normalise t) λ norm →
    bindTC (unquoteTC norm) λ _ →
    returnTC _

b = mac test

Replacing the PathP by another record removes the internal error as well.

record A : Set₀ where
  constructor mk
  field
    out : ⊤

record B : Set₀ where
  constructor hi
  field
    bye : A

test : B
test = λ where .B.bye .A.out → tt

[...]

The error does still occur if the order of PathP and record are swapped:

record A : Set₀ where
  constructor mk
  field
    out : PathP (λ _ → ⊤) tt tt

test : A
test = λ where .A.out i → tt

[...]

[plt-amy]

Fascinating! Here's what's going on:

test : PathP (λ _ → ⊤) tt tt
test = λ where i → tt

This isn't a pattern-matching lambda, even though it looks like one! It's just a lam, so you can quote/unquote it just fine. This is a pattern-matching lambda:

test₃ : PathP (λ _ → ⊤) tt tt
test₃ = λ where
  i → tt
  i → tt

and it also explodes, because Agda can't unquote IApply co/patterns.