HB tries to redeclare existing mixin

[Tragicus]

As reported by @mkerjean on Zulip, we have an issue when some key has an instance for some mixin which is valid for any value of some parameter and we try to use a factory that builds this mixin. HB finds that the mixin is already instantiated and tries to reinstantiate the same mixin (whith the canonical value that is already declared). However, since the instance is valid for any value of the parameter, this produces an evar which makes the declaration fail, see below.

From HB Require Import structures.

HB.mixin Record isA (p n : nat) := {}.

HB.structure Definition A (p : nat) := {n of isA p n}.

HB.factory Record isB (p n : nat) := {}.

HB.builders Context p n of isB p n.
HB.instance Definition _ := isA.Build p n.
HB.end.

HB.instance Definition _ (p : nat) := isA.Build p 0.
HB.instance Definition _ (p : nat) := isB.Build p 0.

[CohenCyril]

So this error occurs solely when trying to reinstantiate an already instantiated mixin?

[Tragicus]

Yes, if you remove the last but one line, it works. We also only observe a failure when there is a parameter involved, which is not instantiated by the instance.