diff --git a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden index 82904055..92d1b39b 100644 --- a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden +++ b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden @@ -353,11 +353,11 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations type SchSym1 :: [Attribute] -> Schema type family SchSym1 (a0123456789876543210 :: [Attribute]) :: Schema where SchSym1 a0123456789876543210 = Sch a0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 (name0123456789876543210 :: [AChar]) name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym0 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210 (name0123456789876543210 :: [AChar]) name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name' - type family Case_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 t where + type family Case_0123456789876543210 (name0123456789876543210 :: [AChar]) name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 t where Case_0123456789876543210 name name' u attrs 'True = u Case_0123456789876543210 name name' u attrs 'False = Apply (Apply LookupSym0 name) (Apply SchSym0 attrs) type LookupSym0 :: (~>) [AChar] ((~>) Schema U) diff --git a/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden b/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden index 57d99177..f362b3bd 100644 --- a/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden +++ b/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden @@ -61,11 +61,11 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations insertionSort :: [Nat] -> [Nat] insertionSort [] = [] insertionSort (h : t) = insert h (insertionSort t) - type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 (n0123456789876543210 :: Nat) h0123456789876543210 t0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210 (n0123456789876543210 :: Nat) h0123456789876543210 t0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h - type family Case_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: Nat) h0123456789876543210 t0123456789876543210 t where Case_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t) Case_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t) type InsertionSortSym0 :: (~>) [Nat] [Nat] diff --git a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden index a362be6f..83e553cb 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden @@ -37,11 +37,11 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations in z foo5 :: a -> a foo5 x = case x of y -> (\ _ -> x) y - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 y0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 y x _ = x - type family Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 y x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 y x arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 y0123456789876543210 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 @@ -49,29 +49,29 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 y0123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 x y = Apply (Lambda_0123456789876543210Sym0 y x) y - type family Let0123456789876543210ZSym0 a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + type family Let0123456789876543210ZSym0 a0123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where Let0123456789876543210ZSym0 a0123456789876543210 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where Let0123456789876543210Z a y x = y - type family Case_0123456789876543210 a0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 a x y = Let0123456789876543210ZSym0 a y x - type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) where Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 b0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 b0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) where Let0123456789876543210Scrutinee_0123456789876543210 a b = Apply (Apply Tuple2Sym0 a) b - type family Case_0123456789876543210 a0123456789876543210 b0123456789876543210 t where + type family Case_0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) t where Case_0123456789876543210 a b '(p, _) = p - type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 d0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 (d0123456789876543210 :: a0123456789876543210) where Let0123456789876543210Scrutinee_0123456789876543210Sym0 d0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 d0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 d0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) where Let0123456789876543210Scrutinee_0123456789876543210 d = Apply JustSym0 d - type family Case_0123456789876543210 d0123456789876543210 t where + type family Case_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 d ('Just y) = y - type family Case_0123456789876543210 d0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) t where Case_0123456789876543210 d x ('Just y) = y Case_0123456789876543210 d x 'Nothing = d type Foo5Sym0 :: (~>) a a diff --git a/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden index 5db7414f..ba88b0e1 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden @@ -6,7 +6,7 @@ Singletons/EmptyShowDeriving.hs:(0,0)-(0,0): Splicing declarations ======> data Foo deriving instance Show Foo - type family Case_0123456789876543210 v_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (v_01234567898765432100123456789876543210 :: Foo) (a_01234567898765432100123456789876543210 :: GHC.Types.Symbol) t where type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Foo -> GHC.Types.Symbol -> GHC.Types.Symbol type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Foo) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where diff --git a/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden index 0301f280..eff74451 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden @@ -24,13 +24,13 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations type Q2Sym0 :: Quux type family Q2Sym0 :: Quux where Q2Sym0 = Q2 - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = BumSym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = BazSym0 Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 2)) - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = BarSym0 Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1)) type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> Foo @@ -117,10 +117,10 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations Singletons/EnumDeriving.hs:0:0:: Splicing declarations singEnumInstance ''Quux ======> - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = Q2Sym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = Q1Sym0 Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1)) type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> Quux diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden index d0a2ce77..143160a6 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden @@ -60,9 +60,9 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type MkT2Sym1 :: forall x a. Maybe x -> T x a type family MkT2Sym1 @x @a (a0123456789876543210 :: Maybe x) :: T x a where MkT2Sym1 a0123456789876543210 = MkT2 a0123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -70,11 +70,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -82,16 +82,16 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 type Fmap_0123456789876543210 :: forall a b x. (~>) a b -> T x a -> T x b type family Fmap_0123456789876543210 @a @b @x (a :: (~>) a b) (a :: T x a) :: T x b where Fmap_0123456789876543210 @a @b @x (_f_0123456789876543210 :: (~>) a b) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (Lambda_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply FmapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply FmapSym0 _f_0123456789876543210)) a_0123456789876543210) Fmap_0123456789876543210 @a @b @x (_f_0123456789876543210 :: (~>) a b) (MkT2 a_0123456789876543210 :: T x a) = Apply MkT2Sym0 (Apply (Lambda_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210) a_0123456789876543210) - type family Lambda_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -99,11 +99,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = _z_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -111,11 +111,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _z_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -123,7 +123,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 type TFHelper_0123456789876543210 :: forall a x b. a -> T x b -> T x a @@ -133,9 +133,9 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance PFunctor (T x) where type Fmap a a = Fmap_0123456789876543210 a a type (<$) a a = TFHelper_0123456789876543210 a a - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = MemptySym0 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -143,11 +143,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = MemptySym0 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 @@ -155,16 +155,16 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 type FoldMap_0123456789876543210 :: forall a m x. (~>) a m -> T x a -> m type family FoldMap_0123456789876543210 @a @m @x (a :: (~>) a m) (a :: T x a) :: m where FoldMap_0123456789876543210 @a @m @x (_f_0123456789876543210 :: (~>) a m) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply MappendSym0 (Apply (Lambda_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply (Apply FoldMapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FoldMapSym0 (Apply FoldMapSym0 _f_0123456789876543210)) a_0123456789876543210))) FoldMap_0123456789876543210 @a @m @x (_f_0123456789876543210 :: (~>) a m) (MkT2 a_0123456789876543210 :: T x a) = Apply (Lambda_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210) a_0123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = n2_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 @@ -172,7 +172,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 @@ -180,11 +180,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym2 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = Apply (Apply (Apply FoldrSym0 _f_0123456789876543210) n2_0123456789876543210) n1_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 @@ -192,7 +192,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 @@ -200,11 +200,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym2 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 x n1_0123456789876543210 n2_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = Apply (Apply (Apply FoldrSym0 _f_0123456789876543210) n2_0123456789876543210) n1_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 @@ -212,7 +212,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym1 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 @@ -220,11 +220,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym2 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = Apply (Apply (Apply FoldrSym0 (Lambda_0123456789876543210Sym0 x n1_0123456789876543210 n2_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210)) n2_0123456789876543210) n1_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 @@ -232,7 +232,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 @@ -240,11 +240,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym2 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = n2_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 @@ -252,7 +252,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 @@ -260,7 +260,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym2 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 type Foldr_0123456789876543210 :: forall a b x. (~>) a ((~>) b b) -> b -> T x a -> b @@ -277,12 +277,12 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations Traverse_0123456789876543210 @a @f @b @x (_f_0123456789876543210 :: (~>) a (f b)) (MkT2 a_0123456789876543210 :: T x a) = Apply (Apply FmapSym0 MkT2Sym0) (Apply PureSym0 a_0123456789876543210) instance PTraversable (T x) where type Traverse a a = Traverse_0123456789876543210 a a - type family Case_0123456789876543210 v_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (v_01234567898765432100123456789876543210 :: Empty a0123456789876543210) t where type Fmap_0123456789876543210 :: forall a b. (~>) a b -> Empty a -> Empty b type family Fmap_0123456789876543210 @a @b (a :: (~>) a b) (a :: Empty a) :: Empty b where Fmap_0123456789876543210 @a @b _ v_0123456789876543210 = Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210 - type family Case_0123456789876543210 v_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (v_01234567898765432100123456789876543210 :: Empty b0123456789876543210) t where type TFHelper_0123456789876543210 :: forall a b. a -> Empty b -> Empty a type family TFHelper_0123456789876543210 @a @b (a :: a) (a :: Empty b) :: Empty a where @@ -296,7 +296,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations FoldMap_0123456789876543210 @a @m _ _ = MemptySym0 instance PFoldable Empty where type FoldMap a a = FoldMap_0123456789876543210 a a - type family Case_0123456789876543210 v_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (v_01234567898765432100123456789876543210 :: Empty a0123456789876543210) t where type Traverse_0123456789876543210 :: forall a f b. (~>) a (f b) -> Empty a -> f (Empty b) type family Traverse_0123456789876543210 @a @f @b (a :: (~>) a (f b)) (a :: Empty a) :: f (Empty b) where diff --git a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden index b5824362..4c2b873f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden @@ -62,12 +62,12 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations type RightSym1 :: forall a b. b -> Either a b type family RightSym1 @a @b (a0123456789876543210 :: b) :: Either a b where RightSym1 a0123456789876543210 = Right a0123456789876543210 - type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) t where Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'True = Apply SuccSym0 (Apply SuccSym0 n) Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'False = n - type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n b where + type family Lambda_0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) n b where Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n b = Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 b - data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 + data Lambda_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) n0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 @@ -75,7 +75,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 + data Lambda_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) n0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 arg) => Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 @@ -83,14 +83,14 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 where + type family Lambda_0123456789876543210Sym2 (a_01234567898765432100123456789876543210 :: [Nat]) (a_01234567898765432100123456789876543210 :: [Bool]) n0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 - type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 t where + type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) t where Case_0123456789876543210 n b ns bs 'True = Apply SuccSym0 (Apply SuccSym0 n) Case_0123456789876543210 n b ns bs 'False = n - type family Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 n b where + type family Lambda_0123456789876543210 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) n b where Lambda_0123456789876543210 ns bs n b = Case_0123456789876543210 n b ns bs b - data Lambda_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 + data Lambda_0123456789876543210Sym0 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) n0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210) arg) (Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 arg) => Lambda_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 @@ -98,7 +98,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 ns0123456789876543210 bs0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 + data Lambda_0123456789876543210Sym1 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) n0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 n0123456789876543210) arg) (Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 arg) => Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 @@ -106,7 +106,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 ns0123456789876543210 bs0123456789876543210 n0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 where + type family Lambda_0123456789876543210Sym2 (ns0123456789876543210 :: [Nat]) (bs0123456789876543210 :: [Bool]) n0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym2 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 n0123456789876543210 b0123456789876543210 type EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat]) data EtadSym0 :: (~>) [Nat] ((~>) [Bool] [Nat]) diff --git a/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden b/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden index c1000eb8..c03040aa 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden @@ -29,11 +29,11 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations (Just d) foo3 :: a -> b -> a foo3 a b = (\case (p, _) -> p) (a, b) - type family Case_0123456789876543210 x_01234567898765432100123456789876543210 a0123456789876543210 b0123456789876543210 t where + type family Case_0123456789876543210 x_01234567898765432100123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) t where Case_0123456789876543210 x_0123456789876543210 a b '(p, _) = p - type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x_0123456789876543210 where + type family Lambda_0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) x_0123456789876543210 where Lambda_0123456789876543210 a b x_0123456789876543210 = Case_0123456789876543210 x_0123456789876543210 a b x_0123456789876543210 - data Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 @@ -41,14 +41,14 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x_01234567898765432100123456789876543210 d0123456789876543210 t where + type family Case_0123456789876543210 x_01234567898765432100123456789876543210 (d0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 x_0123456789876543210 d ('Just y) = y Case_0123456789876543210 x_0123456789876543210 d 'Nothing = d - type family Lambda_0123456789876543210 d0123456789876543210 x_0123456789876543210 where + type family Lambda_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) x_0123456789876543210 where Lambda_0123456789876543210 d x_0123456789876543210 = Case_0123456789876543210 x_0123456789876543210 d x_0123456789876543210 - data Lambda_0123456789876543210Sym0 d0123456789876543210 x_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (d0123456789876543210 :: a0123456789876543210) x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 d0123456789876543210) arg) (Lambda_0123456789876543210Sym1 d0123456789876543210 arg) => Lambda_0123456789876543210Sym0 d0123456789876543210 x_01234567898765432100123456789876543210 @@ -56,14 +56,14 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 d0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 d0123456789876543210 x_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (d0123456789876543210 :: a0123456789876543210) x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 d0123456789876543210 x_01234567898765432100123456789876543210 = Lambda_0123456789876543210 d0123456789876543210 x_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x_01234567898765432100123456789876543210 d0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 x_01234567898765432100123456789876543210 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) t where Case_0123456789876543210 x_0123456789876543210 d x ('Just y) = y Case_0123456789876543210 x_0123456789876543210 d x 'Nothing = d - type family Lambda_0123456789876543210 d0123456789876543210 x0123456789876543210 x_0123456789876543210 where + type family Lambda_0123456789876543210 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) x_0123456789876543210 where Lambda_0123456789876543210 d x x_0123456789876543210 = Case_0123456789876543210 x_0123456789876543210 d x x_0123456789876543210 - data Lambda_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210 x_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 d0123456789876543210 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210 x_01234567898765432100123456789876543210 @@ -71,7 +71,7 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 d0123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 d0123456789876543210 x0123456789876543210 x_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (d0123456789876543210 :: a0123456789876543210) (x0123456789876543210 :: Maybe a0123456789876543210) x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 d0123456789876543210 x0123456789876543210 x_01234567898765432100123456789876543210 = Lambda_0123456789876543210 d0123456789876543210 x0123456789876543210 x_01234567898765432100123456789876543210 type Foo3Sym0 :: (~>) a ((~>) b a) data Foo3Sym0 :: (~>) a ((~>) b a) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden index ccd92fb1..8ca09770 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden @@ -59,11 +59,11 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations type FooSym2 :: forall a b. a -> b -> Foo a b type family FooSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Foo a b where FooSym2 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (x0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 x (Foo a _) = a - type family Lambda_0123456789876543210 x0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (x0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 arg_01234567898765432100123456789876543210 @@ -71,13 +71,13 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: Foo a0123456789876543210 b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 x y '(_, b) = b - type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 @@ -85,13 +85,13 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 a0123456789876543210 b0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 x a b _ = x - type family Lambda_0123456789876543210 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 x a b arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x a b arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 a0123456789876543210 b0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 @@ -99,11 +99,11 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 a0123456789876543210 b0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x where + type family Lambda_0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) x where Lambda_0123456789876543210 a b x = Lambda_0123456789876543210Sym0 x a b - data Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 x0123456789876543210 @@ -111,11 +111,11 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (a0123456789876543210 :: a0123456789876543210) (b0123456789876543210 :: b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 x where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) x where Lambda_0123456789876543210 x y x = x - data Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 x0123456789876543210 @@ -123,14 +123,14 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 x0123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 z0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) (z0123456789876543210 :: c0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 arg_0123456789876543210 x y z '(_, _) = x - type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) (z0123456789876543210 :: c0123456789876543210) arg_0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x y z arg_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 arg_0123456789876543210 x y z (Apply (Apply Tuple2Sym0 arg_0123456789876543210) arg_0123456789876543210) - data Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) (z0123456789876543210 :: c0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 z0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 @@ -138,7 +138,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 z0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) (z0123456789876543210 :: c0123456789876543210) arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 @@ -146,11 +146,11 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym2 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) (z0123456789876543210 :: c0123456789876543210) arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 y where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) y where Lambda_0123456789876543210 x y = y - data Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) y0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 @@ -158,13 +158,13 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) y0123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 x y _ = x - type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 @@ -172,13 +172,13 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 x a_0123456789876543210 _ = x - type family Lambda_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 x a_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x a_0123456789876543210 arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 @@ -186,11 +186,11 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x y where + type family Lambda_0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) x y where Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 x y = x - data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 @@ -198,7 +198,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - data Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 + data Lambda_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) x0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym1KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 arg) => Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 @@ -206,7 +206,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) - type family Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 where + type family Lambda_0123456789876543210Sym2 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) x0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym2 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 type Foo8Sym0 :: (~>) (Foo a b) a data Foo8Sym0 :: (~>) (Foo a b) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden index 6a10b015..89d394d7 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden @@ -189,29 +189,29 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations foo13_ y = y foo14 :: Nat -> (Nat, Nat) foo14 x = let (y, z) = (Succ x, x) in (z, y) - type family Case_0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 (x0123456789876543210 :: Nat) t where Case_0123456789876543210 x '(_, y_0123456789876543210) = y_0123456789876543210 - type family Case_0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 (x0123456789876543210 :: Nat) t where Case_0123456789876543210 x '(y_0123456789876543210, _) = y_0123456789876543210 - type family Let0123456789876543210ZSym0 x0123456789876543210 where + type family Let0123456789876543210ZSym0 (x0123456789876543210 :: Nat) where Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210 - type family Let0123456789876543210YSym0 x0123456789876543210 where + type family Let0123456789876543210YSym0 (x0123456789876543210 :: Nat) where Let0123456789876543210YSym0 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210 - type family Let0123456789876543210X_0123456789876543210Sym0 x0123456789876543210 where + type family Let0123456789876543210X_0123456789876543210Sym0 (x0123456789876543210 :: Nat) where Let0123456789876543210X_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210X_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z x0123456789876543210 where + type family Let0123456789876543210Z (x0123456789876543210 :: Nat) where Let0123456789876543210Z x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym0 x) - type family Let0123456789876543210Y x0123456789876543210 where + type family Let0123456789876543210Y (x0123456789876543210 :: Nat) where Let0123456789876543210Y x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym0 x) - type family Let0123456789876543210X_0123456789876543210 x0123456789876543210 where + type family Let0123456789876543210X_0123456789876543210 (x0123456789876543210 :: Nat) where Let0123456789876543210X_0123456789876543210 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x - type family Let0123456789876543210BarSym0 a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + type family Let0123456789876543210BarSym0 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where Let0123456789876543210BarSym0 a0123456789876543210 x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + type family Let0123456789876543210Bar a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where Let0123456789876543210Bar a x = x - data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 :: (~>) Nat ((~>) Nat Nat) + data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) (x0123456789876543210 :: Nat) :: (~>) Nat ((~>) Nat Nat) where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 arg) => (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 a0123456789876543210 @@ -219,7 +219,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) ()) - data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 (a0123456789876543210 :: Nat) :: (~>) Nat Nat + data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: (~>) Nat Nat where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 arg) => (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 @@ -227,14 +227,14 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) ()) - type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 (a :: Nat) (a :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%) (x0123456789876543210 :: Nat) (a :: Nat) (a :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x) n) x) - type family Let0123456789876543210ZSym0 x0123456789876543210 :: Nat where + type family Let0123456789876543210ZSym0 (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210 - data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 :: (~>) Nat ((~>) Nat Nat) + data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) (x0123456789876543210 :: Nat) :: (~>) Nat ((~>) Nat Nat) where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 arg) => (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 a0123456789876543210 @@ -242,7 +242,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) ()) - data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 (a0123456789876543210 :: Nat) :: (~>) Nat Nat + data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: (~>) Nat Nat where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 arg) => (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 @@ -250,14 +250,14 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) ()) - type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210Z x0123456789876543210 :: Nat where + type family Let0123456789876543210Z (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210Z x = x - type family (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 (a :: Nat) (a :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%) (x0123456789876543210 :: Nat) (a :: Nat) (a :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x) n) m) - data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 :: (~>) Nat ((~>) Nat Nat) + data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) (x0123456789876543210 :: Nat) :: (~>) Nat ((~>) Nat Nat) where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 arg) => (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 a0123456789876543210 @@ -265,7 +265,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) ()) - data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 (a0123456789876543210 :: Nat) :: (~>) Nat Nat + data (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: (~>) Nat Nat where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) :: SameKind (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 arg) => (<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 @@ -273,14 +273,14 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$###) ()) - type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 (a :: Nat) (a :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%) (x0123456789876543210 :: Nat) (a :: Nat) (a :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$) x) n) m) - type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 x where + type family Lambda_0123456789876543210 (a_01234567898765432100123456789876543210 :: Nat) (x0123456789876543210 :: Nat) x where Lambda_0123456789876543210 a_0123456789876543210 x x = x - data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: Nat) (x0123456789876543210 :: Nat) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 @@ -288,9 +288,9 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: Nat) (x0123456789876543210 :: Nat) x0123456789876543210 where Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 x0123456789876543210 - data Let0123456789876543210ZSym0 x0123456789876543210 :: (~>) Nat Nat + data Let0123456789876543210ZSym0 (x0123456789876543210 :: Nat) :: (~>) Nat Nat where Let0123456789876543210ZSym0KindInference :: SameKind (Apply (Let0123456789876543210ZSym0 x0123456789876543210) arg) (Let0123456789876543210ZSym1 x0123456789876543210 arg) => Let0123456789876543210ZSym0 x0123456789876543210 a0123456789876543210 @@ -298,13 +298,13 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210ZSym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210ZSym0KindInference ()) - type family Let0123456789876543210ZSym1 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where + type family Let0123456789876543210ZSym1 (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210ZSym1 x0123456789876543210 a0123456789876543210 = Let0123456789876543210Z x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210Z x0123456789876543210 (a :: Nat) :: Nat where + type family Let0123456789876543210Z (x0123456789876543210 :: Nat) (a :: Nat) :: Nat where Let0123456789876543210Z x a_0123456789876543210 = Apply (Lambda_0123456789876543210Sym0 a_0123456789876543210 x) a_0123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 x where + type family Lambda_0123456789876543210 (x0123456789876543210 :: Nat) x where Lambda_0123456789876543210 x x = x - data Lambda_0123456789876543210Sym0 x0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: Nat) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 x0123456789876543210 @@ -312,17 +312,17 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: Nat) x0123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 x0123456789876543210 - type family Let0123456789876543210ZSym0 x0123456789876543210 :: Nat where + type family Let0123456789876543210ZSym0 (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210 - type family Let0123456789876543210Z x0123456789876543210 :: Nat where + type family Let0123456789876543210Z (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210Z x = Apply (Lambda_0123456789876543210Sym0 x) ZeroSym0 - type family Let0123456789876543210XSym0 x0123456789876543210 :: Nat where + type family Let0123456789876543210XSym0 (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210XSym0 x0123456789876543210 = Let0123456789876543210X x0123456789876543210 - type family Let0123456789876543210X x0123456789876543210 :: Nat where + type family Let0123456789876543210X (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210X x = ZeroSym0 - data Let0123456789876543210FSym0 x0123456789876543210 :: (~>) Nat Nat + data Let0123456789876543210FSym0 (x0123456789876543210 :: Nat) :: (~>) Nat Nat where Let0123456789876543210FSym0KindInference :: SameKind (Apply (Let0123456789876543210FSym0 x0123456789876543210) arg) (Let0123456789876543210FSym1 x0123456789876543210 arg) => Let0123456789876543210FSym0 x0123456789876543210 a0123456789876543210 @@ -330,19 +330,19 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210FSym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210FSym0KindInference ()) - type family Let0123456789876543210FSym1 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where + type family Let0123456789876543210FSym1 (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210FSym1 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210F x0123456789876543210 (a :: Nat) :: Nat where + type family Let0123456789876543210F (x0123456789876543210 :: Nat) (a :: Nat) :: Nat where Let0123456789876543210F x y = Apply SuccSym0 y - type family Let0123456789876543210ZSym0 x0123456789876543210 :: Nat where + type family Let0123456789876543210ZSym0 (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210ZSym0 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210 - type family Let0123456789876543210Z x0123456789876543210 :: Nat where + type family Let0123456789876543210Z (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210Z x = Apply (Let0123456789876543210FSym0 x) x - type family Let0123456789876543210ZSym0 y0123456789876543210 x0123456789876543210 :: Nat where + type family Let0123456789876543210ZSym0 (y0123456789876543210 :: Nat) (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210ZSym0 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: Nat where + type family Let0123456789876543210Z (y0123456789876543210 :: Nat) (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210Z y x = Apply SuccSym0 y - data Let0123456789876543210FSym0 x0123456789876543210 :: (~>) Nat Nat + data Let0123456789876543210FSym0 (x0123456789876543210 :: Nat) :: (~>) Nat Nat where Let0123456789876543210FSym0KindInference :: SameKind (Apply (Let0123456789876543210FSym0 x0123456789876543210) arg) (Let0123456789876543210FSym1 x0123456789876543210 arg) => Let0123456789876543210FSym0 x0123456789876543210 a0123456789876543210 @@ -350,11 +350,11 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210FSym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210FSym0KindInference ()) - type family Let0123456789876543210FSym1 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where + type family Let0123456789876543210FSym1 (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210FSym1 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210F x0123456789876543210 (a :: Nat) :: Nat where + type family Let0123456789876543210F (x0123456789876543210 :: Nat) (a :: Nat) :: Nat where Let0123456789876543210F x y = Apply SuccSym0 (Let0123456789876543210ZSym0 y x) - data Let0123456789876543210FSym0 x0123456789876543210 :: (~>) Nat Nat + data Let0123456789876543210FSym0 (x0123456789876543210 :: Nat) :: (~>) Nat Nat where Let0123456789876543210FSym0KindInference :: SameKind (Apply (Let0123456789876543210FSym0 x0123456789876543210) arg) (Let0123456789876543210FSym1 x0123456789876543210 arg) => Let0123456789876543210FSym0 x0123456789876543210 a0123456789876543210 @@ -362,13 +362,13 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210FSym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210FSym0KindInference ()) - type family Let0123456789876543210FSym1 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where + type family Let0123456789876543210FSym1 (x0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210FSym1 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210F x0123456789876543210 (a :: Nat) :: Nat where + type family Let0123456789876543210F (x0123456789876543210 :: Nat) (a :: Nat) :: Nat where Let0123456789876543210F x y = Apply SuccSym0 y - type family Let0123456789876543210YSym0 x0123456789876543210 :: Nat where + type family Let0123456789876543210YSym0 (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210YSym0 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210 - type family Let0123456789876543210Y x0123456789876543210 :: Nat where + type family Let0123456789876543210Y (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210Y x = Apply SuccSym0 x type family Let0123456789876543210ZSym0 where Let0123456789876543210ZSym0 = Let0123456789876543210Z @@ -378,9 +378,9 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations Let0123456789876543210Z = Apply SuccSym0 Let0123456789876543210YSym0 type family Let0123456789876543210Y where Let0123456789876543210Y = Apply SuccSym0 ZeroSym0 - type family Let0123456789876543210YSym0 x0123456789876543210 :: Nat where + type family Let0123456789876543210YSym0 (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210YSym0 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210 - type family Let0123456789876543210Y x0123456789876543210 :: Nat where + type family Let0123456789876543210Y (x0123456789876543210 :: Nat) :: Nat where Let0123456789876543210Y x = Apply SuccSym0 ZeroSym0 type Foo14Sym0 :: (~>) Nat (Nat, Nat) data Foo14Sym0 :: (~>) Nat (Nat, Nat) diff --git a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden index 668699c8..77c1c34e 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden @@ -188,7 +188,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations foo2 t@(# x, y #) = case t of (# a, b #) -> (\ _ -> a) b silly :: a -> () silly x = case x of _ -> () - type family Case_0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 x _ = Tuple0Sym0 type family Let0123456789876543210TSym0 x0123456789876543210 y0123456789876543210 where Let0123456789876543210TSym0 x0123456789876543210 y0123456789876543210 = Let0123456789876543210T x0123456789876543210 y0123456789876543210 diff --git a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden index fd62e9f6..5bad23c9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden @@ -103,10 +103,10 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations instance PBounded S where type MinBound = MinBound_0123456789876543210 type MaxBound = MaxBound_0123456789876543210 - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = S2Sym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = S1Sym0 Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 1)) type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> S diff --git a/singletons-base/tests/compile-and-dump/Singletons/T136.golden b/singletons-base/tests/compile-and-dump/Singletons/T136.golden index fd182d37..27f7452d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136.golden @@ -39,13 +39,13 @@ Singletons/T136.hs:(0,0)-(0,0): Splicing declarations Pred_0123456789876543210 '[] = Apply ErrorSym0 "pred 0" Pred_0123456789876543210 ('(:) 'False as) = Apply (Apply (:@#@$) TrueSym0) (Apply PredSym0 as) Pred_0123456789876543210 ('(:) 'True as) = Apply (Apply (:@#@$) FalseSym0) as - type family Case_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 i arg_0123456789876543210 'True = NilSym0 Case_0123456789876543210 i arg_0123456789876543210 'False = Apply SuccSym0 (Apply ToEnumSym0 (Apply PredSym0 i)) - type family Case_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 i0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 i arg_0123456789876543210 'True = Apply ErrorSym0 "negative toEnum" Case_0123456789876543210 i arg_0123456789876543210 'False = Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (==@#@$) i) (FromInteger 0)) - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (arg_01234567898765432100123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 arg_0123456789876543210 i = Case_0123456789876543210 i arg_0123456789876543210 (Apply (Apply (<@#@$) i) (FromInteger 0)) type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> [Bool] diff --git a/singletons-base/tests/compile-and-dump/Singletons/T150.golden b/singletons-base/tests/compile-and-dump/Singletons/T150.golden index 855b977b..5d705000 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T150.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T150.golden @@ -148,7 +148,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations type ObjSym1 :: a -> Obj type family ObjSym1 @a (a0123456789876543210 :: a) :: Obj where ObjSym1 a0123456789876543210 = Obj a0123456789876543210 - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: Fin n0123456789876543210) t where type TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c)) data TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c)) where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T160.golden b/singletons-base/tests/compile-and-dump/Singletons/T160.golden index 85c177ca..edd35549 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T160.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T160.golden @@ -5,11 +5,11 @@ Singletons/T160.hs:(0,0)-(0,0): Splicing declarations ======> foo :: (Num a, Eq a) => a -> a foo x = if (x == 0) then 1 else (typeError $ ShowType x) - type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) where Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) where Let0123456789876543210Scrutinee_0123456789876543210 x = Apply (Apply (==@#@$) x) (FromInteger 0) - type family Case_0123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 x 'True = FromInteger 1 Case_0123456789876543210 x 'False = Apply (Apply ($@#@$) TypeErrorSym0) (Apply ShowTypeSym0 x) type FooSym0 :: (~>) a a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T166.golden b/singletons-base/tests/compile-and-dump/Singletons/T166.golden index c6c415de..45eb93dd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T166.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T166.golden @@ -44,9 +44,9 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations type FooSym1 :: forall a. a -> [Bool] type family FooSym1 @a (a0123456789876543210 :: a) :: [Bool] where FooSym1 a0123456789876543210 = Foo a0123456789876543210 - type family Lambda_0123456789876543210 a0123456789876543210 x0123456789876543210 s where + type family Lambda_0123456789876543210 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) s where Lambda_0123456789876543210 a x s = Apply (Apply (Apply FoosPrecSym0 (FromInteger 0)) x) s - data Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 s0123456789876543210 + data Lambda_0123456789876543210Sym0 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) s0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 s0123456789876543210 @@ -54,7 +54,7 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 s0123456789876543210 where + type family Lambda_0123456789876543210Sym1 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) s0123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 s0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 x0123456789876543210 s0123456789876543210 type Foo_0123456789876543210 :: forall a. a -> [Bool] type family Foo_0123456789876543210 @a (a :: a) :: [Bool] where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T176.golden b/singletons-base/tests/compile-and-dump/Singletons/T176.golden index 7a2105ee..5c5b4d1e 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T176.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T176.golden @@ -22,11 +22,11 @@ Singletons/T176.hs:(0,0)-(0,0): Splicing declarations baz2 :: a quux2 :: Foo2 a => a -> a quux2 x = (x `bar2` baz2) - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (x0123456789876543210 :: a0123456789876543210) t where Case_0123456789876543210 arg_0123456789876543210 x _ = Baz1Sym0 - type family Lambda_0123456789876543210 x0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) arg_0123456789876543210 where Lambda_0123456789876543210 x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 x0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 arg_01234567898765432100123456789876543210 @@ -34,7 +34,7 @@ Singletons/T176.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 type Quux2Sym0 :: (~>) a a data Quux2Sym0 :: (~>) a a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T183.golden b/singletons-base/tests/compile-and-dump/Singletons/T183.golden index 55105eb9..3b690c91 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T183.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T183.golden @@ -59,7 +59,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations g :: a -> b -> a g y _ = y in g x () - data Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210) + data Let0123456789876543210GSym0 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) :: (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210) where Let0123456789876543210GSym0KindInference :: SameKind (Apply (Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210) arg) (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 arg) => Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210 a0123456789876543210 @@ -67,7 +67,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210GSym0 a0123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym0KindInference ()) - data Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 a0123456789876543210 + data Let0123456789876543210GSym1 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 a0123456789876543210 where Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 a0123456789876543210 arg) => Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 @@ -75,13 +75,13 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym1KindInference ()) - type family Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: a0123456789876543210 where + type family Let0123456789876543210GSym2 a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: a0123456789876543210 where Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210G a0123456789876543210 x0123456789876543210 (a :: a0123456789876543210) (a :: b) :: a0123456789876543210 where + type family Let0123456789876543210G a0123456789876543210 (x0123456789876543210 :: a0123456789876543210) (a :: a0123456789876543210) (a :: b) :: a0123456789876543210 where Let0123456789876543210G a x y _ = y - type family Let0123456789876543210XSym0 a0123456789876543210 wild_01234567898765432100123456789876543210 where + type family Let0123456789876543210XSym0 a0123456789876543210 (wild_01234567898765432100123456789876543210 :: a0123456789876543210) where Let0123456789876543210XSym0 a0123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210X a0123456789876543210 wild_01234567898765432100123456789876543210 - type family Let0123456789876543210X a0123456789876543210 wild_01234567898765432100123456789876543210 where + type family Let0123456789876543210X a0123456789876543210 (wild_01234567898765432100123456789876543210 :: a0123456789876543210) where Let0123456789876543210X a wild_0123456789876543210 = Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a type family Let0123456789876543210XSym0 a0123456789876543210 where Let0123456789876543210XSym0 a0123456789876543210 = Let0123456789876543210X a0123456789876543210 @@ -93,12 +93,15 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations Let0123456789876543210Scrutinee_0123456789876543210 a x = x :: Maybe a type family Case_0123456789876543210 a0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 a x ('Just (y :: a) :: Maybe a) = Apply JustSym0 (Apply JustSym0 (y :: a) :: Maybe a) - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (a_01234567898765432100123456789876543210 :: (a0123456789876543210, + b0123456789876543210)) t where Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 '(x :: a, y :: b) = Apply (Apply Tuple2Sym0 (y :: b)) (x :: a) - type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (a_01234567898765432100123456789876543210 :: (a0123456789876543210, + b0123456789876543210)) arg_0123456789876543210 where Lambda_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: (a0123456789876543210, + b0123456789876543210)) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 @@ -106,7 +109,8 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: (a0123456789876543210, + b0123456789876543210)) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T184.golden b/singletons-base/tests/compile-and-dump/Singletons/T184.golden index e11f4865..c94946a5 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T184.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T184.golden @@ -25,9 +25,9 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations cartProd xs ys = [(x, y) | x <- xs, y <- ys] trues :: [Bool] -> [Bool] trues xs = [x | x <- xs, x] - type family Lambda_0123456789876543210 xs0123456789876543210 x where + type family Lambda_0123456789876543210 (xs0123456789876543210 :: [Bool]) x where Lambda_0123456789876543210 xs x = Apply (Apply (>>@#@$) (Apply GuardSym0 x)) (Apply ReturnSym0 x) - data Lambda_0123456789876543210Sym0 xs0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (xs0123456789876543210 :: [Bool]) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 xs0123456789876543210) arg) (Lambda_0123456789876543210Sym1 xs0123456789876543210 arg) => Lambda_0123456789876543210Sym0 xs0123456789876543210 x0123456789876543210 @@ -35,11 +35,11 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 xs0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 xs0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (xs0123456789876543210 :: [Bool]) x0123456789876543210 where Lambda_0123456789876543210Sym1 xs0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y where + type family Lambda_0123456789876543210 x0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) y where Lambda_0123456789876543210 x xs ys y = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y) - data Lambda_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 + data Lambda_0123456789876543210Sym0 x0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) y0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg) => Lambda_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 @@ -47,11 +47,11 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 x0123456789876543210 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 where + type family Lambda_0123456789876543210Sym1 x0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) y0123456789876543210 where Lambda_0123456789876543210Sym1 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 - type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x where + type family Lambda_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) x where Lambda_0123456789876543210 xs ys x = Apply (Apply (>>=@#@$) ys) (Lambda_0123456789876543210Sym0 x xs ys) - data Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) => Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 @@ -59,11 +59,11 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) x0123456789876543210 where Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x where + type family Lambda_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) x where Lambda_0123456789876543210 xs ys x = Apply ReturnSym0 x - data Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) => Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 @@ -71,11 +71,11 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) x0123456789876543210 where Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y where + type family Lambda_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) y where Lambda_0123456789876543210 xs ys y = Apply ReturnSym0 y - data Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 + data Lambda_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) y0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) => Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 @@ -83,14 +83,14 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) y0123456789876543210 where Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 - type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 xs0123456789876543210 ys0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) t where Case_0123456789876543210 arg_0123456789876543210 xs ys '(x, y) = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y) - type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) arg_0123456789876543210 where Lambda_0123456789876543210 xs ys arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 xs ys arg_0123456789876543210 - data Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 + data Lambda_0123456789876543210Sym0 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) arg) (Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg) => Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 @@ -98,11 +98,11 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 xs0123456789876543210 ys0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 where + type family Lambda_0123456789876543210Sym1 (xs0123456789876543210 :: [a0123456789876543210]) (ys0123456789876543210 :: [b0123456789876543210]) arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym1 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b where + type family Lambda_0123456789876543210 a0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) b where Lambda_0123456789876543210 a ma mb b = Apply (Apply (>>@#@$) (Apply GuardSym0 b)) (Apply ReturnSym0 a) - data Lambda_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 + data Lambda_0123456789876543210Sym0 a0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) b0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 @@ -110,11 +110,11 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 ma0123456789876543210 mb0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 where + type family Lambda_0123456789876543210Sym1 a0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) b0123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 - type family Lambda_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a where + type family Lambda_0123456789876543210 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a where Lambda_0123456789876543210 ma mb a = Apply (Apply (>>=@#@$) mb) (Lambda_0123456789876543210Sym0 a ma mb) - data Lambda_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 + data Lambda_0123456789876543210Sym0 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210) arg) (Lambda_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210 arg) => Lambda_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 @@ -122,7 +122,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 ma0123456789876543210 mb0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (ma0123456789876543210 :: Maybe a0123456789876543210) (mb0123456789876543210 :: Maybe Bool) a0123456789876543210 where Lambda_0123456789876543210Sym1 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 = Lambda_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a0123456789876543210 type TruesSym0 :: (~>) [Bool] [Bool] data TruesSym0 :: (~>) [Bool] [Bool] diff --git a/singletons-base/tests/compile-and-dump/Singletons/T190.golden b/singletons-base/tests/compile-and-dump/Singletons/T190.golden index f51bab20..5724a319 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T190.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T190.golden @@ -20,7 +20,7 @@ Singletons/T190.hs:0:0:: Splicing declarations Compare_0123456789876543210 T T = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0 instance POrd T where type Compare a a = Compare_0123456789876543210 a a - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = TSym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> T diff --git a/singletons-base/tests/compile-and-dump/Singletons/T287.golden b/singletons-base/tests/compile-and-dump/Singletons/T287.golden index e83654c2..0b9593d9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T287.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T287.golden @@ -31,9 +31,9 @@ Singletons/T287.hs:(0,0)-(0,0): Splicing declarations (<<>>@#@$$$) a0123456789876543210 a0123456789876543210 = (<<>>) a0123456789876543210 a0123456789876543210 class PS a where type family (<<>>) (arg :: a) (arg :: a) :: a - type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 x where + type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 (f0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (g0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) x where Lambda_0123456789876543210 a b f g x = Apply (Apply (<<>>@#@$) (Apply f x)) (Apply g x) - data Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 (f0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (g0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 x0123456789876543210 @@ -41,7 +41,7 @@ Singletons/T287.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 (f0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) (g0123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) x0123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 f0123456789876543210 g0123456789876543210 x0123456789876543210 type TFHelper_0123456789876543210 :: forall a b. (~>) a b -> (~>) a b -> (~>) a b diff --git a/singletons-base/tests/compile-and-dump/Singletons/T312.golden b/singletons-base/tests/compile-and-dump/Singletons/T312.golden index 1b46afcb..ec7b5bef 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T312.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T312.golden @@ -60,7 +60,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations type Bar_0123456789876543210 :: forall a b. a -> b -> b type family Bar_0123456789876543210 @a @b (a :: a) (a :: b) :: b where Bar_0123456789876543210 @a @b (_ :: a) (x :: b) = x - data Let0123456789876543210HSym0 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 :: (~>) c0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210) + data Let0123456789876543210HSym0 a0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) :: (~>) c0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210) where Let0123456789876543210HSym0KindInference :: SameKind (Apply (Let0123456789876543210HSym0 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) arg) (Let0123456789876543210HSym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 arg) => Let0123456789876543210HSym0 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 @@ -68,7 +68,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210HSym0 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210HSym0KindInference ()) - data Let0123456789876543210HSym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a0123456789876543210 :: c0123456789876543210) :: (~>) b0123456789876543210 b0123456789876543210 + data Let0123456789876543210HSym1 a0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) (a0123456789876543210 :: c0123456789876543210) :: (~>) b0123456789876543210 b0123456789876543210 where Let0123456789876543210HSym1KindInference :: SameKind (Apply (Let0123456789876543210HSym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210) arg) (Let0123456789876543210HSym2 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 arg) => Let0123456789876543210HSym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 @@ -76,9 +76,9 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210HSym1 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210HSym1KindInference ()) - type family Let0123456789876543210HSym2 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a0123456789876543210 :: c0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: b0123456789876543210 where + type family Let0123456789876543210HSym2 a0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) (a0123456789876543210 :: c0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: b0123456789876543210 where Let0123456789876543210HSym2 a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210H a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210H a0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a :: c) (a :: b0123456789876543210) :: b0123456789876543210 where + type family Let0123456789876543210H a0123456789876543210 b0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) (a_01234567898765432100123456789876543210 :: b0123456789876543210) (a :: c) (a :: b0123456789876543210) :: b0123456789876543210 where Let0123456789876543210H a b a_0123456789876543210 a_0123456789876543210 (_ :: c) (x :: b) = x type Baz_0123456789876543210 :: forall a b. a -> b -> b type family Baz_0123456789876543210 @a @b (a :: a) (a :: b) :: b where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T433.golden b/singletons-base/tests/compile-and-dump/Singletons/T433.golden index 904ca780..6adcc054 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T433.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T433.golden @@ -75,7 +75,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations where g :: b -> a -> b g y _ = y - data Let0123456789876543210GSym0 x0123456789876543210 :: (~>) b0123456789876543210 ((~>) a0123456789876543210 b0123456789876543210) + data Let0123456789876543210GSym0 (x0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 ((~>) a0123456789876543210 b0123456789876543210) where Let0123456789876543210GSym0KindInference :: SameKind (Apply (Let0123456789876543210GSym0 x0123456789876543210) arg) (Let0123456789876543210GSym1 x0123456789876543210 arg) => Let0123456789876543210GSym0 x0123456789876543210 a0123456789876543210 @@ -83,7 +83,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210GSym0 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym0KindInference ()) - data Let0123456789876543210GSym1 x0123456789876543210 (a0123456789876543210 :: b0123456789876543210) :: (~>) a0123456789876543210 b0123456789876543210 + data Let0123456789876543210GSym1 (x0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: (~>) a0123456789876543210 b0123456789876543210 where Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 arg) => Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210 a0123456789876543210 @@ -91,21 +91,21 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym1KindInference ()) - type family Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: b0123456789876543210) (a0123456789876543210 :: a0123456789876543210) :: b0123456789876543210 where + type family Let0123456789876543210GSym2 (x0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) (a0123456789876543210 :: a0123456789876543210) :: b0123456789876543210 where Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210G x0123456789876543210 (a :: b) (a :: a) :: b where + type family Let0123456789876543210G (x0123456789876543210 :: a0123456789876543210) (a :: b) (a :: a) :: b where Let0123456789876543210G x y _ = y - type family Let0123456789876543210GSym0 b0123456789876543210 x0123456789876543210 where + type family Let0123456789876543210GSym0 b0123456789876543210 (x0123456789876543210 :: b0123456789876543210) where Let0123456789876543210GSym0 b0123456789876543210 x0123456789876543210 = Let0123456789876543210G b0123456789876543210 x0123456789876543210 - type family Let0123456789876543210G b0123456789876543210 x0123456789876543210 where + type family Let0123456789876543210G b0123456789876543210 (x0123456789876543210 :: b0123456789876543210) where Let0123456789876543210G b x = x :: b - type family Let0123456789876543210GSym0 b0123456789876543210 x0123456789876543210 where + type family Let0123456789876543210GSym0 b0123456789876543210 (x0123456789876543210 :: b0123456789876543210) where Let0123456789876543210GSym0 b0123456789876543210 x0123456789876543210 = Let0123456789876543210G b0123456789876543210 x0123456789876543210 - type family Let0123456789876543210G b0123456789876543210 x0123456789876543210 where + type family Let0123456789876543210G b0123456789876543210 (x0123456789876543210 :: b0123456789876543210) where Let0123456789876543210G b x = x :: b - type family Let0123456789876543210GSym0 a0123456789876543210 a_01234567898765432100123456789876543210 where + type family Let0123456789876543210GSym0 a0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) where Let0123456789876543210GSym0 a0123456789876543210 a_01234567898765432100123456789876543210 = Let0123456789876543210G a0123456789876543210 a_01234567898765432100123456789876543210 - type family Let0123456789876543210G a0123456789876543210 a_01234567898765432100123456789876543210 where + type family Let0123456789876543210G a0123456789876543210 (a_01234567898765432100123456789876543210 :: a0123456789876543210) where Let0123456789876543210G a a_0123456789876543210 = IdSym0 :: (~>) a a data Let0123456789876543210GSym0 local0123456789876543210 :: (~>) a0123456789876543210 a0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T445.golden b/singletons-base/tests/compile-and-dump/Singletons/T445.golden index ae0562bf..62340b25 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T445.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T445.golden @@ -21,9 +21,9 @@ Singletons/T445.hs:(0,0)-(0,0): Splicing declarations filterEvenGt7 :: [Nat] -> [Nat] filterEvenGt7 = filter (\ x -> evenb x && x > lit 7) |] ======> - type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x where + type family Lambda_0123456789876543210 (a_01234567898765432100123456789876543210 :: [Nat]) x where Lambda_0123456789876543210 a_0123456789876543210 x = Apply (Apply (&&@#@$) (Apply EvenbSym0 x)) (Apply (Apply (>@#@$) x) (Apply LitSym0 (FromInteger 7))) - data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 x0123456789876543210 + data Lambda_0123456789876543210Sym0 (a_01234567898765432100123456789876543210 :: [Nat]) x0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210) arg) (Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 arg) => Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 x0123456789876543210 @@ -31,7 +31,7 @@ Singletons/T445.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210 where + type family Lambda_0123456789876543210Sym1 (a_01234567898765432100123456789876543210 :: [Nat]) x0123456789876543210 where Lambda_0123456789876543210Sym1 a_01234567898765432100123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 type FilterEvenGt7Sym0 :: (~>) [Nat] [Nat] data FilterEvenGt7Sym0 :: (~>) [Nat] [Nat] diff --git a/singletons-base/tests/compile-and-dump/Singletons/T54.golden b/singletons-base/tests/compile-and-dump/Singletons/T54.golden index 31ff7828..1712127d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T54.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T54.golden @@ -5,11 +5,11 @@ Singletons/T54.hs:(0,0)-(0,0): Splicing declarations ======> g :: Bool -> Bool g e = (case [not] of [_] -> not) e - type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 e0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210Sym0 (e0123456789876543210 :: Bool) where Let0123456789876543210Scrutinee_0123456789876543210Sym0 e0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 e0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 e0123456789876543210 where + type family Let0123456789876543210Scrutinee_0123456789876543210 (e0123456789876543210 :: Bool) where Let0123456789876543210Scrutinee_0123456789876543210 e = Apply (Apply (:@#@$) NotSym0) NilSym0 - type family Case_0123456789876543210 e0123456789876543210 t where + type family Case_0123456789876543210 (e0123456789876543210 :: Bool) t where Case_0123456789876543210 e '[_] = NotSym0 type GSym0 :: (~>) Bool Bool data GSym0 :: (~>) Bool Bool diff --git a/singletons-base/tests/compile-and-dump/Singletons/T581.golden b/singletons-base/tests/compile-and-dump/Singletons/T581.golden index ab69c130..39301c1f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T581.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T581.golden @@ -130,9 +130,9 @@ Singletons/T581.hs:(0,0)-(0,0): Splicing declarations M2_0123456789876543210 @b @a (_ :: b) = NothingSym0 :: Maybe (Maybe a) instance PC2 (Maybe a) where type M2 a = M2_0123456789876543210 a - type family Lambda_0123456789876543210 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx where + type family Lambda_0123456789876543210 a0123456789876543210 (x0123456789876543210 :: Maybe a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) xx where Lambda_0123456789876543210 a x y xx = xx :: a - data Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 + data Lambda_0123456789876543210Sym0 a0123456789876543210 (x0123456789876543210 :: Maybe a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) xx0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 @@ -140,7 +140,7 @@ Singletons/T581.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 where + type family Lambda_0123456789876543210Sym1 a0123456789876543210 (x0123456789876543210 :: Maybe a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) xx0123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 type M3_0123456789876543210 :: forall a b. Maybe a -> b -> (Maybe a, b) @@ -149,9 +149,9 @@ Singletons/T581.hs:(0,0)-(0,0): Splicing declarations M3_0123456789876543210 @a @b (x :: Maybe a) (y :: b) = Apply (Apply Tuple2Sym0 (Apply (Apply FmapSym0 (Lambda_0123456789876543210Sym0 a x y)) x)) y instance PC3 (Maybe a) where type M3 a a = M3_0123456789876543210 a a - type family Lambda_0123456789876543210 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx where + type family Lambda_0123456789876543210 a0123456789876543210 (x0123456789876543210 :: [a0123456789876543210]) (y0123456789876543210 :: b0123456789876543210) xx where Lambda_0123456789876543210 a x y xx = xx :: a - data Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 + data Lambda_0123456789876543210Sym0 a0123456789876543210 (x0123456789876543210 :: [a0123456789876543210]) (y0123456789876543210 :: b0123456789876543210) xx0123456789876543210 where Lambda_0123456789876543210Sym0KindInference :: SameKind (Apply (Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210) arg) (Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 y0123456789876543210 arg) => Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 @@ -159,7 +159,7 @@ Singletons/T581.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Lambda_0123456789876543210Sym0 a0123456789876543210 x0123456789876543210 y0123456789876543210) where suppressUnusedWarnings = snd ((,) Lambda_0123456789876543210Sym0KindInference ()) - type family Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 where + type family Lambda_0123456789876543210Sym1 a0123456789876543210 (x0123456789876543210 :: [a0123456789876543210]) (y0123456789876543210 :: b0123456789876543210) xx0123456789876543210 where Lambda_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 x0123456789876543210 y0123456789876543210 xx0123456789876543210 type M3_0123456789876543210 :: forall a b. [a] -> b -> ([a], b) type family M3_0123456789876543210 @a @b (a :: [a]) (a :: b) :: ([a], diff --git a/singletons-base/tests/compile-and-dump/Singletons/T89.golden b/singletons-base/tests/compile-and-dump/Singletons/T89.golden index a2097f46..3f1dbc91 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T89.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T89.golden @@ -10,7 +10,7 @@ Singletons/T89.hs:0:0:: Splicing declarations type FooSym0 :: Foo type family FooSym0 :: Foo where FooSym0 = Foo - type family Case_0123456789876543210 n0123456789876543210 t where + type family Case_0123456789876543210 (n0123456789876543210 :: GHC.Num.Natural.Natural) t where Case_0123456789876543210 n 'True = FooSym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 (FromString "toEnum: bad argument") type ToEnum_0123456789876543210 :: GHC.Num.Natural.Natural -> Foo diff --git a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden index 21dec653..59d26bfe 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden @@ -124,16 +124,16 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations Case_0123456789876543210 ('Bar _ y_0123456789876543210) = y_0123456789876543210 type family Case_0123456789876543210 t where Case_0123456789876543210 ('Bar y_0123456789876543210 _) = y_0123456789876543210 - type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (a_01234567898765432100123456789876543210 :: Bool) t where Case_0123456789876543210 a_0123456789876543210 '(_, y_0123456789876543210) = y_0123456789876543210 - type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (a_01234567898765432100123456789876543210 :: Bool) t where Case_0123456789876543210 a_0123456789876543210 '(y_0123456789876543210, _) = y_0123456789876543210 - type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (a_01234567898765432100123456789876543210 :: Bool) t where Case_0123456789876543210 a_0123456789876543210 '[_, y_0123456789876543210] = y_0123456789876543210 - type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where + type family Case_0123456789876543210 (a_01234567898765432100123456789876543210 :: Bool) t where Case_0123456789876543210 a_0123456789876543210 '[y_0123456789876543210, _] = y_0123456789876543210 type MSym0 :: Bool diff --git a/singletons-th/singletons-th.cabal b/singletons-th/singletons-th.cabal index 7f6aec1e..28e72277 100644 --- a/singletons-th/singletons-th.cabal +++ b/singletons-th/singletons-th.cabal @@ -94,6 +94,7 @@ library Data.Singletons.TH.Single.Ord Data.Singletons.TH.Single.Type Data.Singletons.TH.Syntax + Data.Singletons.TH.Syntax.LocalVar Data.Singletons.TH.Util -- singletons re-exports diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 41ca17e2..bf6d2af7 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -218,7 +218,7 @@ promoteLetDecs mb_let_uniq decls = do binds :: [LetBind] binds = - [ (name, foldType (DConT sym) (map DVarT locals)) + [ (name, foldTypeLocalVars (DConT sym) locals) | (name, (pro_name, locals)) <- let_dec_proms , let sym = defunctionalizedName0 opts pro_name ] (decs, let_dec_env') <- letBind binds $ promoteLetDecEnv mb_let_uniq let_dec_env @@ -965,7 +965,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do UFunction clauses -> promote_function_rhs all_locals clauses where -- Promote the RHS of a UFunction (or a UValue with a function type). - promote_function_rhs :: [Name] + promote_function_rhs :: [LocalVar] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS) promote_function_rhs all_locals clauses = do numArgs <- count_args clauses @@ -983,7 +983,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do -- -- * For UFunctions, `prom_a` is [DTySynEqn] and `a` is [DClause]. promote_let_dec_rhs - :: [Name] -- Local variables bound in this scope + :: [LocalVar] -- Local variables bound in this scope -> Maybe LetDecRHSKindInfo -- Information about the promoted kind (if present) -> Int -- The number of promoted function arguments -> PrM (prom_a, a) -- Promote the RHS @@ -1052,7 +1052,8 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do , defun_decs , mk_alet_dec_rhs thing ) - promote_let_dec_ty :: [Name] -- The local variables that the let-dec closes + promote_let_dec_ty :: [LocalVar] + -- The local variables that the let-dec closes -- over. If this is non-empty, we cannot -- produce a standalone kind signature. -- See Note [No SAKs for let-decs with local variables] @@ -1281,13 +1282,24 @@ promoteClause :: Maybe Uniq -- ^ Name of the function being promoted -> Maybe LetDecRHSKindInfo -- ^ Information about the promoted kind (if present) - -> [Name] + -> [LocalVar] -- ^ The local variables currently in scope -> DClause -> PrM (DTySynEqn, ADClause) promoteClause mb_let_uniq name m_ldrki all_locals (DClause pats exp) = do - -- promoting the patterns creates variable bindings. These are passed - -- to the function promoted the RHS - ((types, pats'), prom_pat_infos) <- evalForPair $ mapAndUnzipM promotePat pats + -- First, check to see if we know the kinds of the patterns in the clause... + let m_kinds = fmap (\(LDRKI _ _ _ kinds _) -> kinds) m_ldrki + -- ...if so, use these kinds when promoting the patterns to the type level. + -- Promoting patterns can create LocalVars, and these LocalVars are brought + -- into scope when promoting the RHS of the clause. Recording the kinds of + -- each LocalVar will make the lambda-lifted code more precise. (See + -- Note [Local variables and kind information] in + -- D.S.TH.Promote.Syntax.LocalVar.) + ((types, pats'), prom_pat_infos) <- evalForPair $ + case m_kinds of + Just kinds -> + unzip <$> zipWithM (\kind -> promotePat (Just kind)) kinds pats + Nothing -> + mapAndUnzipM (promotePat Nothing) pats -- If the function has scoped type variables, then we annotate each argument -- in the promoted type family equation with its kind. -- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad for an @@ -1315,7 +1327,7 @@ promoteMatch :: DType -- What to use as the LHS of the promoted type family promoteMatch pro_case_fun (DMatch pat exp) = do -- promoting the patterns creates variable bindings. These are passed -- to the function promoted the RHS - ((ty, pat'), prom_pat_infos) <- evalForPair $ promotePat pat + ((ty, pat'), prom_pat_infos) <- evalForPair $ promotePat Nothing pat let PromDPatInfos { prom_dpat_vars = new_vars , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos (rhs, ann_exp) <- scopedBind sig_kvs $ @@ -1324,18 +1336,28 @@ promoteMatch pro_case_fun (DMatch pat exp) = do return $ ( DTySynEqn Nothing (pro_case_fun `DAppT` ty) rhs , ADMatch new_vars pat' ann_exp) --- promotes a term pattern into a type pattern, accumulating bound variable names -promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat) -promotePat (DLitP lit) = (, ADLitP lit) <$> promoteLitPat lit -promotePat (DVarP name) = do +-- | Promote a term pattern into a type pattern, accumulating bound variable +-- names in 'PromDPatInfos'. +promotePat :: + Maybe DKind + -- ^ The kind of the pattern ('Just' if known, 'Nothing' if unknown). When + -- the kind is known, we can record a 'LocalVar' for variable patterns (see + -- the 'DVarP' case below) that includes more precise kind information. See + -- @Note [Local variables and kind information] (Wrinkle: Binding positions + -- versus argument positions)@ in + -- "Data.Singletons.TH.Promote.Syntax.LocalVar" for more information. + -> DPat + -> QWithAux PromDPatInfos PrM (DType, ADPat) +promotePat _ (DLitP lit) = (, ADLitP lit) <$> promoteLitPat lit +promotePat m_ki (DVarP name) = do -- term vars can be symbols... type vars can't! tyName <- mkTyName name - tell $ PromDPatInfos [(name, tyName)] OSet.empty + tell $ PromDPatInfos [(name, (tyName, m_ki))] OSet.empty return (DVarT tyName, ADVarP name) -promotePat (DConP name tys pats) = do +promotePat _ (DConP name tys pats) = do opts <- getOptions kis <- traverse (promoteType_options conOptions) tys - (types, pats') <- mapAndUnzipM promotePat pats + (types, pats') <- mapAndUnzipM (promotePat Nothing) pats let name' = promotedDataTypeOrConName opts name return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats') where @@ -1344,24 +1366,24 @@ promotePat (DConP name tys pats) = do -- will produce code that GHC will accept. conOptions :: PromoteTypeOptions conOptions = defaultPromoteTypeOptions{ptoAllowWildcards = True} -promotePat (DTildeP pat) = do +promotePat m_ki (DTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern in promotion" - second ADTildeP <$> promotePat pat -promotePat (DBangP pat) = do + second ADTildeP <$> promotePat m_ki pat +promotePat m_ki (DBangP pat) = do qReportWarning "Strict pattern converted into regular pattern in promotion" - second ADBangP <$> promotePat pat -promotePat (DSigP pat ty) = do + second ADBangP <$> promotePat m_ki pat +promotePat _ (DSigP pat ty) = do -- We must maintain the invariant that any promoted pattern signature must -- not have any wildcards in the underlying pattern. -- See Note [Singling pattern signatures]. wildless_pat <- removeWilds pat - (promoted, pat') <- promotePat wildless_pat ki <- promoteType ty + (promoted, pat') <- promotePat (Just ki) wildless_pat tell $ PromDPatInfos [] (fvDType ki) return (DSigT promoted ki, ADSigP promoted pat' ki) -promotePat DWildP = return (DWildCardT, ADWildP) -promotePat p@(DTypeP _) = fail ("Embedded type patterns cannot be promoted: " ++ show p) -promotePat p@(DInvisP _) = fail ("Invisible type patterns cannot be promoted: " ++ show p) +promotePat _ DWildP = return (DWildCardT, ADWildP) +promotePat _ p@(DTypeP _) = fail ("Embedded type patterns cannot be promoted: " ++ show p) +promotePat _ p@(DInvisP _) = fail ("Invisible type patterns cannot be promoted: " ++ show p) promoteExp :: DExp -> PrM (DType, ADExp) promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name @@ -1381,25 +1403,26 @@ promoteExp (DLamE names exp) = do opts <- getOptions lambdaName <- newUniqueName "Lambda" tyNames <- mapM mkTyName names - let var_proms = zip names tyNames + let var_proms = zipWith (\name tyName -> (name, localVarNoKind tyName)) names tyNames (rhs, ann_exp) <- lambdaBind var_proms $ promoteExp exp all_locals <- allLocals let tvbs = map (`DPlainTV` BndrReq) tyNames - all_args = all_locals ++ tyNames + all_args = all_locals ++ map localVarNoKind tyNames tfh = dTypeFamilyHead_with_locals lambdaName all_locals tvbs DNoSig emitDecs [DClosedTypeFamilyD tfh [DTySynEqn Nothing - (foldType (DConT lambdaName) (map DVarT all_args)) + (foldTypeLocalVars (DConT lambdaName) all_args) rhs]] emitDecsM $ defunctionalize lambdaName Nothing $ DefunNoSAK all_locals tvbs Nothing - let promLambda = foldType (DConT (defunctionalizedName opts lambdaName 0)) - (map DVarT all_locals) + let promLambda = foldTypeLocalVars + (DConT (defunctionalizedName opts lambdaName 0)) + all_locals return (promLambda, ADLamE tyNames promLambda names ann_exp) promoteExp (DCaseE exp matches) = do caseTFName <- newUniqueName "Case" all_locals <- allLocals - let prom_case = foldType (DConT caseTFName) (map DVarT all_locals) + let prom_case = foldTypeLocalVars (DConT caseTFName) all_locals (exp', ann_exp) <- promoteExp exp (eqns, ann_matches) <- mapAndUnzipM (promoteMatch prom_case) matches tyvarName <- qNewName "t" @@ -1468,7 +1491,7 @@ promoteLetDecName :: -- ^ Name of the function being promoted -> Maybe LetDecRHSKindInfo -- ^ Information about the promoted kind (if present) - -> [Name] + -> [LocalVar] -- ^ The local variables currently in scope -> PrM DType promoteLetDecName mb_let_uniq name m_ldrki all_locals = do @@ -1498,7 +1521,7 @@ promoteLetDecName mb_let_uniq name m_ldrki all_locals = do -> map dTyVarBndrVisToDTypeArg $ tvbSpecsToBndrVis tvbs _ -> -- ...otherwise, return the local variables as explicit arguments -- using DTANormal. - map (DTANormal . DVarT) all_locals + map localVarToTypeArg all_locals pure $ applyDType (DConT proName) type_args -- Construct a 'DTypeFamilyHead' that closes over some local variables. We @@ -1507,30 +1530,31 @@ promoteLetDecName mb_let_uniq name m_ldrki all_locals = do dTypeFamilyHead_with_locals :: Name -- ^ Name of type family - -> [Name] + -> [LocalVar] -- ^ Local variables -> [DTyVarBndrVis] -- ^ Variables for type family arguments -> DFamilyResultSig -- ^ Type family result -> DTypeFamilyHead -dTypeFamilyHead_with_locals tf_nm local_nms arg_tvbs res_sig = +dTypeFamilyHead_with_locals tf_nm local_vars arg_tvbs res_sig = DTypeFamilyHead tf_nm - (map (`DPlainTV` BndrReq) local_nms' ++ arg_tvbs') + (map (localVarToTvb BndrReq) local_vars' ++ arg_tvbs') res_sig' Nothing where - -- We take care to only apply `noExactName` to the local variables and not + -- We take care to only apply `noExactTyVars` to the local variables and not -- to any of the argument/result types. The latter are much more likely to - -- show up in the Haddocks, and `noExactName` produces incredibly long Names - -- that are much harder to read in the rendered Haddocks. - local_nms' = map noExactName local_nms + -- show up in the Haddocks, and `noExactTyVars` produces incredibly long + -- Names that are much harder to read in the rendered Haddocks. + local_vars' = noExactTyVars local_vars -- Ensure that all references to local_nms are substituted away. subst1 = Map.fromList $ - zipWith (\local_nm local_nm' -> (local_nm, DVarT local_nm')) - local_nms - local_nms' + zipWith + (\(local_nm, _) (local_nm', _) -> (local_nm, DVarT local_nm')) + local_vars + local_vars' (subst2, arg_tvbs') = substTvbs subst1 arg_tvbs (_subst3, res_sig') = substFamilyResultSig subst2 res_sig diff --git a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs index f1e2110c..42317ce5 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs @@ -294,13 +294,13 @@ defunctionalize name m_fixity defun_ki = do -- (see Note [Defunctionalization game plan], Wrinkle 1: Partial kinds) -- or a non-vanilla kind -- (see Note [Defunctionalization game plan], Wrinkle 2: Non-vanilla kinds). - defun_fallback :: [Name] -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec] + defun_fallback :: [LocalVar] -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec] defun_fallback locals tvbs' m_res' = do opts <- getOptions extra_name <- qNewName "arg" -- Use noExactTyVars below to avoid GHC#11812. -- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util. - let locals' = map noExactName locals + let locals' = noExactTyVars locals (tvbs, m_res) <- eta_expand (noExactTyVars tvbs') (noExactTyVars m_res') let tvbs_n = length tvbs @@ -327,7 +327,7 @@ defunctionalize name m_fixity defun_ki = do -- the result kind is not always fully known. go :: Int -> [DTyVarBndrVis] -> [DTyVarBndrVis] -> (Maybe DKind, [DDec]) go n arg_tvbs res_tvbss = - let all_tvbs = map (`DPlainTV` BndrReq) locals' ++ arg_tvbs in + let all_tvbs = map (localVarToTvb BndrReq) locals' ++ arg_tvbs in case res_tvbss of [] -> let sat_decs = mk_sat_decs opts n [] all_tvbs m_res @@ -477,7 +477,7 @@ data DefunKindInfo -- signature. See Note [Defunctionalization game plan] (Wrinkle 1: Partial -- kinds) for examples. | DefunNoSAK - [Name] -- The local variables currently in scope + [LocalVar] -- The local variables currently in scope [DTyVarBndrVis] -- The arguments, along with their kinds (if known) (Maybe DKind) -- The result kind (if known) diff --git a/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs b/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs index a21989ce..bd92c4d3 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs @@ -33,7 +33,7 @@ data PrEnv = , pr_scoped_vars :: OSet Name -- ^ The set of scoped type variables currently in scope. -- See @Note [Scoped type variables]@. - , pr_lambda_vars :: OMap Name Name + , pr_lambda_vars :: OMap Name LocalVar -- ^ Map from term-level 'Name's of variables bound in lambdas and -- function clauses to their type-level counterparts. -- See @Note [Tracking local variables]@. @@ -65,11 +65,11 @@ instance OptionsMonad PrM where getOptions = asks pr_options -- return *type-level* names -allLocals :: MonadReader PrEnv m => m [Name] +allLocals :: MonadReader PrEnv m => m [LocalVar] allLocals = do scoped <- asks (F.toList . pr_scoped_vars) lambdas <- asks (OMap.assocs . pr_lambda_vars) - return $ scoped ++ map snd lambdas + return $ map localVarNoKind scoped ++ map snd lambdas emitDecs :: MonadWriter [DDec] m => [DDec] -> m () emitDecs = tell @@ -95,9 +95,10 @@ lambdaBind binds = local add_binds , pr_local_vars = locals }) = -- Per Note [Tracking local variables], these will be added to both -- `pr_lambda_vars` and `pr_local_vars`. - let new_locals = OMap.fromList [ (tmN, DVarT tyN) | (tmN, tyN) <- binds ] in - env { pr_lambda_vars = OMap.fromList binds `OMap.union` lambdas - , pr_local_vars = new_locals `OMap.union` locals } + let new_lambdas = OMap.fromList binds + new_locals = fmap localVarToType new_lambdas in + env { pr_lambda_vars = new_lambdas `OMap.union` lambdas + , pr_local_vars = new_locals `OMap.union` locals } -- ^ A pair consisting of a term-level 'Name' of a variable, bound in a @let@ -- binding or @where@ clause, and its type-level counterpart. The type will diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs index a3b3100c..c25153c7 100644 --- a/singletons-th/src/Data/Singletons/TH/Single.hs +++ b/singletons-th/src/Data/Singletons/TH/Single.hs @@ -545,7 +545,7 @@ singTySig defns types name (prom_name, prom_locals) = do opts <- getOptions let sName = singledValueName opts name prom_defun_name = defunctionalizedName0 opts prom_name - prom_defun_ty = foldType (DConT prom_defun_name) prom_local_tys + prom_defun_ty = foldTypeLocalVars (DConT prom_defun_name) prom_locals case OMap.lookup name types of Nothing -> do num_args <- guess_num_args @@ -571,8 +571,8 @@ singTySig defns types name (prom_name, prom_locals) = do , Just res_ki , singIDefuns ) where - prom_local_tys = map DVarT prom_locals - prom_ty = foldType (DConT prom_name) prom_local_tys + prom_ty :: DType + prom_ty = foldTypeLocalVars (DConT prom_name) prom_locals guess_num_args :: SgM Int guess_num_args = @@ -714,7 +714,7 @@ singClause (ADClause var_proms pats exp) = do sBody <- bindLambdas lambda_binds $ singExp exp return $ DClause sPats $ mkSigPaCaseE sigPaExpsSigs sBody -singPat :: Map Name Name -- from term-level names to type-level names +singPat :: Map Name LocalVar -- from term-level names to type-level names -> ADPat -> QWithAux SingDSigPaInfos SgM DPat singPat var_proms = go @@ -727,7 +727,7 @@ singPat var_proms = go tyname <- case Map.lookup name var_proms of Nothing -> fail "Internal error: unknown variable when singling pattern" - Just tyname -> return tyname + Just (tyname, _) -> return tyname pure $ DVarP (singledValueName opts name) `DSigP` (singFamily `DAppT` DVarT tyname) go (ADConP name tys pats) = do diff --git a/singletons-th/src/Data/Singletons/TH/Syntax.hs b/singletons-th/src/Data/Singletons/TH/Syntax.hs index 7f09c638..756086c5 100644 --- a/singletons-th/src/Data/Singletons/TH/Syntax.hs +++ b/singletons-th/src/Data/Singletons/TH/Syntax.hs @@ -10,7 +10,10 @@ Converts a list of DLetDecs into a LetDecEnv for easier processing, and contains various other AST definitions. -} -module Data.Singletons.TH.Syntax where +module Data.Singletons.TH.Syntax + ( module Data.Singletons.TH.Syntax + , module Data.Singletons.TH.Syntax.LocalVar + ) where import Prelude hiding ( exp ) import Data.Kind (Constraint, Type) @@ -20,7 +23,11 @@ import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap import Language.Haskell.TH.Desugar.OMap.Strict (OMap) import Language.Haskell.TH.Desugar.OSet (OSet) -type VarPromotions = [(Name, Name)] -- from term-level name to type-level name +import Data.Singletons.TH.Syntax.LocalVar + +-- | Pairs of term-level variable 'Name's and their corresponding type-level +-- names (encoded as 'LocalVar's). +type VarPromotions = [(Name, LocalVar)] -- Information that is accumulated when promoting patterns. data PromDPatInfos = PromDPatInfos @@ -168,7 +175,7 @@ type ULetDecRHS = LetDecRHS Unannotated -- convenient to fully apply the promoted name to all of its arguments (e.g., -- when singling type signatures), in which case we can avoid needing to involve -- defunctionalization symbols at all. -type LetDecProm = (Name, [Name]) +type LetDecProm = (Name, [LocalVar]) data LetDecEnv ann = LetDecEnv { lde_defns :: OMap Name (LetDecRHS ann) diff --git a/singletons-th/src/Data/Singletons/TH/Syntax/LocalVar.hs b/singletons-th/src/Data/Singletons/TH/Syntax/LocalVar.hs new file mode 100644 index 00000000..b7d61472 --- /dev/null +++ b/singletons-th/src/Data/Singletons/TH/Syntax/LocalVar.hs @@ -0,0 +1,231 @@ +module Data.Singletons.TH.Syntax.LocalVar + ( LocalVar + , foldTypeLocalVars + , localVarNoKind + , localVarToTvb + , localVarToType + , localVarToTypeArg + ) where + +import Language.Haskell.TH.Desugar +import Language.Haskell.TH.Syntax + +-- | A local variable that is captured in a lambda-lifted type family. (See +-- @Note [Tracking local variables]@ in "Data.Singletons.TH.Promote.Monad" for +-- an explanation of how lambda lifting works.) A 'LocalVar' consists of: +-- +-- * A 'Name' that corresponds to the promoted, type-level version of a +-- term-level variable name. +-- +-- * An optional kind (in the form of @'Maybe' 'DKind'@). When the kind of a +-- local variable is known, we can use it to generate code with more precise +-- kind information. See @Note [Local variables and kind information]@. +-- +-- A 'LocalVar' is very close in design to a 'DTyVarBndrUnit', as both contain +-- 'Name's and optional 'DKind's. We use a separate 'LocalVar' type to represent +-- local variables because 'LocalVar's can occur both in binding and argument +-- positions in generated code (see @Note [Local variables and kind information] +-- (Wrinkle: Binding positions versus argument positions)@), and using +-- 'DTyVarBndrUnit's to represent type arguments feels somewhat awkward. +type LocalVar = (Name, Maybe DKind) + +-- | Apply a 'DType' to a list of 'LocalVar' arguments. Because these +-- 'LocalVar's occur in argument positions, they will not contain any kind +-- information. See @Note [Local variables and kind information] (Wrinkle: +-- Binding positions versus argument positions)@. +foldTypeLocalVars :: DType -> [LocalVar] -> DType +foldTypeLocalVars ty = applyDType ty . map localVarToTypeArg + +-- | Construct a 'LocalVar' with no kind information. +localVarNoKind :: Name -> LocalVar +localVarNoKind nm = (nm, Nothing) + +-- | Convert a 'LocalVar' used in a binding position to a 'DTyVarBndr' using the +-- supplied @flag@. Because this is used in a binding position, we include kind +-- information (if available) in the 'DTyVarBndr'. See @Note [Local variables +-- and kind information] (Wrinkle: Binding positions versus argument +-- positions)@. +localVarToTvb :: flag -> LocalVar -> DTyVarBndr flag +localVarToTvb flag (nm, mbKind) = + case mbKind of + Nothing -> DPlainTV nm flag + Just kind -> DKindedTV nm flag kind + +-- | Convert a 'LocalVar' used in an argument position to a 'DType'. Because +-- this is used in an argument positions, it will not kind any kind information. +-- See @Note [Local variables and kind information] (Wrinkle: Binding positions +-- versus argument positions)@. +localVarToType :: LocalVar -> DType +localVarToType (local_nm, _) = DVarT local_nm + +-- | Convert a 'LocalVar' used in an argument position to a 'DTypeArg'. Because +-- this is used in an argument positions, it will not kind any kind information. +-- See @Note [Local variables and kind information] (Wrinkle: Binding positions +-- versus argument positions)@. +localVarToTypeArg :: LocalVar -> DTypeArg +localVarToTypeArg = DTANormal . localVarToType + +{- +Note [Local variables and kind information] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the following function, which we want to promote to the type level: + + f :: forall a. a -> a + f x = y + where + y = y + +Per Note [Tracking local variables]@ in Data.Singletons.TH.Promote.Monad, we +observe that `y` closes over two local variables, `a` and `x`. A naïve attempt +at promoting this code would result in generate code that looks something like +this: + + type F :: forall a. a -> a + type family F x where + F @a x = LetY a x + + type family LetY a x where + LetY a x = x + +In today's GHC, this kind-checks. However, the generated code is somewhat +unsatisfying, as GHC infers a kind for LetY that is way more general than it +should be: + + LetY :: forall k1 k2. k1 -> k2 -> k2 + +Note that this inferred kind says nothing about the relationship between the +first and second visible arguments. In today's GHC, this works because the body +of LetY requires the kind of the second visible argument to be equal to the +first visible argument in order to match. It would be as if you had written +this code: + + type LetY :: forall k1 k2. k1 -> k2 -> k2 + type family LetY a x where + LetY @Type @a (a :: Type) (x :: a) = x + +This sort of thing will cause problems once +https://gitlab.haskell.org/ghc/ghc/-/issues/23515 is implemented. As such, we +should strive to do better. + +Fortunately, there is a relatively easy fix that works well here. We observe +that we know what the kind of `x` just by looking at the syntax of `f`'s +definition, as we can pair up the `x` argument with the `a` argument type in +`f`'s type. As such, we can remember that `x :: a` and instead generate: + + type family LetY a (x :: a) where + LetY a x = x + +Now GHC infers exactly the kind we'd want for LetY: + + LetY :: forall a -> a -> a + +On the implementation side, we achive this by tracking optional kind +information in each LocalVar (in the form of a `Maybe DKind` field). A key +place in the code where kind information is propagated through to LocalVars is +the `promotePat` function in Data.Singletons.TH.Promote, which takes a `Maybe +DKind` field that describes the kind of the pattern being promoted (if it is +known). This allows recording the types of DSigP patterns (e.g., the `y :: b` +pattern in `g (y :: b) = Nothing :: Maybe b`), as well as recording the kinds +of variable patterns whose types are described by top-level top signatures +(e.g., the `x` pattern in the `f x = y` example above). + +This approach has its limitations. Consider this slightly more complicated +example: + + f' :: forall a. [a] -> Maybe (a, [a]) + f' [] = Nothing + f' (x:xs) = y + where + y = Just (x, xs) + +Note that the patterns for the arguments to `f'` aren't bare variables this +time, but rather constructor patterns. As such, we don't know the types of `x` +and `xs` just by looking at the syntax of `f'`. Instead, we'd have to do some +more clever analysis to conclude that `x :: a` and `xs :: [a]`. This is perhaps +doable, but it would require something akin to implementing type inference in +Template Haskell, which is a direction of travel that I am reluctant to go +down. + +As such, we do not record the types of the `x` or `xs` variables in this +example, meaning that we promote `f'` to the following: + + type F' :: forall a. [a] -> Maybe (a, [a]) + type family F' l where + F' @a '[] = Nothing + F' @a (x:xs) = LetY a x xs + + type family LetY a x xs where + LetY a x xs = Just '(x, xs) + +And GHC will infer an overly polymorphic kind for LetY: + + LetY :: k1 -> k2 -> k3 -> Maybe (k2, k3) + +If this proves to be troublesome in the future, we could consider refining this +approach. It is also worth nothing that in the event that singletons-th +generates a local definition with an overly polymorphic kind, one can always +constrain the kind by inserting more pattern signatures. For instance, if you +redefine `f'` to be the following: + + f' :: forall a. [a] -> Maybe (a, [a]) + f' [] = Nothing + f' ((x :: a) : (xs :: [a])) = y -- This line now has pattern signatures + where + y = Just (x, xs) + +Then singletons-th will now realize what the kinds of `x` and `xs` are, and it +will generate code for `LetY` that uses these kinds. + +----- +-- Wrinkle: Binding positions versus argument positions +----- + +Although we track the kinds of local variables throughout promotion, we don't +want to necessarily generate code involving the kind in all circumstances. +Consider this example: + +fNoScope :: a -> a +fNoScope x = y + where + y = x + +`fNoScope` is like `f` above, except that `a` does not scope over the body of +the function due to the lack of an outermost `forall` in the type signature. On +the other hand, `x` /does/ scope over the body, so we close over `x` when +lambda lifting `y`. Moreover, we know that the type of `x` is `a`. However, we +must be careful not to promote `fNoScope` to the following: + + type FNoScope :: a -> a + type family FNoScope x where + FNoScope x = LetY (x :: a) + + type family LetY (x :: a) where + LetY (x :: a) = x + +The problem with this code lies here: + + FNoScope x = LetY (x :: a) + +Note that `a` is not in scope in this line! Even though we know that `x :: a`, +that doesn't mean that we can unconditionally generate the code `x :: a` in all +places, since `a` may not be in scope in all places. Of course, we /do/ want to +generate `x :: a` in this line: + + type family LetY (x :: a) where + +The distinction between the two lines is one of binding positions versus +argument positions. In the former case, `x` occurs as an argument to a `LetY` +application, whereas in the latter case, `x` occurs as a type variable binder +when defining `LetY`. In binding positions such as these, `x :: a` will +implicitly quantify `a`, so it is fine to unconditionally use `x :: a` in these +positions. Implicit quantification does not occur in argument positions, +however, so we leave out the `:: a` kind signature in these positions. (This is +perfectly fine to do, since `x` will be bound somewhere else, and that binder +will include the `a` kind information.) + +Implementation-wise, the difference between these two positions is embodied in +the `localVarToTvb` function (for converting `LocalVar`s to binding positions) +and the `localVarToType` function (for converting `LocalVar`s to argument +positions). Note that the derived functions `localVarToTypeArg` and +`foldTypeLocalVars` also treat `LocalVar`s as argument positions. +-} diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs index 472a89b5..17500e9e 100644 --- a/singletons-th/src/Data/Singletons/TH/Util.hs +++ b/singletons-th/src/Data/Singletons/TH/Util.hs @@ -31,6 +31,8 @@ import Data.Traversable import Data.Generics import Data.Maybe +import Data.Singletons.TH.Syntax.LocalVar + -- like reportWarning, but generalized to any Quasi qReportWarning :: Quasi q => String -> q () qReportWarning = qReport False @@ -438,6 +440,7 @@ noExactTyVars = everywhere go `extT` fix_tvb @BndrVis `extT` fix_ty `extT` fix_inj_ann + `extT` fix_local_var fix_tvb :: Typeable flag => DTyVarBndr flag -> DTyVarBndr flag fix_tvb (DPlainTV n f) = DPlainTV (noExactName n) f @@ -449,6 +452,9 @@ noExactTyVars = everywhere go fix_inj_ann (InjectivityAnn lhs rhs) = InjectivityAnn (noExactName lhs) (map noExactName rhs) + fix_local_var :: LocalVar -> LocalVar + fix_local_var (n, mbKind) = (noExactName n, mbKind) + -- Changes a unique Name with a NameU or NameL namespace to a non-unique Name. -- See Note [Pitfalls of NameU/NameL] for why this is useful. noExactName :: Name -> Name