@Enrico Tassi

`builtin coq.env.add-const: 2th argument: expected closed_term: got [...]`

How can this happen when we typecheck the term first?

The elaboration should be able to fill the holes, what am I missing?

closed term means no evars and no "free" variables. Are you under a `pi x\ decl x ty => ...`

?

typechecking can be performend under a context, while addition to the environment no.

@Enrico Tassi oops, I missed your answers... I definitely have evars (elpi variables `X34`

or something) that should be unified for typechecking to succeed (and it does succeed), but the evars stay. Should I reexamine (one more time) my belief that these evars are constrained by typechecking or could I be missing something else?

It can also be a bug, maybe Coq's type checker assigns it and my code does not bring the assignment to Elpi (in some very remote case, since we use that all over the place).

If you pass `-debug`

to coqtop then elpi prints much more stuff, including the embeddnig/readback of terms... It's not "super clear" but this is what I would do to start the investigation.

Maybe just write there the result of `std.spy(coq.typecheck ....)`

.

:joy_cat: if I pass `-debug`

to `coqc`

I get a `Error: Anomaly "Uncaught exception Not_found."`

oops. And before it? No print?

Nop

oh yes, lots of stuff are printed...

That I'm not sure how to decipher

I cannot spot the place where typechecking is called

cf https://github.com/math-comp/hierarchy-builder/pull/81

In the current status, the culprits are `X5`

and `X6`

...

running make on that branch reproduces the bug?

Enrico Tassi said:

running make on that branch reproduces the bug?

it should

I've to go now, but I can debug it tomorrow probably

OK

Cyril Cohen said:

In the current status, the culprits are

`X5`

and`X6`

...

In file `readme.v`

, They are supposed to be the type of two mixins that appear in the rest of the term (`c6`

and `c1`

), so the term should not typecheck without filling those...

The complaining `coq.env.add-const`

is line 894 of hb.elpi and the potentially guilty typechecking is line 893

[long explanation ahead, for the records; you can skip to the very last piece of text to see the actual problem]

There was a silly debug print raising errors, I'll push a fix in master. With that solved, here the term received by `add-const`

:

```
lp2term: out=(fun (A : Type) (m : AddComoid_of_Type.axioms_ A)
(s : AddComoid.type)
(_ : @unify Type Type A (AddComoid.sort s) nomsg)
(class : AddComoid.axioms A)
(_ : @unify AddComoid.type AddComoid.type s
(AddComoid.Pack A class) nomsg)
(m0 : AddComoid_of_Type.axioms_ A)
(_ : @unify (?e8@{A:=A; m0:=m; m:=A} m0)
(?e10@{A:=A; m0:=m; m:=A} m0) m0 m nomsg)
(opp : forall _ : A, A)
(addNr : forall x : A,
@eq (AddComoid.sort (A_is_a_AddComoid A m))
(@add (A_is_a_AddComoid A m) (opp x) x)
(@zero (A_is_a_AddComoid A m))) =>
Axioms_ A m opp addNr)
```

And here the link between Elpi and Coq holes. The holes are named `?e8`

and `?e10`

, their number in Coq is `?X16`

and `?X18`

which are mapped to Elpi's `X16`

and `X17`

(FTR in Coq evars can have names, and the ones linked with elpi are called `e`

something).

```
elpi2coq:
?X16 <-> X16
?X18 <-> X17
?X19 <-> X33
?X22 <-> X35
```

Then the Coq evar map (and all its extra contents):

```
EVARS:
?X22==[A m0 m |- Type] (domain of ?X17) {?T0}
?X19==[A m0 m |- Type] (domain of ?X15) {?T}
?X18==[A m0 m |- forall _ : ?T0, Type] (internal placeholder) {?e10}
?X16==[A m0 m |- forall _ : ?T, Type] (internal placeholder) {?e8}
?X23==[A m0 m x |- Type => Type] (codomain of ?X17)
?X20==[A m0 m x |- Type => Type] (codomain of ?X15)
?X17==[A m0 m |- Type => forall _ : ?T0, Type] (internal placeholder)
?X15==[A m0 m |- Type => forall _ : ?T, Type] (internal placeholder)
?X14==[A m class |- Type => AddComoid.type] (internal placeholder)
?X13==[A m class |- Type => Type] (internal placeholder)
?X12==[A m class |- Type => AddComoid.type] (internal placeholder)
?X11==[A m class |- Type => Type] (internal placeholder)
?X10==[A m s |- Type => Type] (internal placeholder)
?X9==[A m s |- Type => Type] (internal placeholder)
?X8==[A m s |- Type => Type] (internal placeholder)
?X7==[A m s |- Type => Type] (internal placeholder)
UNIVERSES: <cut>
ALGEBRAIC UNIVERSES: <cut>
UNDEFINED UNIVERSES: <cut>
WEAK CONSTRAINTS:
```

What is problematic is that Coq's type checker (Coq unification actually did not solve the following constraints):

