Stream: Hierarchy Builder devs & users

Topic: Non-forgetful inheritance and modules

view this post on Zulip Arthur Azevedo de Amorim (Oct 19 2023 at 18:58):

Consider the following example:

From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Module Type FOO.

Parameter T : eqType.

End FOO.

Module Export Foo : FOO.

Definition T : eqType := HB.pack unit (Equality.on unit).

End Foo.

HB.instance Definition _ := Equality.on T.

When I define the instance, HB complains that it detected a non-forgetful inheritance. This example has been simplified; in the situation I am actually facing, T would belong to a more complicated class C with several superclasses, the rest of the module posits properties related to that more complicated class C, and the instance defined outside of the module would be of a subclass of C.

Is there any clean way of handling a situation like this? I don't want to list every mixin definition inside of the module signature, because there are several dependencies between mixins. And I would prefer not to expose the definition of the type T either.

Last updated: Apr 21 2024 at 01:02 UTC