Feature request: adding target to HB.instance

[CohenCyril]

If we add a directive to HB.instance in order to specify exacly which structures (and super-structures) are meant to be instanciated, we gain in stability, and error messages become more accurate (e.g. when one wants to instanciate a structure and nothing happens, they get an error message). The only problem, @Tragicus mentionned, is the case of mixins which are not enough to instanciate a full structure: we should come up with a way to deal with that.

[CohenCyril]

@Tragicus do you have examples in mind for such mixins?

[Tragicus]

Not off the top of my head, but there is a trivial solution, which is giving an empty list of structures to the directive.

[gares]

Like this?

#[ensures(eqType,foobarType)]
HB.instance Definition _ : fooMixin subject := ...

[CohenCyril]

• ensures(A) means A and super-structures have been instantiated, but maybe more, errors if A is not instantiated
• exactly(A) means A and super-structures have been instantiated, but nothing more, errors if A is not instantiated.