Description of the problem
When an inductive type has one constructor and one computational field, extraction classifies it as Singleton. Declaring that sole field with Extraction Implicit removes the field from the constructor signature, but Singleton lowering still assumes that exactly one argument remains.
Extracting the constructor application raises:
Error: Anomaly "Uncaught exception Failure(\"hd\")."
Called from Extraction_plugin__Extraction.extract_cons_app.head
A match that ignores the field reaches the same inconsistent representation and instead fails the assertion that the Singleton branch has exactly one retained binder.
I would expect no anomaly. If the implicit field is absent from the final code, the type can use the ordinary zero-argument constructor representation. If the extracted computation still depends on that field, the existing Extraction SafeImplicits check should report An implicit occurs after extraction.
The Singleton classification currently filters logical fields but does not filter constructor arguments declared through Extraction Implicit, whereas the later constructor-signature construction does filter them. I am preparing a fix for this classification mismatch together with regression tests for constructor applications and matches.
The same failure occurs with an ordinary one-constructor inductive instead of a record, so record projections are not required to trigger it.
Small Rocq / Coq file to reproduce the bug
From Corelib Require Extraction.
Record box : Type := make_box {
value : nat
}.
Extraction Implicit make_box [1].
Definition entry : nat := value (make_box 1).
Extraction TestCompile entry.Version of Rocq / Coq where this bug occurs
Rocq 9.1.1 with OCaml 4.14.2; master 6df5ae3 (9.4+alpha)
Interface of Rocq / Coq where this bug occurs
rocq compile via Extraction TestCompile
Last version of Rocq / Coq where the bug did not occur
Unknown
Description of the problem
When an inductive type has one constructor and one computational field, extraction classifies it as
Singleton. Declaring that sole field withExtraction Implicitremoves the field from the constructor signature, but Singleton lowering still assumes that exactly one argument remains.Extracting the constructor application raises:
A match that ignores the field reaches the same inconsistent representation and instead fails the assertion that the Singleton branch has exactly one retained binder.
I would expect no anomaly. If the implicit field is absent from the final code, the type can use the ordinary zero-argument constructor representation. If the extracted computation still depends on that field, the existing
Extraction SafeImplicitscheck should reportAn implicit occurs after extraction.The Singleton classification currently filters logical fields but does not filter constructor arguments declared through
Extraction Implicit, whereas the later constructor-signature construction does filter them. I am preparing a fix for this classification mismatch together with regression tests for constructor applications and matches.The same failure occurs with an ordinary one-constructor inductive instead of a record, so record projections are not required to trigger it.
Small Rocq / Coq file to reproduce the bug
Version of Rocq / Coq where this bug occurs
Rocq 9.1.1 with OCaml 4.14.2; master 6df5ae3 (9.4+alpha)
Interface of Rocq / Coq where this bug occurs
rocq compile via Extraction TestCompile
Last version of Rocq / Coq where the bug did not occur
Unknown