unquoteExpr: inst✝².2 : Expr

Stream: mathlib4

[Eric Wieser]

In !4#3427 I'm getting an unhelpful error from Qq while trying to quote docs#Matrix.of; my guess is that it's tripping over the coercion from equiv to function?

The error message is just unquoteExpr: inst✝².2 : Expr

[Eric Wieser]

!4#3430 is slightly more self-contained

[Gabriel Ebner]

Qq tries to reduce types when unquoting them, this also unfolds let-bindings. The easy fix is just to replace let by have.

[Eric Wieser]

Is this also the reason that I can't seem to inline the lets into the q(...)?

[Gabriel Ebner]

And unfolding throws away the type annotation from the Q(...) tag, in case it's not clear. The error message is a bit cryptic though.

[Gabriel Ebner]

Eric Wieser said:

Is this also the reason that I can't seem to inline the lets into the q(...)?

You can do this:

q(vecCons $(show Q($eα) from toExpr (vecHead v))
  $(show Q(Fin $n → $eα) from toExpr (vecTail v)))

[Eric Wieser]

Oh, so there's no need to call ToExpr.toExpr on n?

[Gabriel Ebner]

Yes, it will automatically insert that. But it only really works for terms of closed type (Nat) which have a ToExpr instance available.

[Gabriel Ebner]

Like it doesn't know that α and eα are related so it can't automatically convert (vecHead v : α)

[Eric Wieser]

Could it be taught the relationship between toTypeExpr and toExpr?

[Eric Wieser]

Something like this perhaps:

open Lean Qq in
nonrec def Qq.toExpr.{u} {α : Type u} [ToLevel.{u}] [ToExpr α] (a : α) :
    Qq.QQ (show Q(Type u) from toTypeExpr α) :=
  toExpr a

[Gabriel Ebner]

This is the closest I've managed to come:

open Lean
open Qq

@[irreducible] def toTypeExprQ (α : Type u) [ToLevel.{u}] [ToExpr α] :
    Q(Type $(toLevel.{u})) :=
  toTypeExpr α

@[irreducible] def toExprQ {α : Type u} [ToLevel.{u}] [ToExpr α] (a : α) :
    Q($(toTypeExprQ α)) :=
  toExpr a

protected instance _root_.PiFin.toExpr [ToLevel.{u}] [ToExpr α] (n : ℕ) : ToExpr (Fin n → α) :=
  have toTypeExpr : Q(Type $(toLevel.{u})) := q(Fin $n → $(toTypeExprQ α))
  match n with
  | 0 => { toTypeExpr, toExpr := fun _ => q(@vecEmpty $(toTypeExprQ α)) }
  | n + 1 =>
    { toTypeExpr, toExpr := fun v =>
      have := PiFin.toExpr n
      have et : Q(Fin $n → $(toTypeExprQ α)) := toExprQ (vecTail v)
      q(vecCons $(toExprQ (vecHead v)) $et) }

[Gabriel Ebner]

Unfortunately, the toTypeExprQ is opaque here, so we don't know that $(vecTail v) has type Fin _ → _.

[Eric Wieser]

Do you think a toQq typeclass that implies toExpr could help here?