So suppose I have a simple data type:
data Thing { thing_id :: ThingId , thing_stuff :: Stuff } newtype ThingId = ThingId String
Stuff is a Monoid, and Things need to be combined as well, so:
instance Monoid Thing where mappend (Thing id1 stuff1) (Thing id2 stuff2) | id1 /= id2 = error "..." | otherwise = Thing id1 (stuff1 `mappend` stuff2) mempty = Thing $ (ThingId "dummy value?") mempty
So clearly both the error and the "dummy value?" are not very nice (and mappend would need a special hack to treat the dummy as compatible with everything). I'd like to be able to lift that ID up to the type level, and then I don't have to worry about incompatible IDs and the mempty can figure out the ID from the type. Now if ThingId were a natural, I gather there's a new GHC feature for type level naturals that can do this kind of thing. Of course any string could be encoded into a large natural, but the resulting type errors would be less than readable. There is probably also a way to encode type level strings in the same way as the traditional way for type level naturals, e.g. 'data A; ... data Z;' and then a type encoding for lists. But I'm guessing that would also lead to excessive compilation times and crazy type errors. In any case, I don't think this can work even if I used naturals instead of ints, because it seems to me I can't write a function '(NatI n) => ThingId -> Thing n' without a statically knowable constant value for 'n'. Otherwise, the value has magically disappeared into the type system and I can't expect to get it back after types are erased. So I need a runtime value for the ThingId, but it still seems like it should be possible to do something better than the 'error' and "dummy value?". Maybe there's a completely different way to ensure that incompatible Things can't be mappended. Any ideas?