Bug in universe inference?

Using Coq
1

Often it matters that Coq places a type in Prop rather than in Type. Here is an example where a type ascription is needed to place a match in Prop.

Inductive even: nat -> Prop :=
| evenB: even 0
| evenS: forall n, even n -> even (S (S n)).

Goal even 1 -> False.
Proof.
  refine (fun a => match a in even n 
                   return match n with 1 => False | _ => True end : Prop
                   with evenB => I | evenS _ _ => I end).
Qed.

The term doesn’t type check without the ascription since Coq places it in Type, which invalidates the match on the proof a. This type checking behavior has the unfortunate consequence that the smart match

Goal even 1 -> False.
Proof.
  refine (fun a => match a with end).
Qed.

doesn’t type check. I don’t know how to annotate the smart match so that it type checks.

So my question is whether this is a design decision or a bug?

Thanks in advance,
Gert

1 Like
2

Maybe I miss something, but I’d be surprised if the smart match worked in “raw Coq”/type theory; it seems you want GADTs/Agda/Idris or finally the Equations Coq plugin.

To know if the universe inference interferes, you could try the smart match when moving everything datatype in Type; I’d be surprised if it worked.

3

:slightly_smiling_face: The smart match work’s like a charme if even is moved to Type. There is a compiler to basic matches, basically compiling to the full code appearing above.

4

It is not a design decision, and since this is all about heuristics, it does not really qualify as a bug either. It is just an unfortunate limitation of the current implementation.

I thought a feature request had already been opened about it, but I cannot find it right now.