Unwrapping an existentially quantified GADT

Question

I have a custom value type Value labeled by its type ValType:

data ValType
  = Text
  | Bool

data Value (tag :: ValType) where
  T :: Text -> Value 'Text
  B :: Bool -> Value 'Bool

and I would like to define a function that unwraps an existentially quantified Value, that is it should have the following type signature:

data SomeValue = forall tag. SomeValue (Value tag)

unwrap :: SomeValue -> Maybe (Value tag)

I can define unwrap for 'Bool and 'Text separately, but how do I define a polymorphic unwrap?

Answer 1

You really can't avoid a typeclass or equivalent here. unwrap, as you've written its type, has no way to know which tag it's looking for, because types are erased. An idiomatic approach uses the singleton pattern.

data SValType v where
  SText :: SValType 'Text
  SBool :: SValType 'Bool

class KnownValType (v :: ValType) where
  knownValType :: SValType v
instance KnownValType 'Text where
  knownValType = SText
instance KnownValType 'Bool where
  knownValType = SBool

unwrap :: forall tag. KnownValType tag => SomeValue -> Maybe (Value tag)
unwrap (SomeValue v) = case knownValType @tag of
  SText
    | T _ <- v -> Just v
    | otherwise -> Nothing
  SBool
    | B _ <- v -> Just v
    | otherwise -> Nothing

Unlike the IsType class of your own answer, KnownValType lets you get type information as well as a value tag out of a pattern match. So you can use it much more generally for handling these types.

For cases where your typeOf is sufficient, we can write it with no trouble:

 typeOf :: KnownValType a => Proxy a -> ValType
 typeOf (_ :: Proxy a) = case knownValType @a of
   SBool -> Bool
   SText -> Text