Stream: Elpi users & devs

Topic: coq.typecheck introduces non-HOAS term

view this post on Zulip Quentin VERMANDE (Nov 27 2023 at 16:20):

Hello. Spying on a coq.typecheck prints the following :

----<<---- enter:
coq.typecheck (app [global (const «HB_unnamed_factory_12»), X0^4])
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, c3]]) ok

---->>---- exit:
coq.typecheck (app [global (const «HB_unnamed_factory_12»), c0 c1 c2 c3])
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, c3]]) ok

Later on, I receive the error

   [(Data.Term.Const c2); (Data.Term.Const c3)]))

I assume this is due to the c0 c1 c2 c3 that coq.typecheck replaces X0^4 with. According to the documentation of coq.typecheck, whenever the type argument is provided, the inferred type is unified with it, so I replaced the type argument with a fresh variable and unified the latter with the known type, yielding :

----<<---- enter:
coq.typecheck (app [global (const «HB_unnamed_factory_12»), X1^4]) X2^4 ok

---->>---- exit:
coq.typecheck
 (app [global (const «HB_unnamed_factory_12»), X3 c0 c1 c2 c3])
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, X3 c0 c1 c2 c3]]) ok

----<<---- enter:
coq.unify-leq
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, X3 c0 c1 c2 c3]])
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, c3]]) ok

---->>---- exit:
coq.unify-leq
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, X3 c0 c1 c2 c3]])
 (app
   [global (indt «hasDecEq.axioms_»),
    app
     [global (const «inj_type»), c0,
      app [global (const «Equality.sort»), c1], c2, c3]]) ok

which now has X3 in front of c0 c1 c2 c3. I failed to minimize the error, I do not know what in the context triggers the error. Is there an issue with coq.typecheck, or was that expected?

view this post on Zulip Enrico Tassi (Nov 27 2023 at 16:38):

I believe it is a bug, please keep a way to reproduce it (even if not minimal) so that we can look into it next time we meet.

Last updated: Oct 13 2024 at 01:02 UTC