Coq item 1.2.10 Type cast

Question

Not sure what the following means in the Coq manual v8.7.0 item 1.2.10:

• The expression term : type is a type cast expression. It enforces the type of term to be type.

• term <: type locally sets up the virtual machine for checking that term has type type.

My understanding is that the type check of the first one is done by Coq (some default), whereas the second one is done by a chosen Coq's VM (which might have different typing rules).

I try with the following example, and couldn't see any difference from their error message

Check (3 : bool).
The term "3" has type "nat"
while it is expected to have type "bool".
Check (3 <: bool).
The term "3" has type "nat"
while it is expected to have type "bool".

My question is that: might be this is the case where the default and VM behaves the same?

Moreover, it would be nice to have an example where the : and <: behaves differently, so people could be more careful of choosing one from the other.

Answer

As far as I know, the default reduction machinery and the VM reduction machinery are designed to enforce the same typing rules.

But they don't behave the same in the sense that, for some computations, the verification time may be of a different order of magnitude.

Here is an example

Require Import Arith.
Time Check (refl_equal 1 : (10 ^ 6 - 9 * 10 ^ 5) / 10 ^ 5 = 1).
eq_refl : (10 ^ 6 - 9 * 10 ^ 5) / 10 ^ 5 = 1
     : (10 ^ 6 - 9 * 10 ^ 5) / 10 ^ 5 = 1
Finished transaction in 4.576 secs (4.554u,0.019s) (successful)
Time Check (refl_equal 1 <: (10 ^ 6 - 9 * 10 ^ 5) / 10 ^ 5 = 1).
eq_refl <: (10 ^ 6 - 9 * 10 ^ 5) / 10 ^ 5 = 1
     : (10 ^ 6 - 9 * 10 ^ 5) / 10 ^ 5 = 1
Finished transaction in 0.433 secs (0.425u,0.008s) (successful)

This matters because large computations can occur in the middle of proofs.