How to (unsafely) reflect a map as a constraint?

Question

I want a typeclass that represents membership in a reified Data.Map.Map. So something like:

class Reifies s (Map Text v) => IsMember (x :: Symbol) s where
  value :: Proxy s -> Proxy x -> v

And then I would like to implement a function which returns a Dict instance of this class whenever a symbol is present:

checkMember :: forall s x v. (KnownSymbol x, Reifies s (Map Text v))
  => proxy x -> Maybe (Dict (IsMember x s))
checkMember sx =
  let m = reflect (Proxy @s)
  in  (_ :: v -> Dict (IsMember x s)) <$> Map.lookup (symbolVal sx) m

I don't mind using unsafeCoerce to implement checkMember, but even so I'm having trouble figuring out how to do this (fill in the type hole).

---

Approximate preamble:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Constraint(Dict(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Proxy (Proxy(..))
import Data.Reflection (Reifies, reflect)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)

Answer 1

Why does it have to be a class IsMember? How about a simple type:

newtype Member x s v = Member v

checkMember :: ... => proxy x -> Maybe (Member x s v)

Keeping Member abstract allows to preserve the invariant that a value of type Member x s v belongs to the dictionary associated with s. No unsafeCoerce on your part are needed.

From there, there might also be some way to use reflection to lift Member back to the type level but that sounds overengineered.

---

EDIT: from the discussion, it seems the requirement is external and there isn't much to do about it. Here is a way to implement checkMember.

(reflection implements its own machinery like this too.)

We can abuse the fact that GHC desugars classes with a single method and no superclasses class C a where m :: v directly to the unwrapped method m :: v, and constrained values C a => b to functions v -> b.

• we need a version of IsMember without superclasses (IsMember0)
• we wrap IsMember0 x s v => r in a newtype so it can be coerced to IsMember0 x s v -> r (UnsafeMember)

---

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Constraint(Dict(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Proxy (Proxy(..))
import Data.Reflection (Reifies, reflect, reify)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Unsafe.Coerce (unsafeCoerce)

type Text = String

class IsMember0 (x :: Symbol) s v | s -> v where
  value0 :: Proxy s -> Proxy x -> v

class (Reifies s (Map Text v), IsMember0 x s v) => IsMember (x :: Symbol) s v | s -> v
instance (Reifies s (Map Text v), IsMember0 x s v) => IsMember (x :: Symbol) s v

value :: IsMember x s v => Proxy s -> Proxy x -> v
value = value0

newtype UnsafeMember x s v = UnsafeMember (IsMember0 x s v => Dict (IsMember x s v))

unsafeMember :: forall x s v. Reifies s (Map Text v) => v -> Dict (IsMember x s v)
unsafeMember v = unsafeCoerce (UnsafeMember @x @s @v Dict) (\ _ _ -> v)

checkMember :: forall s x v proxys proxyx. (KnownSymbol x, Reifies s (Map Text v))
  => proxys s -> proxyx x -> Maybe (Dict (IsMember x s v))
checkMember _ sx =
  let m = reflect (Proxy @s)
  in  unsafeMember <$> Map.lookup (symbolVal sx) m

-- Executable example
main :: IO ()
main = do
  let d = Map.fromList [("foo", 33 :: Int)]
      foo = Proxy :: Proxy "foo"
  reify d (\p ->
    case checkMember p foo of
      Nothing -> fail "Not found"
      Just Dict -> print (value0 p foo))