RecordEquiv reflection doesn't seem to handle implicit field arguments

[Trebor-Huang]

MWE:

{-# OPTIONS --cubical #-}
module test where
open import Cubical.Reflection.RecordEquiv using (declareRecordIsoΣ)

postulate
  Bar : Set
  Baz : Bar → Set

record Foo : Set where
  field
    foo : ∀ {A} → Baz A

unquoteDecl FooΣ = declareRecordIsoΣ FooΣ (quote Foo)

This shows for me

Cannot instantiate the metavariable _A_9 to solution A
since it contains the variable A
which is not in scope of the metavariable
when checking that the expression _ has type Baz A

I'm on Agda somewhere around HEAD.

[Trebor-Huang]

I might help debug when I have time, but I'm going to sleep for now.

[maxsnew]

This is my number 1 most wanted feature right now.

[cmcmA20]

@maxsnew
It works if you explicitly write the signature

  foo-iso : Iso Foo ({A : Bar} → Baz A)
  unquoteDef foo-iso = define-record-iso foo-iso (quote Foo)

(and change the macro to provide a definition, not a declaration)

[maxsnew]

Can you share the code @cmcmA20 ?

[cmcmA20]

defineRecordIsoΣ' : R.Name → ΣFormat → R.Name → R.TC Unit
defineRecordIsoΣ' idName σ recordName =
  recordName→isoTy recordName σ >>= λ isoTy →
  R.defineFun idName (recordIsoΣClauses σ)

defineRecordIso : R.Name → R.Name → R.TC Unit
defineRecordIso idName recordName =
  R.getDefinition recordName >>= λ where
  (R.record-type _ fs) →
    let σ = List→ΣFormat (List.map (λ {(R.arg _ n) → n}) fs) in
    defineRecordIsoΣ' idName σ recordName
  _ →
    R.typeError (R.strErr "Not a record type name:" ∷ R.nameErr recordName ∷ [])

module _ where private
  Bar : Type
  Bar = ℕ

  private variable Z : Bar

  Baz : Bar → Type
  Baz 0 = Unit
  Baz _ = ℕ

  record Foo : Type where
    field
      foo : Baz Z

  foo-iso : Iso Foo (∀{A} → Baz A)
  unquoteDef foo-iso = defineRecordIso foo-iso (quote Foo)

[cmcmA20]

@maxsnew
Feel free to merge it yourself, I don't have time to refactor/clean it up properly