Inference of match "return" clause vs. if

Using Rocq
1

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 a return annotation inside), which I did not expect,
  • and in addition, I did not expect that match and if would behave differently.

What’s going on?

1 Like
2

match elaboration indeed uses some heuristics to infer the return clause. IIRC there are 3 different strategies (2 when no expected type is provided) which are tried in some order. I am not aware of a description of these heuristics anywhere.

if elaboration is implemented separately, I guess it is similar to one of the match strategies. So when that strategy is not succesful or is not the one that is picked by match elaboration the results are different.

The let (x1, ..., xn) := ... in ... syntax is another independent implementation of match elaboration. See Use Cases to implement "let (x, y) := ..." instead of adhoc implem by SkySkimmer · Pull Request #14785 · coq/coq · GitHub for an attempt to unify the implementation, which failed due to compatibility issues.

NB: let (x1, ..., xn) := ... in ... not to be confused with let '(x1, ..., xn) := ... in .... In the first one (x1, ..., xn) is primitive syntax and matches any inductive with 1 constructor taking n arguments. In the second one (x1, ..., xn) is a notation (by default for the constructor of prod iterated n-1 times) and it is elaborated exactly like a normal match.
Internally the first one becomes GLetTuple coq/pretyping/glob_term.mli at e9d68d22c6605f2980f6bdccf9ac615c2eb16a0b · coq/coq · GitHub and the second one is GCases with only the case_style (used only by printing) different from a match expression.

(probably they are implemented separately because match elaboration sees constructor names but if and let (...) := don’t)

3

Thanks for clarifying.

While I didn’t expect that match could infer a type if it’s not a supertype of all possible types, I can imagine that being useful. On the other hand, I wonder if I should open a bug report about the if case. Even if we accept that it is not equivalent to match (although the constructors are known in this case because of the : bool annotation), isn’t it weird that Check (fun b : bool => if b then eq_refl true else eq_refl false). gives an error that essentially says “your term is ill-typed”? If Coq doesn’t accept this, it should IMHO error with “cannot infer this type” or something like that.

4

By the way, I tested the same in Lean. There the code

def foo
  | true => Eq.refl true
  | false => Eq.refl false

fails with a type error, and so does

def foo (b : Bool) :=
  if b then Eq.refl true else Eq.refl false

so it appears that Lean has the behavior of if in Coq, for both if and match.