Picking up instances where the key is a variable

[MevenBertrand]

This one is from a discussion with @CohenCyril, I'm a bit out of my waters so he might be able to better explain what's going wrong. The issue appears here, with the need of a notation/definition to force inference to re-infer the right structure for a term. Afaiu, the problem comes from the fact that the carrier for which I want to infer the structure is not a constant, but some set A where set is a variable (and the argument goes that as long as set has a given structure, then set A is a poset). I'll let Cyril minimize it and/or explain it better, he seemed quite keen :)

[CohenCyril]

Partly minimized below, except for the NFI warning that does show up in my minimal example and does not in yours...

From HB Require Import structures.

HB.mixin Record isA (F : unit -> Type) := {}.
HB.structure Definition a := {F & isA F}.
HB.mixin Record isB (T : Type) := {}.
HB.structure Definition b := {T & isB T}.

(* Note: this does trigger a NFI warning! *)
HB.instance Definition ab (F : a.type) : isB (F tt) := isB.Build (F tt).

Module test.
Axioms (F : unit -> Type) (aF : isA F).
HB.instance Definition _ := aF.
Check F : a.type.
Fail Check F tt : b.type.
Check (F : a.type) tt : b.type.
End test.