Match on `CoRec ElField`

I have a co-record with named fields CoRec ElField xs. I also have an encoder type newtype Encoder a = Encoder (a -> Encoded).

I'd like to match this with a record containing encoders for each named field Rec (WrappedField Encoder) xs. WrappedField is a variation on ElField I wrote because it's not possible to write the composition ElField .: Encoder:

data WrappedField f (field :: (Symbol, Type)) where
  WrappedField :: KnownSymbol s => f a -> WrappedField f '( s, a)

I'm stuck in trying to get match to run the co-record against the encoders in the record, because match takes a CoRec Identity xs.

I tried massaging my record and co-record types to ones that match will accept. This basically comes down to dropping their fields, but this changes the kind of xs from [(Symbol, Type)] to [*]:

type family Values (xs :: [(Symbol, Type)]) where
  Values '[] = '[]
  Values ('( s, x) ': xs) = x ': Values xs

mkHandlers :: Rec (WrappedField Coder) xs -> Handlers (Values xs) Encoded
mkHandlers = undefined

dropLabels :: CoRec ElField xs -> CoRec Identity (Values xs)
dropLabels = undefined

So far this type checks, but I can't figure out how to write implementations mkHandlers and dropLabels. Take this naive implementation of dropLabels:

dropLabels :: CoRec ElField xs -> CoRec Identity (Values xs)
dropLabels = CoRec . foldCoRec (\(Field x) -> Identity x)

This fails to compile because I don't know the type of the variant of the sum type I'm constructing.

I don't know a ton about compiler proofs, but think this is maybe a place where one is warranted? I was hoping I might get some feedback on this approach before committing to that rabbit hole. Can this approach even work and/or am I making things unnecessarily hard for myself by going this way? Would super appreciate any help!

VinylRecords / Vinyl

Match on `CoRec ElField` #125