# Bug in universe inference?

**URL:** <https://discourse.rocq-prover.org/t/bug-in-universe-inference/1093>\
**Category:** Using Rocq\
**Created:** [October 26, 2020, 10:18am UTC](https://discourse.rocq-prover.org/t/bug-in-universe-inference/1093 "2020-10-26T10:18:55Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![gert-smolka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gert-smolka/32/20_2.png) [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Post date:** [October 26, 2020, 10:18am UTC](https://discourse.rocq-prover.org/t/bug-in-universe-inference/1093/1 "2020-10-26T10:18:55Z")

</div>

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.

```auto
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

```auto
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

---

<div class="post-metadata">

**Author:** ![Blaisorblade](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/blaisorblade/32/56_2.png) [@Blaisorblade](https://discourse.rocq-prover.org/u/Blaisorblade)\
**Post date:** [October 27, 2020, 2:09am UTC](https://discourse.rocq-prover.org/t/bug-in-universe-inference/1093/2 "2020-10-27T02:09:47Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![gert-smolka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gert-smolka/32/20_2.png) [@gert-smolka](https://discourse.rocq-prover.org/u/gert-smolka)\
**Post date:** [October 27, 2020, 5:47am UTC](https://discourse.rocq-prover.org/t/bug-in-universe-inference/1093/3 "2020-10-27T05:47:52Z")

</div>

🙂 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.

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [October 27, 2020, 9:54am UTC](https://discourse.rocq-prover.org/t/bug-in-universe-inference/1093/4 "2020-10-27T09:54:26Z")

</div>

> [@gert-smolka](#):
>
> So my question is whether this is a design decision or a bug?

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.