Qq matching allows 1 as a function

Stream: lean4

[Robert Maxton]

I seem to have found an unsoundness in Qq:

  #eval show TermElabM _ from do
    let [u, v, w] ← Meta.mkFreshLevelMVars 3 | unreachable!
    let α ← mkFreshExprMVarQ q(Type u)
    let β ← mkFreshExprMVarQ q(Type v)
    let γ ← mkFreshExprMVarQ q(Type w)
    elabTermEnsuringTypeQ (←`(1)) q((($α) : Type u) → (($β) : Type v) → (($γ) : Type w))

happily prints Lean.Expr.mvar (Lean.Name.mkNum `_uniq 336).

[Robert Maxton]

By comparison,

  #eval show TermElabM _ from do
    elabTermEnsuringType (←`(ℕ)) (←elabType (←`(List ?_)))

properly throws type mismatch, and while

  #eval show TermElabM _ from do
    elabTermEnsuringType (←`(1)) (←elabType (←`(List ?_)))

doesn't panic, I do get <CoreM>:0:0: error: failed to synthesize instance OfNat (List ?m.3) 1.

[Eric Wieser]

Your code doesn't work for me due to missing imports; can you make it a #mwe?

[Robert Maxton]

Sure.

[Robert Maxton]

... Hmm, that's fascinating

[Robert Maxton]

import Lean.Meta
import Qq

import Mathlib.Tactic.PPWithUniv
import Mathlib.Tactic -- Comment out this import to make the problem go away.
import Mathlib.Util.Superscript

  open Lean Elab Term Qq Expr

  #eval show TermElabM _ from do
    let [u, v, w] ← Meta.mkFreshLevelMVars 3 | unreachable!
    let α ← mkFreshExprMVarQ q(Type u)
    let β ← mkFreshExprMVarQ q(Type v)
    let γ ← mkFreshExprMVarQ q(Type w)
    elabTermEnsuringTypeQ (←`(1)) q((($α) : Type u) → (($β) : Type v) → (($γ) : Type w))

[Robert Maxton]

Probably should not default to importing all of Mathlib.Tactic anyway but it's convenient in my sandbox file.

[Robert Maxton]

Anyway, something in Mathlib.Tactic (that isn't transitively imported by PPWithUniv) is making Qq unsound, I think. (Note that when the non-panic CoreM error throws, the corresponding output has a sorryAx in it, but doesn't when Mathlib.Tactic is imported.)

[Eric Wieser]

Thanks for the mwe! But what's the problem? That currently logs:

Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.app
      (Lean.Expr.const
        `OfNat.ofNat
        [Lean.Level.max
           (Lean.Level.max (Lean.Level.mvar (Lean.Name.mkNum `_uniq 1)) (Lean.Level.mvar (Lean.Name.mkNum `_uniq 2)))
           (Lean.Level.mvar (Lean.Name.mkNum `_uniq 3))])
      (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 8)))
    (Lean.Expr.lit (Lean.Literal.natVal 1)))
  (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 11))

What do you expect it to log?

[Robert Maxton]

<CoreM>:0:0: error: failed to synthesize instance
  OfNat (?m.4 → ?m.5 → ?m.6) 1

Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.const
      `sorryAx
      [Lean.Level.max
         (Lean.Level.max
           (Lean.Level.succ (Lean.Level.mvar (Lean.Name.mkNum `_uniq 1)))
           (Lean.Level.succ (Lean.Level.mvar (Lean.Name.mkNum `_uniq 2))))
         (Lean.Level.succ (Lean.Level.mvar (Lean.Name.mkNum `_uniq 3)))])
    (Lean.Expr.forallE
      Lean.Name.anonymous
      (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 4))
      (Lean.Expr.forallE
        Lean.Name.anonymous
        (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 5))
        (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 6))
        (Lean.BinderInfo.default))
      (Lean.BinderInfo.default)))
  (Lean.Expr.const `Bool.true [])

is the "correct" answer, I feel (because 1 is not a function that takes two parameters)

[Eric Wieser]

But 1 is a function that takes two parameters, docs#Pi.instOne:

import Mathlib.Algebra.Group.Pi.Basic

#check (1 : Nat -> Nat -> Nat)

[Robert Maxton]

.... Oh. >.>;

[Robert Maxton]

Fair enough, then!

[Eric Wieser]

I guess it's kind of interesting that the presence of the instance makes your example work even though the generated term doesn't actually contain the instance

[Notification Bot]

14 messages were moved here from #lean4 > Qq matching on -> error: cannot quote level mvar by Eric Wieser.

[Eric Wieser]

But I think this is just because elabTermEnsuringType is super permissive