motive in pattern matching has curious type

Stream: general

[Gustavo Goretkin]

The recursors of inductive types take a "motive", which is a type family (a function to Sort u) that determines the type of the result. For example:

Bool.rec : {motive : Bool → Sort u} → motive false → motive true → (t : Bool) → motive t

So, for example, an explicit motive can be provided as a lambda:

Bool.rec (motive := fun (_ : Bool) => Nat) 3 5 true

But for pattern matching, the motive is a Pi type rather than a type family:

fun b : Bool =>
  match (motive := (_ : Bool) -> Nat) b with
  | true => 3
  | false => 5

Why is the motive a type family in the former but a (Pi) type in the latter?

[Aaron Liu]

I have no idea

[Aaron Liu]

in the match compiler there's code to convert the type family into a lambda

[Aaron Liu]

and if you check the terms it generates you can see the term contains a lambda

[Robin Arnez]

I think it's supposed to be the type of

(match · with
| true => 3
| false => 5)

i.e. the type of the match if you just look at the discriminants and the result type