{-# LANGUAGE TypeFamilies, FunctionalDependencies, LambdaCase #-}
module SOP.Sums where
import MyPrelude
import GHC.Generics
import Data.Void
import Optics
type family Sum (xs :: [*]) :: *
where
Sum '[] = Void
Sum (x ': xs) = Either x (Sum xs)
class Coproduct c xs | c -> xs
where
asCoproduct :: Iso' c (Sum xs)
instance Coproduct (U1 p) '[()]
where
asCoproduct = iso (\U1 -> Left ()) (either (const U1) absurd)
instance Coproduct (K1 i c p) '[c]
where
asCoproduct = iso (\(K1 c) -> Left c) (either K1 absurd)
instance (Functor f, Coproduct (f p) xs) => Coproduct (M1 i c f p) xs
where
asCoproduct = iso (\(M1 fp) -> fwd asCoproduct fp) (M1 . bwd asCoproduct)
type family xs ++ ys :: [*]
where
'[] ++ xs = xs
(x ': xs) ++ ys = x ': (xs ++ys)
instance (Coproduct (f p) xs, Coproduct (g p) ys) => Coproduct ((f :+: g) p) (xs ++ ys)
where
asCoproduct = iso (\case { L1 fp -> Left fp; R1 gp -> Right $ fwd asCoproduct gp }) (either L1 (R1 . bwd asCoproduct))

[typecheck] [E] /mnt/data/depot/git/haskell/repos/co-optics/src/SOP/Sums.hs:38:54: error:
• Illegal type synonym family application in instance: xs ++ ys
• In the instance declaration for
‘Coproduct ((f :+: g) p) (xs ++ ys)’

The continuation-passing way is to use a ternary class, quantifying over "the rest of the sum". Then you won't need an auxiliary Append constraint for the (:+:) instance.

What's the easiest way to make this work

Right now it gives:

`instance (Coproduct (f p) xs, Coproduct (g p) ys, xs ++ ys ~ zs) => Coproduct ((f :+: g) p) zs`

perhaps?You will need more constraints to inject

`Sum xs`

and`Sum ys`

into`Sum (xs ++ ys)`

.Yeah, I ended up doing the weird hack I resort to in these situations

There's usually a compact continuation-passing solution too.

Alas, now I've realized I might not have enough information altogether:

What's the error?

There's no error, but I've ended up needing to produce

`Sum zs -> (f :+: g) p`

idk if I can do that without an extra index or something. maybe I'm not thinking about it clearly though

What I need is

`Iso (Either (Sum xs) (Sum ys)) (Sum zs)`

, right?or can I get away with the unidirectional thing I have now somehow

yes you need

`Append`

or whatever constraint you end up with to contain an isoThe continuation-passing way is to use a ternary class, quantifying over "the rest of the sum". Then you won't need an auxiliary

`Append`

constraint for the`(:+:)`

instance.@Lysxia You think I can actually implement the cons instance as an iso?

without additional type level information I mean

I got back up to where I was before, now I need to do the backwards case:

sure that looks feasible

weird, it worked out

i just filled out the holes, but I don't really get how one direction doesn't destroy some information

like, mashing them together

whew

ok, so it all works, I'll add a note to do it the right way with the CPS approach later

conveniently we can link to messages in this thing, so I won't have to ask you five more times :sweat_smile:

Here's the whole thing for anyone who's interested: https://gist.github.com/masaeedu/f80f47bb1fcf8412dccc3edef1bbd21a