synthInstance after Mathlib import

Stream: mathlib4

[Chase Norman]

In the following code segment, the synthInstance call is successful:

import Mathlib.Data.ZMod.Basic
-- import Mathlib

open Lean Meta
#eval (do
  let e : Expr := .app (.const `AddCommMagma [Level.zero])
           (.app (.const `ZMod []) (← mkFreshExprMVar (some (.const `Nat []))))

  dbg_trace (← synthInstance e)
)

However, if you uncomment import Mathlib the synthInstance call fails. Any advice?

[Aaron Liu]

confusion

[Aaron Liu]

it thinks it needs more stuff than it actually does

[Aaron Liu]

maybe I can figure this out after I learn how typeclass works

[Eric Wieser]

Maybe synthesis is willing to assign a metavariable if there is only one thing that unifies?

[Aaron Liu]

But I don't think that's what's happening here

[Aaron Liu]

assigning metavariables doesn't do anything

[Robin Arnez]

synthInstance fails if it thinks that it could succeed when more metavariables were assigned.
In this case, the instance docs#DirectSum.GradeZero.commRing which has type CommRing (A 0) makes it think that: if the metavariable would be assigned 0, then this instance could be used (it thinks); so it just fails and leaves it to the caller to delay the synthesization.

[Robin Arnez]

What you might be looking for is docs#Lean.Elab.Term.mkInstMVar; this function also takes on the responsibility of registering an instance metavariable as pending.

[Chase Norman]

Would that function succeed in generating an instance or fail in this case? Because my workaround was going to be replacing all metavariables with free variables, and then replacing them back with the metavariables when synthInstance is done. I want the metavariables to be treated just like meta-level variables.

[Chase Norman]

And this happens even if the metavariable is syntheticOpaque

[Chase Norman]

In short, the metavariable is _not_ pending and I do _not_ want synthInstance to consider potential assignments to it.

[Bhavik Mehta]

For what it's worth, you can see the same behaviour like this (which to me makes it clearer that something is weird here)

import Mathlib.Data.ZMod.Basic
-- import Mathlib

#synth AddCommMagma (ZMod _)