Good evening. I am slowly learning Coq-Elpi and experimenting with it. Somehow it looks like the Coq typechecker does not behave the same way in Coq-Elpi and in Coq.

Let me show an example with the MathComp `int`

type and ring notations.

```
Variable x : int.
Check (2%:Z + x * 3)%R.
```

This gives `int_Zmodtype`

in Coq whereas `coq.typecheck`

under an `Elpi Query`

gives a type error because it thinks `3`

is of type `nat`

.

```
Elpi Query lp:{{ T = {{ (2%:Z + x * 3)%R }}, coq.typecheck T Ty Diag. }}.
```

```
Illegal application:
The term "GRing.mul" of type "forall R : ringType, R -> R -> R"
cannot be applied to the terms
"int_Ring" : "ringType"
"x" : "int"
"3" : "nat"
The 3rd term has type "nat" which should be coercible to
"GRing.Ring.sort int_Ring".
```

Is there an external reason for that, like Elpi not having access to some notations / coercions / structure instances? As I am far from being an expert on these topics, I cannot manage to find the origin of the error. Do you have an idea? Thanks in advance!

Long story short: Coq has many typecheckers ;-)

The one behind `Check`

is available via the `elaborate-skeleton`

API https://github.com/LPCIC/coq-elpi/blob/master/coq-builtin.elpi#L878 .

The one you are calling is used internally in Coq in many places, but I don't think there is a command like `Check`

for it. It cannot insert coercions (compare the the types of the two APIs, one cannot return an update term, but only assign its metavariables).

If you look for `skeleton`

around in the file, you may find a few more APIs and comments on this "data".

The idea of "skeletons" is that the API does not modify that term, but rather use it as a skeleton to produce a new term which is somewhat related, but may contain more nodes (eg coercions).

Last updated: Jun 06 2023 at 23:01 UTC