`All2 c xss` should imply `All SListI xss`

[mniip]

This came up during ekmett's haskell stream: There's no nice way to do a double fold on an All2 c xss => xss because the type system doesn't know the inner lists are lists, i.e All SListI xss. The workaround was to write direct recursion on nil/cons cases.

[phadej]

The implication should indeed by there, but what you mean by the double fold? For example:

garbitrary :: forall a. (Generic a, All2 Arbitrary (Code a)) => Gen a
garbitrary = liftM to $ hsequence =<< elements (apInjs_POP $ hcpure p arbitrary)
  where
    p :: Proxy Arbitrary
    p = Proxy

http://hackage.haskell.org/package/generics-sop-0.3.2.0/docs/Generics-SOP-NS.html#v:apInjs_POP

Or was Edward playing with hcfoldMap ?

[phadej]

In other words, what's the code you want to write, but you cannot? (so it can be added as a test).

[mniip]

Double fold a-la foldr (f2 :: b -> c -> c) (z2 :: c) . map (foldr (f1 :: a -> b -> b) (z1 :: b)) :: [[a]] -> c. I.e with different functions on the outer and inner NP of the POP.

[phadej]

I'd prefer a code snippet I can insert into an editor and see it fail.

[mniip]

A vast simplification of the code is:

{-# LANGUAGE TypeApplications, RankNTypes, ScopedTypeVariables, DefaultSignatures, FlexibleContexts, AllowAmbiguousTypes, PolyKinds, DataKinds #-}

import GHC.Generics as GHC
import Generics.SOP
import Generics.SOP.Constraint
import Generics.SOP.GGP

class Cnt a where
    cnt :: Int
    default cnt :: (GHC.Generic a, GFrom a, All2 Cnt (GCode a)) => Int
    cnt = gcnt @(GCode a)

gcnt :: forall xss. (All SListI xss, All2 Cnt xss) => Int
gcnt = sum $ hcollapse np
    where
        np :: NP (K Int) xss
        np = hcmap (Proxy @SListI) (\xs -> K (product $ hcollapse xs)) npnp

        npnp :: NP (NP (K Int)) xss
        npnp = unPOP $ hcpure (Proxy @Cnt) kcnt

        kcnt :: forall a. Cnt a => K Int a
        kcnt = K (cnt @a)

NB: inner fold uses product, outer fold uses sum.

[phadej]

diff --git a/src/Generics/SOP/Constraint.hs b/src/Generics/SOP/Constraint.hs
index 321677e..0252cbf 100644
--- a/src/Generics/SOP/Constraint.hs
+++ b/src/Generics/SOP/Constraint.hs
@@ -77,8 +77,8 @@ type SListI2 = All SListI
 -- means that 'f' can assume that all elements of the sum
 -- of product satisfy 'Eq'.
 --
-class (AllF (All f) xss, SListI xss) => All2 f xss
-instance (AllF (All f) xss, SListI xss) => All2 f xss
+class (AllF (All f) xss, All SListI xss, SListI xss) => All2 f xss
+instance (AllF (All f) xss, All SListI xss, SListI xss) => All2 f xss
 --
 -- NOTE:
 --
diff --git a/src/Generics/SOP/Dict.hs b/src/Generics/SOP/Dict.hs
index a2cf88a..656fbe3 100644
--- a/src/Generics/SOP/Dict.hs
+++ b/src/Generics/SOP/Dict.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 -- | Explicit dictionaries.
 --
 -- When working with compound constraints such as constructed
@@ -141,8 +142,16 @@ unAll2 Dict = Dict
 --
 -- @since 0.2
 --
-all2 :: Dict (All (All c)) xss -> Dict (All2 c) xss
-all2 Dict = Dict
+all2 :: forall c xss. Dict (All (All c)) xss -> Dict (All2 c) xss
+all2 Dict = case aux :: Dict (All SListI) xss of Dict -> Dict
+  where
+    aux :: forall yss. All (All c) yss => Dict (All SListI) yss
+    aux = case sList :: SList yss of
+        SNil  -> Dict
+        SCons -> aux'
+
+    aux' :: forall ys yss. (All c ys, All (All c) yss) => Dict (All SListI) (ys ': yss)
+    aux' = case aux :: Dict (All SListI) yss of Dict -> Dict

Solves the issue so the modified example

{-# LANGUAGE TypeApplications, RankNTypes, ScopedTypeVariables, DefaultSignatures, FlexibleContexts, AllowAmbiguousTypes, PolyKinds, DataKinds #-}

import GHC.Generics as GHC
import Generics.SOP
import Generics.SOP.Constraint
import Generics.SOP.GGP

class Cnt a where
    cnt :: Int
    default cnt :: (GHC.Generic a, GFrom a, All2 Cnt (GCode a)) => Int
    cnt = gcnt @(GCode a)

-- note: no All SListI xss
gcnt :: forall xss. All2 Cnt xss => Int
gcnt = sum $ hcollapse np
    where
        np :: NP (K Int) xss
        np = hcmap (Proxy @SListI) (\xs -> K (product $ hcollapse xs)) npnp

        npnp :: NP (NP (K Int)) xss
        npnp = unPOP $ hcpure (Proxy @Cnt) kcnt

        kcnt :: forall a. Cnt a => K Int a
        kcnt = K (cnt @a)

compiles.

---

all2 becomes ugly. I'd be in favour of making changes and adding Cnt.hs into examples so e.g. solution to https://github.com/well-typed/generics-sop/issues/32 would not-break it, but on opposite make this case nicer.

[mniip]

Ah yes sorry All SListI xss in gcnt's type was probably me copying a not-completely-edited file.

[phadej]

Another variant, which doesn't require changing generics-sop is to write double hcollapse as:

{-# LANGUAGE TypeApplications, RankNTypes, ScopedTypeVariables, DefaultSignatures, FlexibleContexts, AllowAmbiguousTypes, PolyKinds, DataKinds #-}

import GHC.Generics as GHC
import Generics.SOP
import Generics.SOP.Constraint
import Generics.SOP.GGP

class Cnt a where
    cnt :: Int
    default cnt :: (GHC.Generic a, GFrom a, All2 Cnt (GCode a)) => Int
    cnt = gcnt @(GCode a)

gcnt :: forall xss. All2 Cnt xss => Int
gcnt = sum $ hcollapse np
    where
        -- Another variant: @SListI -> All Cnt
        np :: NP (K Int) xss
        np = hcmap (Proxy @(All Cnt)) (\xs -> K (product $ hcollapse xs)) npnp

        npnp :: NP (NP (K Int)) xss
        npnp = unPOP $ hcpure (Proxy @Cnt) kcnt

        kcnt :: forall a. Cnt a => K Int a
        kcnt = K (cnt @a)

[kosmikus]

Yes, @phadej 's last variant is what I would suggest to use here. I agree that one can argue that the suggested implication should directly hold. I'd rather replace SListI with All Top in the long term though.

[kosmikus]

See #32.

[kosmikus]

Somewhat related: with quantified constraints, we can say

class (..., forall d . (forall x . c x => d x) => All d xs) => All c xs

in replacement of

class (..., All SListI xs) => All c xs

and it will give us better superclass behaviour for All. We'll have to wait until we can make GHC 8.6 the lower dependency bound of the library though.

[kosmikus]

With #32 done, I think the quantified constraint would be the main improvement we could make here, but I'm not yet prepared to move to 8.6 as minimum.