elabTerm with class

Stream: lean4

[Marcus Rossel]

I don't understand the following behavior of elabTerm:

import Lean
open Lean Meta Elab Term

def f {x : Nat} : Nat := x

#eval do
  let e ← elabTerm (← `(f)) none
  return e
  /-
  Lean.Expr.app (Lean.Expr.const `f []) (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 1))
  -/

theorem g [Append α] (a : α) : a ++ a = a ++ a := rfl

#eval do
  let e ← elabTerm (← `(g)) none
  return e
  /-
  Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.const `g [Lean.Level.mvar (Lean.Name.mkNum `_uniq 1)])
    (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 2)))
  (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 3))
  -/

class C (α) where
  add       : α → α → α
  add_assoc : ∀ a b c, add (add a b) c = add a (add b c)

#eval do
  let e ← elabTerm (← `(C.add_assoc)) none
  return e
  /-
  <CoreM>:0:0: error: failed to synthesize instance
  C ?m.2
  -/

In the first two examples, Lean happily elaborates the terms and uses mvars for implicit arguments and type class arguments. Why doesn't it do so in the third example? (And is there a way I can make it behave the same as in the other examples?)

[Damiano Testa]

I don't know why this happens, but try adding a fake instance before the last eval:

import Lean
open Lean Meta Elab Term

class C (α) where
  add       : α → α → α
  add_assoc : ∀ a b c, add (add a b) c = add a (add b c)

instance : C Nat := sorry

#eval do
  let e ← elabTerm (← `(C.add_assoc)) none
  return e
/-
Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.const `C.add_assoc [Lean.Level.mvar (Lean.Name.mkNum `_uniq 1)])
    (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 2)))
  (Lean.Expr.mvar (Lean.Name.mkNum `_uniq 3))
-/

[Damiano Testa]

Here is a slightly shorter version:

import Lean.Elab.Term

class C where c : Unit

open Lean.Elab.Term

-- works always
#eval do elabTerm (← `(@C.c)) none

-- comment this instance to make the following `#eval` fail
instance : C := ⟨()⟩

-- only works if the previous instance is not commented
#eval do elabTerm (← `(C.c)) none

[Eric Wieser]

That last one works without the instance for me.

[Eric Wieser]

Oh wait, the error is being printed without a red squiggle:

<CoreM>:0:0: error: failed to synthesize instance
  C

[Damiano Testa]

Yes, I am very surprised by this.

[Damiano Testa]

It really seems to have to do with whether the environment contains some instance of the correct class.

[Damiano Testa]

And if you define a local instance in its section and the #eval is outside the section, then it also does not work.

[Damiano Testa]

And the mangled expression that elabTerm produces also contains Bool.true.

[Eric Wieser]

I think that's just an argument to docs#sorryAx

[Damiano Testa]

You are right:

#check sorryAx  -- sorryAx.{u} (α : Sort u) (synthetic : Bool := false) : α

it is probably the synthetic argument.

[Damiano Testa]

It seems that unless there is an instance registered, then Lean refuses to create the metavariable for the instance, unless you really ask it, by either using @ or by passing the implicit self argument with an underscore.

[Damiano Testa]

I find this very bizarre!

[Sebastian Ullrich]

You are trying to second-guess when and how Lean synthesizes synthetic metavariables, that is not a robust elaboration strategy

[Damiano Testa]

I am not sure whether your comment dispels or increases how mystic all this feels! :smile: