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