Super classes with All from generics-sop

Question

I'm trying to use All from generics-sop to constrain a list of types. Everything works as expected with simple classes like All Typeable xs, but I'd like to be able to do something like the following:

class (Typeable a) => TestClass (a :: k)
instance (Typeable a) => TestClass a

foo :: (All Typeable xs) => NP f xs -> z
foo = undefined

bar :: (All TestClass xs) => NP f xs -> z
bar = foo 

This gives the error

Could not deduce: Generics.SOP.Constraint.AllF Typeable xs
  arising from a use of ‘foo’
  from the context: All TestClass xs

The generics-sop documentation states that

"All Eq '[ Int, Bool, Char ] is equivalent to the constraint (Eq Int, Eq Bool, Eq Char)

But in this case it doesn't seem to be, since

foo2 :: (Typeable a, Typeable b) => NP f '[a,b] -> z
foo2 = undefined

bar2 :: (TestClass a, TestClass b) => NP f '[a,b] -> z
bar2 = foo2

compiles fine.

My questions

1) Is this the expected behaviour? 2) If so, is there any workaround?

My use case for this is that I want to pass around a type level list of types constrained by a bunch of different classes under a single class name (like class (Typeable a, Eq a, Show a) => MyClass a) but also be able to call less specialised functions that only require some subset of those classes.

Searching for answers turned up superclasses aren't considered, but I don't think that is the issue here - I think it is something to do with the way the All constraint is put together in generics-sop. It is as if the compiler is simply comparing the two All constraints, rather than expanding them both and then type checking.

Answer 1

All f xs is actually equivalent to (AllF f xs, SListI xs). AllF is a type family:

type family AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
  AllF _ '[] = ()
  AllF c (x:xs) = (c x, All c xs)

You see that it cannot reduce unless xs is in WHNF, so it gets stuck in your case. You can use mapAll:

import Generics.SOP.Dict

mapAll :: forall c d xs.
          (forall a. Dict c a -> Dict d a) ->
          Dict (All c) xs -> Dict (All d) xs
-- ::ish forall f g xs. (forall a. f a -> g a) -> All f xs -> All g xs

-- stores a constraint in a manipulatable way
data Dict (f :: k -> Constraint) (a :: k) where
     Dict :: f a => Dict f a

bar :: forall xs f z. (All TestClass xs) => NP f xs -> z
bar = case mapAll @TestClass @Typeable @xs (\Dict -> Dict) Dict of
           Dict -> foo

-- TestClass a -> Typeable a pretty trivially:
--   match Dict to reveal TestClass a
--   put the Typeable part of the TestClass instance into another Dict
-- We already know All TestClass xs; place that into a Dict
-- mapAll magic makes a Dict (All Typeable) xs
-- match on it to reveal
-- foo's constraint is satisfied