From 7815a555f33be8b8cb89f6fa918fd8a8bad642b4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 23 Jul 2023 18:07:40 -0400 Subject: [PATCH] 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