on finfun_eqMixin aT (rT : eqType) :=
  Eval hnf in [eqMixin of @finfun_type aT rT by <:].
Canonical finfun_eqType aT (rT : eqType) :=
  Eval hnf in EqType (finfun_type aT rT) (finfun_eqMixin aT rT).

(* These are intermediate structure we don't know yet *)
Definition finfun_choiceMixin aT (rT : choiceType) :=
  [choiceMixin of finfun_type aT rT by <:].
Canonical finfun_choiceType aT rT :=
  Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT).
Canonical finfun_of_choiceType (aT : finType) (rT : choiceType) 