Exact_no_check fails on Type

Using Coq
1

Given the following code:

Definition evil_type := nat : Type. (* the type annotation is necessary *)

Goal evil_type = evil_type.
Proof.
  exact (eq_refl  evil_type).
Qed.


Goal  evil_type = evil_type.
Proof.
  exact_no_check (eq_refl evil_type).
Qed.

Is there a succinct explanation why the exact works, but exact_no_check fails?

The term "eq_refl" has type "@eq Type@{Unnamed_thm0.u1} MUTATED MUTATED"
while it is expected to have type
 "@eq Type@{Unnamed_thm0.u0} MUTATED MUTATED".

I only partially understand the function of the Type Sort (Documentation), but I would assume that e.g. a failure to recognise that one Type is a subtype of Type should not differ between exact and exact_no_check.

2

The problem is the implicit argument of eq/eq_refl. The goal is @eq Type@{u0} _ _ but eq_refl evil_type produces the term eq_refl Type@{u1} evil_type (where u1 is fresh).
Without the type annotation you get @eq Set _ _ / @eq_refl Set _ because of some unification heuristic which when infering Set <= ?X does ?X := Set but when inferring Type@{u} <= ?X does ?X := Type@{u'} with fresh u' >= u.

1 Like
3

and exact just runs some “stronger” unification than exact_no_check?

4

exact will unify the inferred type with the expected type (ie the goal)
exact_no_check won’t (that’s why it’s called no_check)