5

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.

Sridhar Ratnakumar
  • 81,433
  • 63
  • 146
  • 187
matchwood
  • 257
  • 1
  • 7

1 Answers1

5

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
HTNW
  • 27,182
  • 1
  • 32
  • 60
  • Excellent, I was wondering if something like this might work. One question though - how can you tell that in my example `xs` is not in WHNF? In functions of the type `bar :: (All TestClass xs) => NP f xs -> (forall a. Typeable a => f a -> [z]) -> [z] bar np f = cfoldMap_NP (Proxy :: Proxy TestClass) f np` The constraint is solved succesfully, even though no more information seems to be provided to the compiler than in my failing case. – matchwood Jun 09 '18 at 23:08
  • @matchwood I said it couldn't *reduce*. The constraint is still *there*, but without knowing `xs` you can't break it down to its constituent constraints. Many functions are OK with this, and will simply take the whole constraint and break it down within themselves, but your case isn't one of those. – HTNW Jun 09 '18 at 23:42
  • I understand that it can't reduce, but I'd like to understand why it can in some cases but not in others. I think I get it though - the reduction is forced by anything that uses the individual types in the type level list, which makes sense - there has to be some explicit point where the compiler has reached a requirement of a simple "Class a" constraint, which it can then match against a provided superclass constraint. – matchwood Jun 10 '18 at 08:35
  • Type families reduce when an equation matches. `All` needs the list to be either `[]` or `(x:xs)` before an equation matches. In neither case of `bar` do you know what `xs` is, so in neither case the constraint can reduce. Reduction has nothing to do with *use*. It has to do with how much you know about the arguments. – HTNW Jun 10 '18 at 11:18
  • 1
    Ah, I think I have it now. If I understand you correctly then the only place the reduction can take place is in places like https://github.com/well-typed/generics-sop/blob/master/src/Generics/SOP/NP.hs#L523 - where the actual traversal through NP takes place. Everywhere else, things only work because functions have been defined in terms of constraints. So in my `bar` in the comments, the compiler does not know that the Typeable function can be used because of the All constraint, it just knows that it needs some function that can fulfill the TestClass constraint in the cfoldMap_NP function. – matchwood Jun 10 '18 at 13:09
  • And any function solely constrained by a superclass of a class can be safely 'lifted', as it were, into a function constrained by the class. – matchwood Jun 10 '18 at 13:10