Combine clauses of record-selector function declarations

src/Data/Singletons/Promote.hs

@@ -27,6 +27,7 @@ import Data.Singletons.Util
 import Data.Singletons.Syntax
 import Prelude hiding (exp)
 import Control.Monad
+import Data.List (partition)
 import qualified Data.Map.Strict as Map
 import Data.Map.Strict ( Map )
 import Data.Maybe
@@ -189,7 +190,55 @@ promoteDataDecs data_decs = do
       let arg_ty = foldType (DConT data_name)
                             (map tvbToType tvbs)
       in
-      concatMapM (getRecordSelectors arg_ty) cons
+      mergeLetDecs <$> concatMapM (getRecordSelectors arg_ty) cons
+
+-- After retrieving the record selectors from a data type's constructors, it
+-- may be necessary to do some post-processing to ensure that the returned
+-- list of DLetDecs makes sense. Why? Consider this example:
+--
+--   data X = X1 {y :: Symbol} | X2 {y :: Symbol}
+--
+-- After calling getRecordSelectors on each constructor, you end up with this
+-- list of DLetDecs:
+--
+--   [ DSigD y (DAppT (DAppT DArrowT (DConT X)) (DConT Symbol))
+--   , DFunD y [DClause [DConPa X1 [DVarPa field]] (DVarE field)]
+
+--   , DSigD y (DAppT (DAppT DArrowT (DConT X)) (DConT Symbol))
+--   , DFunD y [DClause [DConPa X2 [DVarPa field]] (DVarE field)] ]
+--
+-- This is not ideal, because the record selector 'y' is defined with two
+-- separate function declarations. In fact, when singletons build a LetDecEnv
+-- out of this, it will only keep the second definition of 'y', as it believes
+-- that 'y' must only be defined once! This means that the promoted version of
+-- 'y' will incorrectly be:
+--
+--   type family Y (a0 :: X) :: Symbol
+--     where [(field0 :: Symbol)] Y ('X2 field0) = field0
+--
+-- See #180 for an example of where this happened. To prevent it, mergeLetDecs
+-- is used to combine all of the clauses of each record selector into a
+-- single DFunD so that the promoted definition covers all constructors for
+-- which the record selector is present.
+mergeLetDecs :: [DLetDec] -> [DLetDec]
+mergeLetDecs [] = []
+mergeLetDecs (x:xs)
+  -- If we encounter a function declaration, looks for all other function
+  -- declarations in the rest of the list with the same name, and concat
+  -- their clauses.
+  | DFunD n clauses <- x
+  = let (eq_n, neq_n)  = partition (\case DFunD n2 _ -> n == n2; _ -> False) xs
+        merged_clauses = concat $ clauses:map (\(DFunD _ cls) -> cls) eq_n
+        merged_x       = DFunD n merged_clauses
+     in merged_x:mergeLetDecs neq_n
+  -- If we encounter a type signature, simply delete all other type signatures
+  -- in the rest of the list with the same name, as they are guaranteed to
+  -- have the same type signature.
+  | DSigD n _ <- x
+  = let neq_n = filter (\case DSigD n2 _ -> n /= n2; _ -> True) xs
+     in x:mergeLetDecs neq_n
+
+  | otherwise = x:mergeLetDecs xs
 
 -- curious about ALetDecEnv? See the LetDecEnv module for an explanation.
 promoteLetDecs :: (String, String) -- (alpha, symb) prefixes to use

tests/SingletonsTestSuite.hs

@@ -73,6 +73,7 @@ tests =
     , compileAndDumpStdTest "Newtypes"
     , compileAndDumpStdTest "Pragmas"
     , compileAndDumpStdTest "Prelude"
+    , compileAndDumpStdTest "T180"
     ],
     testGroup "Database client"
     [ compileAndDumpTest "GradingClient/Database" ghcOpts

tests/compile-and-dump/Promote/T180.ghc80.template

@@ -0,0 +1,48 @@
+Promote/T180.hs:(0,0)-(0,0): Splicing declarations
+    promote
+      [d| z (X1 x) = x
+          z (X2 x) = x
+
+          data X = X1 {y :: Symbol} | X2 {y :: Symbol} |]
+  ======>
+    data X = X1 {y :: Symbol} | X2 {y :: Symbol}
+    z (X1 x) = x
+    z (X2 x) = x
+    type ZSym1 t = Z t
+    instance SuppressUnusedWarnings ZSym0 where
+      suppressUnusedWarnings _
+        = snd (GHC.Tuple.(,) ZSym0KindInference GHC.Tuple.())
+    data ZSym0 l
+      = forall arg. Data.Singletons.SameKind (Apply ZSym0 arg) (ZSym1 arg) =>
+        ZSym0KindInference
+    type instance Apply ZSym0 l = Z l
+    type family Z a where
+      Z (X1 x) = x
+      Z (X2 x) = x
+    type YSym1 (t :: X) = Y t
+    instance SuppressUnusedWarnings YSym0 where
+      suppressUnusedWarnings _
+        = snd (GHC.Tuple.(,) YSym0KindInference GHC.Tuple.())
+    data YSym0 (l :: TyFun X Symbol)
+      = forall arg. Data.Singletons.SameKind (Apply YSym0 arg) (YSym1 arg) =>
+        YSym0KindInference
+    type instance Apply YSym0 l = Y l
+    type family Y (a :: X) :: Symbol where
+      Y (X1 field) = field
+      Y (X2 field) = field
+    type X1Sym1 (t :: Symbol) = X1 t
+    instance SuppressUnusedWarnings X1Sym0 where
+      suppressUnusedWarnings _
+        = snd (GHC.Tuple.(,) X1Sym0KindInference GHC.Tuple.())
+    data X1Sym0 (l :: TyFun Symbol X)
+      = forall arg. Data.Singletons.SameKind (Apply X1Sym0 arg) (X1Sym1 arg) =>
+        X1Sym0KindInference
+    type instance Apply X1Sym0 l = X1 l
+    type X2Sym1 (t :: Symbol) = X2 t
+    instance SuppressUnusedWarnings X2Sym0 where
+      suppressUnusedWarnings _
+        = snd (GHC.Tuple.(,) X2Sym0KindInference GHC.Tuple.())
+    data X2Sym0 (l :: TyFun Symbol X)
+      = forall arg. Data.Singletons.SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>
+        X2Sym0KindInference
+    type instance Apply X2Sym0 l = X2 l

tests/compile-and-dump/Promote/T180.hs

@@ -0,0 +1,10 @@
+module T180 where
+
+import Data.Promotion.TH
+import GHC.TypeLits
+
+$(promote [d|
+  data X = X1 {y :: Symbol} | X2 {y :: Symbol}
+  z (X1 x) = x
+  z (X2 x) = x
+  |])