Elaborator behavior on `Prod.casesOn` in these examples

Stream: general

[nrs]

Consider these three examples of applications of Prod.casesOn (the first is from TPiL).

def prod_example (p : Bool × Nat) : Nat := Prod.casesOn (motive := fun (somep : Bool × Nat) => Nat) p (fun b n => cond b (2 * n) (2 * n + 1))
def nonworking_prod_example (p : Bool × Nat) : Nat := Prod.casesOn (fun (somep : Bool × Nat) => Nat) p (fun b n => cond b (2 * n) (2 * n + 1))
def fixed_prod_example (p : Bool × Nat) : Nat := @Prod.casesOn Bool Nat (fun (somep : Bool × Nat) => Nat) p (fun b n => cond b (2 * n) (2 * n + 1))

The second example fails with the error
application type mismatch Prod.casesOn fun somep ↦ Nat argument fun somep ↦ Nat has type Bool × Nat → Type : Type 1 but is expected to have type ?m.28129 × ?m.28130 : Type (max ?u.28113 ?u.28112)

Could someone explain how specifying (motive := ...) makes the elaborator behave as if we had used the fixed_prod_example declaration? I don't understand how this gives more information beyond what nonworking_prod_example gives, so I don't understand why it typechecks.

[Floris van Doorn]

motive is an implicit argument, so doesn't have to be given, and Lean can figure out what it is from the expected type and the given arguments. Removing the first argument from your second def fixes it:

def now_working_prod_example (p : Bool × Nat) : Nat :=
  Prod.casesOn p (fun b n => cond b (2 * n) (2 * n + 1))

[nrs]

Floris van Doorn said:

motive is an implicit argument, so doesn't have to be given, and Lean can figure out what it is from the expected type and the given arguments. Removing the first argument from your second def fixes it:

def now_working_prod_example (p : Bool × Nat) : Nat :=
  Prod.casesOn p (fun b n => cond b (2 * n) (2 * n + 1))

Thank you very much! Very curious, I would have expected then for

def another_prod_example (p : Bool × Nat) : Nat := Prod.casesOn _ p (fun b n => cond b (2 * n) (2 * n + 1))

to typecheck, but it doesn't and your version does! Thanks for the example I will try to see if I can figure out how this is working.

[nrs]

by any chance do you know of a trace class that renders the differences here explicitly?

[Kyle Miller]

Why are you expecting to be able to put _ in this context? When you do that, it stands for an explicit argument. The type of Prod.casesOn shows only two explicit arguments:

#check Prod.casesOn
/-
Prod.casesOn.{u_1, u, v} {α : Type u} {β : Type v} {motive : α × β → Sort u_1} (t : α × β)
  (mk : (fst : α) → (snd : β) → motive (fst, snd)) : motive t
-/

[Kyle Miller]

Here's a simpler example. Are you surprised that the second one fails to elaborate?

#check id 2
#check id _ 2

[nrs]

Kyle Miller said:

Why are you expecting to be able to put _ in this context? When you do that, it stands for an explicit argument. The type of Prod.casesOn shows only two explicit arguments:

#check Prod.casesOn
/-
Prod.casesOn.{u_1, u, v} {α : Type u} {β : Type v} {motive : α × β → Sort u_1} (t : α × β)
  (mk : (fst : α) → (snd : β) → motive (fst, snd)) : motive t
-/

ohhhhh!!! I got confused, I had never encountered the (implicitArg := ...) notation and I didn't realize the way it was being passed! Thanks a lot for pointing that out!