near notation inference issues

[zstone1]

I'm encountering some issues with certain applications of the near tactics. One set of issues is getting instances of \near F, ... to typecheck. The example that I encountered was

Lemma uniform_limit_continuous {U : topologicalType} {V : uniformType}
    (F : set (set (U -> V))) (f : U -> V) :
  ProperFilter F -> (\near F, continuous F) ->
                              ^^^^^^^^^^^^^^
  { uniform, F --> f } -> continuous f.

Gives the error

The term "inPhantom (forall F0 : U -> ?fX0@{F0:=F}, continuous F0)" has type
 "phantom Prop (forall F0 : U -> ?fX0@{F0:=F}, continuous F0)"
while it is expected to have type "phantom Prop (forall x : U -> V, ?P x)"
(cannot satisfy constraint
"let (sort, _) := ?fX in sort" == "Topological.sort U").

It seems unable to determine the topology for continuous despite a canonical structure on U -> V. Even giving that structure explicitly doesn't help.

Lemma uniform_limit_continuous {U : topologicalType} {V : uniformType}
    (F : set (set (fct_topologicalType U V))) (f : U -> V) :
  ProperFilter F -> (\near F, continuous F) ->
                             ^^^^^^^^^^^^^^
  { uniform, F --> f } -> continuous f.

gives an equally unhelpful error

The term "inPhantom (forall F0 : U -> ?fX0@{F0:=F}, continuous F0)" has type
 "phantom Prop (forall F0 : U -> ?fX0@{F0:=F}, continuous F0)"
while it is expected to have type
 "phantom Prop (forall x : fct_topologicalType U V, ?P x)" (cannot satisfy
constraint "let (sort, _) := ?fX in sort" == "Choice.sort U").