What information is used to help synthesis?

Stream: lean4

[Thomas Murrills]

And: when do you need to instantiate mvars to help synthesis along?

Here's the situation: I'm given a target type t and a theorem thm of type a → b → ... → t', where t' matched t via a discrtree. I want to apply thm to t, and try to synthesize as much as I can using heuristics for the unsolved goals.

It seems like the first step is computing (hs, bs, t') ← forallMetaTelescopeReducing <thm's type>, then unifying t' with t. I expect this will assign some metavariables now present in t' (unless lean4#2054 presents an issue here).

The issue is then what the best way to step through hs is to deal with implicits and heuristic solving together. Here are a couple examples of slightly different approaches:

1. sequential: step through the arguments one by one; insert a natural metavariable for implicit (unification-solved) arguments; insert a metavariable to solve via TC for instance arguments, and try to solve them immediately; apply heuristics to each other hs as soon as it's encountered.
2. implicits first: Attempt to synthesize all implicit/instance arguments first, then apply heuristics to each other argument that remains.
3. implicits second: Create mvars for each implicit argument, and try to solve each other metavariable with heuristics. Then go back and try to synthesize any instance arguments that were encountered.

The crux of the question here is: which order provides the most information to each solving process? For example, can attempting to solve later arguments by heuristics influence TC search in earlier instance arguments? (Do instance/implicit arguments always come first, and thus two of these options are equivalent?)

[Mario Carneiro]

Metavariables for instance subgoals are added to a pending list, and you can solve them using something like trySynthPendingMVars which takes no arguments

[Thomas Murrills]

But when should you try to solve them? Before you've solved the other goals, or after, or both? (Or each step of the way?)

[Mario Carneiro]

I don't think there is a good answer to that. Everything can potentially help or be helped by something else

[Thomas Murrills]

Hmm. Is calling something like trySynthPendingMVars relatively expensive to do over and over?

[Mario Carneiro]

no idea

[Mario Carneiro]

I would just follow the lead of something like the app elaborator

[Thomas Murrills]

sounds reasonable, I'll poke around in Lean.Elab.App