`keys` and kind erasure

[mniip]

Consider the type of keys:

keys :: TypeRepMap f -> [SomeTypeRep]

this looks fine until you consider the kinds:

keys :: forall k (f :: k -> Type). TypeRepMap f -> [SomeTypeRep]

the value of k is erased! We can try to get it back by patching on SomeTypeRep and getting rep :: TypeRep (a' :: k') and typeRepKind rep:: TypeRep k', then we could try to testEquality, but that requires an extra Typeable constraint on the k, which isn't actually anywhere to be found if say the map is empty.

[int-index]

Could you elaborate why that is a problem?

[mniip]

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

[int-index]

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?

[mniip]

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.

[int-index]

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

[mniip]

If you're going to do this, I'd also appreciate a fold function of a similar signature (including the values).

[int-index]

Would you be interested in writing a patch for this?