Unclear error message "input has no global reference"

[Tragicus]

As mentioned in the corresponding Zulip thread, the following code fails with the error "term->gref: input has no global reference", which is not very clear. Here, id should be replaced by idfun.

From HB Require Import structures.
From mathcomp Require Import ssrbool ssrfun.
Require Import preliminaries.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Declare Scope rel_scope.

HB.mixin Record hasRel T := { rel_op : rel T }.

#[mathcomp, short(type="relType")]
HB.structure Definition Relation := { T of hasRel T }.

Definition sub_relation (T U : relType) (f : T -> U) :=
  ((injective f) * {mono f : x y / rel_op x y})%type.

HB.mixin Record isSubRel (T U : relType) (f : T -> U) := {
  sub_relation_subproof : sub_relation f;
}.

#[infer(T,U),mathcomp(axiom="sub_relation")]
HB.structure Definition SubRel (T U : relType) :=
  {f of @isSubRel T U f}.

Fail HB.instance Definition _ (T : relType) :=
  (isSubRel.Build T T (id : T -> T) (conj (@inj_id T) (@mono_id T bool rel_op))).