Sorry, it’s me again…
This works and infers a type (without any existential variables):
Check (fun b : bool => match b with true => eq_refl true | false => eq_refl false end).
Coq replies:
fun b : bool => if b as b0 return (b0 = b0) then eq_refl else eq_refl
: forall b : bool, b = b
I find this surprising, because Coq happily gave the term a type which is not the most general possible (as far as I can tell, there is no “most general unifier” type in this case). For example, these also type-check, with two types that are not definitionally equal to the previous (and not even propositionally equal without functional extensionality):
Check (fun b : bool => match b with true => eq_refl true | false => eq_refl false end)
: forall b : bool, if b then true = true else false = false.
Check (fun b : bool => match b with true => eq_refl true | false => eq_refl false end)
: forall b : bool, if b then b = true else b = false.
What is more, I would have expected this code to be fully equivalent to this:
Fail Check (fun b : bool => if b then eq_refl true else eq_refl false).
since I learnt that if ... then ... else ...
is just syntactic sugar for match
. The documentation comes close to stating that they are equivalent on this page. Yet the one with if
gives an error:
Error:
In environment
b : bool
The term "eq_refl" has type "false = false" while it is expected to have type "true = true".
which means that Coq apparently refused to infer a dependent product in this case and tried to infer bool -> true = true
based on the first match
arm.
Actually, with if
, it seems that an explicit annotation outside the fun
is not accepted either. These fail:
Fail Check (fun b : bool => if b then eq_refl true else eq_refl false)
: forall b : bool, b = b.
Fail Check (fun b : bool => if b then eq_refl true else eq_refl false)
: forall b : bool, if b then true = true else false = false.
Fail Check (fun b : bool => if b then eq_refl true else eq_refl false)
: forall b : bool, if b then b = true else b = false.
On the other hand, an explicit return
annotation of course works:
Check (fun b : bool => if b return b = b then eq_refl true else eq_refl false).
Check (fun b : bool => if b return (if b then true = true else false = false) then eq_refl true else eq_refl false).
Check (fun b : bool => if b return (if b then b = true else b = false) then eq_refl true else eq_refl false).
In summary:
match
accepts to vary the type based on an outside annotation, as I expected,- but
match
infers a type without any annotation, which I did not expect, if
does not accept to vary the type based on an outside annotation at all (it requires areturn
annotation inside), which I did not expect,- and in addition, I did not expect that
match
andif
would behave differently.
What’s going on?