Failure to synthesize definitionally true proposition

Stream: general

[nrs]

In the following code, Lean correctly infers the second argument to congrFun but fails to infer the first argument, which is definitionally true and provable with rfl. How come argument inference fails in this case? Is there anything we can do to help Lean infer it?

structure WType where
  s : Type
  p : s -> Type

def ListP : WType := ⟨Nat, (Fin .)⟩

theorem zW : Fin n = ListP.p n := congrFun _ _

[Kyle Miller]

Yes, you write congrFun rfl _

[Kyle Miller]

There's no algorithm in Lean to try filling in placeholders with arbitrary terms — placeholders only get solved for through unification.

[Kyle Miller]

There's no need for congrFun here, theorem zW : Fin n = ListP.p n := rfl suffices.

[nrs]

Kyle Miller said:

There's no algorithm in Lean to try filling in placeholders with arbitrary terms — placeholders only get solved for through unification.

ah I see, thank you! Are all cases of successfully inferred arguments in Lean purely due to unification?

[Kyle Miller]

Yes, for _'s and implicit arguments.

[nrs]

Kyle Miller said:

Yes, for _'s and implicit arguments.

I see, thank you for the help!

[Kyle Miller]

Instance implicit arguments (from square brackets) use typeclass synthesis instead.