«если» не просто сахар для «матча»

Question

В чем разница между этими двумя определениями:

Definition f : forall x:bool, if x then bool else nat :=
  fun x => match x with
           | true => true
           | false => 42
           end.
(* ^ Accepted by Coq *)

Definition g : forall x:bool, if x then bool else nat :=
  fun x => if x then true else 42.
(* ^ REJECTED *)

Раньше я предполагал, что if буквально является сахаром для match, но кажется, что это более ограничительно, когда речь заходит о зависимом паттерне-соответствие, даже если он все равно поддерживает синтаксис return.

Является ли это намеренным, и если да, то какое правило?

Answer 1

Для меня это похоже на ошибку: если вы попросите Coq напечатать f, он покажет match как if.

f = 
fun x : bool =>
if x as x0 return (if x0 then bool else nat) then true else 42
     : forall x : bool, if x then bool else nat

f is not universe polymorphic
Argument scope is [bool_scope]