Skip to content

Let tagToEnum# work with GADTs

Motivation

It seems that GHC doesn't consider GADTs enumeration types when checking tagToEnum#. This seems unfortunate.

reflex uses an IntMap to represent a map keyed by an enumeration-like GADT. When dealing with folds and such, we want something like this:

data Tag a where
  T1 :: Tag X
  T2 :: Tag Y
  ...

-- An existentially quantified key-value pair
data KV v = forall a. KV !(Tag a) (v a)

-- A "fake" version of KV with the Tag
-- represented by an Int and the existential
-- stripped
data FakeKV v = FakeKV !Int (v Any)

-- Prepare to install a key and value in a map
toFake :: Tag a -> v a -> FakeKV a
toFake k v = FakeKV (I# (dataToTag# k)) (unsafeCoerce v)

-- Assuming the key and value were pulled out of a well-formed
-- map, build a valid key-value pair
unsafeToKV :: Int -> v Any -> KV v
unsafeToKV (I# ki) va = KV (tagToEnum# ki :: Tag Any) va

Unfortunately, the tagToEnum# call is rejected.

Proposal

Allow tagToEnum# to work for enumeration-like GADTS. That is, GADTs whose constructors have neither fields nor class constraints, but may have (unboxed) equality or (when we get them) coercion constraints. Obviously, this can break type safety, but that's par for the course in GHC.Exts.

Edited by David Feuer
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information