HB fails to infer and to warn properly about missing type information

[CohenCyril]

From HB Require Import structures.

HB.mixin Record hasPoint T := { point : T }.
HB.structure Definition Pointed := { T of hasPoint T }.
Definition image_type {T} {iT} (f : T -> iT) := iT.
Fail HB.instance Definition _ (pT : Pointed.type) iT f :=
   hasPoint.Build (image_type f) (f point).

fails with error message

Unification problem outside the pattern fragment. ((Data.Term.AppUVar ([...])))

instead of either inferring f or saying it should be explicitly annotated.

[gares]

is [...] containing "point"?

[CohenCyril]

What's the point?

Answer: no

Error:
Unification problem outside the pattern fragment. ((Data.Term.AppUVar (
   { Data.Term.contents = please extend this printer; uid_private = -2801 },
   0,
   [(Data.Term.UVar (
       { Data.Term.contents = please extend this printer; uid_private = 2838
         },
       0, 0))
     ]
   )) == (Data.Term.App (sort, (Data.Term.App (typ, (Data.Term.Arg (0, 0)), [])), []))) Pass -delay-problems-outside-pattern-fragment (elpi command line utility) or set delay_outside_fragment to true (Elpi_API) in order to delay (deprecated, for Teyjus compatibility).

[CohenCyril]

is [...] containing "point"?

If the inference worked it would rely both on image_type and point though... (for a complete inference), and neither occur in the error message. How is it relevant?