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?