[DO NOT MERGE] Attempt to remove dffun

[pi8027]

Motivation for this change

This PR attempts to merge {dffun fT} and {ffun fT} to close issue #701, but it is unsuccessful due to some limitations of unification. I open this PR to make it easier for others to investigate the issue.

Things done/to do

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries)
• [ ] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and make sure there is a milestone.

[pi8027]

The unification trace obtained by UniCoq (see https://github.com/math-comp/math-comp/issues/701#issuecomment-843729180 for the first attempt with Set Debug "unification"): https://github.com/math-comp/math-comp/blob/7db7a5fbce42ff387a5750f9fbde5436a9aab1cc/mathcomp/algebra/matrix.v#L342-L343

eqType =<= Type (App-FO) ERR
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
?T =<= nat (Meta-Inst) OK
_Set =<= Type (Reduce-Same) OK
(Equality.mixin_of ?sT) =<= (Equality.mixin_of 'M_(m, n)) (App-FO) ERR
_Equality.mixin_of =<= Equality.mixin_of (Rigid-Same) OK
_(sub_sort ?sT) =?= 'M_(m, n) (CS) ERR
__(Equality.sort ?T) =?= \{ffun 'I_?n * 'I_?n0 -> ?T0\} (CS) ERR
___?t =?= (prod_finType (ordinal_finType ?n) (ordinal_finType ?n0)) (Meta-Inst) OK
____finType =<= finType (Reduce-Same) OK
___(fun=> ?T0) =?= (fun x : prod_finType (ordinal_finType ?n) (ordinal_finType ?n0) => Equality.sort (?t x : eqType)) (App-FO) ERR
____(fun=> ?T0) =?= (fun x : prod_finType (ordinal_finType ?n) (ordinal_finType ?n0) => Equality.sort (?t x : eqType)) (Lam-Same) ERR
_____(Finite.sort (prod_finType (ordinal_finType ?n) (ordinal_finType ?n0))) =?= ('I_?n * 'I_?n0)\%type (CS) OK
______(Finite.sort ?t0) =?= 'I_?n (CS) OK
_______?n1 =?= ?n (Meta-Inst) OK
________nat =<= nat (Reduce-Same) OK
_______?t0 =?= (ordinal_finType ?n) (Meta-Inst) OK
________finType =<= finType (Reduce-Same) OK
______(Finite.sort ?t0) =?= 'I_?n0 (CS) OK
_______?n1 =?= ?n0 (Meta-Inst) OK
________nat =<= nat (Reduce-Same) OK
_______?t0 =?= (ordinal_finType ?n0) (Meta-Inst) OK
________finType =<= finType (Reduce-Same) OK
______(prod_finType (ordinal_finType ?n) (ordinal_finType ?n0)) =?= (prod_finType (ordinal_finType ?n) (ordinal_finType ?n0)) (App-FO) OK
_______prod_finType =?= prod_finType (Rigid-Same) OK
_______(ordinal_finType ?n) =?= (ordinal_finType ?n) (App-FO) OK
________ordinal_finType =?= ordinal_finType (Rigid-Same) OK
________?n =?= ?n (Meta-Same-Same) OK
_______(ordinal_finType ?n0) =?= (ordinal_finType ?n0) (App-FO) OK
________ordinal_finType =?= ordinal_finType (Rigid-Same) OK
________?n0 =?= ?n0 (Meta-Same-Same) OK
_____?T0 =?= (Equality.sort (?t x : eqType)) (Meta-Inst) ERR
_____?T0 =?= (Equality.sort (?t x : eqType)) (Meta-Reduce) ERR
______?T0 =?= (let (sort, _) := ?t x in sort) (Meta-Inst) ERR
__(Equality.sort ?T) =?= \{ffun 'I_?n * 'I_?n0 -> ?T0\} (Cons-DeltaL) ERR
_(sub_sort ?sT) =?= 'M_(m, n) (App-FO) ERR
_(sub_sort ?sT) =?= 'M_(m, n) (Cons-DeltaL) ERR
The command has indeed failed with message:
In environment
R : eqType
m : nat
n : nat
The term "SubEqMixin ?sT" has type "Equality.mixin_of ?sT" while it is expected to have type "Equality.mixin_of 'M_(m, n)".

I don't get why ?T0 does not get instantiated with R.