Bad elaboration of `if` on indexed inductive

[SkySkimmer]

Inductive bool' : bool -> Set := true' : bool' true | false' : bool' false.

Check if true' then 0 else 0.
(* The term "0" has type "nat" while it is expected to have type "fun _ : bool' true' => ?T" *)

(fun _ : bool' true' => ?T is not a type)

Can probably be massaged to get anomalies out.