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.
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