Circumvented the measurableTypeR rT problem but stack overflowed

theories/lebesgue_integral.v

@@ -325,14 +325,14 @@ HB.instance Definition _ f g := MeasurableFun.copy (\- f) (- f).
 HB.instance Definition _ f g := MeasurableFun.copy (f \- g) (f - g).
 HB.instance Definition _ f g := MeasurableFun.copy (f \* g) (f * g).
 
-Definition mindic (D : set aT) of measurable D : aT -> rT := \1_D.
+Definition mindic (D : set aT) of measurable D : aT -> measurableTypeR rT := \1_D.
 Lemma mindicE (D : set aT) (mD : measurable D) :
   mindic mD = (fun x => (x \in D)%:R).
 Proof. by rewrite /mindic funeqE => t; rewrite indicE. Qed.
 HB.instance Definition _ (D : set aT) (mD : measurable D) :
-   @FImFun aT rT (mindic mD) := FImFun.on (mindic mD).
+   @FImFun aT (measurableTypeR rT) (mindic mD) := FImFun.on (mindic mD).
 Lemma indic_mfun_subproof (D : set aT) (mD : measurable D) :
-  @isMeasurableFun d _ aT rT (mindic mD).
+  @isMeasurableFun d _ aT (measurableTypeR rT) (mindic mD).
 Proof.
 split=> mA /= B mB; rewrite preimage_indic.
 case: ifPn => B1; case: ifPn => B0 //.
@@ -341,25 +341,25 @@ case: ifPn => B1; case: ifPn => B0 //.
 - by apply: measurableI => //; apply: measurableC.
 - by rewrite setI0.
 Qed.
-HB.instance Definition _ D mD := @indic_mfun_subproof D mD.
+HB.instance Definition _ D mD := @indic_mfun_subproof D mD. (* FIXME: remove measurableTypeR here? *)
 
 Definition indic_mfun (D : set aT) (mD : measurable D) :=
-  [the {mfun aT >-> rT} of mindic mD].
+  [the {mfun aT >-> (measurableTypeR rT)} of mindic mD].
 
 HB.instance Definition _ k f := MeasurableFun.copy (k \o* f) (f * cst_mfun k).
 Definition scale_mfun k f := [the {mfun aT >-> rT} of k \o* f].
 
 Lemma max_mfun_subproof f g : @isMeasurableFun d _ aT rT (f \max g).
 Proof. by split; apply: measurable_maxr. Qed.
 HB.instance Definition _ f g := max_mfun_subproof f g.
-Definition max_mfun f g := [the {mfun aT >-> _} of f \max g].
+Definition max_mfun f g := [the {mfun aT >-> rT} of f \max g].
 
 End ring.
 Arguments indic_mfun {d aT rT} _.
 
 Lemma measurable_indic d (T : measurableType d) (R : realType)
     (D A : set T) : measurable A ->
-  measurable_fun D (\1_A : T -> R).
+  measurable_fun D (\1_A : T -> (measurableTypeR R)).
 Proof.
 by move=> mA; apply/measurable_funTS; rewrite (_ : \1__ = mindic R mA).
 Qed.
@@ -398,12 +398,12 @@ End sfun_pred.
 
 Section sfun.
 Context {d} {aT : measurableType d} {rT : realType}.
-Notation T := {sfun aT >-> rT}.
-Notation sfun := (@sfun _ aT rT).
+Notation T := {sfun aT >-> (measurableTypeR rT)}.
+Notation sfun := (@sfun _ aT (measurableTypeR rT)).
 Section Sub.
-Context (f : aT -> rT) (fP : f \in sfun).
+Context (f : aT -> measurableTypeR rT) (fP : f \in sfun).
 Definition sfun_Sub1_subproof :=
-  @isMeasurableFun.Build d _ aT rT f (set_mem (sub_sfun_mfun fP)).
+  @isMeasurableFun.Build d _ aT (measurableTypeR rT) f (set_mem (sub_sfun_mfun fP)).
 #[local] HB.instance Definition _ := sfun_Sub1_subproof.
 Definition sfun_Sub2_subproof :=
   @FiniteImage.Build aT rT f (set_mem (sub_sfun_fimfun fP)).