meta variable confusion

Stream: lean4

[Joachim Breitner]

@Jireh Loreaux reported a bug with the new #find command. Here is a self-contained reproducer,
It prints (true, false). Why does the second one fail? I assume I am doing something wrong with the metavariables, but what?

import Mathlib.Tactic.Basic
import Mathlib.Tactic.RunCmd

set_option autoImplicit false
-- set_option pp.raw false

open Lean Meta Elab Command

class Star (R : Type _) where star : R → R
export Star(star)
-- Without an instance, `#check (star _)` will always fail
instance : Star Unit where star := fun () => ()
theorem star_comm_self' {R} [Mul R] [Star R] (x : R) : star x * x = x * star x := sorry

def ConstMatcher := ConstantInfo → MetaM Bool

def matchAnywhere (t : Expr) : MetaM ConstMatcher := withReducible do
  let head := t.toHeadIndex
  let head_args := t.headNumArgs
  let pat ← abstractMVars (← instantiateMVars t)
  -- dbg_trace (pat.expr)
  pure fun (c : ConstantInfo) => withReducible do
    let found  ← IO.mkRef false
    let cTy := c.instantiateTypeLevelParams (← mkFreshLevelMVars c.numLevelParams)
    Lean.Meta.forEachExpr' cTy fun sub_e => do
      if head == sub_e.toHeadIndex && head_args == sub_e.headNumArgs then do
        withNewMCtxDepth $ do
          let pat := pat.expr.instantiateLevelParamsArray pat.paramNames
            (← mkFreshLevelMVars pat.numMVars).toArray
          let (_, _, pat) ← lambdaMetaTelescope pat
          -- dbg_trace (pat, sub_e)
          Lean.logInfo m!"{pat}\n{sub_e}"
          if ← isDefEq pat sub_e
          then found.set true
      not <$> found.get
    found.get

run_cmd liftTermElabM do
  let s1 ← `(term|star ?a * ?a = ?a * star ?_)
  let t1 ← Lean.Elab.Term.elabTerm s1 none
  let matcher1 ← matchAnywhere t1

  let s2 ← `(term|star ?a * ?a = ?a * star ?a)
  let t2 ← Lean.Elab.Term.elabTerm s2 none
  let matcher2 ← matchAnywhere t2

  let ci := (← getEnv).constants.find! ``star_comm_self'
  dbg_trace (← matcher1 ci, ← matcher2 ci)

[Mario Carneiro]

this line is wrong:

          let pat := pat.expr.instantiateLevelParamsArray pat.paramNames
            (← mkFreshLevelMVars pat.numMVars).toArray

pat.numMVars is the number of expr metavariables abstracted (which you should be passing to lambdaMetaTelescope), while the number of universe metavariables is pat.paramNames.size

[Joachim Breitner]

Spot on, thanks!

[Joachim Breitner]

I guess I could just write

          let (_, _, pat) ← openAbstractMVarsResult pat

instead

[Kyle Miller]

@Joachim Breitner Here's a way to elaborate the term while allowing typeclass failures. That lets you delete instance : Star Unit where star := fun () => ().

open Lean.Elab in
def elabTerm' (t : Term) (expectedType? : Option Expr) : TermElabM Expr := do
  withTheReader Term.Context (fun ctx => { ctx with ignoreTCFailures := true }) do
    let t ← Term.elabTerm t expectedType?
    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
    return t

[Joachim Breitner]

Thanks! ignoreTcFailures looks scary … what kind of errors would I not catch this way?

[Joachim Breitner]

And why does the presence of an instance which does not even apply make a difference to the elaborator in the first place? This is not just my code, it’s even

class Star (R : Type _) where star : R → R
-- instance : Star Unit where star := fun () => ()
#check (Star.star _)

where I didn’t expect this to fail.

[Kyle Miller]

It fails because when it elaborates Star.star _, it triggers typeclass inference to fill in the instance argument, and it quickly detects that this problem will never have a solution (there are no instances), so it fails.

[Kyle Miller]

ignoreTCFailures is used when elaborating patterns in match expressions for example. You don't care if there are actually any instances out there when you're elaborating a pattern.

[Joachim Breitner]

Hmm, it seems strange to rely on the absence of type class instances, due to their open world nature. But it’s probably a corner case that doesn’t matter a lot. I’ll copy your elabTerm' into the #find implementation.

[Kyle Miller]

When you're elaborating a term, it switches to a closed world assumption -- no one is going to add new instances while a term is being elaborated.

[Kyle Miller]

I didn't mention that the concrete consequence of these options is that all the instance argument metavariables become plain metavariables when they fail to be synthesized. That seems to be what you want for a pattern.

[Joachim Breitner]

I just pushed a failing test to the joachim/find branch, where

#assert_match List.map (?a -> ?b) -> List ?a -> List ?b

doesn’t match (using the #find machinery), at the end of test/Find.lean – if someone wants to have a look why.

Oddly,

#assert_match List.map |- (?a -> ?b) -> List ?a -> List ?b

using the “conclusion matcher” rather than the “everywhere matcher” works.

[Mario Carneiro]

isn't that a parsing issue? you just asked to find something of the form ((List.map (?a -> ?b)) -> List ?a -> List ?b)

[Mario Carneiro]

i.e. you got bit by the parsing problem I had but in reverse

[Joachim Breitner]

No, the #assert_match is an ad-hoc command I created for the test, takes an ident, an optional turnstile, and an expression. Probably I should add a mandatory matches keyword there, for clarity :-)

[Joachim Breitner]

I found the problem: docs#Lean.Meta.forEachExpr' did not quite work as I thought it does: Given a type a → b → c, it does not visit b → c. Now (not yet deployed, have to rebuild mathlib…) List.map is found as it should.
(And that every deployment takes 3h because I rebuild all of mathlib using the nix setup is a bit silly…)