Hi, I would like to have a KnownWord constraint to implement a type-safe efficient sum type. For now [1] I have: data V (vs :: [Type]) = Variant !Word Any where Word is a tag used as an index in the vs list and Any a value (unsafeCoerced to the appropriate type). Instead I would like to have something like: data V (vs :: [Type]) = Variant (forall w. KnownWord w => Proxy w -> Index w vs) Currently if I use KnownNat (instead of the proposed KnownWord), the code isn't very good because Natural equality is implemented using `naturalEq` which isn't inlined and we end up with sequences of comparisons instead of single case-expressions with unboxed literal alternatives. I could probably implement KnownWord and the required stuff (axioms and whatnot), but then someone will want KnownInt and so on. So would it instead make sense to generalise the different "Known*" we currently have with: class KnownValue t (v :: t) where valueSing :: SValue t v newtype SValue t (v :: t) = SValue t litVal :: KnownValue t v => proxy v -> t type KnownNat = KnownValue Natural type KnownChar = KnownValue Char type KnownSymbol = KnownValue String type KnownWord = KnownValue Word Thoughts? Sylvain [1] https://hackage.haskell.org/package/haskus-utils-variant-3.1/docs/Haskus-Uti...