```
CONSTRAINTS:[] [A m s unif_struct class unif_arbitrary m0] |-
AddComoid_of_Type.axioms_ A <= ?X19@{__:=A; __:=m; __:=A}
[] [A m s unif_struct class unif_arbitrary m0] |-
AddComoid_of_Type.axioms_ A <= ?X22@{__:=A; __:=m; __:=A}
[] [A m s unif_struct class unif_arbitrary m0] |-
AddComoid_of_Type.axioms_ A <= ?X16@{__:=A; __:=m; __:=A} m0
[] [A m s unif_struct class unif_arbitrary m0] |-
AddComoid_of_Type.axioms_ A <= ?X18@{__:=A; __:=m; __:=A} m0
```

It's a bug in Coq-Elpi not to call the "right" API to force their resolution, or fail, since these are not really visible in Elpi and I still have to wrap my mind around unification constraints (too many things are broken if you suspend unification, totally unlike suspending typing). So the "right" way to call Coq's type checker is to force it to solve things. There is a clear API for calling unification and enforce that, for typing it is not there so I need to find the right API to call on the resulting evar map.

Looking and these unification problems, they are suspended because they are not in the pattern fragment. `A`

occurs twice, for example. I've no clue if this is really needed, I guess your code puts too many variables in scope (the original term seems to suggest so). I guess forcing Coq to solve this will result in type checking failure.

I'll come back to this in the afternoon, but the fix in Coq-Elpi is probably not solving the problem you see (but make it more explicit, eg type check failure)

Fun fact, the printing error is also caused by the uncommon `app [X a b c, d]`

(eg `?X16`

has 3 arguments + an extra one which is OK, from a typing perspective, since it is a function. But also not so common, since unification typically assigns to it a \lambda for the extra argument and obtain the more canonical `X' a b c d`

.

With the bugfix I finally see the type checking error:

```
elpi: mk-phant-abbrev: T illtyped :
In environment
A : Type
m0 : AddComoid_of_Type.axioms_ A
m : AddComoid_of_Type.axioms_ _UNBOUND_REL_4
Unable to unify "AddComoid_of_Type.axioms_ _UNBOUND_REL_4" with
"Type".
File "./readme.v", line 21, characters 0-126:
```

Which shows another bug, since the proof context is wrong. I'll dig deeper.

It's a bug in Coq-Elpi, when the Elpi unification variables is "restricted" (some stuff is not in scope) and occurs deep in a term, its context is computed wrongly

It's getting late and I cannot even work around the bug, the new code for phant- abbrevs is hard. My guess is that the current code works if the variables are all in scope (eg X c0 c1 ... cn) while the code for phant leaves some binders out, the one for `unif_struct`

for example, and this triggers a bug I will try to solve next week. I tried to rework the code not to "prune" some variables, but I got lost. @Cyril Cohen if you manager, you may still be able to continue on your new branch. If not, I'll try to fix the code for generating a Coq evar out of a random elpi unif variable with some missing names in scope. I fixed some problems but not all of them.

@Enrico Tassi I resumed working and successfully elaborated the term fully myself. It is a shame since it requires a few more `decl`

directives to micro-manage typechecking here and there but it is ok overall and the overhead is not too awful. However, I encountered another problem of the same nature but for which I cannot do anything... reproducing it by hand in Coq works, while doing in Elpi fails, and this time I believe no workaround is possible :crying_cat: cf https://github.com/math-comp/hierarchy-builder/pull/81/files#diff-c8f066ba20fb2fadcb124dd6596484d5R69-R76 (running `make`

in the branch `new-phant-abbrev`

will take you there)

Are you going to be in the office or joinable via skype this week?

Enrico Tassi said:

Are you going to be in the office or joinable via skype this week?

today until 18:00 and tomorrow until 15:30 (we have a meeting in the morning AFAIR)

Cyril Cohen said:

Enrico Tassi I resumed working and successfully elaborated the term fully myself. It is a shame since it requires a few more

`decl`

directives to micro-manage typechecking here and there but it is ok overall and the overhead is not too awful. However, I encountered another problem of the same nature but for which I cannot do anything... reproducing it by hand in Coq works, while doing in Elpi fails, and this time I believe no workaround is possible :crying_cat: cf https://github.com/math-comp/hierarchy-builder/pull/81/files#diff-c8f066ba20fb2fadcb124dd6596484d5R69-R76 (running`make`

in the branch`new-phant-abbrev`

will take you there)

@Enrico Tassi this was indeed a mistake of mine, and it is fixed!!!!

See https://github.com/math-comp/hierarchy-builder/pull/92 (which requires https://github.com/LPCIC/coq-elpi/pull/160 )

Even if the new code you wrote does not trigger this bug, I looked at it and ended up cleaning up the code a bit and as a byproduct we can now also get rid of the super ugly hack we had to do in order to "refresh" unification variables (it is now an option to coq-elpi's API)

I tried to comment/explain the option, but I believe the doc is not very good. Comments welcome.

Last updated: Mar 02 2024 at 16:01 UTC