Define SListI in terms of All

[kosmikus]

This is a reminder for myself.

I think it would be nicer to refactor the definitions such that

type SListI = All Top

Currently, All Top implies SListI (via superclass constraint), but not vice versa. I think it'd be nicer if both are equivalent. In many cases, this would make the c and non-c versions of functions coincide.

Consider for example the following two functions as they are currently:

cpure_NP :: All c xs => proxy c -> (forall x . c x => f x) -> NP f xs
pure_NP :: SListI xs => (forall x . f x) -> NP f xs

With the equivalence, we have

pure_NP f = cpure_NP (Proxy :: Proxy Top) f

[kosmikus]

It might make sense to combine this change with the work that is in the wip-static-case branch.

[kosmikus]

This may be a bit tricker than expected, because GHC cannot automatically infer

All c xs => All Top xs

At the moment, SListI xs is a superclass of All c xs. We cannot have All Top xs as a superclass for All c xs because that'd be a true cycle. But the absence of the superclass constraint leads to some things failing to type-check, which is due to the lack of the implication above.

[kosmikus]

I've been looking at this and also the static case work again. In particular for static case, I cannot see a way currently to make it work without using undecidable super classes in such a way that it is incompatible with GHC <8. As there's currently a chance that we'll retain GHC-7 compatibility for the type-level metadata work, I'll move this from 0.3 to 0.4.