Reflected code reduction failure in the presence of erasure

[cmcmA20]

Trying to reduce or normalise the type of a constructor for a datatype with Type parameters breaks macros. Only user-defined datatypes are affected, builtin ones are fine.

IMO error message is also not very helpful:

Variable A is declared erased, so it cannot be used here
when checking that the expression A has type _68

Reproducer:

{-# OPTIONS --erasure --safe #-}
module ErasedReflectionBug where

open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
open import Agda.Primitive

_>>=_ : {a b : Level} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
_>>=_ = bindTC

_>>_ : {a b : Level} {A : Set a} {B : Set b} → TC A → TC B → TC B
_>>_ = λ mx my → bindTC mx λ _ → my

macro
  go : Name → Term → TC ⊤
  go cons-name hole = do
    raw-ty ← getType cons-name
    ty ← reduce raw-ty --<-- here
    returnTC _

data Copy {ℓ} (A : Set ℓ) : Set ℓ where
  mk-copy : A → Copy A

success1 success2 : ⊤
success1 = go []
success2 = go _∷_

fail : ⊤
fail = go mk-copy

Agda master (0259fe0fd)

[nad]

@jespercockx, I guess this is related to issue #6124.

[cmcmA20]

  go2 : Name → Term → TC ⊤
  go2 cons-name hole = do
    raw-ty ← getType cons-name
    inf-ty ← inferType (con cons-name [])
    unify inf-ty raw-ty
    returnTC _

Same error.

fail2 : Set₁
fail2 = {@0 A : Set} → A → Copy A

mk-copy' : {@0 A : Set} → A → Copy A 
mk-copy' = mk-copy

Inlining fail2 in the signature of mk-copy' is OK, but standalone fail2 raises an error.

[cmcmA20]

Btw, for a simplified example

data Copy (A : Set) : Set where
  mk-copy : A → Copy A

checkExpr reports a peculiar type

Checking {@0 A : Set₀} (z : A) → Copy A : Set
            at  $HOME/ErasedReflectionBug.agda:34,8-19
     -->  Set

This is universe inconsistent, Set must be Set1.

[andreasabel]

The following variant passes with Agda 2.6.3 but fails with 2.6.4, so it could be labelled regression:

{-# OPTIONS --erase-record-parameters --safe #-}

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

_>>=_ : {a b : Level} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
_>>=_ = bindTC

macro
  go : Name → Term → TC ⊤
  go cons-name hole = do
    raw-ty ← getType cons-name
    ty ← reduce raw-ty --<-- here
    returnTC _

record Copy {ℓ} (A : Set ℓ) : Set ℓ where
  constructor mk-copy
  field the-copy : A

success1 success2 : ⊤
success1 = go []
success2 = go _∷_

fail : ⊤
fail = go mk-copy

[andreasabel]

@cmcmA20 Is your issue related/identical to this one?

• https://github.com/agda/agda/issues/6400

[cmcmA20]

@andreasabel I guess it is. Slapping workOnTypes on top of all typechecker calls inside tcReduce resolves the problem with go but it feels ad hoc.

[andreasabel]

Maybe since you are reducing a type, using workOnTypes isn't so strange to request here. The general story is #6400. Closing as duplicate then...