[Haskell-cafe] Help with GHC.Generics -- How to get field selector name into value level?

[Compl Yue]

Greetings!

I’m stuck:

```hs
-- | a named (with a selector) field
instance
  (KnownSymbol sel, DbaStorable' f, f ~ K1 R c, DbaField c ft, Typeable c) =>
  DbaStorable' (M1 S ('MetaSel ('Just sel) su ss ds) f)
  where
  --

  _loadDbaField store bsp fno cno vin =
    M1 <$> _loadDbaField store fsp fno cno vin
    where
      fieldName = symbolVal (Proxy @sel)
      fieldPath = fieldName ++ "::" ++ dbaBasePath @c
      fsp = case bsp of
        "" -> fieldPath -- a field of a top level record
        _ -> bsp ++ "/" ++ fieldPath -- a field of a nested record

  _storeDbaField store bsp fno cno m@(M1 xr) =
    _storeDbaField store fsp fno cno xr
    where
      fieldName = selName m
      fieldPath = fieldName ++ "::" ++ dbaBasePath @c
      fsp = case bsp of
        "" -> fieldPath -- a field of a top level record
        _ -> bsp ++ "/" ++ fieldPath -- a field of a nested record

```

With the `selName` approach as in the `_storeDbaField ` above, it’s rejected as:

```log
    • Could not deduce (GHC.Generics.SingI su)
        arising from a use of ‘selName’
      from the context: (KnownSymbol sel, DbaStorable' f, f ~ K1 R c,
                         DbaField c ft, Typeable c)
        bound by the instance declaration
        at src/Frp/DbaStore/Internal.hs:(646,3)-(647,55)
    • In the expression: selName m
      In an equation for ‘fieldName’: fieldName = selName m
      In an equation for ‘_storeDbaField’:
```

But can I really evident `SingI` instance from my side? Which is unexpected from GHC.Generics...

Otherwise with the `symbolVal` approach as in the `_loadDbaField ` above, there’s the complain against the ultimate use site:

```log
    • No instance for (GHC.TypeLits.KnownSymbol sel0)
        arising from a use of ‘storeDba’
    • In a stmt of a 'do' block: storeDba rootDir series'data
      In the expression:
        do forM_ series'data print
           storeDba rootDir series'data
           sd <- loadDba @(Envelope2D Double) rootDir
           forM_ sd print
```

But I failed to prove `KnownSymbol sel` with all methods I can think of.

Help please!

With best regards,
Compl

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20240507/56b46d48/attachment.html>