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