Stream: Hierarchy Builder devs & users

Topic: expected closed_term error after typechecking


view this post on Zulip Cyril Cohen (Jul 06 2020 at 15:06):

@Enrico Tassi

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

How can this happen when we typecheck the term first?

view this post on Zulip Cyril Cohen (Jul 06 2020 at 15:07):

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

view this post on Zulip Enrico Tassi (Jul 06 2020 at 17:56):

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

view this post on Zulip Enrico Tassi (Jul 06 2020 at 17:56):

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

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:44):

@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?

view this post on Zulip Enrico Tassi (Jul 09 2020 at 17:46):

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

view this post on Zulip Enrico Tassi (Jul 09 2020 at 17:48):

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.

view this post on Zulip Enrico Tassi (Jul 09 2020 at 17:51):

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

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:51):

:joy_cat: if I pass -debug to coqc I get a Error: Anomaly "Uncaught exception Not_found."

view this post on Zulip Enrico Tassi (Jul 09 2020 at 17:52):

oops. And before it? No print?

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:55):

Nop

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:56):

oh yes, lots of stuff are printed...

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:56):

That I'm not sure how to decipher

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:56):

I cannot spot the place where typechecking is called

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:56):

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

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:58):

In the current status, the culprits are X5 and X6...

view this post on Zulip Enrico Tassi (Jul 09 2020 at 17:58):

running make on that branch reproduces the bug?

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:58):

Enrico Tassi said:

running make on that branch reproduces the bug?

it should

view this post on Zulip Enrico Tassi (Jul 09 2020 at 17:58):

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

view this post on Zulip Cyril Cohen (Jul 09 2020 at 17:59):

OK

view this post on Zulip Cyril Cohen (Jul 09 2020 at 18:00):

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

view this post on Zulip Cyril Cohen (Jul 09 2020 at 18:06):

The complaining coq.env.add-const is line 894 of hb.elpi and the potentially guilty typechecking is line 893

view this post on Zulip Enrico Tassi (Jul 10 2020 at 08:13):

[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)

view this post on Zulip Enrico Tassi (Jul 10 2020 at 08:23):

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.

view this post on Zulip Enrico Tassi (Jul 10 2020 at 11:33):

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.

view this post on Zulip Enrico Tassi (Jul 10 2020 at 12:24):

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

view this post on Zulip Enrico Tassi (Jul 10 2020 at 14:25):

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.

view this post on Zulip Cyril Cohen (Jul 15 2020 at 12:36):

@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)

view this post on Zulip Enrico Tassi (Jul 15 2020 at 12:37):

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

view this post on Zulip Cyril Cohen (Jul 15 2020 at 12:38):

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)

view this post on Zulip Cyril Cohen (Jul 15 2020 at 20:20):

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!!!!

view this post on Zulip Enrico Tassi (Jul 20 2020 at 13:54):

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

view this post on Zulip Enrico Tassi (Jul 20 2020 at 13:56):

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)

view this post on Zulip Enrico Tassi (Jul 20 2020 at 13:57):

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


Last updated: Jan 29 2023 at 16:02 UTC