(semi-)out-params

Stream: lean4

[Marcus Rossel]

Upon updating to Lean 4 nightly 2023-04-20, I've run into the following issue when using Coe:

structure A (α : Type) where
  a : α

structure A.With (a' : α) extends A α where
  a_eq : a = a'

/-
instance does not provide concrete values for (semi-)out-params
  Coe (A.With ?a) (A α)
-/
instance {a : α} : Coe (A.With a) (A α) where
  coe := A.With.toA

I'm not well-versed when it comes to type class inference, so in this example I'm guessing I'm doing something bad which Lean is now capable of informing me about. What is the problem here though, and how do I fix or work around it?

[Sebastian Ullrich]

Does https://leanprover-community.github.io/mathlib4_docs/Init/Coe.html#Important-typeclasses help?

[Marcus Rossel]

Sebastian Ullrich said:

Does https://leanprover-community.github.io/mathlib4_docs/Init/Coe.html#Important-typeclasses help?

Thanks, I think it did! Would the right move be to use CoeOut?

[Eric Rodriguez]

To me it seems CoeDep is the right way, no?

[Marcus Rossel]

Eric Rodriguez said:

To me it seems CoeDep is the right way, no?

The type A α doesn't depend on the precise term of type A.With a though.