typeclass mvars unassigned after elab

Stream: lean4

[James Gallicchio]

I'm elaborating and evaluating an array literal expression, but for some reason when it reaches > 32 elements and starts nesting lists, some of the metavariables in the expression that I thought should be assigned during elaboration are instead left unassigned?

MWE:

import Lean
import Std
import Qq

open Lean Elab Qq Command Meta

elab "genStatusCodes!" codes:term : command => liftTermElabM do
  let expectedType := q(Array Nat)
  let expr ← instantiateMVars <| ← Term.elabTermEnsuringType codes (expectedType? := some expectedType)
  let unassigned := (← getUnassignedExprMVars).map (·.name)
  if !unassigned.isEmpty then
    IO.println unassigned
    IO.println expr
    throwError default

genStatusCodes! #[
  00,01,02,03,04,05,06,07,08,09,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31
  -- uncomment for error
  --, 32
]

The metavariables are all the typeclass args of the OfNat expressions.

I assume I need something beyond instantiateMVars, but I'm not quite sure what I'm missing!

[Kyle Miller]

The missing piece is docs#Lean.Elab.Term.synthesizeSyntheticMVars (or the combinator version docs#Lean.Elab.Term.withSynthesize, which also handles default instances)

let expr ← instantiateMVars <| ← Term.withSynthesize <| Term.elabTermEnsuringType codes (expectedType? := some expectedType)

[Kyle Miller]

This combinator ensures that all typeclass problems are solved for (and in general, that all synthetic metavariables have their associated code be evaluated)

[James Gallicchio]

works perfectly, thank you!!

is there a list of metaprogramming book to-dos? typeclass elaboration (and I guess synthetic mvars?) would be a nice topic to have some more discussion of