finmap Port to `HB.lock`

This PR:

removes the use of phantom types, and
ports the keyed- and module-locking to HB.lock.

Note that unlocking fsfun_of_ffun does not give the same result as before (because it was implemented in a weird way). We need to use fsfun_ffun instead.

Oct 01 '25 16:10 pi8027

FTR, Cyril's feedback on locking was that we should probably switch from keyed locking to module locking (like HB.lock). We can still keep the key by module-locking the definitions that take the key.

Oct 17 '25 12:10 pi8027

The breakage of multinomials should be fixed by math-comp/multinomials#118.

Oct 20 '25 18:10 pi8027

In the end, locking fun_of_fsfun does not seem to fix the issue in multinomials. So, I leave it unlocked here. In any case, this PR reduces some boilerplate code.

Oct 20 '25 21:10 pi8027

T in {fset T} is not interpreted in type_scope anymore. I will fix it. (It would be better if we address math-comp/math-comp#1136 though.)

Oct 21 '25 13:10 pi8027

T in {fset T} is not interpreted in type_scope anymore. I will fix it. (It would be better if we address math-comp/math-comp#1136 though.)

Fixed.

Oct 21 '25 23:10 pi8027