Allow `cpara_SList` to put constraint on the `ys` as well

[SeungheonOh]

Currently,

cpara_SList :: All c xs => proxy c -> r ('[] :: [k]) -> (forall (y :: k) (ys :: [k]). (c y, All c ys) => r ys -> r (y ': ys)) -> r xs

allows to put constraint on the "current" element(y) in the type list. I found myself (re)writing cpara_SList that allows to put constraint on the both the current element y and remaining types in the type list ys like following:

ccpara_SList ::
    Proxy c ->
    Proxy d ->
    r '[] ->
    (forall y ys. (c y, d ys, MyAll c d ys) => r ys -> r (y ': ys)) ->
    r xs

Would this be something that can be upstreamed? I don't see any drawbacks since it's just more general version of original cpara_SList. If yes, I will make a PR. I already have the implementation

[phadej]

There is already c , why a separate additional constraint is needed?

[SeungheonOh]

c is constraint on y and d is constraint on ys, and having ys constrainted with c doesn't implies All c ys

[phadej]

Where from d comes from then?

ccpara_SList ::
    Proxy c ->
    Proxy d ->
    r '[] ->
    (forall y ys. (c y, d ys, MyAll c d ys) => r ys -> r (y ': ys)) ->
    r xs

doesn't have All c xs => present in current version. How does your version works? Please show the code if you have a working implementation.

[SeungheonOh]

I should've included the full code my apologies:

type family MyAllF (c :: k -> Constraint) (d :: [k] -> Constraint) (xs :: [k]) :: Constraint where
  MyAllF _c _d '[] = ()
  MyAllF c d (x ': xs) = (c x, d xs, MyAll c d xs)

class (MyAllF c d xs, SListI xs) => MyAll (c :: k -> Constraint) (d :: [k] -> Constraint) (xs :: [k]) where
  my_cpara_SList ::
    Proxy c ->
    Proxy d ->
    r '[] ->
    (forall y ys. (c y, d ys, MyAll c d ys) => r ys -> r (y ': ys)) ->
    r xs

instance MyAll c d '[] where
  my_cpara_SList _p _d nil _cons = nil
  {-# INLINE my_cpara_SList #-}

instance (c x, d xs, MyAll c d xs) => MyAll c d (x ': xs) where
  my_cpara_SList p d nil cons =
    cons (my_cpara_SList p d nil cons)
  {-# INLINE my_cpara_SList #-}

MyAll adds constraint c on y and constraint d on ys.

[phadej]

I see, so we can have d which is not of form All c'; but what is the use case? Can't the additional premise for induction be encoded in r ys?

[SeungheonOh]

Actually, that works too. Thanks for the suggestion. Only thing is that this would force using data while having extra constraint doesn't--which might be useful in some instance, maybe?

If you think it's better not to add this, I think it's okay either way.