From 7815a555f33be8b8cb89f6fa918fd8a8bad642b4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 23 Jul 2023 18:07:40 -0400 Subject: [PATCH 1/2] Use noExactTyVars when promoting functions with local variables Whenever we promote a function that closes over one or more local variables, we now use `noExactTyVars` to ensure that none of the local variables reuse unique `Name`s. This isn't strictly necessary right now, but this will be required in a future patch that will panic (triggering https://gitlab.haskell.org/ghc/ghc/-/issues/11812) unless `noExactTyVars` is used. While I was in the neighborhood, I took the opportunity to write `Note [Pitfalls of NameU/NameL]` with more context about why `noExactTyVars` is necessary in the first place, and I added references to the Note in all the places where we use it. --- .../GradingClient/Database.golden | 4 +- .../InsertionSort/InsertionSortImp.golden | 4 +- .../Singletons/AsPattern.golden | 10 +- .../Singletons/CaseExpressions.golden | 20 ++-- .../Singletons/EmptyShowDeriving.golden | 2 +- .../Singletons/EnumDeriving.golden | 10 +- .../Singletons/FunctorLikeDeriving.golden | 30 ++--- .../Singletons/HigherOrder.golden | 8 +- .../Singletons/LambdaCase.golden | 12 +- .../Singletons/Lambdas.golden | 32 +++--- .../Singletons/LetStatements.golden | 44 ++++---- .../Singletons/PatternMatching.golden | 14 +-- .../Singletons/StandaloneDeriving.golden | 4 +- .../compile-and-dump/Singletons/T136.golden | 6 +- .../compile-and-dump/Singletons/T150.golden | 2 +- .../compile-and-dump/Singletons/T160.golden | 4 +- .../compile-and-dump/Singletons/T166.golden | 2 +- .../compile-and-dump/Singletons/T176.golden | 4 +- .../compile-and-dump/Singletons/T183.golden | 22 ++-- .../compile-and-dump/Singletons/T184.golden | 18 +-- .../compile-and-dump/Singletons/T190.golden | 2 +- .../compile-and-dump/Singletons/T287.golden | 2 +- .../compile-and-dump/Singletons/T312.golden | 2 +- .../compile-and-dump/Singletons/T378b.golden | 2 +- .../compile-and-dump/Singletons/T445.golden | 2 +- .../compile-and-dump/Singletons/T54.golden | 4 +- .../compile-and-dump/Singletons/T89.golden | 2 +- .../Singletons/TopLevelPatterns.golden | 8 +- .../src/Data/Singletons/TH/Promote.hs | 79 +++++++++---- .../src/Data/Singletons/TH/Promote/Defun.hs | 4 + singletons-th/src/Data/Singletons/TH/Util.hs | 106 ++++++++++++++++-- 31 files changed, 296 insertions(+), 169 deletions(-) diff --git a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden index 5910e874..4bc4cac7 100644 --- a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden +++ b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden @@ -449,9 +449,9 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym4 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs where + type family Let0123456789876543210Scrutinee_0123456789876543210 name0123456789876543210 name'0123456789876543210 u0123456789876543210 attrs0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 name name' u attrs = Apply (Apply (==@#@$) name) name' - type family Case_0123456789876543210 name name' u attrs t where + type family Case_0123456789876543210 name0123456789876543210 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 13a4fc3b..20368cb2 100644 --- a/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden +++ b/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden @@ -96,9 +96,9 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 n h t where + type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h - type family Case_0123456789876543210 n h t t where + type family Case_0123456789876543210 n0123456789876543210 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/AsPattern.golden b/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden index 87d84673..d12ce8d8 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/AsPattern.golden @@ -75,7 +75,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210PSym0KindInference ()) type family Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 where Let0123456789876543210PSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 - type family Let0123456789876543210P wild_0123456789876543210 where + type family Let0123456789876543210P wild_01234567898765432100123456789876543210 where Let0123456789876543210P wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) NilSym0 data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 where @@ -103,7 +103,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210PSym2KindInference ()) type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 - type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where + type family Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply (:@#@$) wild_0123456789876543210) (Apply (Apply (:@#@$) wild_0123456789876543210) wild_0123456789876543210) data Let0123456789876543210PSym0 wild_01234567898765432100123456789876543210 where @@ -123,7 +123,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210PSym1KindInference ()) type family Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where Let0123456789876543210PSym2 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 - type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 where + type family Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 = Apply (Apply Tuple2Sym0 wild_0123456789876543210) wild_0123456789876543210 type family Let0123456789876543210PSym0 where Let0123456789876543210PSym0 = Let0123456789876543210P @@ -155,7 +155,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210PSym2KindInference ()) type family Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where Let0123456789876543210PSym3 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 - type family Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 where + type family Let0123456789876543210P wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 wild_01234567898765432100123456789876543210 where Let0123456789876543210P wild_0123456789876543210 wild_0123456789876543210 wild_0123456789876543210 = Apply JustSym0 (Apply (Apply (Apply BazSym0 wild_0123456789876543210) wild_0123456789876543210) wild_0123456789876543210) data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 where @@ -167,7 +167,7 @@ Singletons/AsPattern.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210XSym0KindInference ()) type family Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 where Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210 - type family Let0123456789876543210X wild_0123456789876543210 where + type family Let0123456789876543210X wild_01234567898765432100123456789876543210 where Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 wild_0123456789876543210 type family Let0123456789876543210PSym0 where Let0123456789876543210PSym0 = Let0123456789876543210P diff --git a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden index 7aba4f34..d032e58d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden @@ -37,9 +37,9 @@ 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_0123456789876543210 y x t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 y0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 y x _ = x - type family Lambda_0123456789876543210 y x arg_0123456789876543210 where + type family Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 y x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 y x arg_0123456789876543210 data Lambda_0123456789876543210Sym0 y0123456789876543210 where @@ -67,7 +67,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 y) x) y data Let0123456789876543210ZSym0 y0123456789876543210 where @@ -87,9 +87,9 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210ZSym1KindInference ()) type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z y x :: a where + type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: a where Let0123456789876543210Z y x = y - type family Case_0123456789876543210 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x y = Let0123456789876543210ZSym2 y x data Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 where @@ -115,9 +115,9 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 b0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 b0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 a b where + type family Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 b0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 a b = Apply (Apply Tuple2Sym0 a) b - type family Case_0123456789876543210 a b t where + type family Case_0123456789876543210 a0123456789876543210 b0123456789876543210 t where Case_0123456789876543210 a b '(p, _) = p data Let0123456789876543210Scrutinee_0123456789876543210Sym0 d0123456789876543210 where @@ -132,11 +132,11 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 d0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym1 d0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 d0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 d where + type family Let0123456789876543210Scrutinee_0123456789876543210 d0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 d = Apply JustSym0 d - type family Case_0123456789876543210 d t where + type family Case_0123456789876543210 d0123456789876543210 t where Case_0123456789876543210 d ('Just y) = y - type family Case_0123456789876543210 d x t where + type family Case_0123456789876543210 d0123456789876543210 x0123456789876543210 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 c888d04b..5e18ef69 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_0123456789876543210 a_0123456789876543210 t where + type family Case_0123456789876543210 v_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 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 5389b0de..8bb26d8f 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 n t where + type family Case_0123456789876543210 n0123456789876543210 t where Case_0123456789876543210 n 'True = BumSym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 t where Case_0123456789876543210 n 'True = BazSym0 Case_0123456789876543210 n 'False = Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 2)) - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 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 @@ -148,10 +148,10 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations Singletons/EnumDeriving.hs:0:0:: Splicing declarations singEnumInstance ''Quux ======> - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 t where Case_0123456789876543210 n 'True = Q2Sym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 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 4230dc26..66bcf471 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden @@ -60,7 +60,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type MkT2Sym1 :: forall x a. Maybe x -> T x a type family MkT2Sym1 (a0123456789876543210 :: Maybe x) :: T x a where MkT2Sym1 a0123456789876543210 = MkT2 a0123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -112,7 +112,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym5KindInference ()) type family Lambda_0123456789876543210Sym6 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym6 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -166,7 +166,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type Fmap_0123456789876543210Sym2 :: (~>) a b -> T x a -> T x b type family Fmap_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: T x a) :: T x b where Fmap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Fmap_0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Lambda_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 data Lambda_0123456789876543210Sym0 _z_01234567898765432100123456789876543210 where @@ -218,7 +218,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym5KindInference ()) type family Lambda_0123456789876543210Sym6 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym6 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = _z_0123456789876543210 data Lambda_0123456789876543210Sym0 _z_01234567898765432100123456789876543210 where @@ -270,7 +270,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym5KindInference ()) type family Lambda_0123456789876543210Sym6 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym6 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 data Lambda_0123456789876543210Sym0 _z_01234567898765432100123456789876543210 where @@ -326,7 +326,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance PFunctor (T x) where type Fmap a a = Apply (Apply Fmap_0123456789876543210Sym0 a) a type (<$) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a - type family Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = MemptySym0 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -378,7 +378,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym5KindInference ()) type family Lambda_0123456789876543210Sym6 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym6 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 n_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = MemptySym0 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -431,7 +431,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type FoldMap_0123456789876543210Sym2 :: (~>) a m -> T x a -> m type family FoldMap_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a m) (a0123456789876543210 :: T x a) :: m where FoldMap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = FoldMap_0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = n2_0123456789876543210 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -499,7 +499,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym7KindInference ()) type family Lambda_0123456789876543210Sym8 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym8 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_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 _f_01234567898765432100123456789876543210 where @@ -567,7 +567,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym7KindInference ()) type family Lambda_0123456789876543210Sym8 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym8 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 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 n1_01234567898765432100123456789876543210 where @@ -651,7 +651,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym9KindInference ()) type family Lambda_0123456789876543210Sym10 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym10 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = Apply (Apply (Apply FoldrSym0 (Apply (Apply (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 n1_0123456789876543210) n2_0123456789876543210) _f_0123456789876543210) _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210)) n2_0123456789876543210) n1_0123456789876543210 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -719,7 +719,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym7KindInference ()) type family Lambda_0123456789876543210Sym8 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym8 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where + type family Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_0123456789876543210 n2_0123456789876543210 where Lambda_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 n1_0123456789876543210 n2_0123456789876543210 = n2_0123456789876543210 data Lambda_0123456789876543210Sym0 _f_01234567898765432100123456789876543210 where @@ -834,7 +834,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations Traverse_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Traverse_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PTraversable (T x) where type Traverse a a = Apply (Apply Traverse_0123456789876543210Sym0 a) a - type family Case_0123456789876543210 v_0123456789876543210 t where + type family Case_0123456789876543210 v_01234567898765432100123456789876543210 t where type Fmap_0123456789876543210 :: (~>) a b -> Empty a -> Empty b type family Fmap_0123456789876543210 (a :: (~>) a b) (a :: Empty a) :: Empty b where Fmap_0123456789876543210 _ v_0123456789876543210 = Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210 @@ -860,7 +860,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type Fmap_0123456789876543210Sym2 :: (~>) a b -> Empty a -> Empty b type family Fmap_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Empty a) :: Empty b where Fmap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Fmap_0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Case_0123456789876543210 v_0123456789876543210 t where + type family Case_0123456789876543210 v_01234567898765432100123456789876543210 t where type TFHelper_0123456789876543210 :: a -> Empty b -> Empty a type family TFHelper_0123456789876543210 (a :: a) (a :: Empty b) :: Empty a where TFHelper_0123456789876543210 _ v_0123456789876543210 = Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210 @@ -916,7 +916,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations FoldMap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = FoldMap_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PFoldable Empty where type FoldMap a a = Apply (Apply FoldMap_0123456789876543210Sym0 a) a - type family Case_0123456789876543210 v_0123456789876543210 t where + type family Case_0123456789876543210 v_01234567898765432100123456789876543210 t where type Traverse_0123456789876543210 :: (~>) a (f b) -> Empty a -> f (Empty b) type family Traverse_0123456789876543210 (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 39459454..1ea1dfce 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden @@ -62,10 +62,10 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations type RightSym1 :: forall a b. b -> Either a b type family RightSym1 (a0123456789876543210 :: b) :: Either a b where RightSym1 a0123456789876543210 = Right a0123456789876543210 - type family Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 t where + type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 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_0123456789876543210 a_0123456789876543210 n b where + type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 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 where @@ -101,10 +101,10 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) type family Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n0123456789876543210 b0123456789876543210 - type family Case_0123456789876543210 n b ns bs t where + type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 ns0123456789876543210 bs0123456789876543210 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 ns bs n b where + type family Lambda_0123456789876543210 ns0123456789876543210 bs0123456789876543210 n b where Lambda_0123456789876543210 ns bs n b = Case_0123456789876543210 n b ns bs b data Lambda_0123456789876543210Sym0 ns0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden b/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden index 937f4ac4..aaedca51 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden @@ -29,9 +29,9 @@ 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_0123456789876543210 a b t where + type family Case_0123456789876543210 x_01234567898765432100123456789876543210 a0123456789876543210 b0123456789876543210 t where Case_0123456789876543210 x_0123456789876543210 a b '(p, _) = p - type family Lambda_0123456789876543210 a b x_0123456789876543210 where + type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x_0123456789876543210 where Lambda_0123456789876543210 a b x_0123456789876543210 = Case_0123456789876543210 x_0123456789876543210 a b x_0123456789876543210 data Lambda_0123456789876543210Sym0 a0123456789876543210 where @@ -59,10 +59,10 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x_0123456789876543210 d t where + type family Case_0123456789876543210 x_01234567898765432100123456789876543210 d0123456789876543210 t where Case_0123456789876543210 x_0123456789876543210 d ('Just y) = y Case_0123456789876543210 x_0123456789876543210 d 'Nothing = d - type family Lambda_0123456789876543210 d x_0123456789876543210 where + type family Lambda_0123456789876543210 d0123456789876543210 x_0123456789876543210 where Lambda_0123456789876543210 d x_0123456789876543210 = Case_0123456789876543210 x_0123456789876543210 d x_0123456789876543210 data Lambda_0123456789876543210Sym0 d0123456789876543210 where @@ -82,10 +82,10 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) type family Lambda_0123456789876543210Sym2 d0123456789876543210 x_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 d0123456789876543210 x_01234567898765432100123456789876543210 = Lambda_0123456789876543210 d0123456789876543210 x_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x_0123456789876543210 d x t where + type family Case_0123456789876543210 x_01234567898765432100123456789876543210 d0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x_0123456789876543210 d x ('Just y) = y Case_0123456789876543210 x_0123456789876543210 d x 'Nothing = d - type family Lambda_0123456789876543210 d x x_0123456789876543210 where + type family Lambda_0123456789876543210 d0123456789876543210 x0123456789876543210 x_0123456789876543210 where Lambda_0123456789876543210 d x x_0123456789876543210 = Case_0123456789876543210 x_0123456789876543210 d x x_0123456789876543210 data Lambda_0123456789876543210Sym0 d0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden index c3859eff..ada73a02 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden @@ -59,9 +59,9 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations type FooSym2 :: forall a b. a -> b -> Foo a b type family FooSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Foo a b where FooSym2 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 x t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x (Foo a _) = a - type family Lambda_0123456789876543210 x arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -81,9 +81,9 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) type family Lambda_0123456789876543210Sym2 x0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 x y t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x y '(_, b) = b - type family Lambda_0123456789876543210 x y arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -111,9 +111,9 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 x a b t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 a0123456789876543210 b0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x a b _ = x - type family Lambda_0123456789876543210 x a b arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x a b arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x a b arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -149,7 +149,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) type family Lambda_0123456789876543210Sym4 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym4 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 a0123456789876543210 b0123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 a b x where + type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x where Lambda_0123456789876543210 a b x = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) a) b data Lambda_0123456789876543210Sym0 a0123456789876543210 where @@ -177,7 +177,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym3 a0123456789876543210 b0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 x y x where + type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 x where Lambda_0123456789876543210 x y x = x data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -205,10 +205,10 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 x0123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 arg_0123456789876543210 x y z t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 z0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 arg_0123456789876543210 x y z '(_, _) = x - type family Lambda_0123456789876543210 x y z arg_0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 z0123456789876543210 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 where @@ -252,7 +252,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym4KindInference ()) type family Lambda_0123456789876543210Sym5 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym5 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 z0123456789876543210 arg_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 x y where + type family Lambda_0123456789876543210 x0123456789876543210 y where Lambda_0123456789876543210 x y = y data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -272,9 +272,9 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) type family Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 x y t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x y _ = x - type family Lambda_0123456789876543210 x y arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -302,9 +302,9 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 x a_0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x a_0123456789876543210 _ = x - type family Lambda_0123456789876543210 x a_0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x a_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x a_0123456789876543210 arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -332,7 +332,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 x y where + type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 x y where Lambda_0123456789876543210 a_0123456789876543210 a_0123456789876543210 x y = x data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden index 850f81a4..a041eaf0 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden @@ -189,10 +189,10 @@ 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 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x '(_, y_0123456789876543210) = y_0123456789876543210 - type family Case_0123456789876543210 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x '(y_0123456789876543210, _) = y_0123456789876543210 data Let0123456789876543210ZSym0 x0123456789876543210 @@ -227,11 +227,11 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations Let0123456789876543210X_0123456789876543210Sym0KindInference ()) type family Let0123456789876543210X_0123456789876543210Sym1 x0123456789876543210 where Let0123456789876543210X_0123456789876543210Sym1 x0123456789876543210 = Let0123456789876543210X_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z x where + type family Let0123456789876543210Z x0123456789876543210 where Let0123456789876543210Z x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x) - type family Let0123456789876543210Y x where + type family Let0123456789876543210Y x0123456789876543210 where Let0123456789876543210Y x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x) - type family Let0123456789876543210X_0123456789876543210 x where + type family Let0123456789876543210X_0123456789876543210 x0123456789876543210 where Let0123456789876543210X_0123456789876543210 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x data Let0123456789876543210BarSym0 x0123456789876543210 where @@ -243,7 +243,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210BarSym0KindInference ()) type family Let0123456789876543210BarSym1 x0123456789876543210 :: a0123456789876543210 where Let0123456789876543210BarSym1 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210 - type family Let0123456789876543210Bar x :: a where + type family Let0123456789876543210Bar x0123456789876543210 :: a where Let0123456789876543210Bar x = x data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 where @@ -271,7 +271,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) ()) type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family (<<<%%%%%%%%%%%%%%%%%%%%) x (a :: Nat) (a :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 (a :: Nat) (a :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) n) x) data Let0123456789876543210ZSym0 x0123456789876543210 @@ -310,9 +310,9 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) ()) type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210Z x :: Nat where + type family Let0123456789876543210Z x0123456789876543210 :: Nat where Let0123456789876543210Z x = x - type family (<<<%%%%%%%%%%%%%%%%%%%%) x (a :: Nat) (a :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 (a :: Nat) (a :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%) x 'Zero m = m (<<<%%%%%%%%%%%%%%%%%%%%) x ('Succ n) m = Apply SuccSym0 (Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) n) m) data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 @@ -341,10 +341,10 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) (:<<<%%%%%%%%%%%%%%%%%%%%@#@$$$###) ()) type family (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where (<<<%%%%%%%%%%%%%%%%%%%%@#@$$$$) x0123456789876543210 a0123456789876543210 a0123456789876543210 = (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family (<<<%%%%%%%%%%%%%%%%%%%%) x (a :: Nat) (a :: Nat) :: Nat where + type family (<<<%%%%%%%%%%%%%%%%%%%%) x0123456789876543210 (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_0123456789876543210 x x where + type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x0123456789876543210 x where Lambda_0123456789876543210 a_0123456789876543210 x x = x data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 where @@ -390,9 +390,9 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210ZSym1KindInference ()) type family Let0123456789876543210ZSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210ZSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210Z x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210Z x (a :: Nat) :: Nat where + type family Let0123456789876543210Z x0123456789876543210 (a :: Nat) :: Nat where Let0123456789876543210Z x a_0123456789876543210 = Apply (Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) x) a_0123456789876543210 - type family Lambda_0123456789876543210 x x where + type family Lambda_0123456789876543210 x0123456789876543210 x where Lambda_0123456789876543210 x x = x data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -422,7 +422,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210ZSym0KindInference ()) type family Let0123456789876543210ZSym1 x0123456789876543210 :: Nat where Let0123456789876543210ZSym1 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210 - type family Let0123456789876543210Z x :: Nat where + type family Let0123456789876543210Z x0123456789876543210 :: Nat where Let0123456789876543210Z x = Apply (Apply Lambda_0123456789876543210Sym0 x) ZeroSym0 data Let0123456789876543210XSym0 x0123456789876543210 where @@ -434,7 +434,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210XSym0KindInference ()) type family Let0123456789876543210XSym1 x0123456789876543210 :: Nat where Let0123456789876543210XSym1 x0123456789876543210 = Let0123456789876543210X x0123456789876543210 - type family Let0123456789876543210X x :: Nat where + type family Let0123456789876543210X x0123456789876543210 :: Nat where Let0123456789876543210X x = ZeroSym0 data Let0123456789876543210FSym0 x0123456789876543210 where @@ -454,7 +454,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210FSym1KindInference ()) type family Let0123456789876543210FSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210FSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210F x (a :: Nat) :: Nat where + type family Let0123456789876543210F x0123456789876543210 (a :: Nat) :: Nat where Let0123456789876543210F x y = Apply SuccSym0 y data Let0123456789876543210ZSym0 x0123456789876543210 where @@ -466,7 +466,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210ZSym0KindInference ()) type family Let0123456789876543210ZSym1 x0123456789876543210 :: Nat where Let0123456789876543210ZSym1 x0123456789876543210 = Let0123456789876543210Z x0123456789876543210 - type family Let0123456789876543210Z x :: Nat where + type family Let0123456789876543210Z x0123456789876543210 :: Nat where Let0123456789876543210Z x = Apply (Let0123456789876543210FSym1 x) x data Let0123456789876543210ZSym0 y0123456789876543210 where @@ -486,7 +486,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210ZSym1KindInference ()) type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: Nat where Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z y x :: Nat where + type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: Nat where Let0123456789876543210Z y x = Apply SuccSym0 y data Let0123456789876543210FSym0 x0123456789876543210 where @@ -506,7 +506,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210FSym1KindInference ()) type family Let0123456789876543210FSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210FSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210F x (a :: Nat) :: Nat where + type family Let0123456789876543210F x0123456789876543210 (a :: Nat) :: Nat where Let0123456789876543210F x y = Apply SuccSym0 (Let0123456789876543210ZSym2 y x) data Let0123456789876543210FSym0 x0123456789876543210 where @@ -526,7 +526,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210FSym1KindInference ()) type family Let0123456789876543210FSym2 x0123456789876543210 (a0123456789876543210 :: Nat) :: Nat where Let0123456789876543210FSym2 x0123456789876543210 a0123456789876543210 = Let0123456789876543210F x0123456789876543210 a0123456789876543210 - type family Let0123456789876543210F x (a :: Nat) :: Nat where + type family Let0123456789876543210F x0123456789876543210 (a :: Nat) :: Nat where Let0123456789876543210F x y = Apply SuccSym0 y data Let0123456789876543210YSym0 x0123456789876543210 where @@ -538,7 +538,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210YSym0KindInference ()) type family Let0123456789876543210YSym1 x0123456789876543210 :: Nat where Let0123456789876543210YSym1 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210 - type family Let0123456789876543210Y x :: Nat where + type family Let0123456789876543210Y x0123456789876543210 :: Nat where Let0123456789876543210Y x = Apply SuccSym0 x type family Let0123456789876543210ZSym0 where Let0123456789876543210ZSym0 = Let0123456789876543210Z @@ -558,7 +558,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210YSym0KindInference ()) type family Let0123456789876543210YSym1 x0123456789876543210 :: Nat where Let0123456789876543210YSym1 x0123456789876543210 = Let0123456789876543210Y x0123456789876543210 - type family Let0123456789876543210Y x :: Nat where + type family Let0123456789876543210Y x0123456789876543210 :: 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 bf1c9e0c..859b86f9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden @@ -228,7 +228,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 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x _ = Tuple0Sym0 data Let0123456789876543210TSym0 x0123456789876543210 where @@ -248,11 +248,11 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210TSym1KindInference ()) type family Let0123456789876543210TSym2 x0123456789876543210 y0123456789876543210 where Let0123456789876543210TSym2 x0123456789876543210 y0123456789876543210 = Let0123456789876543210T x0123456789876543210 y0123456789876543210 - type family Let0123456789876543210T x y where + type family Let0123456789876543210T x0123456789876543210 y0123456789876543210 where Let0123456789876543210T x y = Apply (Apply Tuple2Sym0 x) y - type family Case_0123456789876543210 arg_0123456789876543210 a b x y t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 a b x y _ = a - type family Lambda_0123456789876543210 a b x y arg_0123456789876543210 where + type family Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 a b x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 a b x y arg_0123456789876543210 data Lambda_0123456789876543210Sym0 a0123456789876543210 where @@ -296,12 +296,12 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym4KindInference ()) type family Lambda_0123456789876543210Sym5 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym5 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 b0123456789876543210 x0123456789876543210 y0123456789876543210 arg_01234567898765432100123456789876543210 - type family Case_0123456789876543210 x y t where + type family Case_0123456789876543210 x0123456789876543210 y0123456789876543210 t where Case_0123456789876543210 x y '(a, b) = Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) b) x) y) b - type family Case_0123456789876543210 arg_0123456789876543210 x y t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 y0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x y _ = x - type family Lambda_0123456789876543210 x y arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 y0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x y arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x y arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden index 9cc572a8..08799f53 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden @@ -260,10 +260,10 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations instance PBounded S where type MinBound = MinBound_0123456789876543210Sym0 type MaxBound = MaxBound_0123456789876543210Sym0 - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 t where Case_0123456789876543210 n 'True = S2Sym0 Case_0123456789876543210 n 'False = Apply ErrorSym0 "toEnum: bad argument" - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 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 9677967b..8fa94875 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136.golden @@ -63,13 +63,13 @@ Singletons/T136.hs:(0,0)-(0,0): Splicing declarations type Pred_0123456789876543210Sym1 :: [Bool] -> [Bool] type family Pred_0123456789876543210Sym1 (a0123456789876543210 :: [Bool]) :: [Bool] where Pred_0123456789876543210Sym1 a0123456789876543210 = Pred_0123456789876543210 a0123456789876543210 - type family Case_0123456789876543210 i arg_0123456789876543210 t where + type family Case_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 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 i arg_0123456789876543210 t where + type family Case_0123456789876543210 i0123456789876543210 arg_01234567898765432100123456789876543210 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_0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 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 89bddde7..9a1156fd 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 (a0123456789876543210 :: a) :: Obj where ObjSym1 a0123456789876543210 = Obj a0123456789876543210 - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 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 4a10cd73..563abd1c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T160.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T160.golden @@ -18,9 +18,9 @@ Singletons/T160.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 x where + type family Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 x = Apply (Apply (==@#@$) x) (FromInteger 0) - type family Case_0123456789876543210 x t where + type family Case_0123456789876543210 x0123456789876543210 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 bba67cad..29f30832 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T166.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T166.golden @@ -44,7 +44,7 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations type FooSym1 :: forall a. a -> [Bool] type family FooSym1 (a0123456789876543210 :: a) :: [Bool] where FooSym1 a0123456789876543210 = Foo a0123456789876543210 - type family Lambda_0123456789876543210 x s where + type family Lambda_0123456789876543210 x0123456789876543210 s where Lambda_0123456789876543210 x s = Apply (Apply (Apply FoosPrecSym0 (FromInteger 0)) x) s data Lambda_0123456789876543210Sym0 x0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T176.golden b/singletons-base/tests/compile-and-dump/Singletons/T176.golden index e0fc0b8d..b0670af1 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T176.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T176.golden @@ -22,9 +22,9 @@ 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_0123456789876543210 x t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x _ = Baz1Sym0 - type family Lambda_0123456789876543210 x arg_0123456789876543210 where + type family Lambda_0123456789876543210 x0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 x arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 x arg_0123456789876543210 data Lambda_0123456789876543210Sym0 x0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T183.golden b/singletons-base/tests/compile-and-dump/Singletons/T183.golden index caab6509..c13c0c7d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T183.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T183.golden @@ -67,7 +67,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Let0123456789876543210GSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym0KindInference ()) - data Let0123456789876543210GSym1 x0123456789876543210 :: (~>) a ((~>) b0123456789876543210 a) + data Let0123456789876543210GSym1 x0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210) where Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 x0123456789876543210) arg) (Let0123456789876543210GSym2 x0123456789876543210 arg) => Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210 @@ -75,7 +75,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210GSym1 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym1KindInference ()) - data Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: a) :: (~>) b0123456789876543210 a + data Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 a0123456789876543210 where Let0123456789876543210GSym2KindInference :: SameKind (Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 arg) => Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 a0123456789876543210 @@ -83,9 +83,9 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym2KindInference ()) - type family Let0123456789876543210GSym3 x0123456789876543210 (a0123456789876543210 :: a) (a0123456789876543210 :: b0123456789876543210) :: a where + type family Let0123456789876543210GSym3 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: a0123456789876543210 where Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210G x (a :: a) (a :: b) :: a where + type family Let0123456789876543210G x0123456789876543210 (a :: a) (a :: b) :: a where Let0123456789876543210G x y _ = y data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 where @@ -97,7 +97,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210XSym0KindInference ()) type family Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 where Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210 - type family Let0123456789876543210X wild_0123456789876543210 where + type family Let0123456789876543210X wild_01234567898765432100123456789876543210 where Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a type family Let0123456789876543210XSym0 where Let0123456789876543210XSym0 = Let0123456789876543210X @@ -116,14 +116,14 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 x where + type family Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 x = x :: Maybe a - type family Case_0123456789876543210 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x ('Just (y :: a) :: Maybe a) = Apply JustSym0 (Apply JustSym0 (y :: a) :: Maybe a) - type family Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 '(x :: a, y :: b) = Apply (Apply Tuple2Sym0 (y :: b)) (x :: a) - type family Lambda_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 where + type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 arg_0123456789876543210 data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 where @@ -156,9 +156,9 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 x where + type family Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 x = Apply JustSym0 x - type family Case_0123456789876543210 x t where + type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x ('Just y :: Maybe Bool) = y :: Bool type Foo9Sym0 :: (~>) a a data Foo9Sym0 :: (~>) a a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T184.golden b/singletons-base/tests/compile-and-dump/Singletons/T184.golden index 0d99a340..e9469d65 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T184.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T184.golden @@ -25,7 +25,7 @@ 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 xs x where + type family Lambda_0123456789876543210 xs0123456789876543210 x where Lambda_0123456789876543210 xs x = Apply (Apply (>>@#@$) (Apply GuardSym0 x)) (Apply ReturnSym0 x) data Lambda_0123456789876543210Sym0 xs0123456789876543210 where @@ -45,7 +45,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym1KindInference ()) type family Lambda_0123456789876543210Sym2 xs0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym2 xs0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 x xs ys y where + type family Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y where Lambda_0123456789876543210 x xs ys y = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y) data Lambda_0123456789876543210Sym0 x0123456789876543210 where @@ -81,7 +81,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) type family Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym4 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 - type family Lambda_0123456789876543210 xs ys x where + type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x where Lambda_0123456789876543210 xs ys x = Apply (Apply (>>=@#@$) ys) (Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) xs) ys) data Lambda_0123456789876543210Sym0 xs0123456789876543210 where @@ -109,7 +109,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 xs ys x where + type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x where Lambda_0123456789876543210 xs ys x = Apply ReturnSym0 x data Lambda_0123456789876543210Sym0 xs0123456789876543210 where @@ -137,7 +137,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 x0123456789876543210 - type family Lambda_0123456789876543210 xs ys y where + type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y where Lambda_0123456789876543210 xs ys y = Apply ReturnSym0 y data Lambda_0123456789876543210Sym0 xs0123456789876543210 where @@ -165,10 +165,10 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 y0123456789876543210 - type family Case_0123456789876543210 arg_0123456789876543210 xs ys t where + type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 xs0123456789876543210 ys0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 xs ys '(x, y) = Apply ReturnSym0 (Apply (Apply Tuple2Sym0 x) y) - type family Lambda_0123456789876543210 xs ys arg_0123456789876543210 where + type family Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_0123456789876543210 where Lambda_0123456789876543210 xs ys arg_0123456789876543210 = Case_0123456789876543210 arg_0123456789876543210 xs ys arg_0123456789876543210 data Lambda_0123456789876543210Sym0 xs0123456789876543210 where @@ -196,7 +196,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym2KindInference ()) type family Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 xs0123456789876543210 ys0123456789876543210 arg_01234567898765432100123456789876543210 - type family Lambda_0123456789876543210 a ma mb b where + type family Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b where Lambda_0123456789876543210 a ma mb b = Apply (Apply (>>@#@$) (Apply GuardSym0 b)) (Apply ReturnSym0 a) data Lambda_0123456789876543210Sym0 a0123456789876543210 where @@ -232,7 +232,7 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Lambda_0123456789876543210Sym3KindInference ()) type family Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 where Lambda_0123456789876543210Sym4 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 = Lambda_0123456789876543210 a0123456789876543210 ma0123456789876543210 mb0123456789876543210 b0123456789876543210 - type family Lambda_0123456789876543210 ma mb a where + type family Lambda_0123456789876543210 ma0123456789876543210 mb0123456789876543210 a where Lambda_0123456789876543210 ma mb a = Apply (Apply (>>=@#@$) mb) (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) ma) mb) data Lambda_0123456789876543210Sym0 ma0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T190.golden b/singletons-base/tests/compile-and-dump/Singletons/T190.golden index 0edd4919..9c808a64 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T190.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T190.golden @@ -62,7 +62,7 @@ Singletons/T190.hs:0:0:: Splicing declarations Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd T where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a - type family Case_0123456789876543210 n t where + type family Case_0123456789876543210 n0123456789876543210 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 4f572b6f..d8000518 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T287.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T287.golden @@ -31,7 +31,7 @@ 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 f g x where + type family Lambda_0123456789876543210 f0123456789876543210 g0123456789876543210 x where Lambda_0123456789876543210 f g x = Apply (Apply (<<>>@#@$) (Apply f x)) (Apply g x) data Lambda_0123456789876543210Sym0 f0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T312.golden b/singletons-base/tests/compile-and-dump/Singletons/T312.golden index fb09e3d4..9e4e6758 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T312.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T312.golden @@ -115,7 +115,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210HSym3KindInference ()) type family Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a0123456789876543210 :: c0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: b0123456789876543210 where Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210H a_0123456789876543210 a_0123456789876543210 (a :: c) (a :: b) :: b where + type family Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a :: c) (a :: b) :: b where Let0123456789876543210H a_0123456789876543210 a_0123456789876543210 _ x = x type Baz_0123456789876543210 :: a -> b -> b type family Baz_0123456789876543210 (a :: a) (a :: b) :: b where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden index d6c521c8..2ef783d0 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden @@ -33,7 +33,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Let0123456789876543210ASym0KindInference ()) type family Let0123456789876543210ASym1 wild_01234567898765432100123456789876543210 where Let0123456789876543210ASym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210A wild_01234567898765432100123456789876543210 - type family Let0123456789876543210A wild_0123456789876543210 where + type family Let0123456789876543210A wild_01234567898765432100123456789876543210 where Let0123456789876543210A wild_0123456789876543210 = Apply SuccSym0 wild_0123456789876543210 type NatMinusSym0 :: (~>) Nat ((~>) Nat Nat) data NatMinusSym0 :: (~>) Nat ((~>) Nat Nat) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T445.golden b/singletons-base/tests/compile-and-dump/Singletons/T445.golden index 0bc5e9e3..5069b00e 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T445.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T445.golden @@ -21,7 +21,7 @@ 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_0123456789876543210 x where + type family Lambda_0123456789876543210 a_01234567898765432100123456789876543210 x where Lambda_0123456789876543210 a_0123456789876543210 x = Apply (Apply (&&@#@$) (Apply EvenbSym0 x)) (Apply (Apply (>@#@$) x) (Apply LitSym0 (FromInteger 7))) data Lambda_0123456789876543210Sym0 a_01234567898765432100123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T54.golden b/singletons-base/tests/compile-and-dump/Singletons/T54.golden index b42a0216..f40240f9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T54.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T54.golden @@ -18,9 +18,9 @@ Singletons/T54.hs:(0,0)-(0,0): Splicing declarations ()) type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 e0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym1 e0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 e0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 e where + type family Let0123456789876543210Scrutinee_0123456789876543210 e0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210 e = Apply (Apply (:@#@$) NotSym0) NilSym0 - type family Case_0123456789876543210 e t where + type family Case_0123456789876543210 e0123456789876543210 t where Case_0123456789876543210 e '[_] = NotSym0 type GSym0 :: (~>) Bool Bool data GSym0 :: (~>) Bool Bool diff --git a/singletons-base/tests/compile-and-dump/Singletons/T89.golden b/singletons-base/tests/compile-and-dump/Singletons/T89.golden index 2a0e0b77..8db09927 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 n t where + type family Case_0123456789876543210 n0123456789876543210 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 07cf1123..9d827b84 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_0123456789876543210 t where + type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 a_0123456789876543210 '(_, y_0123456789876543210) = y_0123456789876543210 - type family Case_0123456789876543210 a_0123456789876543210 t where + type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 a_0123456789876543210 '(y_0123456789876543210, _) = y_0123456789876543210 - type family Case_0123456789876543210 a_0123456789876543210 t where + type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 a_0123456789876543210 '[_, y_0123456789876543210] = y_0123456789876543210 - type family Case_0123456789876543210 a_0123456789876543210 t where + type family Case_0123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 a_0123456789876543210 '[y_0123456789876543210, _] = y_0123456789876543210 type MSym0 :: Bool diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 2db513e2..952e63c3 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -744,27 +744,28 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do m_fixity = OMap.lookup name fix_env mk_tf_head :: [DTyVarBndrUnit] -> DFamilyResultSig -> DTypeFamilyHead - mk_tf_head tvbs res_sig = DTypeFamilyHead proName tvbs res_sig Nothing + mk_tf_head arg_tvbs res_sig = + dTypeFamilyHead_with_locals proName all_locals arg_tvbs res_sig (m_sak_dec, defun_ki, tf_head) = -- There are three possible cases: case m_ldrki of -- 1. We have no kind information whatsoever. Nothing -> - let all_args = local_tvbs ++ map (`DPlainTV` ()) tyvarNames in + let arg_tvbs = map (`DPlainTV` ()) tyvarNames in ( Nothing - , DefunNoSAK all_args Nothing - , mk_tf_head all_args DNoSig + , DefunNoSAK (local_tvbs ++ arg_tvbs) Nothing + , mk_tf_head arg_tvbs DNoSig ) -- 2. We have some kind information in the form of a LetDecRHSKindInfo. Just (LDRKI m_sak argKs resK) -> - let all_args = local_tvbs ++ zipWith (`DKindedTV` ()) tyvarNames argKs in + let arg_tvbs = zipWith (`DKindedTV` ()) tyvarNames argKs in case m_sak of -- 2(a). We do not have a standalone kind signature. Nothing -> ( Nothing - , DefunNoSAK all_args (Just resK) - , mk_tf_head all_args (DKindSig resK) + , DefunNoSAK (local_tvbs ++ arg_tvbs) (Just resK) + , mk_tf_head arg_tvbs (DKindSig resK) ) -- 2(b). We have a standalone kind signature. Just sak -> @@ -774,7 +775,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do -- the body of the type family declaration even if it is -- given a standalone kind signature. -- See Note [Keep redundant kind information for Haddocks]. - , mk_tf_head all_args (DKindSig resK) + , mk_tf_head arg_tvbs (DKindSig resK) ) defun_decs <- defunctionalize proName m_fixity defun_ki @@ -1022,18 +1023,16 @@ promoteExp (DLamE names exp) = do let var_proms = zip names tyNames (rhs, ann_exp) <- lambdaBind var_proms $ promoteExp exp all_locals <- allLocals - let all_args = all_locals ++ tyNames - tvbs = map (`DPlainTV` ()) all_args - emitDecs [DClosedTypeFamilyD (DTypeFamilyHead - lambdaName - tvbs - DNoSig - Nothing) - [DTySynEqn Nothing - (foldType (DConT lambdaName) $ - map DVarT all_args) - rhs]] - emitDecsM $ defunctionalize lambdaName Nothing $ DefunNoSAK tvbs Nothing + let tvbs = map (`DPlainTV` ()) tyNames + all_args = all_locals ++ tyNames + all_tvbs = map (`DPlainTV` ()) all_args + tfh = dTypeFamilyHead_with_locals lambdaName all_locals tvbs DNoSig + emitDecs [DClosedTypeFamilyD + tfh + [DTySynEqn Nothing + (foldType (DConT lambdaName) (map DVarT all_args)) + rhs]] + emitDecsM $ defunctionalize lambdaName Nothing $ DefunNoSAK all_tvbs Nothing let promLambda = foldApply (DConT (defunctionalizedName opts lambdaName 0)) (map DVarT all_locals) return (promLambda, ADLamE tyNames promLambda names ann_exp) @@ -1044,9 +1043,9 @@ promoteExp (DCaseE exp matches) = do (exp', ann_exp) <- promoteExp exp (eqns, ann_matches) <- mapAndUnzipM (promoteMatch prom_case) matches tyvarName <- qNewName "t" - let all_args = all_locals ++ [tyvarName] - tvbs = map (`DPlainTV` ()) all_args - emitDecs [DClosedTypeFamilyD (DTypeFamilyHead caseTFName tvbs DNoSig Nothing) eqns] + let tvbs = [DPlainTV tyvarName ()] + tfh = dTypeFamilyHead_with_locals caseTFName all_locals tvbs DNoSig + emitDecs [DClosedTypeFamilyD tfh eqns] -- See Note [Annotate case return type] in Single let applied_case = prom_case `DAppT` exp' return ( applied_case @@ -1092,3 +1091,37 @@ promoteLitPat (StringL str) = return $ DLitT (StrTyLit str) promoteLitPat (CharL c) = return $ DLitT (CharTyLit c) promoteLitPat lit = fail ("Only string, natural number, and character literals can be promoted: " ++ show lit) + +-- Construct a 'DTypeFamilyHead' that closes over some local variables. We +-- apply `noExactName` to each local variable to avoid GHC#11812. +-- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util. +dTypeFamilyHead_with_locals :: + Name + -- ^ Name of type family + -> [Name] + -- ^ Local variables + -> [DTyVarBndrUnit] + -- ^ Variables for type family arguments + -> DFamilyResultSig + -- ^ Type family result + -> DTypeFamilyHead +dTypeFamilyHead_with_locals tf_nm local_nms arg_tvbs res_sig = + DTypeFamilyHead + tf_nm + (map (`DPlainTV` ()) local_nms' ++ arg_tvbs') + res_sig' + Nothing + where + -- We take care to only apply `noExactName` 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 + + -- 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' + (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 6d1b3a07..c3777ccf 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Defun.hs @@ -206,6 +206,7 @@ defunctionalize name m_fixity defun_ki = do extra_name <- qNewName "arg" let sak_arg_n = length sak_arg_kis -- Use noExactName below to avoid GHC#17537. + -- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util. arg_names <- replicateM sak_arg_n (noExactName <$> qNewName "a") let -- The inner loop. @go n arg_nks res_nks@ returns @(res_k, decls)@. @@ -286,6 +287,7 @@ defunctionalize name m_fixity defun_ki = 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. (tvbs, m_res) <- eta_expand (noExactTyVars tvbs') (noExactTyVars m_res') let tvbs_n = length tvbs @@ -415,6 +417,8 @@ defunctionalize name m_fixity defun_ki = do DVisFADep tvb -> pure tvb DVisFAAnon k -> (\n -> DKindedTV n () k) <$> -- Use noExactName below to avoid GHC#19743. + -- See also Note [Pitfalls of NameU/NameL] + -- in Data.Singletons.TH.Util. (noExactName <$> qNewName "e") mk_fix_decl :: Name -> Fixity -> DDec diff --git a/singletons-th/src/Data/Singletons/TH/Util.hs b/singletons-th/src/Data/Singletons/TH/Util.hs index 26e88146..38bf7a19 100644 --- a/singletons-th/src/Data/Singletons/TH/Util.hs +++ b/singletons-th/src/Data/Singletons/TH/Util.hs @@ -373,7 +373,9 @@ filterInvisTvbArgs (DFAForalls tele args) = DForallVis _ -> res DForallInvis tvbs' -> tvbs' ++ res --- changes all TyVars not to be NameU's. Workaround for GHC#11812/#17537/#19743 +-- Change all unique Names with a NameU or NameL namespace to non-unique Names +-- by performing a syb-based traversal. See Note [Pitfalls of NameU/NameL] for +-- why this is useful. noExactTyVars :: Data a => a -> a noExactTyVars = everywhere go where @@ -393,10 +395,92 @@ noExactTyVars = everywhere go fix_inj_ann (InjectivityAnn lhs rhs) = InjectivityAnn (noExactName lhs) (map noExactName rhs) --- changes a Name not to be a NameU. Workaround for GHC#11812/#17537/#19743 +-- 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 -noExactName (Name (OccName occ) (NameU unique)) = mkName (occ ++ show unique) -noExactName n = n +noExactName n@(Name (OccName occ) ns) = + case ns of + NameU unique -> mk_name unique + NameL unique -> mk_name unique + _ -> n + where + mk_name unique = mkName (occ ++ show unique) + +{- +Note [Pitfalls of NameU/NameL] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Most of the Names used in singletons-th come from reified or quoted Template +Haskell definitions. Because these definitions have passed through GHC's +renamer, they have unique Names with unique a NameU/NameL namespace. For the +sake of convenience, we often reuse these Names in the definitions that we +generate. For example, if singletons-th is given a declaration +`f :: forall a_123. a_123 -> a_123`, it will produce a standalone kind signature +`type F :: forall a_123. a_123 -> a_123`, reusing the unique Name `a_123`. + +While reusing unique Names is convenient, it does have a downside. In +particular, GHC can sometimes get confused when the same unique Name is reused +in distinct type variable scopes. In the best case, this can lead to confusing +type errors, but in the worst case, it can cause GHC to panic, as seen in the +following issues (all of which were first observed in singletons-th): + +* https://gitlab.haskell.org/ghc/ghc/-/issues/11812 +* https://gitlab.haskell.org/ghc/ghc/-/issues/17537 +* https://gitlab.haskell.org/ghc/ghc/-/issues/19743 + +This is pretty terrible. Arguably, we are abusing Template Haskell here, since +GHC likely assumes the invariant that each unique Name only has a single +binding site. On the other hand, rearchitecting singletons-th to uphold this +invariant would require a substantial amount of work. + +A far easier solution is to identify any problematic areas where unique Names +are reused and work around the issue by changing unique Names to non-unique +Names. The issues above all have a common theme: they arise when unique Names +are reused in the type variable binders of a data type or type family +declaration. For instance, when promoting a function like this: + + f :: forall a_123. a_123 -> a_123 + f x_456 = g + where + g = x_456 + +We must promote `f` and `g` to something like this: + + type F :: forall a_123. a_123 -> a_123 + type family F (arg :: a_123) :: a_123 where + F x_456 = G x_456 + + type family LetG x_456 where + LetG x_456 = x_456 + +This looks sensible enough. But note that we are reusing the same unique Name +`x_456` in three different scopes: once in the equation for `F`, once in the +the equation for `G`, and once more in the type variable binder in +`type family LetG x_456`. The last of these scopes in particular is enough to +confuse GHC in some situations and trigger GHC#11812. + +Our workaround is to apply the `noExactName` function to such names, which +converts any Names with NameU/NameL namespaces into non-unique Names with +longer OccNames. For instance, `noExactName x_456` will return a non-unique +Name with the OccName `x456`. We use `noExactName` when generating `LetG` so +that it will instead be: + + type family LetG x456 where + LetG x_456 = x_456 + +Here, `x456` is a non-unique Name, and `x_456` is a Unique name. Thankfully, +this is sufficient to work around GHC#11812. There is still some amount of +risk, since we are reusing `x_456` in two different type family equations (one +for `LetG` and one for `F`), but GHC accepts this for now. We prefer to use the +`noExactName` in as few places as possible, as using longer OccNames makes the +Haddocks harder to read, so we will continue to reuse unique Names unless GHC +forces us to behave differently. + +In addition to the type family example above, we also make use of `noExactName` +(as well as its cousin, `noExactTyVars`) when generating defunctionalization +symbols, as these also require reusing Unique names in several type family and +data type declarations. See references to this Note in the code for particular +locations where we must apply this workaround. +-} substKind :: Map Name DKind -> DKind -> DKind substKind = substType @@ -425,16 +509,22 @@ substType _ ty@(DLitT {}) = ty substType _ ty@DWildCardT = ty subst_tele :: Map Name DKind -> DForallTelescope -> (Map Name DKind, DForallTelescope) -subst_tele s (DForallInvis tvbs) = second DForallInvis $ subst_tvbs s tvbs -subst_tele s (DForallVis tvbs) = second DForallVis $ subst_tvbs s tvbs +subst_tele s (DForallInvis tvbs) = second DForallInvis $ substTvbs s tvbs +subst_tele s (DForallVis tvbs) = second DForallVis $ substTvbs s tvbs -subst_tvbs :: Map Name DKind -> [DTyVarBndr flag] -> (Map Name DKind, [DTyVarBndr flag]) -subst_tvbs = mapAccumL substTvb +substTvbs :: Map Name DKind -> [DTyVarBndr flag] -> (Map Name DKind, [DTyVarBndr flag]) +substTvbs = mapAccumL substTvb substTvb :: Map Name DKind -> DTyVarBndr flag -> (Map Name DKind, DTyVarBndr flag) substTvb s tvb@(DPlainTV n _) = (Map.delete n s, tvb) substTvb s (DKindedTV n f k) = (Map.delete n s, DKindedTV n f (substKind s k)) +substFamilyResultSig :: Map Name DKind -> DFamilyResultSig -> (Map Name DKind, DFamilyResultSig) +substFamilyResultSig s frs@DNoSig = (s, frs) +substFamilyResultSig s (DKindSig k) = (s, DKindSig (substKind s k)) +substFamilyResultSig s (DTyVarSig tvb) = let (s', tvb') = substTvb s tvb in + (s', DTyVarSig tvb') + dropTvbKind :: DTyVarBndr flag -> DTyVarBndr flag dropTvbKind tvb@(DPlainTV {}) = tvb dropTvbKind (DKindedTV n f _) = DPlainTV n f From 965f1ae18d2668032de03474754e002289472787 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 23 Jul 2023 20:04:05 -0400 Subject: [PATCH 2/2] Implement partial support for promoting scoped type variables `singletons-th` can now promote a good number of uses of scoped type variables, save for the two exceptions now listed in the `singletons` `README`. This is accomplished by a combination of: 1. Bringing scoped type variables into scope on the left-hand sides of promoted type family equations through invisible `@` arguments when a function uses an outermost `forall` in its type signature (and does not close over any local variables). 2. Bringing scoped type variables into scope on the left-hand sides of promoted type family equations through explicit kind annotations on each of the type family's arguments when a function has an outermost `forall` in its type signature. 3. Closing over scoped type variables when lambda-lifting to ensure that the type variables are accessible when scoping over local definitions. See the new `Note [Scoped type variables]` in `Data.Singletons.TH.Promote.Monad` for more about how this is implemented. Fixes #433. --- README.md | 168 +++++++-- .../tests/SingletonsBaseTestSuite.hs | 1 + .../Singletons/CaseExpressions.golden | 42 ++- .../Singletons/LetStatements.golden | 26 +- .../Singletons/Records.golden | 4 +- .../compile-and-dump/Singletons/T183.golden | 133 ++++--- .../compile-and-dump/Singletons/T296.golden | 40 +- .../compile-and-dump/Singletons/T312.golden | 2 +- .../compile-and-dump/Singletons/T378a.golden | 2 +- .../compile-and-dump/Singletons/T378b.golden | 2 +- .../compile-and-dump/Singletons/T412.golden | 8 +- .../compile-and-dump/Singletons/T433.golden | 349 ++++++++++++++++++ .../tests/compile-and-dump/Singletons/T433.hs | 72 ++++ singletons-th/CHANGES.md | 3 + .../src/Data/Singletons/TH/Promote.hs | 117 ++++-- .../src/Data/Singletons/TH/Promote/Monad.hs | 246 ++++++++++-- .../src/Data/Singletons/TH/Syntax.hs | 17 + 17 files changed, 1037 insertions(+), 195 deletions(-) create mode 100644 singletons-base/tests/compile-and-dump/Singletons/T433.golden create mode 100644 singletons-base/tests/compile-and-dump/Singletons/T433.hs diff --git a/README.md b/README.md index e99daef8..4b9705fd 100644 --- a/README.md +++ b/README.md @@ -839,6 +839,7 @@ The following constructs are fully supported: The following constructs are partially supported: +* scoped type variables * `deriving` * finite arithmetic sequences * records @@ -850,6 +851,132 @@ The following constructs are partially supported: See the following sections for more details. +### Scoped type variables + +`singletons-th` makes an effort to track scoped type variables during promotion +so that they "just work". For instance, this function: + +```hs +f :: forall a. a -> a +f x = (x :: a) +``` + +Will be promoted to the following type family: + +```hs +type F :: forall a. a -> a +type family F x where + F @a x = (x :: a) +``` + +Note the use of `@a` on the left-hand side of the type family equation, which +ensures that `a` is in scope on the right-hand side. This also works for local +definitions, so this: + +```hs +f :: forall a. a -> a +f x = g + where + g = (x :: a) +``` + +Will promote to the following type families: + +```hs +type F :: forall a. a -> a +type family F x where + F @a x = LetG a x + +type family LetG a x where + LetG a x = (x :: a) +``` + +Note that `LetG` includes both `a` and `x` as arguments to ensure that they are +in scope on the right-hand side. + +Besides `forall`s in type signatures, scoped type variables can also come +from pattern signatures. For example, this will also work: + +```hs +f (x :: a) = g + where + g = (x :: a) +``` + +Not all forms of scoped type variables are currently supported: + +* If a type signature brings a type variable into scope over the body of a + function with a `forall`, then any pattern signatures must consistently use + the same type variable in argument types that mention it. For example, while + this will work: + + ```hs + f :: forall a. a -> a + f (x :: a) = a -- (x :: a) mentions the same type variable `a` from the type signature + ``` + + The following will _not_ work: + + ```hs + f' :: forall a. a -> a + f' (x :: b) = b -- BAD: (x :: b) mentions `b` instead of `a` + ``` + + This is because `singletons-th` would attempt to promote `f'` to the + following: + + ```hs + type F' :: forall a. a -> a + type family F' x where + F' @a (x :: b) = b + ``` + + And GHC will not infer that `b` should stand for `a`. + +* There is limited support for local variables that themselves bring type + variables into scope with `forall`s in their type signatures. For example, + this example works: + + ```hs + f local = g + where + g :: forall a. a -> a + g x = const (x :: a) local + ``` + + This is because `f` and `g` will be promoted like so: + + ```hs + type family F local where + F local = G local + + type family G local x where + G local (x :: a) = Const (x :: a) local + ``` + + It is not straightforward to give `G` a standalone kind signature, and + without a standalone kind signature, GHC will not allow writing `@a` on the + left-hand side of `G`'s type family equation. On the other hand, we can still + ensure that `a` is brought into scope by writing `(x :: a)` instead of `x` on + the left-hand side. While the `:: a` signature was not present in the + original definition, we include it anyway during promotion to ensure that + definitions like `G` kind-check. + + This trick only works if the scoped type variable is mentioned in one of the + local definition's arguments, however. If the scoped type variable is only + mentioned in the return type, then the promoted definition will not + kind-check. This means that examples like this one will not work: + + ```hs + konst :: a -> Maybe Bool -> a + konst x _ = x + + f x = konst x y + where + y :: forall b. Maybe b + y = Nothing :: Maybe b + ``` + ### `deriving` `singletons-th` is slightly more conservative with respect to `deriving` than @@ -1304,7 +1431,6 @@ underyling pattern instead. The following constructs are either unsupported or almost never work: -* scoped type variables * datatypes that store arrows or `Symbol` * rank-n types * promoting `TypeRep`s @@ -1315,46 +1441,6 @@ The following constructs are either unsupported or almost never work: See the following sections for more details. -### Scoped type variables - -Promoting functions that rely on the behavior of `ScopedTypeVariables` is very -tricky—see -[this GitHub issue](https://github.com/goldfirere/singletons/issues/433) for an -extended discussion on the topic. This is not to say that promoting functions -that rely on `ScopedTypeVariables` is guaranteed to fail, but it is rather -fragile. To demonstrate how fragile this is, note that the following function -will promote successfully: - -```hs -f :: forall a. a -> a -f x = id x :: a -``` - -But this one will not: - -```hs -g :: forall a. a -> a -g x = id (x :: a) -``` - -There are usually workarounds one can use instead of `ScopedTypeVariables`: - -1. Use pattern signatures: - - ```hs - g :: forall a. a -> a - g (x :: a) = id (x :: a) - ``` -2. Use local definitions: - - ```hs - g :: forall a. a -> a - g x = id' a - where - id' :: a -> a - id' x = x - ``` - ### Arrows, `Symbol`, and literals As described in the promotion paper, automatic promotion of datatypes that diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs index 1747b03c..d2ea3e6d 100644 --- a/singletons-base/tests/SingletonsBaseTestSuite.hs +++ b/singletons-base/tests/SingletonsBaseTestSuite.hs @@ -132,6 +132,7 @@ tests = , compileAndDumpStdTest "T410" , compileAndDumpStdTest "T412" , compileAndDumpStdTest "T414" + , compileAndDumpStdTest "T433" , compileAndDumpStdTest "T443" , afterSingletonsNat . compileAndDumpStdTest "T445" diff --git a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden index d032e58d..32bb0544 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden @@ -69,28 +69,36 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations Lambda_0123456789876543210Sym3 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 = Lambda_0123456789876543210 y0123456789876543210 x0123456789876543210 arg_01234567898765432100123456789876543210 type family Case_0123456789876543210 x0123456789876543210 t where Case_0123456789876543210 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 y) x) y - data Let0123456789876543210ZSym0 y0123456789876543210 + data Let0123456789876543210ZSym0 a0123456789876543210 where Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) => - Let0123456789876543210ZSym0 y0123456789876543210 - type instance Apply Let0123456789876543210ZSym0 y0123456789876543210 = Let0123456789876543210ZSym1 y0123456789876543210 + Let0123456789876543210ZSym0 a0123456789876543210 + type instance Apply Let0123456789876543210ZSym0 a0123456789876543210 = Let0123456789876543210ZSym1 a0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210ZSym0KindInference ()) - data Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210 + data Let0123456789876543210ZSym1 a0123456789876543210 y0123456789876543210 where - Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 y0123456789876543210) arg) (Let0123456789876543210ZSym2 y0123456789876543210 arg) => - Let0123456789876543210ZSym1 y0123456789876543210 x0123456789876543210 - type instance Apply (Let0123456789876543210ZSym1 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210 - instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 y0123456789876543210) where + Let0123456789876543210ZSym1KindInference :: SameKind (Apply (Let0123456789876543210ZSym1 a0123456789876543210) arg) (Let0123456789876543210ZSym2 a0123456789876543210 arg) => + Let0123456789876543210ZSym1 a0123456789876543210 y0123456789876543210 + type instance Apply (Let0123456789876543210ZSym1 a0123456789876543210) y0123456789876543210 = Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210ZSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210ZSym1KindInference ()) - type family Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where - Let0123456789876543210ZSym2 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z y0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Z y0123456789876543210 x0123456789876543210 :: a where - Let0123456789876543210Z y x = y - type family Case_0123456789876543210 x0123456789876543210 t where - Case_0123456789876543210 x y = Let0123456789876543210ZSym2 y x + data Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 x0123456789876543210 + where + Let0123456789876543210ZSym2KindInference :: SameKind (Apply (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) arg) (Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 arg) => + Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210 x0123456789876543210 + type instance Apply (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210ZSym2 a0123456789876543210 y0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210ZSym2KindInference ()) + type family Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + Let0123456789876543210ZSym3 a0123456789876543210 y0123456789876543210 x0123456789876543210 = Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 + type family Let0123456789876543210Z a0123456789876543210 y0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + Let0123456789876543210Z a y x = y + type family Case_0123456789876543210 a0123456789876543210 x0123456789876543210 t where + Case_0123456789876543210 a x y = Let0123456789876543210ZSym3 a y x data Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) => @@ -223,7 +231,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations Foo5 x = Case_0123456789876543210 x x type Foo4 :: forall a. a -> a type family Foo4 (a :: a) :: a where - Foo4 x = Case_0123456789876543210 x x + Foo4 @a (x :: a) = Case_0123456789876543210 a x x type Foo3 :: a -> b -> a type family Foo3 (a :: a) (a :: b) :: a where Foo3 a b = Case_0123456789876543210 a b (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a b) @@ -262,11 +270,11 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations sY) sFoo4 (sX :: Sing x) = id - @(Sing (Case_0123456789876543210 x x)) + @(Sing (Case_0123456789876543210 a x x)) (case sX of (sY :: Sing y) -> let - sZ :: (Sing (Let0123456789876543210ZSym2 y x :: a) :: Type) + sZ :: (Sing (Let0123456789876543210ZSym3 a y x :: a) :: Type) sZ = sY in sZ) sFoo3 (sA :: Sing a) (sB :: Sing b) diff --git a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden index a041eaf0..2e8ac33d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden @@ -233,18 +233,26 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations Let0123456789876543210Y x = Case_0123456789876543210 x (Let0123456789876543210X_0123456789876543210Sym1 x) type family Let0123456789876543210X_0123456789876543210 x0123456789876543210 where Let0123456789876543210X_0123456789876543210 x = Apply (Apply Tuple2Sym0 (Apply SuccSym0 x)) x - data Let0123456789876543210BarSym0 x0123456789876543210 + data Let0123456789876543210BarSym0 a0123456789876543210 where Let0123456789876543210BarSym0KindInference :: SameKind (Apply Let0123456789876543210BarSym0 arg) (Let0123456789876543210BarSym1 arg) => - Let0123456789876543210BarSym0 x0123456789876543210 - type instance Apply Let0123456789876543210BarSym0 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210 + Let0123456789876543210BarSym0 a0123456789876543210 + type instance Apply Let0123456789876543210BarSym0 a0123456789876543210 = Let0123456789876543210BarSym1 a0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210BarSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210BarSym0KindInference ()) - type family Let0123456789876543210BarSym1 x0123456789876543210 :: a0123456789876543210 where - Let0123456789876543210BarSym1 x0123456789876543210 = Let0123456789876543210Bar x0123456789876543210 - type family Let0123456789876543210Bar x0123456789876543210 :: a where - Let0123456789876543210Bar x = x + data Let0123456789876543210BarSym1 a0123456789876543210 x0123456789876543210 + where + Let0123456789876543210BarSym1KindInference :: SameKind (Apply (Let0123456789876543210BarSym1 a0123456789876543210) arg) (Let0123456789876543210BarSym2 a0123456789876543210 arg) => + Let0123456789876543210BarSym1 a0123456789876543210 x0123456789876543210 + type instance Apply (Let0123456789876543210BarSym1 a0123456789876543210) x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210BarSym1 a0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210BarSym1KindInference ()) + type family Let0123456789876543210BarSym2 a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + Let0123456789876543210BarSym2 a0123456789876543210 x0123456789876543210 = Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 + type family Let0123456789876543210Bar a0123456789876543210 x0123456789876543210 :: a0123456789876543210 where + Let0123456789876543210Bar a x = x data (<<<%%%%%%%%%%%%%%%%%%%%@#@$) x0123456789876543210 where (:<<<%%%%%%%%%%%%%%%%%%%%@#@$###) :: SameKind (Apply (<<<%%%%%%%%%%%%%%%%%%%%@#@$) arg) ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) arg) => @@ -726,7 +734,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations Foo13_ y = y type Foo13 :: forall a. a -> a type family Foo13 (a :: a) :: a where - Foo13 x = Apply Foo13_Sym0 (Let0123456789876543210BarSym1 x) + Foo13 @a (x :: a) = Apply Foo13_Sym0 (Let0123456789876543210BarSym2 a x) type Foo12 :: Nat -> Nat type family Foo12 (a :: Nat) :: Nat where Foo12 x = Apply (Apply ((<<<%%%%%%%%%%%%%%%%%%%%@#@$$) x) x) (Apply SuccSym0 (Apply SuccSym0 ZeroSym0)) @@ -832,7 +840,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations sFoo13_ (sY :: Sing y) = sY sFoo13 (sX :: Sing x) = let - sBar :: (Sing (Let0123456789876543210BarSym1 x :: a) :: Type) + sBar :: (Sing (Let0123456789876543210BarSym2 a x :: a) :: Type) sBar = sX in applySing (singFun1 @Foo13_Sym0 sFoo13_) sBar sFoo12 (sX :: Sing x) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Records.golden b/singletons-base/tests/compile-and-dump/Singletons/Records.golden index 1954a9e4..757c3ca1 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Records.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Records.golden @@ -46,10 +46,10 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations Field1Sym1 a0123456789876543210 = Field1 a0123456789876543210 type Field2 :: forall a. Record a -> Bool type family Field2 (a :: Record a) :: Bool where - Field2 (MkRecord _ field) = field + Field2 @a (MkRecord _ field :: Record a) = field type Field1 :: forall a. Record a -> a type family Field1 (a :: Record a) :: a where - Field1 (MkRecord field _) = field + Field1 @a (MkRecord field _ :: Record a) = field sField2 :: forall a (t :: Record a). Sing t -> Sing (Apply Field2Sym0 t :: Bool) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T183.golden b/singletons-base/tests/compile-and-dump/Singletons/T183.golden index c13c0c7d..1f358258 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T183.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T183.golden @@ -59,67 +59,102 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations g :: a -> b -> a g y _ = y in g x () - data Let0123456789876543210GSym0 x0123456789876543210 + data Let0123456789876543210GSym0 a0123456789876543210 where Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) => - Let0123456789876543210GSym0 x0123456789876543210 - type instance Apply Let0123456789876543210GSym0 x0123456789876543210 = Let0123456789876543210GSym1 x0123456789876543210 + Let0123456789876543210GSym0 a0123456789876543210 + type instance Apply Let0123456789876543210GSym0 a0123456789876543210 = Let0123456789876543210GSym1 a0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210GSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym0KindInference ()) - data Let0123456789876543210GSym1 x0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210) + data Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 where - Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 x0123456789876543210) arg) (Let0123456789876543210GSym2 x0123456789876543210 arg) => - Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210 - type instance Apply (Let0123456789876543210GSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 - instance SuppressUnusedWarnings (Let0123456789876543210GSym1 x0123456789876543210) where + Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 a0123456789876543210) arg) (Let0123456789876543210GSym2 a0123456789876543210 arg) => + Let0123456789876543210GSym1 a0123456789876543210 x0123456789876543210 + type instance Apply (Let0123456789876543210GSym1 a0123456789876543210) x0123456789876543210 = Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym1KindInference ()) - data Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 a0123456789876543210 + data Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 a0123456789876543210) where - Let0123456789876543210GSym2KindInference :: SameKind (Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 arg) => - Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 a0123456789876543210 - type instance Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) a0123456789876543210 = Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 - instance SuppressUnusedWarnings (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) where + Let0123456789876543210GSym2KindInference :: SameKind (Apply (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210) arg) (Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 arg) => + Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210 a0123456789876543210 + type instance Apply (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym2 a0123456789876543210 x0123456789876543210) where suppressUnusedWarnings = snd ((,) Let0123456789876543210GSym2KindInference ()) - type family Let0123456789876543210GSym3 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: a0123456789876543210 where - Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 - type family Let0123456789876543210G x0123456789876543210 (a :: a) (a :: b) :: a where - Let0123456789876543210G x y _ = y - data Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 + data Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) :: (~>) b0123456789876543210 a0123456789876543210 + where + Let0123456789876543210GSym3KindInference :: SameKind (Apply (Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym4 a0123456789876543210 x0123456789876543210 a0123456789876543210 arg) => + Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 + type instance Apply (Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 a0123456789876543210) a0123456789876543210 = Let0123456789876543210G a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym3 a0123456789876543210 x0123456789876543210 a0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym3KindInference ()) + type family Let0123456789876543210GSym4 a0123456789876543210 x0123456789876543210 (a0123456789876543210 :: a0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: a0123456789876543210 where + Let0123456789876543210GSym4 a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G a0123456789876543210 x0123456789876543210 a0123456789876543210 a0123456789876543210 + type family Let0123456789876543210G a0123456789876543210 x0123456789876543210 (a :: a0123456789876543210) (a :: b) :: a0123456789876543210 where + Let0123456789876543210G a x y _ = y + data Let0123456789876543210XSym0 a0123456789876543210 where Let0123456789876543210XSym0KindInference :: SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) => - Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 - type instance Apply Let0123456789876543210XSym0 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210 + Let0123456789876543210XSym0 a0123456789876543210 + type instance Apply Let0123456789876543210XSym0 a0123456789876543210 = Let0123456789876543210XSym1 a0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210XSym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210XSym0KindInference ()) - type family Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 where - Let0123456789876543210XSym1 wild_01234567898765432100123456789876543210 = Let0123456789876543210X wild_01234567898765432100123456789876543210 - type family Let0123456789876543210X wild_01234567898765432100123456789876543210 where - Let0123456789876543210X wild_0123456789876543210 = Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a - type family Let0123456789876543210XSym0 where - Let0123456789876543210XSym0 = Let0123456789876543210X - type family Let0123456789876543210X where - Let0123456789876543210X = NothingSym0 :: Maybe a - data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 + data Let0123456789876543210XSym1 a0123456789876543210 wild_01234567898765432100123456789876543210 + where + Let0123456789876543210XSym1KindInference :: SameKind (Apply (Let0123456789876543210XSym1 a0123456789876543210) arg) (Let0123456789876543210XSym2 a0123456789876543210 arg) => + Let0123456789876543210XSym1 a0123456789876543210 wild_01234567898765432100123456789876543210 + type instance Apply (Let0123456789876543210XSym1 a0123456789876543210) wild_01234567898765432100123456789876543210 = Let0123456789876543210X a0123456789876543210 wild_01234567898765432100123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210XSym1 a0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210XSym1KindInference ()) + type family Let0123456789876543210XSym2 a0123456789876543210 wild_01234567898765432100123456789876543210 where + Let0123456789876543210XSym2 a0123456789876543210 wild_01234567898765432100123456789876543210 = Let0123456789876543210X a0123456789876543210 wild_01234567898765432100123456789876543210 + type family Let0123456789876543210X a0123456789876543210 wild_01234567898765432100123456789876543210 where + Let0123456789876543210X a wild_0123456789876543210 = Apply JustSym0 (wild_0123456789876543210 :: a) :: Maybe a + data Let0123456789876543210XSym0 a0123456789876543210 + where + Let0123456789876543210XSym0KindInference :: SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) => + Let0123456789876543210XSym0 a0123456789876543210 + type instance Apply Let0123456789876543210XSym0 a0123456789876543210 = Let0123456789876543210X a0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210XSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210XSym0KindInference ()) + type family Let0123456789876543210XSym1 a0123456789876543210 where + Let0123456789876543210XSym1 a0123456789876543210 = Let0123456789876543210X a0123456789876543210 + type family Let0123456789876543210X a0123456789876543210 where + Let0123456789876543210X a = NothingSym0 :: Maybe a + data Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 where Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) => - Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 - type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 + Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 + type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 a0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 a0123456789876543210 instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where suppressUnusedWarnings = snd ((,) Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference ()) - type family Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 where - Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 - type family Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210 where - Let0123456789876543210Scrutinee_0123456789876543210 x = x :: Maybe a - type family Case_0123456789876543210 x0123456789876543210 t where - Case_0123456789876543210 x ('Just (y :: a) :: Maybe a) = Apply JustSym0 (Apply JustSym0 (y :: a) :: Maybe a) + data Let0123456789876543210Scrutinee_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 + where + Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 a0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 arg) => + Let0123456789876543210Scrutinee_0123456789876543210Sym1 a0123456789876543210 x0123456789876543210 + type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 a0123456789876543210) x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 x0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 a0123456789876543210) where + suppressUnusedWarnings + = snd + ((,) + Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference + ()) + type family Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 x0123456789876543210 where + Let0123456789876543210Scrutinee_0123456789876543210Sym2 a0123456789876543210 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 x0123456789876543210 + type family Let0123456789876543210Scrutinee_0123456789876543210 a0123456789876543210 x0123456789876543210 where + 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 Case_0123456789876543210 arg_0123456789876543210 a_0123456789876543210 '(x :: a, y :: b) = Apply (Apply Tuple2Sym0 (y :: b)) (x :: a) @@ -306,17 +341,17 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations F1Sym1 a0123456789876543210 = F1 a0123456789876543210 type Foo9 :: a -> a type family Foo9 (a :: a) :: a where - Foo9 (x :: a) = Apply (Apply (Let0123456789876543210GSym1 x) x) Tuple0Sym0 + Foo9 (x :: a) = Apply (Apply (Let0123456789876543210GSym2 a x) x) Tuple0Sym0 type Foo8 :: forall a. Maybe a -> Maybe a type family Foo8 (a :: Maybe a) :: Maybe a where - Foo8 ('Just (wild_0123456789876543210 :: a) :: Maybe a) = Let0123456789876543210XSym1 wild_0123456789876543210 - Foo8 ('Nothing :: Maybe a) = Let0123456789876543210XSym0 + Foo8 @a ('Just (wild_0123456789876543210 :: a) :: Maybe a :: Maybe a) = Let0123456789876543210XSym2 a wild_0123456789876543210 + Foo8 @a ('Nothing :: Maybe a :: Maybe a) = Let0123456789876543210XSym1 a type Foo7 :: a -> b -> a type family Foo7 (a :: a) (a :: b) :: a where Foo7 (x :: a) (wild_0123456789876543210 :: b) = x :: a type Foo6 :: Maybe (Maybe a) -> Maybe (Maybe a) type family Foo6 (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where - Foo6 ('Just x :: Maybe (Maybe a)) = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) + Foo6 ('Just x :: Maybe (Maybe a)) = Case_0123456789876543210 a x (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a x) type Foo5 :: Maybe (Maybe a) -> Maybe (Maybe a) type family Foo5 (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where Foo5 ('Just ('Just (x :: a) :: Maybe a) :: Maybe (Maybe a)) = Apply JustSym0 (Apply JustSym0 (x :: a) :: Maybe a) :: Maybe (Maybe a) @@ -325,10 +360,10 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations Foo4 a_0123456789876543210 = Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210 type Foo3 :: forall a. Maybe a -> a type family Foo3 (a :: Maybe a) :: a where - Foo3 ('Just x) = x :: a + Foo3 @a ('Just x :: Maybe a) = x :: a type Foo2 :: forall a. Maybe a -> a type family Foo2 (a :: Maybe a) :: a where - Foo2 ('Just x :: Maybe a) = x :: a + Foo2 @a ('Just x :: Maybe a :: Maybe a) = x :: a type Foo1 :: Maybe a -> a type family Foo1 (a :: Maybe a) :: a where Foo1 ('Just x :: Maybe a) = x :: a @@ -376,11 +411,11 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations (forall (t :: a) (t :: b). Sing t -> Sing t - -> Sing (Apply (Apply (Let0123456789876543210GSym1 x) t) t :: a) :: Type) + -> Sing (Apply (Apply (Let0123456789876543210GSym2 a x) t) t :: a) :: Type) sG (sY :: Sing y) _ = sY in applySing - (applySing (singFun2 @(Let0123456789876543210GSym1 x) sG) sX) + (applySing (singFun2 @(Let0123456789876543210GSym2 a x) sG) sX) STuple0 sFoo8 (SJust (sWild_0123456789876543210 :: Sing wild_0123456789876543210)) @@ -394,7 +429,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations (_ :: Sing ('Just (wild_0123456789876543210 :: a) :: Maybe a)) -> let sX :: - Sing @_ (Let0123456789876543210XSym1 wild_0123456789876543210) + Sing @_ (Let0123456789876543210XSym2 a wild_0123456789876543210) sX = applySing (singFun1 @JustSym0 SJust) @@ -406,7 +441,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations = case SNothing of (_ :: Sing ('Nothing :: Maybe a)) -> let - sX :: Sing @_ Let0123456789876543210XSym0 + sX :: Sing @_ (Let0123456789876543210XSym1 a) sX = SNothing :: Sing (NothingSym0 :: Maybe a) in sX sFoo7 @@ -425,11 +460,11 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations (_ :: Sing ('Just x :: Maybe (Maybe a))) -> let sScrutinee_0123456789876543210 :: - Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) + Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a x) sScrutinee_0123456789876543210 = sX :: Sing (x :: Maybe a) in id - @(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x))) + @(Sing (Case_0123456789876543210 a x (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a x))) (case sScrutinee_0123456789876543210 of SJust (sY :: Sing y) -> case (,) (sY :: Sing y) (SJust (sY :: Sing y)) of diff --git a/singletons-base/tests/compile-and-dump/Singletons/T296.golden b/singletons-base/tests/compile-and-dump/Singletons/T296.golden index 8ca6565f..baa3bf10 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T296.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T296.golden @@ -23,16 +23,30 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations type MyProxySym0 :: forall (a :: Type). MyProxy (a :: Type) type family MyProxySym0 :: MyProxy (a :: Type) where MyProxySym0 = MyProxy - type Let0123456789876543210ZSym0 :: MyProxy a - type family Let0123456789876543210ZSym0 :: MyProxy a where - Let0123456789876543210ZSym0 = Let0123456789876543210Z - type Let0123456789876543210Z :: MyProxy a - type family Let0123456789876543210Z :: MyProxy a where - Let0123456789876543210Z = MyProxySym0 - type family Let0123456789876543210XSym0 where - Let0123456789876543210XSym0 = Let0123456789876543210X - type family Let0123456789876543210X where - Let0123456789876543210X = Let0123456789876543210ZSym0 + data Let0123456789876543210ZSym0 a0123456789876543210 + where + Let0123456789876543210ZSym0KindInference :: SameKind (Apply Let0123456789876543210ZSym0 arg) (Let0123456789876543210ZSym1 arg) => + Let0123456789876543210ZSym0 a0123456789876543210 + type instance Apply Let0123456789876543210ZSym0 a0123456789876543210 = Let0123456789876543210Z a0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210ZSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210ZSym0KindInference ()) + type family Let0123456789876543210ZSym1 a0123456789876543210 :: MyProxy a0123456789876543210 where + Let0123456789876543210ZSym1 a0123456789876543210 = Let0123456789876543210Z a0123456789876543210 + type family Let0123456789876543210Z a0123456789876543210 :: MyProxy a0123456789876543210 where + Let0123456789876543210Z a = MyProxySym0 + data Let0123456789876543210XSym0 a0123456789876543210 + where + Let0123456789876543210XSym0KindInference :: SameKind (Apply Let0123456789876543210XSym0 arg) (Let0123456789876543210XSym1 arg) => + Let0123456789876543210XSym0 a0123456789876543210 + type instance Apply Let0123456789876543210XSym0 a0123456789876543210 = Let0123456789876543210X a0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210XSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210XSym0KindInference ()) + type family Let0123456789876543210XSym1 a0123456789876543210 where + Let0123456789876543210XSym1 a0123456789876543210 = Let0123456789876543210X a0123456789876543210 + type family Let0123456789876543210X a0123456789876543210 where + Let0123456789876543210X a = Let0123456789876543210ZSym1 a type FSym0 :: forall a. (~>) (MyProxy a) (MyProxy a) data FSym0 :: (~>) (MyProxy a) (MyProxy a) where @@ -46,16 +60,16 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations FSym1 a0123456789876543210 = F a0123456789876543210 type F :: forall a. MyProxy a -> MyProxy a type family F (a :: MyProxy a) :: MyProxy a where - F MyProxy = Let0123456789876543210XSym0 + F @a (MyProxy :: MyProxy a) = Let0123456789876543210XSym1 a sF :: forall a (t :: MyProxy a). Sing t -> Sing (Apply FSym0 t :: MyProxy a) sF SMyProxy = let - sX :: Sing @_ Let0123456789876543210XSym0 + sX :: Sing @_ (Let0123456789876543210XSym1 a) sX = let - sZ :: (Sing (Let0123456789876543210ZSym0 :: MyProxy a) :: Type) + sZ :: (Sing (Let0123456789876543210ZSym1 a :: MyProxy a) :: Type) sZ = SMyProxy in sZ in sX diff --git a/singletons-base/tests/compile-and-dump/Singletons/T312.golden b/singletons-base/tests/compile-and-dump/Singletons/T312.golden index 9e4e6758..1cc43ad6 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T312.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T312.golden @@ -116,7 +116,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations type family Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a0123456789876543210 :: c0123456789876543210) (a0123456789876543210 :: b0123456789876543210) :: b0123456789876543210 where Let0123456789876543210HSym4 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a0123456789876543210 a0123456789876543210 type family Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a :: c) (a :: b) :: b where - Let0123456789876543210H a_0123456789876543210 a_0123456789876543210 _ x = x + Let0123456789876543210H a_0123456789876543210 a_0123456789876543210 (_ :: c) (x :: b) = x type Baz_0123456789876543210 :: a -> b -> b type family Baz_0123456789876543210 (a :: a) (a :: b) :: b where Baz_0123456789876543210 a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Let0123456789876543210HSym2 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) a_0123456789876543210 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378a.golden b/singletons-base/tests/compile-and-dump/Singletons/T378a.golden index 1bc467fa..3e4eb043 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T378a.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T378a.golden @@ -51,7 +51,7 @@ Singletons/T378a.hs:(0,0)-(0,0): Splicing declarations ConstBASym2 a0123456789876543210 a0123456789876543210 = ConstBA a0123456789876543210 a0123456789876543210 type ConstBA :: forall b a. a -> b -> a type family ConstBA (a :: a) (a :: b) :: a where - ConstBA x _ = x + ConstBA @b @a (x :: a) (_ :: b) = x sConstBA :: forall b a (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply ConstBASym0 t) t :: a) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden index 2ef783d0..bf234afd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden @@ -80,7 +80,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations NatMinus ('Succ wild_0123456789876543210) 'Zero = Let0123456789876543210ASym1 wild_0123456789876543210 type F :: forall b a. a -> b -> () type family F (a :: a) (a :: b) :: () where - F _ _ = Tuple0Sym0 + F @b @a (_ :: a) (_ :: b) = Tuple0Sym0 type PC :: forall b a. a -> b -> Constraint class PC x y sNatMinus :: diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden index d2205e13..ac718d4c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden @@ -114,10 +114,10 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations infixr 5 `D1ASym1` type D1B :: forall a b. D1 a b -> b type family D1B (a :: D1 a b) :: b where - D1B (MkD1 _ field) = field + D1B @a @b (MkD1 _ field :: D1 a b) = field type D1A :: forall a b. D1 a b -> a type family D1A (a :: D1 a b) :: a where - D1A (MkD1 field _) = field + D1A @a @b (MkD1 field _ :: D1 a b) = field infixr 5 `D1B` infixr 5 `D1A` infix 5 `PC1` @@ -343,11 +343,11 @@ Singletons/T412.hs:0:0:: Splicing declarations type D2B :: forall (a :: Type) (b :: Type). D2 (a :: Type) (b :: Type) -> b type family D2B (a :: D2 (a :: Type) (b :: Type)) :: b where - D2B ('MkD2 _ field) = field + D2B @a @b ('MkD2 _ field :: D2 (a :: Type) (b :: Type)) = field type D2A :: forall (a :: Type) (b :: Type). D2 (a :: Type) (b :: Type) -> a type family D2A (a :: D2 (a :: Type) (b :: Type)) :: a where - D2A ('MkD2 field _) = field + D2A @a @b ('MkD2 field _ :: D2 (a :: Type) (b :: Type)) = field sD2B :: forall (a :: Type) (b :: Type) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T433.golden b/singletons-base/tests/compile-and-dump/Singletons/T433.golden new file mode 100644 index 00000000..3a7cff36 --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Singletons/T433.golden @@ -0,0 +1,349 @@ +Singletons/T433.hs:(0,0)-(0,0): Splicing declarations + promote + [d| konst1 :: a -> Bool -> a + konst1 x _ = x + konst2 :: a -> Maybe Bool -> a + konst2 x _ = x + f local + = g + where + g :: forall a. a -> a + g x = konst1 (x :: a) local + foo :: forall a. a -> () + foo x = const () (Nothing :: Maybe a) + id2 :: forall a. a -> a + id2 x = id (x :: a) + id3 :: a -> a + id3 (x :: b) = id (x :: b) + id4 :: forall a. a -> a + id4 (x :: a) = id (x :: a) + id5 :: forall a. a -> a + id5 + = g + where + g = id :: a -> a + id6 :: a -> a + id6 (x :: b) + = g + where + g = (x :: b) + id7 (x :: b) + = g + where + g = (x :: b) + id8 :: a -> a + id8 x + = g x True + where + g :: b -> a -> b + g y _ = y |] + ======> + konst1 :: a -> Bool -> a + konst1 x _ = x + konst2 :: a -> Maybe Bool -> a + konst2 x _ = x + f local + = g + where + g :: forall a. a -> a + g x = konst1 (x :: a) local + foo :: forall a. a -> () + foo x = const () (Nothing :: Maybe a) + id2 :: forall a. a -> a + id2 x = id (x :: a) + id3 :: a -> a + id3 (x :: b) = id (x :: b) + id4 :: forall a. a -> a + id4 (x :: a) = id (x :: a) + id5 :: forall a. a -> a + id5 + = g + where + g = id :: a -> a + id6 :: a -> a + id6 (x :: b) + = g + where + g = x :: b + id7 (x :: b) + = g + where + g = x :: b + id8 :: a -> a + id8 x + = g x True + where + g :: b -> a -> b + g y _ = y + data Let0123456789876543210GSym0 x0123456789876543210 + where + Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) => + Let0123456789876543210GSym0 x0123456789876543210 + type instance Apply Let0123456789876543210GSym0 x0123456789876543210 = Let0123456789876543210GSym1 x0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210GSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym0KindInference ()) + data Let0123456789876543210GSym1 x0123456789876543210 :: (~>) b0123456789876543210 ((~>) a0123456789876543210 b0123456789876543210) + where + Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 x0123456789876543210) arg) (Let0123456789876543210GSym2 x0123456789876543210 arg) => + Let0123456789876543210GSym1 x0123456789876543210 a0123456789876543210 + type instance Apply (Let0123456789876543210GSym1 x0123456789876543210) a0123456789876543210 = Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym1 x0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym1KindInference ()) + data Let0123456789876543210GSym2 x0123456789876543210 (a0123456789876543210 :: b0123456789876543210) :: (~>) a0123456789876543210 b0123456789876543210 + where + Let0123456789876543210GSym2KindInference :: SameKind (Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) arg) (Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 arg) => + Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210 a0123456789876543210 + type instance Apply (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) a0123456789876543210 = Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym2 x0123456789876543210 a0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym2KindInference ()) + type family Let0123456789876543210GSym3 x0123456789876543210 (a0123456789876543210 :: b0123456789876543210) (a0123456789876543210 :: a0123456789876543210) :: b0123456789876543210 where + Let0123456789876543210GSym3 x0123456789876543210 a0123456789876543210 a0123456789876543210 = Let0123456789876543210G x0123456789876543210 a0123456789876543210 a0123456789876543210 + type family Let0123456789876543210G x0123456789876543210 (a :: b) (a :: a) :: b where + Let0123456789876543210G x y _ = y + data Let0123456789876543210GSym0 b0123456789876543210 + where + Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) => + Let0123456789876543210GSym0 b0123456789876543210 + type instance Apply Let0123456789876543210GSym0 b0123456789876543210 = Let0123456789876543210GSym1 b0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210GSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym0KindInference ()) + data Let0123456789876543210GSym1 b0123456789876543210 x0123456789876543210 + where + Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 b0123456789876543210) arg) (Let0123456789876543210GSym2 b0123456789876543210 arg) => + Let0123456789876543210GSym1 b0123456789876543210 x0123456789876543210 + type instance Apply (Let0123456789876543210GSym1 b0123456789876543210) x0123456789876543210 = Let0123456789876543210G b0123456789876543210 x0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym1 b0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym1KindInference ()) + type family Let0123456789876543210GSym2 b0123456789876543210 x0123456789876543210 where + Let0123456789876543210GSym2 b0123456789876543210 x0123456789876543210 = Let0123456789876543210G b0123456789876543210 x0123456789876543210 + type family Let0123456789876543210G b0123456789876543210 x0123456789876543210 where + Let0123456789876543210G b x = x :: b + data Let0123456789876543210GSym0 b0123456789876543210 + where + Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) => + Let0123456789876543210GSym0 b0123456789876543210 + type instance Apply Let0123456789876543210GSym0 b0123456789876543210 = Let0123456789876543210GSym1 b0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210GSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym0KindInference ()) + data Let0123456789876543210GSym1 b0123456789876543210 x0123456789876543210 + where + Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 b0123456789876543210) arg) (Let0123456789876543210GSym2 b0123456789876543210 arg) => + Let0123456789876543210GSym1 b0123456789876543210 x0123456789876543210 + type instance Apply (Let0123456789876543210GSym1 b0123456789876543210) x0123456789876543210 = Let0123456789876543210G b0123456789876543210 x0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym1 b0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym1KindInference ()) + type family Let0123456789876543210GSym2 b0123456789876543210 x0123456789876543210 where + Let0123456789876543210GSym2 b0123456789876543210 x0123456789876543210 = Let0123456789876543210G b0123456789876543210 x0123456789876543210 + type family Let0123456789876543210G b0123456789876543210 x0123456789876543210 where + Let0123456789876543210G b x = x :: b + data Let0123456789876543210GSym0 a0123456789876543210 + where + Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) => + Let0123456789876543210GSym0 a0123456789876543210 + type instance Apply Let0123456789876543210GSym0 a0123456789876543210 = Let0123456789876543210GSym1 a0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210GSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym0KindInference ()) + data Let0123456789876543210GSym1 a0123456789876543210 a_01234567898765432100123456789876543210 + where + Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 a0123456789876543210) arg) (Let0123456789876543210GSym2 a0123456789876543210 arg) => + Let0123456789876543210GSym1 a0123456789876543210 a_01234567898765432100123456789876543210 + type instance Apply (Let0123456789876543210GSym1 a0123456789876543210) a_01234567898765432100123456789876543210 = Let0123456789876543210G a0123456789876543210 a_01234567898765432100123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym1 a0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym1KindInference ()) + type family Let0123456789876543210GSym2 a0123456789876543210 a_01234567898765432100123456789876543210 where + Let0123456789876543210GSym2 a0123456789876543210 a_01234567898765432100123456789876543210 = Let0123456789876543210G a0123456789876543210 a_01234567898765432100123456789876543210 + type family Let0123456789876543210G a0123456789876543210 a_01234567898765432100123456789876543210 where + Let0123456789876543210G a a_0123456789876543210 = IdSym0 :: (~>) a a + data Let0123456789876543210GSym0 local0123456789876543210 + where + Let0123456789876543210GSym0KindInference :: SameKind (Apply Let0123456789876543210GSym0 arg) (Let0123456789876543210GSym1 arg) => + Let0123456789876543210GSym0 local0123456789876543210 + type instance Apply Let0123456789876543210GSym0 local0123456789876543210 = Let0123456789876543210GSym1 local0123456789876543210 + instance SuppressUnusedWarnings Let0123456789876543210GSym0 where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym0KindInference ()) + data Let0123456789876543210GSym1 local0123456789876543210 :: (~>) a0123456789876543210 a0123456789876543210 + where + Let0123456789876543210GSym1KindInference :: SameKind (Apply (Let0123456789876543210GSym1 local0123456789876543210) arg) (Let0123456789876543210GSym2 local0123456789876543210 arg) => + Let0123456789876543210GSym1 local0123456789876543210 a0123456789876543210 + type instance Apply (Let0123456789876543210GSym1 local0123456789876543210) a0123456789876543210 = Let0123456789876543210G local0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Let0123456789876543210GSym1 local0123456789876543210) where + suppressUnusedWarnings + = snd ((,) Let0123456789876543210GSym1KindInference ()) + type family Let0123456789876543210GSym2 local0123456789876543210 (a0123456789876543210 :: a0123456789876543210) :: a0123456789876543210 where + Let0123456789876543210GSym2 local0123456789876543210 a0123456789876543210 = Let0123456789876543210G local0123456789876543210 a0123456789876543210 + type family Let0123456789876543210G local0123456789876543210 (a :: a) :: a where + Let0123456789876543210G local (x :: a) = Apply (Apply Konst1Sym0 (x :: a)) local + type Id8Sym0 :: (~>) a a + data Id8Sym0 :: (~>) a a + where + Id8Sym0KindInference :: SameKind (Apply Id8Sym0 arg) (Id8Sym1 arg) => + Id8Sym0 a0123456789876543210 + type instance Apply Id8Sym0 a0123456789876543210 = Id8 a0123456789876543210 + instance SuppressUnusedWarnings Id8Sym0 where + suppressUnusedWarnings = snd ((,) Id8Sym0KindInference ()) + type Id8Sym1 :: a -> a + type family Id8Sym1 (a0123456789876543210 :: a) :: a where + Id8Sym1 a0123456789876543210 = Id8 a0123456789876543210 + data Id7Sym0 a0123456789876543210 + where + Id7Sym0KindInference :: SameKind (Apply Id7Sym0 arg) (Id7Sym1 arg) => + Id7Sym0 a0123456789876543210 + type instance Apply Id7Sym0 a0123456789876543210 = Id7 a0123456789876543210 + instance SuppressUnusedWarnings Id7Sym0 where + suppressUnusedWarnings = snd ((,) Id7Sym0KindInference ()) + type family Id7Sym1 a0123456789876543210 where + Id7Sym1 a0123456789876543210 = Id7 a0123456789876543210 + type Id6Sym0 :: (~>) a a + data Id6Sym0 :: (~>) a a + where + Id6Sym0KindInference :: SameKind (Apply Id6Sym0 arg) (Id6Sym1 arg) => + Id6Sym0 a0123456789876543210 + type instance Apply Id6Sym0 a0123456789876543210 = Id6 a0123456789876543210 + instance SuppressUnusedWarnings Id6Sym0 where + suppressUnusedWarnings = snd ((,) Id6Sym0KindInference ()) + type Id6Sym1 :: a -> a + type family Id6Sym1 (a0123456789876543210 :: a) :: a where + Id6Sym1 a0123456789876543210 = Id6 a0123456789876543210 + type Id5Sym0 :: forall a. (~>) a a + data Id5Sym0 :: (~>) a a + where + Id5Sym0KindInference :: SameKind (Apply Id5Sym0 arg) (Id5Sym1 arg) => + Id5Sym0 a0123456789876543210 + type instance Apply Id5Sym0 a0123456789876543210 = Id5 a0123456789876543210 + instance SuppressUnusedWarnings Id5Sym0 where + suppressUnusedWarnings = snd ((,) Id5Sym0KindInference ()) + type Id5Sym1 :: forall a. a -> a + type family Id5Sym1 (a0123456789876543210 :: a) :: a where + Id5Sym1 a0123456789876543210 = Id5 a0123456789876543210 + type Id4Sym0 :: forall a. (~>) a a + data Id4Sym0 :: (~>) a a + where + Id4Sym0KindInference :: SameKind (Apply Id4Sym0 arg) (Id4Sym1 arg) => + Id4Sym0 a0123456789876543210 + type instance Apply Id4Sym0 a0123456789876543210 = Id4 a0123456789876543210 + instance SuppressUnusedWarnings Id4Sym0 where + suppressUnusedWarnings = snd ((,) Id4Sym0KindInference ()) + type Id4Sym1 :: forall a. a -> a + type family Id4Sym1 (a0123456789876543210 :: a) :: a where + Id4Sym1 a0123456789876543210 = Id4 a0123456789876543210 + type Id3Sym0 :: (~>) a a + data Id3Sym0 :: (~>) a a + where + Id3Sym0KindInference :: SameKind (Apply Id3Sym0 arg) (Id3Sym1 arg) => + Id3Sym0 a0123456789876543210 + type instance Apply Id3Sym0 a0123456789876543210 = Id3 a0123456789876543210 + instance SuppressUnusedWarnings Id3Sym0 where + suppressUnusedWarnings = snd ((,) Id3Sym0KindInference ()) + type Id3Sym1 :: a -> a + type family Id3Sym1 (a0123456789876543210 :: a) :: a where + Id3Sym1 a0123456789876543210 = Id3 a0123456789876543210 + type Id2Sym0 :: forall a. (~>) a a + data Id2Sym0 :: (~>) a a + where + Id2Sym0KindInference :: SameKind (Apply Id2Sym0 arg) (Id2Sym1 arg) => + Id2Sym0 a0123456789876543210 + type instance Apply Id2Sym0 a0123456789876543210 = Id2 a0123456789876543210 + instance SuppressUnusedWarnings Id2Sym0 where + suppressUnusedWarnings = snd ((,) Id2Sym0KindInference ()) + type Id2Sym1 :: forall a. a -> a + type family Id2Sym1 (a0123456789876543210 :: a) :: a where + Id2Sym1 a0123456789876543210 = Id2 a0123456789876543210 + type FooSym0 :: forall a. (~>) a () + data FooSym0 :: (~>) a () + where + FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) => + FooSym0 a0123456789876543210 + type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210 + instance SuppressUnusedWarnings FooSym0 where + suppressUnusedWarnings = snd ((,) FooSym0KindInference ()) + type FooSym1 :: forall a. a -> () + type family FooSym1 (a0123456789876543210 :: a) :: () where + FooSym1 a0123456789876543210 = Foo a0123456789876543210 + data FSym0 a0123456789876543210 + where + FSym0KindInference :: SameKind (Apply FSym0 arg) (FSym1 arg) => + FSym0 a0123456789876543210 + type instance Apply FSym0 a0123456789876543210 = F a0123456789876543210 + instance SuppressUnusedWarnings FSym0 where + suppressUnusedWarnings = snd ((,) FSym0KindInference ()) + type family FSym1 a0123456789876543210 where + FSym1 a0123456789876543210 = F a0123456789876543210 + type Konst2Sym0 :: (~>) a ((~>) (Maybe Bool) a) + data Konst2Sym0 :: (~>) a ((~>) (Maybe Bool) a) + where + Konst2Sym0KindInference :: SameKind (Apply Konst2Sym0 arg) (Konst2Sym1 arg) => + Konst2Sym0 a0123456789876543210 + type instance Apply Konst2Sym0 a0123456789876543210 = Konst2Sym1 a0123456789876543210 + instance SuppressUnusedWarnings Konst2Sym0 where + suppressUnusedWarnings = snd ((,) Konst2Sym0KindInference ()) + type Konst2Sym1 :: a -> (~>) (Maybe Bool) a + data Konst2Sym1 (a0123456789876543210 :: a) :: (~>) (Maybe Bool) a + where + Konst2Sym1KindInference :: SameKind (Apply (Konst2Sym1 a0123456789876543210) arg) (Konst2Sym2 a0123456789876543210 arg) => + Konst2Sym1 a0123456789876543210 a0123456789876543210 + type instance Apply (Konst2Sym1 a0123456789876543210) a0123456789876543210 = Konst2 a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Konst2Sym1 a0123456789876543210) where + suppressUnusedWarnings = snd ((,) Konst2Sym1KindInference ()) + type Konst2Sym2 :: a -> Maybe Bool -> a + type family Konst2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe Bool) :: a where + Konst2Sym2 a0123456789876543210 a0123456789876543210 = Konst2 a0123456789876543210 a0123456789876543210 + type Konst1Sym0 :: (~>) a ((~>) Bool a) + data Konst1Sym0 :: (~>) a ((~>) Bool a) + where + Konst1Sym0KindInference :: SameKind (Apply Konst1Sym0 arg) (Konst1Sym1 arg) => + Konst1Sym0 a0123456789876543210 + type instance Apply Konst1Sym0 a0123456789876543210 = Konst1Sym1 a0123456789876543210 + instance SuppressUnusedWarnings Konst1Sym0 where + suppressUnusedWarnings = snd ((,) Konst1Sym0KindInference ()) + type Konst1Sym1 :: a -> (~>) Bool a + data Konst1Sym1 (a0123456789876543210 :: a) :: (~>) Bool a + where + Konst1Sym1KindInference :: SameKind (Apply (Konst1Sym1 a0123456789876543210) arg) (Konst1Sym2 a0123456789876543210 arg) => + Konst1Sym1 a0123456789876543210 a0123456789876543210 + type instance Apply (Konst1Sym1 a0123456789876543210) a0123456789876543210 = Konst1 a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (Konst1Sym1 a0123456789876543210) where + suppressUnusedWarnings = snd ((,) Konst1Sym1KindInference ()) + type Konst1Sym2 :: a -> Bool -> a + type family Konst1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Bool) :: a where + Konst1Sym2 a0123456789876543210 a0123456789876543210 = Konst1 a0123456789876543210 a0123456789876543210 + type Id8 :: a -> a + type family Id8 (a :: a) :: a where + Id8 x = Apply (Apply (Let0123456789876543210GSym1 x) x) TrueSym0 + type family Id7 a where + Id7 (x :: b) = Let0123456789876543210GSym2 b x + type Id6 :: a -> a + type family Id6 (a :: a) :: a where + Id6 (x :: b) = Let0123456789876543210GSym2 b x + type Id5 :: forall a. a -> a + type family Id5 (a :: a) :: a where + Id5 @a (a_0123456789876543210 :: a) = Apply (Let0123456789876543210GSym2 a a_0123456789876543210) a_0123456789876543210 + type Id4 :: forall a. a -> a + type family Id4 (a :: a) :: a where + Id4 @a (x :: a :: a) = Apply IdSym0 (x :: a) + type Id3 :: a -> a + type family Id3 (a :: a) :: a where + Id3 (x :: b) = Apply IdSym0 (x :: b) + type Id2 :: forall a. a -> a + type family Id2 (a :: a) :: a where + Id2 @a (x :: a) = Apply IdSym0 (x :: a) + type Foo :: forall a. a -> () + type family Foo (a :: a) :: () where + Foo @a (x :: a) = Apply (Apply ConstSym0 Tuple0Sym0) (NothingSym0 :: Maybe a) + type family F a where + F local = Let0123456789876543210GSym1 local + type Konst2 :: a -> Maybe Bool -> a + type family Konst2 (a :: a) (a :: Maybe Bool) :: a where + Konst2 x _ = x + type Konst1 :: a -> Bool -> a + type family Konst1 (a :: a) (a :: Bool) :: a where + Konst1 x _ = x diff --git a/singletons-base/tests/compile-and-dump/Singletons/T433.hs b/singletons-base/tests/compile-and-dump/Singletons/T433.hs new file mode 100644 index 00000000..c619596c --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Singletons/T433.hs @@ -0,0 +1,72 @@ +module T433 where + +import Data.Kind (Type) +import Data.Singletons.Base.TH +import Prelude.Singletons + +$(promote [d| + konst1 :: a -> Bool -> a + konst1 x _ = x + + konst2 :: a -> Maybe Bool -> a + konst2 x _ = x + + f local = g + where + g :: forall a. a -> a + g x = konst1 (x :: a) local + + foo :: forall a. a -> () + foo x = const () (Nothing :: Maybe a) + + id2 :: forall a. a -> a + id2 x = id (x :: a) + + id3 :: a -> a + id3 (x :: b) = id (x :: b) + + id4 :: forall a. a -> a + id4 (x :: a) = id (x :: a) + + id5 :: forall a. a -> a + id5 = g + where + g = id :: a -> a + + id6 :: a -> a + id6 (x :: b) = g + where + g = (x :: b) + + id7 (x :: b) = g + where + g = (x :: b) + + id8 :: a -> a + id8 x = g x True + where + g :: b -> a -> b + g y _ = y + + -- These version will not work. See the singletons README for more about these + -- limitations. + + -- This will not work because the `a` in `forall a` scopes over the body of + -- the function, but the `(x :: b)` pattern refers to `b` instead of `a`. + {- + id9 :: forall a. a -> a + id9 (x :: b) = id (x :: b) + -} + + -- This will not work because the `b` in `Nothing :: Maybe b` is bound by the + -- type signature for `g`, a local variable that closes over `x`. Moreover, + -- `b` is only mentioned in the return type (and not the arguments) of the + -- type signature. + {- + id10 :: forall a. a -> a + id10 x = konst2 x y + where + y :: forall b. Maybe b + y = Nothing :: Maybe b + -} + |]) diff --git a/singletons-th/CHANGES.md b/singletons-th/CHANGES.md index cdfa05ff..ea77dcd7 100644 --- a/singletons-th/CHANGES.md +++ b/singletons-th/CHANGES.md @@ -13,6 +13,9 @@ next [????.??.??] instance Ord (SExample a) where compare _ _ = EQ ``` +* `singletons-th` now makes an effort to promote definitions that use scoped + type variables. See the "Scoped type variables" section of the `README` for + more information about what `singletons-th` can (and can't) do. * Fix a bug in which data types using visible dependent quantification would generate ill-scoped code when singled. * Fix a bug in which singling a local variable that shadows a top-level diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 952e63c3..69d454f2 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -14,6 +14,7 @@ import Language.Haskell.TH.Syntax ( NameSpace(..), Quasi(..), Uniq ) import Language.Haskell.TH.Desugar import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap import Language.Haskell.TH.Desugar.OMap.Strict (OMap) +import qualified Language.Haskell.TH.Desugar.OSet as OSet import Data.Singletons.TH.Deriving.Bounded import Data.Singletons.TH.Deriving.Enum import Data.Singletons.TH.Deriving.Eq @@ -688,15 +689,13 @@ promoteLetDecRHS :: LetDecRHSSort , [DDec] -- defunctionalization , ALetDecRHS ) -- annotated RHS promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do - opts <- getOptions all_locals <- allLocals case let_dec_rhs of UValue exp -> do (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals 0 if ty_num_args == 0 - then - let proName = promotedValueName opts name mb_let_uniq - prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals in + then do + prom_fun_lhs <- promoteLetDecName mb_let_uniq name m_ldrki all_locals promote_let_dec_rhs all_locals m_ldrki 0 (promoteExp exp) (\exp' -> [DTySynEqn Nothing prom_fun_lhs exp']) AValue @@ -711,14 +710,12 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do promote_function_rhs :: [Name] -> [DClause] -> PrM ([DDec], [DDec], ALetDecRHS) promote_function_rhs all_locals clauses = do - opts <- getOptions numArgs <- count_args clauses - let proName = promotedValueName opts name mb_let_uniq - prom_fun_lhs = foldType (DConT proName) $ map DVarT all_locals (m_ldrki, ty_num_args) <- promote_let_dec_ty all_locals numArgs expClauses <- mapM (etaContractOrExpand ty_num_args numArgs) clauses + let promote_clause = promoteClause mb_let_uniq name m_ldrki all_locals promote_let_dec_rhs all_locals m_ldrki ty_num_args - (mapAndUnzipM (promoteClause prom_fun_lhs) expClauses) + (mapAndUnzipM promote_clause expClauses) id (AFunction ty_num_args) -- Promote a UValue or a UFunction. @@ -747,29 +744,33 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do mk_tf_head arg_tvbs res_sig = dTypeFamilyHead_with_locals proName all_locals arg_tvbs res_sig - (m_sak_dec, defun_ki, tf_head) = + (lde_kvs_to_bind, m_sak_dec, defun_ki, tf_head) = -- There are three possible cases: case m_ldrki of -- 1. We have no kind information whatsoever. Nothing -> let arg_tvbs = map (`DPlainTV` ()) tyvarNames in - ( Nothing + ( OSet.empty + , Nothing , DefunNoSAK (local_tvbs ++ arg_tvbs) Nothing , mk_tf_head arg_tvbs DNoSig ) -- 2. We have some kind information in the form of a LetDecRHSKindInfo. - Just (LDRKI m_sak argKs resK) -> - let arg_tvbs = zipWith (`DKindedTV` ()) tyvarNames argKs in + Just (LDRKI m_sak tvbs argKs resK) -> + let arg_tvbs = zipWith (`DKindedTV` ()) tyvarNames argKs + lde_kvs_to_bind' = OSet.fromList (map extractTvbName tvbs) in case m_sak of -- 2(a). We do not have a standalone kind signature. Nothing -> - ( Nothing + ( lde_kvs_to_bind' + , Nothing , DefunNoSAK (local_tvbs ++ arg_tvbs) (Just resK) , mk_tf_head arg_tvbs (DKindSig resK) ) -- 2(b). We have a standalone kind signature. Just sak -> - ( Just $ DKiSigD proName sak + ( lde_kvs_to_bind' + , Just $ DKiSigD proName sak , DefunSAK sak -- We opt to annotate the argument and result kinds in -- the body of the type family declaration even if it is @@ -779,7 +780,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do ) defun_decs <- defunctionalize proName m_fixity defun_ki - (prom_thing, thing) <- promote_thing + (prom_thing, thing) <- scopedBind lde_kvs_to_bind promote_thing return ( catMaybes [ m_sak_dec , Just $ DClosedTypeFamilyD tf_head (mk_prom_eqns prom_thing) ] @@ -814,7 +815,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do -- since we don't apply these functions with visible kind -- applications. let sak = ravelVanillaDType [] [] arg_kis res_ki in - return (Just (LDRKI (Just sak) arg_kis res_ki), length arg_kis) + return (Just (LDRKI (Just sak) [] arg_kis res_ki), length arg_kis) LetBindingRHS | Just ty <- OMap.lookup name type_env -> do @@ -827,7 +828,7 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do -- See Note [No SAKs for let-decs with local variables] | otherwise = Nothing -- invariant: count_args ty == length argKs - return (Just (LDRKI m_sak argKs resultK), length argKs) + return (Just (LDRKI m_sak tvbs argKs resultK), length argKs) | otherwise -> return (Nothing, default_num_args) @@ -858,6 +859,7 @@ data LetDecRHSKindInfo = -- This will be Nothing if the let-dec RHS has local -- variables that it closes over. -- See Note [No SAKs for let-decs with local variables] + [DTyVarBndrSpec] -- The type variable binders of the kind. [DKind] -- The argument kinds. DKind -- The result kind. @@ -940,17 +942,37 @@ information anyway. Thankfully, this is simple to accomplish, as we already compute this information to begin with. -} -promoteClause :: DType -- What to use as the LHS of the promoted type family - -- equation. This should consist of the promoted name of - -- the function to which the clause belongs, applied to - -- any local arguments (e.g., `Go x y z`). +promoteClause :: Maybe Uniq + -- ^ Let-binding unique (if locally bound) + -> Name + -- ^ Name of the function being promoted + -> Maybe LetDecRHSKindInfo + -- ^ Information about the promoted kind (if present) + -> [Name] + -- ^ The local variables currently in scope -> DClause -> PrM (DTySynEqn, ADClause) -promoteClause pro_clause_fun (DClause pats exp) = do +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'), new_vars) <- evalForPair $ mapAndUnzipM promotePat pats - (ty, ann_exp) <- lambdaBind new_vars $ promoteExp exp - return ( DTySynEqn Nothing (foldType pro_clause_fun types) ty + ((types, pats'), prom_pat_infos) <- evalForPair $ mapAndUnzipM promotePat 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 + -- explanation of why we do this. + scoped_tvs <- qIsExtEnabled LangExt.ScopedTypeVariables + let types_w_kinds = + case m_ldrki of + Just (LDRKI _ tvbs kinds _) + | not (null tvbs) && scoped_tvs + -> zipWith DSigT types kinds + _ -> types + let PromDPatInfos { prom_dpat_vars = new_vars + , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos + (ty, ann_exp) <- scopedBind sig_kvs $ + lambdaBind new_vars $ + promoteExp exp + pro_clause_fun <- promoteLetDecName mb_let_uniq name m_ldrki all_locals + return ( DTySynEqn Nothing (foldType pro_clause_fun types_w_kinds) ty , ADClause new_vars pats' ann_exp ) promoteMatch :: DType -- What to use as the LHS of the promoted type family @@ -961,18 +983,22 @@ 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'), new_vars) <- evalForPair $ promotePat pat - (rhs, ann_exp) <- lambdaBind new_vars $ promoteExp exp + ((ty, pat'), prom_pat_infos) <- evalForPair $ promotePat pat + let PromDPatInfos { prom_dpat_vars = new_vars + , prom_dpat_sig_kvs = sig_kvs } = prom_pat_infos + (rhs, ann_exp) <- scopedBind sig_kvs $ + lambdaBind new_vars $ + promoteExp exp 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 VarPromotions PrM (DType, ADPat) +promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat) promotePat (DLitP lit) = (, ADLitP lit) <$> promoteLitPat lit promotePat (DVarP name) = do -- term vars can be symbols... type vars can't! tyName <- mkTyName name - tell $ [(name, tyName)] + tell $ PromDPatInfos [(name, tyName)] OSet.empty return (DVarT tyName, ADVarP name) promotePat (DConP name tys pats) = do opts <- getOptions @@ -999,6 +1025,7 @@ promotePat (DSigP pat ty) = do wildless_pat <- removeWilds pat (promoted, pat') <- promotePat wildless_pat ki <- promoteType ty + tell $ PromDPatInfos [] (fvDType ki) return (DSigT promoted ki, ADSigP promoted pat' ki) promotePat DWildP = return (DWildCardT, ADWildP) @@ -1092,6 +1119,38 @@ promoteLitPat (CharL c) = return $ DLitT (CharTyLit c) promoteLitPat lit = fail ("Only string, natural number, and character literals can be promoted: " ++ show lit) +-- Promote the name of a 'ULetDecRHS' to the type level. If the promoted +-- 'ULetDecRHS' has a standalone type signature and does not close over any +-- local variables, then this will include the scoped type variables from the +-- type signature as invisible arguments. (See Note [Scoped type variables] in +-- Data.Singletons.TH.Promote.Monad.) Otherwise, it will include any local +-- variables that it closes over as explicit arguments. +promoteLetDecName :: + Maybe Uniq + -- ^ Let-binding unique (if locally bound) + -> Name + -- ^ Name of the function being promoted + -> Maybe LetDecRHSKindInfo + -- ^ Information about the promoted kind (if present) + -> [Name] + -- ^ The local variables currently in scope + -> PrM DType +promoteLetDecName mb_let_uniq name m_ldrki all_locals = do + opts <- getOptions + let proName = promotedValueName opts name mb_let_uniq + type_args = + case m_ldrki of + Just (LDRKI m_sak tvbs _ _) + | isJust m_sak + -- Per the comments on LetDecRHSKindInfo, `isJust m_sak` is only True + -- if there are no local variables. Return the scoped type variables + -- `tvbs` as invisible arguments using `DTyArg`... + -> map (DTyArg . DVarT . extractTvbName) tvbs + _ -> -- ...otherwise, return the local variables as explicit arguments + -- using DTANormal. + map (DTANormal . DVarT) all_locals + pure $ applyDType (DConT proName) type_args + -- Construct a 'DTypeFamilyHead' that closes over some local variables. We -- apply `noExactName` to each local variable to avoid GHC#11812. -- See also Note [Pitfalls of NameU/NameL] in Data.Singletons.TH.Util. diff --git a/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs b/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs index 771941e5..fa6810e6 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote/Monad.hs @@ -12,33 +12,42 @@ of DDec, and is wrapped around a Q. module Data.Singletons.TH.Promote.Monad ( PrM, promoteM, promoteM_, promoteMDecs, VarPromotions, allLocals, emitDecs, emitDecsM, - lambdaBind, LetBind, letBind, lookupVarE + scopedBind, lambdaBind, LetBind, letBind, lookupVarE ) where import Control.Monad.Reader import Control.Monad.Writer +import qualified Data.Foldable as F import Language.Haskell.TH.Syntax hiding ( lift ) import Language.Haskell.TH.Desugar import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap import Language.Haskell.TH.Desugar.OMap.Strict (OMap) +import qualified Language.Haskell.TH.Desugar.OSet as OSet +import Language.Haskell.TH.Desugar.OSet (OSet) import Data.Singletons.TH.Options import Data.Singletons.TH.Syntax -- environment during promotion data PrEnv = PrEnv { pr_options :: Options + , 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 -- ^ Map from term-level 'Name's of variables bound in lambdas and -- function clauses to their type-level counterparts. -- See @Note [Tracking local variables]@. , pr_local_vars :: OMap Name DType -- ^ Map from term-level 'Name's of local variables to their - -- type-level counterparts. See @Note [Tracking local variables]@. + -- type-level counterparts. Note that scoped type variables are stored + -- separately in 'pr_scoped_tvs'. + -- See @Note [Tracking local variables]@. , pr_local_decls :: [Dec] } emptyPrEnv :: PrEnv emptyPrEnv = PrEnv { pr_options = defaultOptions + , pr_scoped_vars = OSet.empty , pr_lambda_vars = OMap.empty , pr_local_vars = OMap.empty , pr_local_decls = [] } @@ -58,8 +67,9 @@ instance OptionsMonad PrM where -- return *type-level* names allLocals :: MonadReader PrEnv m => m [Name] allLocals = do + scoped <- asks (F.toList . pr_scoped_vars) lambdas <- asks (OMap.assocs . pr_lambda_vars) - return $ map snd lambdas + return $ scoped ++ map snd lambdas emitDecs :: MonadWriter [DDec] m => [DDec] -> m () emitDecs = tell @@ -69,6 +79,14 @@ emitDecsM action = do decs <- action emitDecs decs +-- ^ Bring a list of type variables into scope for the duration the supplied +-- computation. See @Note [Tracking local variables]@ and +-- @Note [Scoped type variables]@. +scopedBind :: OSet Name -> PrM a -> PrM a +scopedBind binds = + local (\env@(PrEnv { pr_scoped_vars = scoped }) -> + env { pr_scoped_vars = binds `OSet.union` scoped }) + -- ^ Bring a list of 'VarPromotions' into scope for the duration the supplied -- computation. See @Note [Tracking local variables]@. lambdaBind :: VarPromotions -> PrM a -> PrM a @@ -127,17 +145,26 @@ promoteMDecs locals thing = do {- Note [Tracking local variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Handling local variables in singletons-th requires some care. There are two +Handling local variables in singletons-th requires some care. There are three sorts of local variables that singletons-th tracks: -1. Lambda-bound variables, e.g., +1. Scoped type variables, e.g., + + d :: forall a. Maybe a + d = Nothing :: Maybe a + + e (x :: a) = Nothing :: Maybe a + + In both `d` and `e`, the variable `a` in `:: Maybe a` is scoped. + +2. Lambda-bound variables, e.g., f = \x -> x g x = x In both `f` and `g`, the variable `x` is considered lambda-bound. -2. Let-bound variables, e.g., +3. Let-bound variables, e.g., h = let x = 42 in @@ -154,9 +181,21 @@ be promoted differently depending on whether they are local or not. Consider: j = ... x ... -When promoting the `j` function to a type family `J`, there are three possible +When promoting the `j` function to a type family `J`, there are four possible ways of promoting `x`: +* If `x` is a scoped type variable, then `x` must be promoted to the same + name. This is because promoting a type variable to a kind variable is a + no-op. For instance, we would promote this: + + j (z :: x) = (z :: x) + + Here, `(%%)`, `x`, and `y` are lambda-bound variables. But we cannot promote + `j` to this type family: + + type family J arg where + J (z :: x) = (z :: x) + * If `x` is a lambda-bound variable, then `x` must be promoted to a type variable. In general, we cannot promote `x` to the same name. Consider this example: @@ -219,27 +258,178 @@ ways of promoting `x`: J = X Being able to distinguish between all these sorts of variables requires -recording whether they are lambda-/let-bound at their binding sites during -promotion and singling. During promotion, the `pr_local_vars` field of `PrEnv` -is responsible for this. In singling, the `sg_local_vars` field of `SgEnv` is -responsible for this. Each of these fields are Maps from the original, -term-level Names to the promoted or singled versions of the Names. The -`lookupVarE` functions (which can be found in both -Data.Singletons.TH.Promote.Monad and Data.Singletons.TH.Single.Monad) are -responsible for determining what a term-level Name should be mapped to. +recording whether they are scoped, lambda-bound, or let-bound at their binding +sites during promotion and singling. This is primarily done in two places: + +* During promotion, the `pr_local_vars` field of `PrEnv` tracks lambda- and + let-bound variables. + +* During singling, the `sg_local_vars` field of `SgEnv` tracks lambda- and + let-bound variables. + +Each of these fields are Maps from the original, term-level Names to the +promoted or singled versions of the Names. The `lookupVarE` functions (which +can be found in both Data.Singletons.TH.Promote.Monad and +Data.Singletons.TH.Single.Monad) are responsible for determining what a +term-level Name should be mapped to. In addition to `pr_local_vars` and `sg_local_vars`, which include both lambda- -and let-bound variables, `PrEnv` also includes a separate `pr_lambda_vars` -field, which only tracks lambda-bound variables. We must do this because -lambda-bound variables are treated differently during lambda lifting. -Lambda-lifted functions must close over any lambda-bound variables in scope, -but /not/ any let-bound variables in scope, since the latter are lambda-lifted -separately. (Because singling does not do anything akin to lambda lifting, -`SgEnv` does not have anything like `sg_lambda_vars`.) - -A consequence of this is that when we lambda-bind a variable during promotion -(see `lambdaBind`), we add the variable to both `pr_lambda_vars` and -`pr_local_vars`. When we let-bind a variable during promotion (see `letBind`), -we only add the variable to `pr_local_vars`. This means that `pr_lambda_vars` -will always be a subset of `pr_local_vars`. +and let-bound variables, `PrEnv` also includes two additional fields for +tracking other sorts of local variables: + +* The `pr_scoped_vars` field tracks which scoped type variables are currently + in scope. As discussed above, promoting an occurrence of a scoped type + variable is a no-op, and as such, we never need to use `lookupVarE` to figure + out what a scoped type variable promotes to. As such, there is no need to put + the scoped type variables in `pr_local_vars`. + + On the other hand, we /do/ need to track the scoped type variables for + lambda-lifting purposes (see Note [Scoped type variables]), and this is the + only reason why we bother maintaining the `pr_scoped_vars` field in the first + place. See the `scopedBind` function, which is responsible for adding new + scoped type variables to `pr_scoped_vars`. + +* The `pr_lambda_vars` field only tracks lambda-bound variables, unlike + `pr_local_vars`, which also includes let-bound variables. We must do this + because lambda-bound variables are treated differently during lambda lifting. + Lambda-lifted functions must close over any lambda-bound variables in scope, + but /not/ any let-bound variables in scope, since the latter are + lambda-lifted separately. + + A consequence of this is that when we lambda-bind a variable during promotion + (see `lambdaBind`), we add the variable to both `pr_lambda_vars` and + `pr_local_vars`. When we let-bind a variable during promotion (see + `letBind`), we only add the variable to `pr_local_vars`. This means that + `pr_lambda_vars` will always be a subset of `pr_local_vars`. + +Because singling does not do anything akin to lambda lifting, `SgEnv` does not +have anything like `sg_scoped_vars` or `sg_lambda_vars`. + +Note [Scoped type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Scoped type variables are a particular form of local variable (see Note +[Tracking local variables]). They are arguably the trickiest form of local +variable to handle, and as noted in the singletons README, there are still some +forms of scoped type variables that singletons-th cannot handle during +promotion. + +First, let's discuss how singletons-th promotes scoped type variables in +general: + +* When promoting a function with a top-level type signature, we annotate each + argument on the left-hand sides of type family equations with its kind. This + is usually redundant, but it can sometimes be useful for bringing type + variables into scope. For example, this: + + f :: forall a. a -> Maybe a + f x = (Just x :: Maybe a) + + Will be promoted to something like this: + + type F :: forall a. a -> Maybe a + type family F x where + F (x :: a) = (Just x :: Maybe a) + + Note that we gave the `x` on the left-hand side of `F`'s equation an explicit + `:: a` kind signature to ensure that the `a` on the right-hand side of the + type family equation is in scope. + + The `promoteClause` function in Data.Singletons.TH.Promote is responsible for + implementing this. + +* Sometimes, there are no arguments available to bring type variables into + scope. In these situations, we can sometimes use `@` in type family equations + as an alternative. For example, this: + + g :: forall a. Maybe a + g = (Nothing :: Maybe a) + + Will be promoted to this: + + type G :: forall a. Maybe a + type family G where + G @a = (Nothing :: Maybe a) + + Note the `@a` on `G`'s left-hand side. This relies on `G` having a standalone + kind signature to work. + + The `promoteLetDecName` function in Data.Singletons.TH.Promote is responsible + for implementing this. + +* When lambda-lifting, singletons-th tracks the current set of scoped type + variables and includes them as explicit arguments when promoting local + definitions. For example, this: + + h :: forall a. a -> a + h x = i + where + i = (x :: a) + + Will be promoted to this: + + type H :: forall a. a -> a + type family H x where + H @a (x :: a) = LetI a x + + type I a x where + I a x = (x :: a) + + The `I` type family includes both `a` (a scoped type variable) and `x` (a + lambda-bound variable) as explicit arguments to ensure that they are in scope + on the right-hand side, which mentions both of them. + + singletons-th uses the `pr_scoped_vars` field of `PrM` to track scoped type + variables. Whenever new scoped type variables are bound during promotion, the + `scopedBind` function is used to add the variables to `pr_scoped_vars`. + +These three tricks suffice to handle a substantial number of ways that scoped +type variables can be used. The approach is not perfect, however. Here are two +scenarios where singletons-th fails to promote scoped type variables: + +* Funky pattern signatures like this one will not work: + + j :: forall a. a -> a + j (x :: b) = b + + This is because singletons-th will attempt to promote `j` like so: + + type J :: forall a. a -> a + type J x where + J @a ((x :: b) :: a) = b + + But unlike in terms, GHC has no way to know that `a` and `b` are meant to + refer to the same type variable. In order to make this work, we would need to + substitute all occurrences of `a` with `b` in the type family equation (or + vice versa), which seems challenging in the general case. + +* Scoped type variables that are only mentioned in the return types of local + definitions may not always work, such as in this example: + + k x = y + where + y :: forall b. Maybe b + y = Nothing :: Maybe b + + singletons-th would promote `k` and `y` to the following type families: + + type K x where + K x = LetY x + + type LetY x :: Maybe b where + LetY x = Nothing :: Maybe b + + Note that because `LetY` closes over the `x` argument, it cannot easily be + given a standalone kind signature, and this prevents us from writing + `LetY @b x = ...`. Moreover, `LetY` does not have an argument that we can + attach an explicit `:: b` signature to. (Attaching it to `x` would be + incorrect, as that would give `LetY` a less general kind.) + + One possible way forward here would be to give type families the ability to + write result signatures on their left-hand sides, similar to what GHC + proposal #228 + (https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0228-function-result-sigs.rst) + offers: + + type LetY x :: Maybe b where + LetY x :: Maybe b = Nothing :: Maybe b -} diff --git a/singletons-th/src/Data/Singletons/TH/Syntax.hs b/singletons-th/src/Data/Singletons/TH/Syntax.hs index 93c513a6..f6544e49 100644 --- a/singletons-th/src/Data/Singletons/TH/Syntax.hs +++ b/singletons-th/src/Data/Singletons/TH/Syntax.hs @@ -18,9 +18,26 @@ import Language.Haskell.TH.Syntax hiding (Type) import Language.Haskell.TH.Desugar 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 +-- Information that is accumulated when promoting patterns. +data PromDPatInfos = PromDPatInfos + { prom_dpat_vars :: VarPromotions + -- Maps term-level pattern variables to their promoted, type-level counterparts. + , prom_dpat_sig_kvs :: OSet Name + -- Kind variables bound by DSigPas. + -- See Note [Scoped type variables] in Data.Singletons.TH.Promote.Monad. + } + +instance Semigroup PromDPatInfos where + PromDPatInfos vars1 sig_kvs1 <> PromDPatInfos vars2 sig_kvs2 + = PromDPatInfos (vars1 <> vars2) (sig_kvs1 <> sig_kvs2) + +instance Monoid PromDPatInfos where + mempty = PromDPatInfos mempty mempty + -- A list of 'SingDSigPaInfos' is produced when singling pattern signatures, as we -- must case on the 'DExp's and match on them using the supplied 'DType's to -- bring the necessary singleton equality constraints into scope.