Reflected code reduction failure in the presence of erasure

[cmcmA20]

Reflected code reduction failure in the presence of erasure

[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?

• #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...