Hierarchy Builder requires unused structure

[zstone1]

The following code has an error (when "JustPath" is commented out).

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat generic_quotient.
Require Import realfun.
Require Import mathcomp_extra boolp reals ereal set_interval classical_sets.
Require Import signed functions topology normedtype landau sequences derive.
From HB Require Import structures.

Add Search Blacklist "__canonical__".
Add Search Blacklist "__functions_".
Add Search Blacklist "_factory_".
Add Search Blacklist "_mixin_".

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

HB.mixin Record IsPath {R : realType} {T : topologicalType} (f : R -> T) := 
  { dummy_value : nat }.

  (*
HB.structure Definition JustPath {R : realType} {T : topologicalType} 
  := {f of @IsPath R T f}.
  *)

HB.structure Definition Path {R : realType} {T : topologicalType} 
  (B : set T) := {f of @IsPath R T f & @Fun R T `[0,1]%classic B f}.

Notation "{ 'path' R , B }" := (@Path.type R _ B) : form_scope.
Notation "[ 'path' 'of' f ]" := ([the (@Path.type _ _ _) of (f: _ -> _)]) : form_scope.

Section Paths.
Context {R : realType} {T : topologicalType} (B : set T).

Let flip_f (x : subspace `[(0:R),1]) : subspace `[0,1] := `1- x.

Lemma path_rev_funS : @set_fun  _ _ `[0,1]%classic `[0,1]%classic flip_f.
Proof.
rewrite ?set_itvcc => x /= /andP [] xnng xle1; apply/andP. 
split; [exact: onem_ge0| exact: onem_le1].
Qed.

HB.instance Definition _ := 
  @IsFun.Build R R (`[0,1]%classic) (`[0,1]%classic) (flip_f) path_rev_funS.

Section ReversePath.
Variables (f : {path R, B}).

Definition flip_path := [fun of f] \o [fun of flip_f].

Lemma flip_path_funS : @set_fun R T `[0,1]%classic B flip_path.
Proof. by []. Qed.

HB.instance Definition _ := 
  @IsPath.Build R T flip_path 0.

HB.instance Definition _ := 
  @IsFun.Build R T `[0,1]%classic B flip_path flip_path_funS.

Definition reverse_path := [path of flip_path].
End ReversePath.

The definition of reverse_path fails with

In environment
R : realType
T : topologicalType
B : set T
flip_f := [eta onem (R:=R)] : subspace `[(0 : R), 1] -> subspace `[0, 1]
f : { path R, B}
The term
 "(fun s : { path R, ?B} =>
   TheCanonical.Put (flip_path : subspace `[(0 : R), 1] -> T) s s) 
    ?s0" has type "TheCanonical.put flip_path ?s0 ?s0"
while it is expected to have type "TheCanonical.put flip_path flip_path ?s".

However, things work fine with JustPath is defined. What's happening here in HB?

[CohenCyril]

Hi @zstone1 sorry for the delay in reading this... This really looks like a HB problem, to do you try to minimize to an example without using analysis? (Then this minimization could be transferred to an HB issue and dealt with as such)

[zstone1]

This issue is now duplicate of the above ticket in filed in HB repo.