Is Quoted a weak way of typing macros?

Stream: new members

[Xiyu Zhai]

Hi, all. I'm reading the actual implementation of Ring tactics in Mathlib4. The sheer complexity of the construct surprises me.

I'm trying to understand the role of Quoted in the code. It seems that

def Quoted (α : Expr) := Expr

in .lake/packages/Qq/Qq/Typ.lean.

Which means Q(anything) is nothing but Expr.

Now in the code for Ring tactics,

partial def ExSum.cast
    {v : Lean.Level} {β : Q(Type v)} {sβ : Q(CommSemiring $β)} {a : Q($α)} :
    ExSum sα a → Σ a, ExSum sβ a
  | .zero => ⟨_, .zero⟩
  | .add a₁ a₂ => ⟨_, .add a₁.cast.2 a₂.cast.2⟩

end

we then have a is both type Q($α) and type Q($β) and is actually just of type Expr.

So I believe the reasons behind not using type Expr directly is to help make the intention of things more precise?

[Eric Wieser]

There are two unrelated as in that expression, with the different types you identify

[Eric Wieser]

It's not a single a that is typed both ways simultaneously

[Xiyu Zhai]

I'm really sorry. It seems that I pasted the wrong line:

/-- Converts `ExBase sα` to `ExBase sβ`, assuming `sα` and `sβ` are defeq. -/
partial def ExBase.cast
    {v : Lean.Level} {β : Q(Type v)} {sβ : Q(CommSemiring $β)} {a : Q($α)} :
    ExBase sα a → Σ a, ExBase sβ a
  | .atom i => ⟨a, .atom i⟩
  | .sum a => let ⟨_, vb⟩ := a.cast; ⟨_, .sum vb⟩

[Xiyu Zhai]

It seems that I can do this without making lean compiler angry:

def justCast {β: Q(Type)} (x : Q($α)) : Q($β) := x

Is it doing a coercion under the hood? Or for the compiler, the two types are identical.

[Xiyu Zhai]

Sorry, it seems I'm looking at an old version of mathlib4.

[Xiyu Zhai]

I spotted a minor typo:

/--
Constructs the expression corresponding to `.const n`.
(The `.const` constructor does not check that the expression is correct.)
-/
def ExProd.mkNat (n : ℕ) : (e : Q($α)) × ExProd sα e :=
  let lit : Q(ℕ) := mkRawNatLit n
  ⟨q(($lit).rawCast : $α), .const n none⟩

/--
Constructs the expression corresponding to `.const (-n)`.
(The `.const` constructor does not check that the expression is correct.)
-/
def ExProd.mkNegNat (_ : Q(Ring $α)) (n : ℕ) : (e : Q($α)) × ExProd sα e :=
  let lit : Q(ℕ) := mkRawNatLit n
  ⟨q((Int.negOfNat $lit).rawCast : $α), .const (-n) none⟩

/--
Constructs the expression corresponding to `.const (-n)`.
(The `.const` constructor does not check that the expression is correct.)
-/
def ExProd.mkRat (_ : Q(DivisionRing $α)) (q : ℚ) (n : Q(ℤ)) (d : Q(ℕ)) (h : Expr) :
    (e : Q($α)) × ExProd sα e :=
  ⟨q(Rat.rawCast $n $d : $α), .const q h⟩

The last comment should be .const q. lol.

[Eric Wieser]

Xiyu Zhai said:

It seems that I can do this without making lean compiler angry:

def justCast {β: Q(Type)} (x : Q($α)) : Q($β) := x

Is it doing a coercion under the hood? Or for the compiler, the two types are identical.

This is unfortunately a leak in Qq's safety. The safe spelling is

def justCast {β: Q(Type)} (x : Q($α)) : Q($β) := q($x)

which reports the type error you expect

[Xiyu Zhai]

Thanks a lot! Now I understood!