Understanding synthesization order

Stream: lean4

[Siddharth Bhat]

Consider the MWE:

class Case10 (A : outParam Type) (B : Type) extends Inhabited A where
  bar : A

class Case01 (A : Type) (B : outParam Type) extends Inhabited A where
  bar : A

class Case00 (A :  Type) (B : Type) extends Inhabited A where
  bar : A

---

Lean prints out:

~/temp elan run leanprover/lean4:nightly-2023-05-18 lean --version
Lean (version 4.0.0-nightly-2023-05-18, commit df49512880fd, Release)
~/temp elan run leanprover/lean4:nightly-2023-05-18 lean extends.lean
extends.lean:2:2: error: cannot find synthesization order for instance @Case10.toInhabited with type
  {A : outParam Type} → (B : Type) → [self : Case10 A B] → Inhabited A
all remaining arguments have metavariables:
  Case10 A ?B
extends.lean:8:2: error: cannot find synthesization order for instance @Case00.toInhabited with type
  {A : Type} → (B : Type) → [self : Case00 A B] → Inhabited A
all remaining arguments have metavariables:
  Case00 A ?B

---

• First off, I am not even sure what it is trying to synthesize. The error message states that it is trying to synthesize an [Inhabited A] instance.
• For Case00, I wonder we do not synthesize the information in the order of [A, Inhabited A, B].
• For Case10, what is the problem? Is it that A is marked as an outParam, and must thus be synthesized at the end, while also extending from Inhabited A, thereby needing to the synthesized at the beginning?

[Gabriel Ebner]

What the error message says is that Lean can't figure an order in which to process the subgoals of the Case??.toInhabited instance during TC synthesis (you get this instance because you've extended Inhabited). This order is computed when declaring the instance, before synthesizing an actual Inhabited instance.

[Gabriel Ebner]

The problem with Case10 and Case00 is that you could add this instance later on:

instance hugeProblem [AddMonoid G] [AddMonoid H] : Case00 G H where ..

Now think what happens when you then look for an Inhabited Nat instance. We first apply Case00.toInhabited, and get a Case00 Nat ?B subgoal. Then we apply hugeProblem and get two subgoals: AddMonoid Nat and AddMonoid ?B. And that second subgoal is really, really bad. Because Lean will then try to enumerate all possible additive monoids, which will usually diverge. (I say usually, because in this case we could add a high priority AddMonoid PUnit instance to short-circuit it. But in general this won't really work if you've got a subgoal like Module Rat (Prod Nat ?B).)

[Gabriel Ebner]

So to be safe, we statically check that you never get a subgoal with metavariable in non-outparams (like Case00 A ?B here, which could lead to AddMonoid ?B, etc.).

[Mario Carneiro]

I think it would make sense to just not declare the instance in this case, it is weird to be getting an error about an instance the user never wrote

[Gabriel Ebner]

There are two possible fixes here: 1) do not declare the instance, and 2) mark B as (semi)outparam.

[Gabriel Ebner]

Both are valid depending on the circumstances, and it's up to the user to decide. I'd rather not make this choice silently.

[Mario Carneiro]

how does the user "decide" not to declare the instance, if they still want it to be a parent structure as regards other lean behaviors?

[Mario Carneiro]

I don't think we have any syntax to opt into that behavior

[Gabriel Ebner]

class Case00 (A B : Type) where [toInhabited : Inhabited A] seems like a good enough match, at least in this case.

[Gabriel Ebner]

(Although of course it's not a parent structure.)

[Kevin Buzzard]

Is this question another instance of the same thing?

[Bolton Bailey]

I am getting the synthesization order error and I am still confused by the above discussion. The code I have is

class Encodable (α δ : Type _) where
  encode : α → δ
  decode : δ → Except String α

/-- Any `Encodable α δ` instance gives us a trivial `Coe α δ` instance -/
instance [Encodable α δ] : Coe α δ := ⟨Encodable.encode⟩

And it shows the error

cannot find synthesization order for instance @instCoe with type
  {α : Type u_1} → {δ : Type u_2} → [inst : Encodable α δ] → Coe α δ
all remaining arguments have metavariables:
  Encodable ?α δ

[Bolton Bailey]

I am confused by it saying there's a metavariable. If it tries to derive Coe from Encodable, aren't all the variables specified?

[Bolton Bailey]

(Note that this is not the mathlib Encodable)

[Gabriel Ebner]

No, Coe is chained right to left, the first argument is unspecified (a metavariable)

[Gabriel Ebner]

CoeTC might be the best choice here.

[Bolton Bailey]

Ok cool yes, that worked thanks.