Compatibility-mode staged-sop.

Based on work Edsko and I did during Edsko's Regensburg visit.

staged-sop-examples/bench/Bench.hs

@@ -1,9 +1,14 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
-{-# OPTIONS_GHC -ddump-simpl #-}
+
+{-# LANGUAGE IncoherentInstances #-}
+
+{-# OPTIONS_GHC -ddump-splices #-}
+-- {-# OPTIONS_GHC -ddump-simpl -dsuppress-all #-}
 module Main where
 
 import Codec.CBOR.Encoding
@@ -13,6 +18,7 @@ import ExampleTypes
 import ExampleFunctions
 import Gauge.Main
 import Gauge.Main.Options
+import Generics.SOP.Staged
 
 genum_Ordering :: () -> [Ordering]
 genum_Ordering () = genum
@@ -30,7 +36,11 @@ gsappend_Foo :: Foo -> Foo -> Foo
 gsappend_Foo = gsappend
 
 sgsappend_Foo :: Foo -> Foo -> Foo
-sgsappend_Foo = $$(sgsappend')
+sgsappend_Foo  =
+  let
+    c = constraints @Foo
+  in
+    $$(sgsappend' (pallC [|| c ||]))
 
 msappend_Foo :: Foo -> Foo -> Foo
 msappend_Foo (Foo is1 o1 txt1) (Foo is2 o2 txt2) =
@@ -48,7 +58,11 @@ instance Eq a => Eq (Tree GHCGenerics a) where
   (==) = ghcgeq
 
 instance Eq a => Eq (Tree StagedSOP a) where
-  x1 == x2 = $$(sgeq [|| x1 ||] [|| x2 ||])
+  x1 == x2 =
+    let
+      c = constraints @(Tree StagedSOP a)
+    in
+      $$(sgeq (allC [|| c ||]) [|| x1 ||] [|| x2 ||])
 
 instance Eq a => Eq (Tree Manual a) where
   Leaf a1 == Leaf a2 = a1 == a2
@@ -64,7 +78,11 @@ instance Eq (Prop GHCGenerics) where
   (==) = ghcgeq
 
 instance Eq (Prop StagedSOP) where
-  x1 == x2 = $$(sgeq [|| x1 ||] [|| x2 ||])
+  x1 == x2 =
+    let
+      c = constraints @(Prop StagedSOP)
+    in
+      $$(sgeq (allC [|| c ||]) [|| x1 ||] [|| x2 ||])
 
 instance Eq (Prop Manual) where
   Var x1 == Var x2 = x1 == x2
@@ -79,9 +97,21 @@ instance Serialise (Prop GenericsSOP) where
   encode = gencode
   decode = gdecode
 
+-- NOTE: decode currently requires IncoherentInstances because the
+-- way we are passing the Applicative instance for Decoder via an
+-- explicit dictionary, it ends up being in scope twice!
+--
 instance Serialise (Prop StagedSOP) where
-  encode = $$(sgencode)
-  decode = $$(sgdecode)
+  encode =
+    let
+      c = constraints @(Prop StagedSOP)
+    in
+      $$(sgencode (allC [|| c ||]))
+  decode =
+    let
+      c = constraints @(Prop StagedSOP)
+    in
+      $$(sgdecode (allC [|| c ||]))
 
 instance Serialise (Prop GHCGenerics)
 

staged-sop-examples/src/ExampleFunctions.hs

@@ -14,37 +14,47 @@ import Codec.CBOR.Encoding
 import Codec.CBOR.Decoding
 import Codec.Serialise
 import Control.DeepSeq
-import Data.SOP.Constraint (And)
+import Data.Kind
+import Data.SOP
+import Data.SOP.Constraint (And, Top)
+import Data.SOP.NP
+import Data.SOP.NS
 import qualified Generics.SOP as SOP
-import qualified Generics.SOP.NP as SOP
-import qualified Generics.SOP.NS as SOP
+-- import qualified Generics.SOP.NP as SOP
+-- import qualified Generics.SOP.NS as SOP
 import Generics.SOP.Staged
 import GHC.Generics as GHC hiding (C, (:.:))
-import Language.Haskell.TH
+import Language.Haskell.TH hiding (Type)
+import Language.Haskell.TH.Syntax hiding (Type)
 import ExampleTypes
 
 sgsappend ::
-  (SIsProductType a xs, All (Quoted Semigroup) xs) =>
-  Code a -> Code a -> Code a
-sgsappend c1 c2 =
+  SIsProductType a xs =>
+  NP (C :.: Dict Semigroup) xs ->
+  CodeQ a -> CodeQ a -> CodeQ a
+sgsappend dicts c1 c2 =
   sproductTypeFrom c1 $ \ a1 -> sproductTypeFrom c2 $ \ a2 ->
     sproductTypeTo
-      (czipWith_NP (Proxy @(Quoted Semigroup))
-        (mapCCC [|| (<>) ||]) a1 a2
+      (zipWith3_NP
+        (\ (Comp (C d)) (C a1) (C a2) -> C [|| case $$d of Dict -> ($$a1 <> $$a2) ||])
+        dicts a1 a2
       )
+-- TODO: it would be nice to simplify this, but it's not clear if it can be done;
+-- perhaps by means of quasi-quotation
 
 sgsappend' ::
-  (SIsProductType a xs, All (Quoted Semigroup) xs) =>
-  Code (a -> a -> a)
-sgsappend' =
-  [|| \ a1 a2 -> $$(sgsappend [|| a1 ||] [|| a2 ||]) ||]
+  SIsProductType a xs =>
+  NP (C :.: Dict Semigroup) xs ->
+  CodeQ (a -> a -> a)
+sgsappend' dicts =
+  [|| \ a1 a2 -> $$(sgsappend dicts [|| a1 ||] [|| a2 ||]) ||]
 
 gsappend ::
-  (SOP.IsProductType a xs, SOP.All Semigroup xs) =>
+  (SOP.IsProductType a xs, All Semigroup xs) =>
   a -> a -> a
 gsappend a1 a2 =
   SOP.productTypeTo
-    (SOP.czipWith_NP (Proxy @Semigroup)
+    (czipWith_NP (Proxy @Semigroup)
       (SOP.mapIII (<>)) (SOP.productTypeFrom a1) (SOP.productTypeFrom a2)
     )
 
@@ -64,25 +74,25 @@ instance Semigroup a => GSappend (K1 r a) where
 instance GSappend a => GSappend (M1 i c a) where
   ghcsappend' (M1 a1) (M1 a2) = M1 (ghcsappend' a1 a2)
 
-ghcsappend :: (GHC.Generic a, GSappend (Rep a)) => a -> a -> a
+ghcsappend :: (GHC.Generic a, GSappend (GHC.Rep a)) => a -> a -> a
 ghcsappend a1 a2 = to (ghcsappend' (from a1) (from a2))
 
-
 sgrnf ::
-  (SGeneric a, All (All (Quoted NFData)) (SDescription a)) =>
-  Code a -> Code ()
-sgrnf c =
+  SGeneric a =>
+  POP (C :.: Dict NFData) (SDescription a) ->
+  CodeQ a -> CodeQ ()
+sgrnf dicts c =
   sfrom c $ \ a ->
     foldr (\ x r -> [|| $$x `seq` $$r ||]) [|| () ||]
-      (collapse_SOP (cmap_SOP (Proxy @(Quoted NFData)) (mapCK [|| rnf ||]) a))
+      (collapse_SOP (selectWith_SOP (\ (Comp (C d)) (C x) -> K [|| withDict $$d (rnf $$x) ||]) dicts a))
 
 gShowEnum ::
   SOP.IsEnumType a => NP (K String) (SOP.Code a) -> a -> String
 gShowEnum names a =
-  SOP.collapse_NS (SOP.hzipWith const names (SOP.enumTypeFrom a))
+  collapse_NS (SOP.hzipWith const names (SOP.enumTypeFrom a))
 
 sgShowEnum ::
-  SIsEnumType a => NP (K String) (SDescription a) -> Code a -> Code String
+  SIsEnumType a => NP (K String) (SDescription a) -> CodeQ a -> CodeQ String
 sgShowEnum names c =
   senumTypeFrom c $ \ a ->
     liftTyped (collapse_NS (selectWith_NS const names a))
@@ -97,29 +107,34 @@ geq ::
 geq a1 a2 =
   SOP.ccompare_SOP (Proxy @Eq)
     False
-    (\ xs1 xs2 -> and (SOP.collapse_NP (SOP.czipWith_NP (Proxy @Eq) (SOP.mapIIK (==)) xs1 xs2)))
+    (\ xs1 xs2 -> and (collapse_NP (czipWith_NP (Proxy @Eq) (SOP.mapIIK (==)) xs1 xs2)))
     False
     (SOP.from a1) (SOP.from a2)
 
+-- This transcription is quite ugly and annoying, because compare_SOP does not exist
+-- with an extra argument ...
 sgeq ::
-  (SGeneric a, All (All (Quoted Eq)) (SDescription a)) =>
-  Code a -> Code a -> Code Bool
-sgeq c1 c2 =
+  SGeneric a =>
+  POP (C :.: Dict Eq) (SDescription a) ->
+  CodeQ a -> CodeQ a -> CodeQ Bool
+sgeq dicts c1 c2 =
   sfrom c1 $ \ a1 -> sfrom c2 $ \ a2 ->
-  ccompare_SOP (Proxy @(Quoted Eq))
-    [|| False ||]
-    (\ xs1 xs2 -> sand (collapse_NP (czipWith_NP (Proxy @(Quoted Eq)) (mapCCK [|| (==) ||]) xs1 xs2)))
-    [|| False ||]
-    a1 a2
+  ccompare_SOP (Proxy @Top)
+    ([|| False ||])
+    (\ xs1 xs2 -> sand (collapse_NP (zipWith_NP (\ (P (Comp (C d)) (C x1)) (C x2) -> K [|| withDict $$d ($$x1 == $$x2) ||]) xs1 xs2)))
+    ([|| False ||])
+    (selectWith_SOP P dicts a1) a2
+
+data P (f :: k -> Type) (g :: k -> Type) (x :: k) = P (f x) (g x)
 
-sand :: [Code Bool] -> Code Bool
+sand :: [CodeQ Bool] -> CodeQ Bool
 sand = foldr (\ x r -> [|| $$x && $$r ||]) [|| True ||]
 
 genum :: (SOP.Generic a, SOP.All ((~) '[]) (SOP.Code a)) => [a]
 genum =
-  SOP.to <$> SOP.apInjs_POP (POP (SOP.cpure_NP (Proxy @((~) '[])) Nil))
+  SOP.to <$> SOP.apInjs_POP (POP (cpure_NP (Proxy @((~) '[])) Nil))
 
-sgenum :: SIsEnumType a => Code [a]
+sgenum :: SIsEnumType a => CodeQ [a]
 sgenum =
   foldr (\ x r -> [|| $$x : $$r ||]) [|| [] ||]
     (sto <$> apInjs_POP (POP (cpure_NP (Proxy @((~) '[])) Nil)))
@@ -150,7 +165,7 @@ ghcgeq a1 a2 = ghcgeq' (from a1) (from a2)
 
 conNumbers :: forall a . (SOP.Generic a) => Proxy a -> NP (K Word) (SOP.Code a)
 conNumbers _ =
-  SOP.ana_NP (\ (K i) -> (K i, K (i + 1))) (K 0)
+  ana_NP (\ (K i) -> (K i, K (i + 1))) (K 0)
 
 sconNumbers :: forall a . (SGeneric a) => Proxy a -> NP (K Word) (SDescription a)
 sconNumbers _ =
@@ -162,7 +177,7 @@ conArities _ =
     go :: forall xs . SOP.SListI xs => K Word xs
     go = K (fromIntegral (SOP.lengthSList (Proxy @xs)))
   in
-    SOP.cpure_NP (Proxy @SOP.SListI) go
+    cpure_NP (Proxy @SOP.SListI) go
 
 sconArities :: forall a . (SGeneric a) => Proxy a -> NP (K Word) (SDescription a)
 sconArities _ =
@@ -172,65 +187,74 @@ sconArities _ =
   in
     cpure_NP (Proxy @SListI) go
 
-
 gencode :: forall a . (SOP.Generic a, SOP.All (SOP.All Serialise) (SOP.Code a)) => a -> Encoding
 gencode x =
   let
     tmp :: SOP (K Encoding) (SOP.Code a)
     tmp =
-      SOP.cmap_SOP (Proxy @Serialise) (SOP.mapIK encode) (SOP.from x)
+      cmap_SOP (Proxy @Serialise) (SOP.mapIK encode) (SOP.from x)
 
     tmp2 :: NS (K Encoding) (SOP.Code a)
     tmp2 =
       SOP.hzipWith3
-        (\ (K i) (K a) es -> K (encodeListLen (a + 1) <> encodeWord i <> mconcat (SOP.collapse_NP es)))
+        (\ (K i) (K a) es -> K (encodeListLen (a + 1) <> encodeWord i <> mconcat (collapse_NP es)))
         (conNumbers (Proxy @a))
         (conArities (Proxy @a))
         (SOP.unSOP tmp)
   in
-    SOP.collapse_NS tmp2
+    collapse_NS tmp2
 
-sgencode :: forall a . (SGeneric a, All (All (Quoted Serialise)) (SDescription a)) => Code (a -> Encoding)
-sgencode =
+sgencode :: forall a . SGeneric a => POP (C :.: Dict Serialise) (SDescription a) -> CodeQ (a -> Encoding)
+sgencode dicts =
   [||
     \ a ->
     $$(sfrom [|| a ||] $ \ a' ->
       let
-        tmp :: SOP (K (Code Encoding)) (SDescription a)
-        tmp =
-          cmap_SOP (Proxy @(Quoted Serialise)) (mapCK [|| encode ||]) a'
-
-        tmp2 :: NS (K (Code Encoding)) (SDescription a)
-        tmp2 =
-          cselectWith_NS
-            (Proxy @(All (Quoted Serialise)))
-            (\ (K (i, a)) es -> let a' = a + 1 in K [|| encodeListLen a' <> encodeWord i <> $$(foldr (\ x y -> [|| $$x <> $$y ||]) [|| mempty ||] (collapse_NP es)) ||])
-            (tmp3 @a) -- (czipWith_NP (Proxy @(All (Quoted Serialise))) (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a)))
-            (unSOP tmp)
-
-        tmp3 :: forall a . (SGeneric a, All (All (Quoted Serialise)) (SDescription a)) => NP (K (Word, Word)) (SDescription a)
+        tmp1 :: SOP (K (CodeQ Encoding)) (SDescription a)
+        tmp1 =
+          selectWith_SOP (\ (Comp (C d)) (C a) -> K [|| withDict $$d (encode $$a) ||]) dicts a'
+
+        tmp2 :: forall a . SGeneric a => Proxy a -> NP (K (Word, Word)) (SDescription a)
+        tmp2 _ =
+          zipWith_NP
+            (\ (K cn) (K ca) -> K (cn, ca))
+            (sconNumbers (Proxy @a)) (sconArities (Proxy @a))
+
+        tmp3 :: NS (K (CodeQ Encoding)) (SDescription a)
         tmp3 =
-          (czipWith_NP (Proxy @(All (Quoted Serialise))) (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a)))
+          selectWith_NS
+            (\ (K (i, a)) es ->
+              let
+                a' = a + 1
+              in
+                K [||
+                     encodeListLen a'
+                  <> encodeWord i
+                  <> $$(foldr (\ x y -> [|| $$x <> $$y ||]) [|| mempty ||] (collapse_NP es))
+                ||]
+            )
+            (tmp2 (Proxy @a))
+            (unSOP tmp1)
       in
-        collapse_NS tmp2
+        collapse_NS tmp3
     )
   ||]
 
-gdecode :: forall a s . (SOP.Generic a, SOP.All (SOP.All Serialise) (SOP.Code a)) => Decoder s a
+gdecode :: forall a s . (SOP.Generic a, All (All Serialise) (SOP.Code a)) => Decoder s a
 gdecode =
   let
     tmp :: POP (Decoder s) (SOP.Code a)
     tmp =
-      SOP.cpure_POP (Proxy @Serialise) decode
+      cpure_POP (Proxy @Serialise) decode
 
     tmp2 :: NP (K (SOP (Decoder s) (SOP.Code a))) (SOP.Code a)
     tmp2 =
-      SOP.apInjs'_POP tmp
+      apInjs'_POP tmp
 
     tmp3 :: NP (K ((Word, Word), Decoder s a)) (SOP.Code a)
     tmp3 =
-      SOP.zipWith3_NP
-        (\ (K i) (K a) (K dec) -> K ((a + 1, i), SOP.to <$> SOP.sequence_SOP dec))
+      zipWith3_NP
+        (\ (K i) (K a) (K dec) -> K ((a + 1, i), SOP.to <$> sequence_SOP dec))
         (conNumbers (Proxy @a))
         (conArities (Proxy @a))
         tmp2
@@ -242,34 +266,36 @@ gdecode =
         Just dec -> dec
         Nothing  -> fail "invalid encoding"
 
-sgdecode :: forall a s . (SGeneric a, LiftT s, All (All (Quoted Serialise)) (SDescription a), All (And (All LiftT) (AllTails (LiftTCurry a))) (SDescription a)) => Code (Decoder s a)
-sgdecode =
+dApplicativeDecoder :: Dict Applicative (Decoder s)
+dApplicativeDecoder = Dict
+
+sgdecode :: forall a s . SGeneric a => POP (C :.: Dict Serialise) (SDescription a) -> CodeQ (Decoder s a)
+sgdecode dicts =
   let
     tmp :: POP (C :.: Decoder s) (SDescription a)
     tmp =
-      cpure_POP (Proxy @(Quoted Serialise)) (Comp (C [|| decode ||]))
+      map_POP (\ (Comp (C d)) -> Comp (C [|| withDict $$d decode ||])) dicts
 
     tmp2 :: NP (K (SOP (C :.: Decoder s) (SDescription a))) (SDescription a)
     tmp2 =
       apInjs'_POP tmp
 
-    tmp3 :: NP (K ((Word, Word), Code (Decoder s a))) (SDescription a)
+    tmp3 :: NP (K ((Word, Word), CodeQ (Decoder s a))) (SDescription a)
     tmp3 =
-      czipWith_NP
-        (Proxy @(All (Quoted Serialise)))
-        (\ (K (i, a)) (K dec) -> K ((a + 1, i), stoA dec))
-        (tmp3' @a)
+      zipWith_NP
+        (\ (K (i, a)) (K dec) -> K ((a + 1, i), stoA [|| dApplicativeDecoder ||] dec))
+        (tmp3' (Proxy @a))
         tmp2
 
-    tmp3' :: forall a . (SGeneric a, All (All (Quoted Serialise)) (SDescription a)) => NP (K (Word, Word)) (SDescription a)
-    tmp3' =
-      (czipWith_NP (Proxy @(All (Quoted Serialise))) (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a)))
+    tmp3' :: forall a . SGeneric a => Proxy a -> NP (K (Word, Word)) (SDescription a)
+    tmp3' _ =
+      zipWith_NP (SOP.mapKKK (,)) (sconNumbers (Proxy @a)) (sconArities (Proxy @a))
 
-    tmp4 :: [((Word, Word), Code (Decoder s a))]
+    tmp4 :: [((Word, Word), CodeQ (Decoder s a))]
     tmp4 =
       collapse_NP tmp3
 
-    tmp5 :: Code (Word, Word) -> [((Word, Word), Code (Decoder s a))] -> Code (Decoder s a)
+    tmp5 :: CodeQ (Word, Word) -> [((Word, Word), CodeQ (Decoder s a))] -> CodeQ (Decoder s a)
     tmp5 _sym []                  = [|| fail "invalid encoding" ||]
     tmp5 sym ((key, rhs) : cases) =
       [|| if $$sym == key then $$rhs else $$(tmp5 sym cases) ||]