search

math-comp / hierarchy-builder

High level commands to declare a hierarchy based on packed classes
MIT License
95 stars 20 forks source link

HB.mixin anomaly when a parameter with structure is reused as a subject. #431

Open screenl opened 1 month ago

screenl commented 1 month ago

The following code gives The elpi tactic/command HB.mixin failed without giving a specific error message. Please report this inconvenience to the authors of the program.;

HB.mixin Record barycentric_interval_of (I:Interval.type) of Baryspace_of I I :={

}.

The types are defined as follows

HB.mixin Record Interval_of I:= {
  ...
}.
HB.mixin Record Baryspace_of (I : Interval.type) A := {
  ...
}.
CohenCyril commented 1 month ago

Hi @screenl, thanks for reporting. Here is a minimized and complete file, so that we can adress this in the future.

From HB Require Import structures.

HB.mixin Record Interval_of I := {}.
HB.structure Definition Interval := {I of Interval_of I}.
HB.mixin Record Baryspace_of (I : Interval.type) A := {}.
HB.structure Definition Baryspace I := {A of @Baryspace_of I A}.

Fail HB.mixin Record barycentric_interval_of (I : Interval.type) of
  Baryspace_of I I := {}.
(* The error message should be that the head of the subject of
   a structure (here Interval.sort) should probably not be a
   projection from the hierarchy. This will probably cause
   forgetful inheritance problems *)

(* This is the alternative we should strive to suggest, however
   for some reason I failed to diagnose, it fails *)
Fail HB.mixin Record barycentric_interval_of I of
   Interval I & @Baryspace_of I I := {}.

(* This should be also be possible, but fails too *)
Fail HB.structure Definition SelfBaryspace :=
  {I of Interval I & @Baryspace_of I I}.
CohenCyril commented 1 month ago

I think this is related to a case we might have missed in https://github.com/math-comp/hierarchy-builder/pull/295