Closed mniip closed 3 years ago
Could you elaborate why that is a problem?
Suppose I wanted to do some check on every key in the map, e.g. I was writing
isSubset :: (forall a. Typeable a => Eq (f a)) => TypeRepMap f -> TypeRepMap f -> Bool
isSubset s1 s2 = all
(\(SomeTypeRep (rep :: TypeRep a)) ->
withTypeable rep $ lookup @a s1 == lookup @a s2)
$ keys s1
This is invalid because a :: k'
where k'
is a rigid type variable introduced by pattern matching on SomeTypeRep
, and it may or may not equal the k
that appears in s1 :: TypeRepMap @k f
Yes, I see. So you’d like keys
to return something like this instead of SomeTypeRep
:
data TypeRepOfKind k where
TypeRepOfKind :: forall k (a :: k). !(TypeRep a) -> TypeRepOfKind k
And its type would be:
keys :: TypeRepMap (f :: k -> Type) -> [TypeRepOfKind k]
Is that right?
This solves the problem yes. However I'm not super sure if that's the best solution (I don't have a different one in mind). The problem is that SomeTypeRep
is defined in base with a number of utils to work with it, and TypeRepOfKind
is not.
I suppose we could let the user define their own wrapper. Something like this:
keysWith :: forall k r. (forall (a :: k). TypeRep a -> r) -> TypeRepMap (f :: k -> Type) -> [r]
Then the existing keys
is a special case:
keys = keysWith SomeTypeRep
And you could define your own for the use case you have:
keysWithKind = keysWith TypeRepOfKind
If you're going to do this, I'd also appreciate a fold
function of a similar signature (including the values).
Would you be interested in writing a patch for this?
Consider the type of
keys
:this looks fine until you consider the kinds:
the value of
k
is erased! We can try to get it back by patching onSomeTypeRep
and gettingrep :: TypeRep (a' :: k')
andtypeRepKind rep:: TypeRep k'
, then we could try totestEquality
, but that requires an extra Typeable constraint on the k, which isn't actually anywhere to be found if say the map is empty.