From b9b357b6efa0a84b5c00a48109da3960b8c332e8 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 11 May 2024 21:08:03 -0400 Subject: [PATCH] Simplify singling of instance method types Previously, `singletons-th` would always attempt to generate instance signatures for singled instance methods, even if the original instance code lacks instance signatures. To do so, `singletons-th` will infer an instance signature by reifying the type of the method (or, if that cannot be found, the singled version of the method) and manually applying a substitution from class variables to instance types. This process is quite involved, and what's more, it doesn't work in all cases: * As noted in #358, inferred instance signatures can sometimes be ill-kinded. * In order to support singling examples like the ones from #581, we need type variables from class method defaults and instance methods to scope over their bodies. However, the approach that `singletons-th` used to reify the method type for the singled code will sometimes reify _different_ type variables than the ones used in the promoted code, leading to disaster. This convention of inferring the instance signature dates all the way back to commit https://github.com/goldfirere/singletons/commit/c9beec58a791af8c63152cdb54c758fd9fb04deb, and it's unclear why this choice was made. At the time of writing #358, I was convinced that inferred instance signatures were necessary to support examples like the one in https://github.com/goldfirere/singletons/issues/358#issuecomment-416691475. However, this example is only problematic due to the use of an explicit kind annotation on a promoted `case` expression, and these explicit kind annotations were removed in the fix for #547. As such, this convention no longer serves a useful purpose. This patch removes the instance signature inference code, greatly simplifying the overall process of singling instance declarations. Fixes #590. --- README.md | 1 - .../GradingClient/Database.golden | 36 --------- .../Singletons/BoundedDeriving.golden | 10 --- .../Singletons/Classes.golden | 25 ------- .../Singletons/Classes2.golden | 5 -- .../Singletons/DataValues.golden | 8 -- .../Singletons/EmptyShowDeriving.golden | 8 -- .../Singletons/EnumDeriving.golden | 16 ---- .../Singletons/EqInstances.golden | 10 --- .../Singletons/FunDeps.golden | 6 -- .../Singletons/FunctorLikeDeriving.golden | 74 ------------------- .../compile-and-dump/Singletons/Maybe.golden | 13 ---- .../compile-and-dump/Singletons/Nat.golden | 18 ----- .../Singletons/OrdDeriving.golden | 20 ----- .../Singletons/PatternMatching.golden | 8 -- .../Singletons/ShowDeriving.golden | 24 ------ .../Singletons/StandaloneDeriving.golden | 46 ------------ .../compile-and-dump/Singletons/Star.golden | 18 ----- .../compile-and-dump/Singletons/T136.golden | 14 ---- .../compile-and-dump/Singletons/T136b.golden | 3 - .../compile-and-dump/Singletons/T167.golden | 6 -- .../compile-and-dump/Singletons/T178.golden | 16 ---- .../compile-and-dump/Singletons/T187.golden | 10 --- .../compile-and-dump/Singletons/T190.golden | 28 ------- .../compile-and-dump/Singletons/T271.golden | 20 ----- .../compile-and-dump/Singletons/T287.golden | 5 -- .../compile-and-dump/Singletons/T358.golden | 2 - .../compile-and-dump/Singletons/T371.golden | 16 ---- .../compile-and-dump/Singletons/T555.golden | 18 ----- .../compile-and-dump/Singletons/T89.golden | 8 -- .../src/Data/Singletons/TH/Single.hs | 45 +++-------- 31 files changed, 10 insertions(+), 527 deletions(-) diff --git a/README.md b/README.md index 2619139b..4a2f6820 100644 --- a/README.md +++ b/README.md @@ -634,7 +634,6 @@ instance POrd Bool where type Compare 'True 'True = 'EQ instance SOrd Bool where - sCompare :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Compare x y) sCompare SFalse SFalse = SEQ sCompare SFalse STrue = SLT sCompare STrue SFalse = SGT diff --git a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden index 9b0f0376..25b1d5fa 100644 --- a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden +++ b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden @@ -92,11 +92,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations toSing (Succ (b :: Demote Nat)) = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c) instance SEq Nat => SEq Nat where - (%==) :: - forall (t1 :: Nat) (t2 :: Nat). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) - -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse @@ -107,11 +102,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SOrd Nat => SOrd Nat where - sCompare :: - forall (t1 :: Nat) (t2 :: Nat). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) - -> Type) t1) t2) sCompare SZero SZero = applySing (applySing @@ -1670,11 +1660,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations = case toSing b :: SomeSing [Attribute] of SomeSing c -> SomeSing (SSch c) instance (SEq U, SEq Nat) => SEq U where - (%==) :: - forall (t1 :: U) (t2 :: U). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun U ((~>) U Bool) - -> Type) t1) t2) (%==) SBOOL SBOOL = STrue (%==) SBOOL SSTRING = SFalse (%==) SBOOL SNAT = SFalse @@ -1705,14 +1690,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210) instance (SShow U, SShow Nat) => SShow U where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: U) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) U ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SBOOL @@ -1772,14 +1749,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations sArg_0123456789876543210))))) sA_0123456789876543210 instance SShow AChar where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: AChar) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) AChar ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SCA @@ -1989,11 +1958,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CZ")) sA_0123456789876543210 instance SEq AChar where - (%==) :: - forall (t1 :: AChar) (t2 :: AChar). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun AChar ((~>) AChar Bool) - -> Type) t1) t2) (%==) SCA SCA = STrue (%==) SCA SCB = SFalse (%==) SCA SCC = SFalse diff --git a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden index 08cc4ba2..525ee9b7 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden @@ -220,28 +220,18 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations of (,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c) instance SBounded Foo1 where - sMinBound :: Sing (MinBoundSym0 :: Foo1) - sMaxBound :: Sing (MaxBoundSym0 :: Foo1) sMinBound = SFoo1 sMaxBound = SFoo1 instance SBounded Foo2 where - sMinBound :: Sing (MinBoundSym0 :: Foo2) - sMaxBound :: Sing (MaxBoundSym0 :: Foo2) sMinBound = SA sMaxBound = SE instance SBounded a => SBounded (Foo3 a) where - sMinBound :: Sing (MinBoundSym0 :: Foo3 a) - sMaxBound :: Sing (MaxBoundSym0 :: Foo3 a) sMinBound = applySing (singFun1 @Foo3Sym0 SFoo3) sMinBound sMaxBound = applySing (singFun1 @Foo3Sym0 SFoo3) sMaxBound instance SBounded (Foo4 a b) where - sMinBound :: Sing (MinBoundSym0 :: Foo4 a b) - sMaxBound :: Sing (MaxBoundSym0 :: Foo4 a b) sMinBound = SFoo41 sMaxBound = SFoo42 instance SBounded Bool => SBounded Pair where - sMinBound :: Sing (MinBoundSym0 :: Pair) - sMaxBound :: Sing (MaxBoundSym0 :: Pair) sMinBound = applySing (applySing (singFun2 @PairSym0 SPair) sMinBound) sMinBound diff --git a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden index cd3f1ce5..29a8861c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden @@ -376,31 +376,16 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations (singFun2 @MycompareSym0 sMycompare) sA_0123456789876543210) sA_0123456789876543210 instance SMyOrd Nat where - sMycompare :: - (forall (t :: Nat) (t :: Nat). - Sing t - -> Sing t - -> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type) sMycompare SZero SZero = SEQ sMycompare SZero (SSucc _) = SLT sMycompare (SSucc _) SZero = SGT sMycompare (SSucc (sN :: Sing n)) (SSucc (sM :: Sing m)) = applySing (applySing (singFun2 @MycompareSym0 sMycompare) sM) sN instance SMyOrd () where - sMycompare :: - (forall (t :: ()) (t :: ()). - Sing t - -> Sing t - -> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type) sMycompare _ (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (applySing (singFun2 @ConstSym0 sConst) SEQ) sA_0123456789876543210 instance SMyOrd Foo where - sMycompare :: - (forall (t :: Foo) (t :: Foo). - Sing t - -> Sing t - -> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type) sMycompare (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -409,11 +394,6 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations (singFun2 @FooCompareSym0 sFooCompare) sA_0123456789876543210) sA_0123456789876543210 instance SEq Foo2 where - (%==) :: - forall (t1 :: Foo2) (t2 :: Foo2). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Foo2 ((~>) Foo2 Bool) - -> Type) t1) t2) (%==) SF SF = STrue (%==) SG SG = STrue (%==) SF SG = SFalse @@ -596,11 +576,6 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations = case toSing b :: SomeSing Nat' of SomeSing c -> SomeSing (SSucc' c) instance SMyOrd Nat' where - sMycompare :: - forall (t :: Nat') (t :: Nat'). Sing t - -> Sing t - -> Sing (Apply (Apply (MycompareSym0 :: TyFun Nat' ((~>) Nat' Ordering) - -> Type) t) t) sMycompare SZero' SZero' = SEQ sMycompare SZero' (SSucc' _) = SLT sMycompare (SSucc' _) SZero' = SGT diff --git a/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden b/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden index 56f640d7..6bf5f3eb 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Classes2.golden @@ -74,11 +74,6 @@ Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations = case toSing b :: SomeSing NatFoo of SomeSing c -> SomeSing (SSuccFoo c) instance SMyOrd NatFoo where - sMycompare :: - forall (t1 :: NatFoo) (t2 :: NatFoo). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (MycompareSym0 :: TyFun NatFoo ((~>) NatFoo Ordering) - -> Type) t1) t2) sMycompare SZeroFoo SZeroFoo = SEQ sMycompare SZeroFoo (SSuccFoo _) = SLT sMycompare (SSuccFoo _) SZeroFoo = SGT diff --git a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden index 2c24a1dd..b3fe76bd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden @@ -142,14 +142,6 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations = case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of (,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c) instance (SShow a, SShow b) => SShow (Pair a b) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Pair a b) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden index 5e18ef69..a32d845f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EmptyShowDeriving.golden @@ -53,14 +53,6 @@ Singletons/EmptyShowDeriving.hs:(0,0)-(0,0): Splicing declarations fromSing x = case x of {} toSing x = SomeSing (case x of {}) instance SShow Foo where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Foo) - (t3 :: GHC.Types.Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ (sV_0123456789876543210 :: Sing v_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden index 8bb26d8f..7716a48b 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EnumDeriving.golden @@ -96,14 +96,6 @@ Singletons/EnumDeriving.hs:(0,0)-(0,0): Splicing declarations toSing Q1 = SomeSing SQ1 toSing Q2 = SomeSing SQ2 instance SEnum Foo where - sToEnum :: - forall (t :: GHC.Num.Natural.Natural). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Foo - -> Type) t) - sFromEnum :: - forall (t :: Foo). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Foo GHC.Num.Natural.Natural - -> Type) t) sToEnum (sN :: Sing n) = id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0)))) @@ -192,14 +184,6 @@ Singletons/EnumDeriving.hs:0:0:: Splicing declarations type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a instance SEnum Quux where - sToEnum :: - forall (t :: GHC.Num.Natural.Natural). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Quux - -> Type) t) - sFromEnum :: - forall (t :: Quux). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Quux GHC.Num.Natural.Natural - -> Type) t) sToEnum (sN :: Sing n) = id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0)))) diff --git a/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden b/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden index d538d165..35a6eb9f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/EqInstances.golden @@ -31,11 +31,6 @@ Singletons/EqInstances.hs:0:0:: Splicing declarations instance PEq Foo where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a instance SEq Foo => SEq Foo where - (%==) :: - forall (t1 :: Foo) (t2 :: Foo). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Foo ((~>) Foo Bool) - -> Type) t1) t2) (%==) SFLeaf SFLeaf = STrue (%==) SFLeaf ((:%+:) _ _) = SFalse (%==) ((:%+:) _ _) SFLeaf = SFalse @@ -80,9 +75,4 @@ Singletons/EqInstances.hs:0:0:: Splicing declarations instance PEq Empty where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a instance SEq Empty where - (%==) :: - forall (t1 :: Empty) (t2 :: Empty). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Empty ((~>) Empty Bool) - -> Type) t1) t2) (%==) _ _ = STrue diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden b/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden index e6173c3f..1808bd31 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden @@ -90,12 +90,6 @@ Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations sL2r :: (forall (t :: a). Sing t -> Sing (Apply L2rSym0 t :: b) :: Type) instance SFD Bool Natural where - sMeth :: - (forall (t :: Bool). - Sing t -> Sing (Apply MethSym0 t :: Bool) :: Type) - sL2r :: - (forall (t :: Bool). - Sing t -> Sing (Apply L2rSym0 t :: Natural) :: Type) sMeth (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (singFun1 @NotSym0 sNot) sA_0123456789876543210 sL2r SFalse = sFromInteger (sing :: Sing 0) diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden index dfa7da96..990995de 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden @@ -988,19 +988,6 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations fromSing x = case x of {} toSing x = SomeSing (case x of {}) instance SFunctor (T x) where - sFmap :: - forall (a :: Type) - (b :: Type) - (t1 :: (~>) a b) - (t2 :: T x a). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (FmapSym0 :: TyFun ((~>) a b) ((~>) (T x a) (T x b)) - -> Type) t1) t2) - (%<$) :: - forall (a :: Type) (b :: Type) (t1 :: a) (t2 :: T x b). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((<$@#@$) :: TyFun a ((~>) (T x b) (T x a)) - -> Type) t1) t2) sFmap (_sf_0123456789876543210 :: Sing _f_0123456789876543210) (SMkT1 (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -1086,25 +1073,6 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations (_ :: Sing n_0123456789876543210) -> sN_0123456789876543210)) sA_0123456789876543210) instance SFoldable (T x) where - sFoldMap :: - forall (a :: Type) - (m :: Type) - (t1 :: (~>) a m) - (t2 :: T x a). SMonoid m => - Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (FoldMapSym0 :: TyFun ((~>) a m) ((~>) (T x a) m) - -> Type) t1) t2) - sFoldr :: - forall (a :: Type) - (b :: Type) - (t1 :: (~>) a ((~>) b b)) - (t2 :: b) - (t3 :: T x a). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (FoldrSym0 :: TyFun ((~>) a ((~>) b b)) ((~>) b ((~>) (T x a) b)) - -> Type) t1) t2) t3) sFoldMap (_sf_0123456789876543210 :: Sing _f_0123456789876543210) (SMkT1 (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -1232,16 +1200,6 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations sA_0123456789876543210) _sz_0123456789876543210 instance STraversable (T x) where - sTraverse :: - forall (a :: Type) - (f :: Type -> Type) - (b :: Type) - (t1 :: (~>) a (f b)) - (t2 :: T x a). SApplicative f => - Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (TraverseSym0 :: TyFun ((~>) a (f b)) ((~>) (T x a) (f (T x b))) - -> Type) t1) t2) sTraverse (_sf_0123456789876543210 :: Sing _f_0123456789876543210) (SMkT1 (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -1277,19 +1235,6 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @FmapSym0 sFmap) (singFun1 @MkT2Sym0 SMkT2)) (applySing (singFun1 @PureSym0 sPure) sA_0123456789876543210) instance SFunctor Empty where - sFmap :: - forall (a :: Type) - (b :: Type) - (t1 :: (~>) a b) - (t2 :: Empty a). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (FmapSym0 :: TyFun ((~>) a b) ((~>) (Empty a) (Empty b)) - -> Type) t1) t2) - (%<$) :: - forall (a :: Type) (b :: Type) (t1 :: a) (t2 :: Empty b). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((<$@#@$) :: TyFun a ((~>) (Empty b) (Empty a)) - -> Type) t1) t2) sFmap _ (sV_0123456789876543210 :: Sing v_0123456789876543210) = id @(Sing (Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210)) @@ -1299,27 +1244,8 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations @(Sing (Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210)) (case sV_0123456789876543210 of {}) instance SFoldable Empty where - sFoldMap :: - forall (a :: Type) - (m :: Type) - (t1 :: (~>) a m) - (t2 :: Empty a). SMonoid m => - Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (FoldMapSym0 :: TyFun ((~>) a m) ((~>) (Empty a) m) - -> Type) t1) t2) sFoldMap _ _ = sMempty instance STraversable Empty where - sTraverse :: - forall (a :: Type) - (f :: Type -> Type) - (b :: Type) - (t1 :: (~>) a (f b)) - (t2 :: Empty a). SApplicative f => - Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (TraverseSym0 :: TyFun ((~>) a (f b)) ((~>) (Empty a) (f (Empty b))) - -> Type) t1) t2) sTraverse _ (sV_0123456789876543210 :: Sing v_0123456789876543210) = applySing (singFun1 @PureSym0 sPure) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden b/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden index 2a9a04c4..2b375527 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden @@ -104,11 +104,6 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations toSing (Just (b :: Demote a)) = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SJust c) instance SEq a => SEq (Maybe a) where - (%==) :: - forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun (Maybe a) ((~>) (Maybe a) Bool) - -> Type) t1) t2) (%==) SNothing SNothing = STrue (%==) SNothing (SJust _) = SFalse (%==) (SJust _) SNothing = SFalse @@ -119,14 +114,6 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SShow a => SShow (Maybe a) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Maybe a) - (t3 :: GHC.Types.Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SNothing diff --git a/singletons-base/tests/compile-and-dump/Singletons/Nat.golden b/singletons-base/tests/compile-and-dump/Singletons/Nat.golden index 6380764d..8d6abc58 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Nat.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Nat.golden @@ -211,11 +211,6 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations toSing (Succ (b :: Demote Nat)) = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c) instance SEq Nat => SEq Nat where - (%==) :: - forall (t1 :: Nat) (t2 :: Nat). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) - -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse @@ -226,14 +221,6 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SShow Nat => SShow Nat where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Nat) - (t3 :: GHC.Types.Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Nat ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SZero @@ -265,11 +252,6 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations sArg_0123456789876543210))) sA_0123456789876543210 instance SOrd Nat => SOrd Nat where - sCompare :: - forall (t1 :: Nat) (t2 :: Nat). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) - -> Type) t1) t2) sCompare SZero SZero = applySing (applySing diff --git a/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden index 2abd0838..3f9c8b9b 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden @@ -584,11 +584,6 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations (,,,) (SomeSing c) (SomeSing c) (SomeSing c) (SomeSing c) -> SomeSing (SF c c c c) instance SEq Nat => SEq Nat where - (%==) :: - forall (t1 :: Nat) (t2 :: Nat). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool) - -> Type) t1) t2) (%==) SZero SZero = STrue (%==) SZero (SSucc _) = SFalse (%==) (SSucc _) SZero = SFalse @@ -599,11 +594,6 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SOrd Nat => SOrd Nat where - sCompare :: - forall (t1 :: Nat) (t2 :: Nat). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering) - -> Type) t1) t2) sCompare SZero SZero = applySing (applySing @@ -627,11 +617,6 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations sCompare SZero (SSucc _) = SLT sCompare (SSucc _) SZero = SGT instance (SEq a, SEq b, SEq c, SEq d) => SEq (Foo a b c d) where - (%==) :: - forall (t1 :: Foo a b c d) (t2 :: Foo a b c d). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun (Foo a b c d) ((~>) (Foo a b c d) Bool) - -> Type) t1) t2) (%==) (SA (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) @@ -844,11 +829,6 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations sB_0123456789876543210))) instance (SOrd a, SOrd b, SOrd c, SOrd d) => SOrd (Foo a b c d) where - sCompare :: - forall (t1 :: Foo a b c d) (t2 :: Foo a b c d). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun (Foo a b c d) ((~>) (Foo a b c d) Ordering) - -> Type) t1) t2) sCompare (SA (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden index 8e2eb964..409f195a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden @@ -142,14 +142,6 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations = case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing b) of (,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c) instance (SShow a, SShow b) => SShow (Pair a b) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Pair a b) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SPair (sArg_0123456789876543210 :: Sing arg_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden index 8c855cb8..9062a3c2 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden @@ -343,14 +343,6 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations of (,) (SomeSing c) (SomeSing c) -> SomeSing (SMkFoo3 c c) instance SShow Foo1 where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Foo1) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo1 ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SMkFoo1 @@ -360,14 +352,6 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "MkFoo1")) sA_0123456789876543210 instance SShow a => SShow (Foo2 a) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Foo2 a) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Foo2 a) ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SMkFoo2a (sArg_0123456789876543210 :: Sing arg_0123456789876543210) @@ -500,14 +484,6 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations sArgR_0123456789876543210)))) sA_0123456789876543210 instance SShow Bool => SShow Foo3 where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Foo3) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Foo3 ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) (SMkFoo3 (sArg_0123456789876543210 :: Sing arg_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden index a9867bef..8defb630 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden @@ -325,11 +325,6 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations toSing S1 = SomeSing SS1 toSing S2 = SomeSing SS2 instance SEq a => SEq (T a ()) where - (%==) :: - forall (t1 :: T a ()) (t2 :: T a ()). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun (T a ()) ((~>) (T a ()) Bool) - -> Type) t1) t2) (%==) ((:%*:) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) @@ -345,11 +340,6 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210) instance SOrd a => SOrd (T a ()) where - sCompare :: - forall (t1 :: T a ()) (t2 :: T a ()). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun (T a ()) ((~>) (T a ()) Ordering) - -> Type) t1) t2) sCompare ((:%*:) (sA_0123456789876543210 :: Sing a_0123456789876543210) (sA_0123456789876543210 :: Sing a_0123456789876543210)) @@ -373,14 +363,6 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations sB_0123456789876543210)) SNil)) instance SShow a => SShow (T a ()) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: T a ()) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec (sP_0123456789876543210 :: Sing p_0123456789876543210) ((:%*:) (sArgL_0123456789876543210 :: Sing argL_0123456789876543210) @@ -413,21 +395,11 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations sArgR_0123456789876543210)))) sA_0123456789876543210 instance SEq S where - (%==) :: - forall (t1 :: S) (t2 :: S). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun S ((~>) S Bool) - -> Type) t1) t2) (%==) SS1 SS1 = STrue (%==) SS1 SS2 = SFalse (%==) SS2 SS1 = SFalse (%==) SS2 SS2 = STrue instance SOrd S where - sCompare :: - forall (t1 :: S) (t2 :: S). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun S ((~>) S Ordering) - -> Type) t1) t2) sCompare SS1 SS1 = applySing (applySing @@ -443,14 +415,6 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations sCompare SS1 SS2 = SLT sCompare SS2 SS1 = SGT instance SShow S where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: S) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) S ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SS1 @@ -468,19 +432,9 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "S2")) sA_0123456789876543210 instance SBounded S where - sMinBound :: Sing (MinBoundSym0 :: S) - sMaxBound :: Sing (MaxBoundSym0 :: S) sMinBound = SS1 sMaxBound = SS2 instance SEnum S where - sToEnum :: - forall (t :: GHC.Num.Natural.Natural). Sing t - -> Sing (Apply (ToEnumSym0 :: TyFun GHC.Num.Natural.Natural S - -> Type) t) - sFromEnum :: - forall (t :: S). Sing t - -> Sing (Apply (FromEnumSym0 :: TyFun S GHC.Num.Natural.Natural - -> Type) t) sToEnum (sN :: Sing n) = id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0)))) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Star.golden b/singletons-base/tests/compile-and-dump/Singletons/Star.golden index 683eb463..313f9e7a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Star.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Star.golden @@ -265,11 +265,6 @@ Singletons/Star.hs:0:0:: Splicing declarations -> Type) where GHC.Internal.Data.Type.Coercion.testCoercion = decideCoercion instance (SEq Type, SEq Nat) => SEq Type where - (%==) :: - forall (t1 :: Type) (t2 :: Type). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Type ((~>) Type Bool) - -> Type) t1) t2) (%==) SNat SNat = STrue (%==) SNat SInt = SFalse (%==) SNat SString = SFalse @@ -314,11 +309,6 @@ Singletons/Star.hs:0:0:: Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210) instance (SOrd Type, SOrd Nat) => SOrd Type where - sCompare :: - forall (t1 :: Type) (t2 :: Type). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun Type ((~>) Type Ordering) - -> Type) t1) t2) sCompare SNat SNat = applySing (applySing @@ -394,14 +384,6 @@ Singletons/Star.hs:0:0:: Splicing declarations sCompare (SVec _ _) SString = SGT sCompare (SVec _ _) (SMaybe _) = SGT instance (SShow Type, SShow Nat) => SShow Type where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Type) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) Type ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SNat diff --git a/singletons-base/tests/compile-and-dump/Singletons/T136.golden b/singletons-base/tests/compile-and-dump/Singletons/T136.golden index 8fa94875..e5ea9563 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136.golden @@ -113,20 +113,6 @@ Singletons/T136.hs:(0,0)-(0,0): Splicing declarations type ToEnum a = Apply ToEnum_0123456789876543210Sym0 a type FromEnum a = Apply FromEnum_0123456789876543210Sym0 a instance SEnum [Bool] where - sSucc :: - forall (t :: [Bool]). Sing t - -> Sing (Apply (SuccSym0 :: TyFun [Bool] [Bool] -> Type) t) - sPred :: - forall (t :: [Bool]). Sing t - -> Sing (Apply (PredSym0 :: TyFun [Bool] [Bool] -> Type) t) - sToEnum :: - forall (t :: GHC.Num.Natural.Natural). Sing t - -> Sing (Apply (ToEnumSym0 :: TyFun GHC.Num.Natural.Natural [Bool] - -> Type) t) - sFromEnum :: - forall (t :: [Bool]). Sing t - -> Sing (Apply (FromEnumSym0 :: TyFun [Bool] GHC.Num.Natural.Natural - -> Type) t) sSucc SNil = applySing (applySing (singFun2 @(:@#@$) SCons) STrue) SNil sSucc (SCons SFalse (sAs :: Sing as)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T136b.golden b/singletons-base/tests/compile-and-dump/Singletons/T136b.golden index 2985b700..dcf06da3 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136b.golden @@ -48,8 +48,5 @@ Singletons/T136b.hs:(0,0)-(0,0): Splicing declarations instance PC Bool where type Meth a = Apply Meth_0123456789876543210Sym0 a instance SC Bool where - sMeth :: - forall (t :: Bool). Sing t - -> Sing (Apply (MethSym0 :: TyFun Bool Bool -> Type) t) sMeth (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing (singFun1 @NotSym0 sNot) sA_0123456789876543210 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T167.golden b/singletons-base/tests/compile-and-dump/Singletons/T167.golden index 56ed9a83..1d5770cf 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T167.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T167.golden @@ -146,12 +146,6 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations (sA_0123456789876543210 :: Sing a_0123456789876543210) = sUndefined sA_0123456789876543210 sA_0123456789876543210 instance SFoo a => SFoo [a] where - sFoosPrec :: - (forall (t :: Natural) (t :: [a]) (t :: [Bool]). - Sing t - -> Sing t - -> Sing t - -> Sing (Apply (Apply (Apply FoosPrecSym0 t) t) t :: [Bool]) :: Type) sFoosPrec _ (sA_0123456789876543210 :: Sing a_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T178.golden b/singletons-base/tests/compile-and-dump/Singletons/T178.golden index 755aab69..45601070 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T178.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T178.golden @@ -157,11 +157,6 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations toSing Opt = SomeSing SOpt toSing Many = SomeSing SMany instance SEq Occ where - (%==) :: - forall (t1 :: Occ) (t2 :: Occ). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Occ ((~>) Occ Bool) - -> Type) t1) t2) (%==) SStr SStr = STrue (%==) SStr SOpt = SFalse (%==) SStr SMany = SFalse @@ -172,11 +167,6 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations (%==) SMany SOpt = SFalse (%==) SMany SMany = STrue instance SOrd Occ where - sCompare :: - forall (t1 :: Occ) (t2 :: Occ). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun Occ ((~>) Occ Ordering) - -> Type) t1) t2) sCompare SStr SStr = applySing (applySing @@ -202,12 +192,6 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations sCompare SMany SStr = SGT sCompare SMany SOpt = SGT instance SShow Occ where - sShowsPrec :: - forall (t1 :: Natural) (t2 :: Occ) (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun Natural ((~>) Occ ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SStr diff --git a/singletons-base/tests/compile-and-dump/Singletons/T187.golden b/singletons-base/tests/compile-and-dump/Singletons/T187.golden index 7578015f..fb4952a7 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T187.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T187.golden @@ -68,18 +68,8 @@ Singletons/T187.hs:(0,0)-(0,0): Splicing declarations fromSing x = case x of {} toSing x = SomeSing (case x of {}) instance SEq Empty where - (%==) :: - forall (t1 :: Empty) (t2 :: Empty). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun Empty ((~>) Empty Bool) - -> Type) t1) t2) (%==) _ _ = STrue instance SOrd Empty where - sCompare :: - forall (t1 :: Empty) (t2 :: Empty). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun Empty ((~>) Empty Ordering) - -> Type) t1) t2) sCompare _ _ = SEQ instance SDecide Empty where (%~) x _ = Proved (case x of {}) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T190.golden b/singletons-base/tests/compile-and-dump/Singletons/T190.golden index 56464bcf..59085dc2 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T190.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T190.golden @@ -160,18 +160,8 @@ Singletons/T190.hs:0:0:: Splicing declarations fromSing ST = T toSing T = SomeSing ST instance SEq T where - (%==) :: - forall (t1 :: T) (t2 :: T). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun T ((~>) T Bool) - -> Type) t1) t2) (%==) ST ST = STrue instance SOrd T where - sCompare :: - forall (t1 :: T) (t2 :: T). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun T ((~>) T Ordering) - -> Type) t1) t2) sCompare ST ST = applySing (applySing @@ -179,14 +169,6 @@ Singletons/T190.hs:0:0:: Splicing declarations SEQ) SNil instance SEnum T where - sToEnum :: - forall (t :: GHC.Num.Natural.Natural). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural T - -> Type) t) - sFromEnum :: - forall (t :: T). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun T GHC.Num.Natural.Natural - -> Type) t) sToEnum (sN :: Sing n) = id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0)))) @@ -199,19 +181,9 @@ Singletons/T190.hs:0:0:: Splicing declarations SFalse -> sError (sing :: Sing "toEnum: bad argument")) sFromEnum ST = sFromInteger (sing :: Sing 0) instance SBounded T where - sMinBound :: Sing (MinBoundSym0 :: T) - sMaxBound :: Sing (MaxBoundSym0 :: T) sMinBound = ST sMaxBound = ST instance SShow T where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: T) - (t3 :: GHC.Types.Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) T ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ ST diff --git a/singletons-base/tests/compile-and-dump/Singletons/T271.golden b/singletons-base/tests/compile-and-dump/Singletons/T271.golden index 52870d77..77c91303 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T271.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T271.golden @@ -177,11 +177,6 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations = case toSing b :: SomeSing a of SomeSing c -> SomeSing (SIdentity c) instance SEq a => SEq (Constant a b) where - (%==) :: - forall (t1 :: Constant a b) (t2 :: Constant a b). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun (Constant a b) ((~>) (Constant a b) Bool) - -> Type) t1) t2) (%==) (SConstant (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SConstant (sB_0123456789876543210 :: Sing b_0123456789876543210)) @@ -189,11 +184,6 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SOrd a => SOrd (Constant a b) where - sCompare :: - forall (t1 :: Constant a b) (t2 :: Constant a b). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun (Constant a b) ((~>) (Constant a b) Ordering) - -> Type) t1) t2) sCompare (SConstant (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SConstant (sB_0123456789876543210 :: Sing b_0123456789876543210)) @@ -209,11 +199,6 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations sB_0123456789876543210)) SNil) instance SEq a => SEq (Identity a) where - (%==) :: - forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun (Identity a) ((~>) (Identity a) Bool) - -> Type) t1) t2) (%==) (SIdentity (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SIdentity (sB_0123456789876543210 :: Sing b_0123456789876543210)) @@ -221,11 +206,6 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210) sB_0123456789876543210 instance SOrd a => SOrd (Identity a) where - sCompare :: - forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun (Identity a) ((~>) (Identity a) Ordering) - -> Type) t1) t2) sCompare (SIdentity (sA_0123456789876543210 :: Sing a_0123456789876543210)) (SIdentity (sB_0123456789876543210 :: Sing b_0123456789876543210)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T287.golden b/singletons-base/tests/compile-and-dump/Singletons/T287.golden index f1e0b444..de058a01 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T287.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T287.golden @@ -94,11 +94,6 @@ Singletons/T287.hs:(0,0)-(0,0): Splicing declarations Sing t -> Sing t -> Sing (Apply (Apply (<<>>@#@$) t) t :: a) :: Type) instance SS b => SS ((~>) a b) where - (%<<>>) :: - (forall (t :: (~>) a b) (t :: (~>) a b). - Sing t - -> Sing t - -> Sing (Apply (Apply (<<>>@#@$) t) t :: (~>) a b) :: Type) (%<<>>) (sF :: Sing f) (sG :: Sing g) = singFun1 @(Apply (Apply Lambda_0123456789876543210Sym0 f) g) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T358.golden b/singletons-base/tests/compile-and-dump/Singletons/T358.golden index e9c8b5b0..79b9f9e4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T358.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T358.golden @@ -107,8 +107,6 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations sMethod1 :: (Sing (Method1Sym0 :: [a]) :: Type) sMethod1 = SNil instance SC2 [a] where - sMethod2a :: - forall b (t :: b). Sing t -> Sing (Apply Method2aSym0 t :: [a]) sMethod2b :: forall b (t :: b). Sing t -> Sing (Apply Method2bSym0 t :: [a]) sMethod2a _ = SNil diff --git a/singletons-base/tests/compile-and-dump/Singletons/T371.golden b/singletons-base/tests/compile-and-dump/Singletons/T371.golden index 2b1ffead..ee820a15 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T371.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T371.golden @@ -146,14 +146,6 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations toSing (Y2 (b :: Demote (X a))) = case toSing b :: SomeSing (X a) of SomeSing c -> SomeSing (SY2 c) instance SShow (Y a) => SShow (X a) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: X a) - (t3 :: GHC.Types.Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (X a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SX1 @@ -185,14 +177,6 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations sArg_0123456789876543210))) sA_0123456789876543210 instance SShow (X a) => SShow (Y a) where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: Y a) - (t3 :: GHC.Types.Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) (Y a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SY1 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T555.golden b/singletons-base/tests/compile-and-dump/Singletons/T555.golden index 922e3c6a..654440b5 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T555.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T555.golden @@ -129,21 +129,11 @@ Singletons/T555.hs:(0,0)-(0,0): Splicing declarations toSing Location = SomeSing SLocation toSing Quaternion = SomeSing SQuaternion instance SEq MyPropKind where - (%==) :: - forall (t1 :: MyPropKind) (t2 :: MyPropKind). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply ((==@#@$) :: TyFun MyPropKind ((~>) MyPropKind Bool) - -> Type) t1) t2) (%==) SLocation SLocation = STrue (%==) SLocation SQuaternion = SFalse (%==) SQuaternion SLocation = SFalse (%==) SQuaternion SQuaternion = STrue instance SOrd MyPropKind where - sCompare :: - forall (t1 :: MyPropKind) (t2 :: MyPropKind). Sing t1 - -> Sing t2 - -> Sing (Apply (Apply (CompareSym0 :: TyFun MyPropKind ((~>) MyPropKind Ordering) - -> Type) t1) t2) sCompare SLocation SLocation = applySing (applySing @@ -159,14 +149,6 @@ Singletons/T555.hs:(0,0)-(0,0): Splicing declarations sCompare SLocation SQuaternion = SLT sCompare SQuaternion SLocation = SGT instance SShow MyPropKind where - sShowsPrec :: - forall (t1 :: GHC.Num.Natural.Natural) - (t2 :: MyPropKind) - (t3 :: Symbol). Sing t1 - -> Sing t2 - -> Sing t3 - -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) Symbol Symbol)) - -> Type) t1) t2) t3) sShowsPrec _ SLocation diff --git a/singletons-base/tests/compile-and-dump/Singletons/T89.golden b/singletons-base/tests/compile-and-dump/Singletons/T89.golden index 8db09927..6342f213 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T89.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T89.golden @@ -55,14 +55,6 @@ Singletons/T89.hs:0:0:: Splicing declarations fromSing SFoo = Foo toSing Foo = SomeSing SFoo instance SEnum Foo where - sToEnum :: - forall (t :: GHC.Num.Natural.Natural). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.ToEnumSym0 :: TyFun GHC.Num.Natural.Natural Foo - -> Type) t) - sFromEnum :: - forall (t :: Foo). Sing t - -> Sing (Apply (Data.Singletons.Base.Enum.FromEnumSym0 :: TyFun Foo GHC.Num.Natural.Natural - -> Type) t) sToEnum (sN :: Sing n) = id @(Sing (Case_0123456789876543210 n (Apply (Apply (==@#@$) n) (FromInteger 0)))) diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs index 1e2f4a57..0369bdd5 100644 --- a/singletons-th/src/Data/Singletons/TH/Single.hs +++ b/singletons-th/src/Data/Singletons/TH/Single.hs @@ -476,22 +476,7 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys sing_meth :: Name -> ALetDecRHS -> SgM [DDec] sing_meth name rhs = do opts <- getOptions - mb_s_info <- dsReify (singledValueName opts name) - inst_kis <- mapM promoteType inst_tys - let mk_subst cls_tvbs = Map.fromList $ zip (map extractTvbName vis_cls_tvbs) inst_kis - where - -- This is a half-hearted attempt to address the underlying problem - -- in #358, where we can sometimes have more class type variables - -- (due to implicit kind arguments) than class arguments. This just - -- ensures that the explicit type variables are properly mapped - -- to the class arguments, leaving the implicit kind variables - -- unmapped. That could potentially cause *other* problems, but - -- those are perhaps best avoided by using InstanceSigs. At the - -- very least, this workaround will make error messages slightly - -- less confusing. - vis_cls_tvbs = drop (length cls_tvbs - length inst_kis) cls_tvbs - - sing_meth_ty :: DType -> SgM DType + let sing_meth_ty :: DType -> SgM DType sing_meth_ty inner_ty = do -- Make sure to expand through type synonyms here! Not doing so -- resulted in #167. @@ -500,24 +485,12 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys <- singType (DConT $ defunctionalizedName0 opts name) raw_ty pure s_ty - s_ty <- case OMap.lookup name inst_sigs of - Just inst_sig -> - -- We have an InstanceSig, so just single that type. - sing_meth_ty inst_sig - Nothing -> case mb_s_info of - -- We don't have an InstanceSig, so we must compute the type to use - -- in the singled instance ourselves through reification. - Just (DVarI _ (DForallT (DForallInvis cls_tvbs) (DConstrainedT _cls_pred s_ty)) _) -> - pure $ substType (mk_subst cls_tvbs) s_ty - _ -> do - mb_info <- dsReify name - case mb_info of - Just (DVarI _ (DForallT (DForallInvis cls_tvbs) - (DConstrainedT _cls_pred inner_ty)) _) -> do - s_ty <- sing_meth_ty inner_ty - pure $ substType (mk_subst cls_tvbs) s_ty - _ -> fail $ "Cannot find type of method " ++ show name - + -- If an instance signature exists, single it. Otherwise, leave it out. + -- Unlike most other places, we don't actually *need* explicit type + -- signatures for instance methods, as GHC can figure out the types of + -- the instance methods on its own. As such, any GADT pattern matching in + -- the singled instance method code will work as expected. + mb_s_ty <- traverse sing_meth_ty $ OMap.lookup name inst_sigs meth' <- singLetDecRHS Map.empty -- Because we are singling an instance declaration, -- we aren't generating defunctionalization symbols @@ -525,7 +498,9 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys -- generating any SingI instances. Therefore, we -- don't need to include anything in this Map. name rhs - return $ map DLetDec [DSigD (singledValueName opts name) s_ty, meth'] + return $ map DLetDec + $ maybeToList (DSigD (singledValueName opts name) <$> mb_s_ty) + ++ [meth'] singLetDecEnv :: ALetDecEnv -> SgM a