Lenses for `Representable`/`FRepresentable`?

[endgame]

From reddit, discussing FRepresentable, but this could exist for Representable also. My motivating thought was when you have a higher-kinded record with its fields indexed by a GADT, you can define a lens at an index for any FRepresentable, provided you can compare the indices:

data Rec f = Rec { f1 :: f Int, f2 :: f Char }

data RecField a where
  F1 :: RecField Int
  F2 :: RecField Char

frlens :: forall f g a . (GEq (FLog f), FRepresentable f) => FLog f a -> Lens' (f g) (g a)
frlens i f fg = rebuild <$> f (findex fg i)
  where
    rebuild :: g a -> f g
    rebuild ga = ftabulate $ \i' -> case geq i i' of
      Nothing -> findex fg i'
      Just Refl -> ga

-- And similarly, @rlens@ into the index of a 'Represesentable'?

It could be nice to provide this to all users, but @ekmett then says:

The main concern is that for the canonical form of this, actual functions, `flens` is actually grossly inefficient. =/

It isn't an unreasonable ask to add something like it to the class, but the GEq constraint on the logarithm is somewhat at odds to what representability is, and such members you can only use with a little bit of an extra constraint usually come with their own dilemmas for users.

The dilemma a user of the class would then have is do they incur the extra constraints they'd need on their particular 'f' to make GEq hold for (FLog f) so they can have an efficient flens or should they not, keeping in mind that that constraint blocks the existence of the entire FRepresentable instance which might otherwise be available to them with fewer constraints, and accept the default GEq-dependent one?

What to do?

• If we provide rlens/frlensas a standalone function, we're forced to demand Eq/GEq because we don't know any structure about Log f/FLog f, plus the lenses get defined on slow instances where you probably don't want them.
• If we declare the lenses as class methods, instances can exploit structure (e.g., frlens can be a record update instead of a rebuild-via-tabulate) and we can avoid demanding GEq instances, but instances where the lens is gonna be slow still have to define them. This may also make automatic derivation more difficult?
• If we put "has lens at index" on a subclass, we increase boilerplate, but solve the other two problems.