From eb697622038d5bb62af6de2ec5a97d08349e4ae9 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 2 May 2024 06:44:37 -0400 Subject: [PATCH] Draft: singletons-base: Accept GHC 9.10 golden test output TODO RGS: The output for `Singletons/PatternMatching.hs` is wrong. It might be fixed when https://gitlab.haskell.org/ghc/ghc/-/merge_requests/12493 is backported to the `ghc-9.10` branch. --- .../GradingClient/Database.golden | 34 +++++++------ .../Promote/GenDefunSymbols.golden | 2 +- .../compile-and-dump/Promote/T361.golden | 2 +- .../Singletons/BoundedDeriving.golden | 22 ++++----- .../Singletons/BoxUnBox.golden | 6 +-- .../Singletons/CaseExpressions.golden | 20 ++++---- .../Singletons/Classes.golden | 12 ++--- .../Singletons/Contains.golden | 4 +- .../Singletons/DataValues.golden | 6 +-- .../compile-and-dump/Singletons/Error.golden | 4 +- .../compile-and-dump/Singletons/Fixity.golden | 6 +-- .../Singletons/FunDeps.golden | 4 +- .../Singletons/FunctorLikeDeriving.golden | 40 ++++++++-------- .../Singletons/HigherOrder.golden | 20 ++++---- .../Singletons/LambdaCase.golden | 12 ++--- .../Singletons/Lambdas.golden | 38 +++++++-------- .../Singletons/LetStatements.golden | 8 ++-- .../compile-and-dump/Singletons/Maybe.golden | 22 +++++---- .../compile-and-dump/Singletons/Nat.golden | 10 ++-- .../Singletons/OrdDeriving.golden | 40 +++++++++------- .../Singletons/PatternMatching.golden | 48 +++++++++++++------ .../Singletons/PolyKinds.golden | 2 +- .../Singletons/PolyKindsApp.golden | 3 +- .../Singletons/Records.golden | 10 ++-- .../Singletons/ReturnFunc.golden | 8 ++-- .../Singletons/ShowDeriving.golden | 12 ++--- .../Singletons/StandaloneDeriving.golden | 34 +++++++------ .../compile-and-dump/Singletons/Star.golden | 10 ++-- .../compile-and-dump/Singletons/T136b.golden | 2 +- .../compile-and-dump/Singletons/T145.golden | 2 +- .../compile-and-dump/Singletons/T150.golden | 38 +++++++-------- .../compile-and-dump/Singletons/T160.golden | 6 +-- .../compile-and-dump/Singletons/T163.golden | 4 +- .../compile-and-dump/Singletons/T166.golden | 10 ++-- .../compile-and-dump/Singletons/T167.golden | 12 ++--- .../compile-and-dump/Singletons/T175.golden | 12 ++--- .../compile-and-dump/Singletons/T176.golden | 16 +++---- .../compile-and-dump/Singletons/T178.golden | 12 ++--- .../compile-and-dump/Singletons/T183.golden | 38 +++++++-------- .../compile-and-dump/Singletons/T184.golden | 16 +++---- .../compile-and-dump/Singletons/T187.golden | 12 ++--- .../compile-and-dump/Singletons/T190.golden | 10 ++-- .../compile-and-dump/Singletons/T197b.golden | 4 +- .../compile-and-dump/Singletons/T204.golden | 4 +- .../compile-and-dump/Singletons/T209.golden | 4 +- .../compile-and-dump/Singletons/T249.golden | 6 +-- .../compile-and-dump/Singletons/T271.golden | 44 ++++++++--------- .../compile-and-dump/Singletons/T287.golden | 6 +-- .../compile-and-dump/Singletons/T296.golden | 6 +-- .../compile-and-dump/Singletons/T297.golden | 6 +-- .../compile-and-dump/Singletons/T312.golden | 12 ++--- .../compile-and-dump/Singletons/T316.golden | 4 +- .../compile-and-dump/Singletons/T326.golden | 4 +- .../compile-and-dump/Singletons/T353.golden | 5 +- .../compile-and-dump/Singletons/T358.golden | 18 +++---- .../compile-and-dump/Singletons/T367.golden | 4 +- .../compile-and-dump/Singletons/T371.golden | 16 +++---- .../compile-and-dump/Singletons/T378a.golden | 12 ++--- .../compile-and-dump/Singletons/T378b.golden | 4 +- .../compile-and-dump/Singletons/T410.golden | 2 +- .../compile-and-dump/Singletons/T412.golden | 24 +++++----- .../compile-and-dump/Singletons/T433.golden | 36 +++++++------- .../compile-and-dump/Singletons/T443.golden | 12 ++--- .../compile-and-dump/Singletons/T450.golden | 6 +-- .../compile-and-dump/Singletons/T470.golden | 6 +-- .../compile-and-dump/Singletons/T489.golden | 4 +- .../compile-and-dump/Singletons/T511.golden | 4 +- .../compile-and-dump/Singletons/T536.golden | 20 ++++---- .../compile-and-dump/Singletons/T555.golden | 12 ++--- .../compile-and-dump/Singletons/T567.golden | 8 ++-- .../compile-and-dump/Singletons/T571.golden | 8 ++-- .../compile-and-dump/Singletons/T585.golden | 4 +- .../Singletons/TopLevelPatterns.golden | 40 +++++++++------- .../Singletons/TypeAbstractions.golden | 16 +++---- 74 files changed, 518 insertions(+), 472 deletions(-) diff --git a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden index 4bc4cac7..9b0f0376 100644 --- a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden +++ b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden @@ -146,12 +146,14 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations instance Eq (SNat (z :: Nat)) where (==) _ _ = True instance SDecide Nat => - Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => - Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SNat (z :: Nat)) where compare _ _ = EQ @@ -1448,7 +1450,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations sScrutinee_0123456789876543210 = applySing (applySing (singFun2 @(==@#@$) (%==)) sName) sName' in - GHC.Base.id + GHC.Internal.Base.id @(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs))) (case sScrutinee_0123456789876543210 of STrue -> sU @@ -2694,12 +2696,14 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations instance Eq (SU (z :: U)) where (==) _ _ = True instance (SDecide U, SDecide Nat) => - Data.Type.Equality.TestEquality (SU :: U -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SU :: U + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance (SDecide U, SDecide Nat) => - Data.Type.Coercion.TestCoercion (SU :: U -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SU :: U + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance SDecide AChar where (%~) SCA SCA = Proved Refl @@ -3380,13 +3384,13 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations (%~) SCZ SCZ = Proved Refl instance Eq (SAChar (z :: AChar)) where (==) _ _ = True - instance Data.Type.Equality.TestEquality (SAChar :: AChar - -> Type) where - Data.Type.Equality.testEquality + instance GHC.Internal.Data.Type.Equality.TestEquality (SAChar :: AChar + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (SAChar :: AChar - -> Type) where - Data.Type.Coercion.testCoercion + instance GHC.Internal.Data.Type.Coercion.TestCoercion (SAChar :: AChar + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance (Data.Singletons.ShowSing.ShowSing U, Data.Singletons.ShowSing.ShowSing Nat) => diff --git a/singletons-base/tests/compile-and-dump/Promote/GenDefunSymbols.golden b/singletons-base/tests/compile-and-dump/Promote/GenDefunSymbols.golden index a107ea36..8407b409 100644 --- a/singletons-base/tests/compile-and-dump/Promote/GenDefunSymbols.golden +++ b/singletons-base/tests/compile-and-dump/Promote/GenDefunSymbols.golden @@ -23,7 +23,7 @@ Promote/GenDefunSymbols.hs:0:0:: Splicing declarations = snd ((,) LiftMaybeSym1KindInference ()) type LiftMaybeSym2 :: forall (a :: Type) (b :: Type). (~>) a b -> Maybe a -> Maybe b - type family LiftMaybeSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where + type family LiftMaybeSym2 @(a :: Type) @(b :: Type) (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where LiftMaybeSym2 a0123456789876543210 a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210 type ZeroSym0 :: NatT type family ZeroSym0 :: NatT where diff --git a/singletons-base/tests/compile-and-dump/Promote/T361.golden b/singletons-base/tests/compile-and-dump/Promote/T361.golden index 0a6c6077..2707f38e 100644 --- a/singletons-base/tests/compile-and-dump/Promote/T361.golden +++ b/singletons-base/tests/compile-and-dump/Promote/T361.golden @@ -2,7 +2,7 @@ Promote/T361.hs:0:0:: Splicing declarations genDefunSymbols [''Proxy] ======> type ProxySym0 :: forall k (t :: k). Proxy t - type family ProxySym0 :: Proxy t where + type family ProxySym0 @k @(t :: k) :: Proxy t where ProxySym0 = 'Proxy Promote/T361.hs:(0,0)-(0,0): Splicing declarations promote diff --git a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden index 42866593..08cc4ba2 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden @@ -58,13 +58,13 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo3Sym0 where suppressUnusedWarnings = snd ((,) Foo3Sym0KindInference ()) type Foo3Sym1 :: forall a. a -> Foo3 a - type family Foo3Sym1 (a0123456789876543210 :: a) :: Foo3 a where + type family Foo3Sym1 @a (a0123456789876543210 :: a) :: Foo3 a where Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210 type Foo41Sym0 :: forall (a :: Type) (b :: Type). Foo4 a b - type family Foo41Sym0 :: Foo4 a b where + type family Foo41Sym0 @(a :: Type) @(b :: Type) :: Foo4 a b where Foo41Sym0 = Foo41 type Foo42Sym0 :: forall (a :: Type) (b :: Type). Foo4 a b - type family Foo42Sym0 :: Foo4 a b where + type family Foo42Sym0 @(a :: Type) @(b :: Type) :: Foo4 a b where Foo42Sym0 = Foo42 type PairSym0 :: (~>) Bool ((~>) Bool Pair) data PairSym0 :: (~>) Bool ((~>) Bool Pair) @@ -116,31 +116,31 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations type MinBound = MinBound_0123456789876543210Sym0 type MaxBound = MaxBound_0123456789876543210Sym0 type MinBound_0123456789876543210 :: Foo3 a - type family MinBound_0123456789876543210 :: Foo3 a where + type family MinBound_0123456789876543210 @a :: Foo3 a where MinBound_0123456789876543210 = Apply Foo3Sym0 MinBoundSym0 type MinBound_0123456789876543210Sym0 :: Foo3 a - type family MinBound_0123456789876543210Sym0 :: Foo3 a where + type family MinBound_0123456789876543210Sym0 @a :: Foo3 a where MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210 type MaxBound_0123456789876543210 :: Foo3 a - type family MaxBound_0123456789876543210 :: Foo3 a where + type family MaxBound_0123456789876543210 @a :: Foo3 a where MaxBound_0123456789876543210 = Apply Foo3Sym0 MaxBoundSym0 type MaxBound_0123456789876543210Sym0 :: Foo3 a - type family MaxBound_0123456789876543210Sym0 :: Foo3 a where + type family MaxBound_0123456789876543210Sym0 @a :: Foo3 a where MaxBound_0123456789876543210Sym0 = MaxBound_0123456789876543210 instance PBounded (Foo3 a) where type MinBound = MinBound_0123456789876543210Sym0 type MaxBound = MaxBound_0123456789876543210Sym0 type MinBound_0123456789876543210 :: Foo4 a b - type family MinBound_0123456789876543210 :: Foo4 a b where + type family MinBound_0123456789876543210 @a @b :: Foo4 a b where MinBound_0123456789876543210 = Foo41Sym0 type MinBound_0123456789876543210Sym0 :: Foo4 a b - type family MinBound_0123456789876543210Sym0 :: Foo4 a b where + type family MinBound_0123456789876543210Sym0 @a @b :: Foo4 a b where MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210 type MaxBound_0123456789876543210 :: Foo4 a b - type family MaxBound_0123456789876543210 :: Foo4 a b where + type family MaxBound_0123456789876543210 @a @b :: Foo4 a b where MaxBound_0123456789876543210 = Foo42Sym0 type MaxBound_0123456789876543210Sym0 :: Foo4 a b - type family MaxBound_0123456789876543210Sym0 :: Foo4 a b where + type family MaxBound_0123456789876543210Sym0 @a @b :: Foo4 a b where MaxBound_0123456789876543210Sym0 = MaxBound_0123456789876543210 instance PBounded (Foo4 a b) where type MinBound = MinBound_0123456789876543210Sym0 diff --git a/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden b/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden index 8224800d..cf5d5ce9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/BoxUnBox.golden @@ -17,7 +17,7 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FBoxSym0 where suppressUnusedWarnings = snd ((,) FBoxSym0KindInference ()) type FBoxSym1 :: forall a. a -> Box a - type family FBoxSym1 (a0123456789876543210 :: a) :: Box a where + type family FBoxSym1 @a (a0123456789876543210 :: a) :: Box a where FBoxSym1 a0123456789876543210 = FBox a0123456789876543210 type UnBoxSym0 :: (~>) (Box a) a data UnBoxSym0 :: (~>) (Box a) a @@ -28,10 +28,10 @@ Singletons/BoxUnBox.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings UnBoxSym0 where suppressUnusedWarnings = snd ((,) UnBoxSym0KindInference ()) type UnBoxSym1 :: Box a -> a - type family UnBoxSym1 (a0123456789876543210 :: Box a) :: a where + type family UnBoxSym1 @a (a0123456789876543210 :: Box a) :: a where UnBoxSym1 a0123456789876543210 = UnBox a0123456789876543210 type UnBox :: Box a -> a - type family UnBox (a :: Box a) :: a where + type family UnBox @a (a :: Box a) :: a where UnBox (FBox a) = a sUnBox :: (forall (t :: Box a). diff --git a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden index 32bb0544..f46fa069 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden @@ -156,7 +156,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo5Sym0 where suppressUnusedWarnings = snd ((,) Foo5Sym0KindInference ()) type Foo5Sym1 :: a -> a - type family Foo5Sym1 (a0123456789876543210 :: a) :: a where + type family Foo5Sym1 @a (a0123456789876543210 :: a) :: a where Foo5Sym1 a0123456789876543210 = Foo5 a0123456789876543210 type Foo4Sym0 :: forall a. (~>) a a data Foo4Sym0 :: (~>) a a @@ -167,7 +167,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo4Sym0 where suppressUnusedWarnings = snd ((,) Foo4Sym0KindInference ()) type Foo4Sym1 :: forall a. a -> a - type family Foo4Sym1 (a0123456789876543210 :: a) :: a where + type family Foo4Sym1 @a (a0123456789876543210 :: a) :: a where Foo4Sym1 a0123456789876543210 = Foo4 a0123456789876543210 type Foo3Sym0 :: (~>) a ((~>) b a) data Foo3Sym0 :: (~>) a ((~>) b a) @@ -186,7 +186,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo3Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo3Sym1KindInference ()) type Foo3Sym2 :: a -> b -> a - type family Foo3Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo3Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo3Sym2 a0123456789876543210 a0123456789876543210 = Foo3 a0123456789876543210 a0123456789876543210 type Foo2Sym0 :: (~>) a ((~>) (Maybe a) a) data Foo2Sym0 :: (~>) a ((~>) (Maybe a) a) @@ -205,7 +205,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo2Sym1KindInference ()) type Foo2Sym2 :: a -> Maybe a -> a - type family Foo2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where + type family Foo2Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where Foo2Sym2 a0123456789876543210 a0123456789876543210 = Foo2 a0123456789876543210 a0123456789876543210 type Foo1Sym0 :: (~>) a ((~>) (Maybe a) a) data Foo1Sym0 :: (~>) a ((~>) (Maybe a) a) @@ -224,22 +224,22 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo1Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo1Sym1KindInference ()) type Foo1Sym2 :: a -> Maybe a -> a - type family Foo1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where + type family Foo1Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where Foo1Sym2 a0123456789876543210 a0123456789876543210 = Foo1 a0123456789876543210 a0123456789876543210 type Foo5 :: a -> a - type family Foo5 (a :: a) :: a where + type family Foo5 @a (a :: a) :: a where Foo5 x = Case_0123456789876543210 x x type Foo4 :: forall a. a -> a - type family Foo4 (a :: a) :: a where + type family Foo4 @a (a :: a) :: a where Foo4 @a (x :: a) = Case_0123456789876543210 a x x type Foo3 :: a -> b -> a - type family Foo3 (a :: a) (a :: b) :: a where + type family Foo3 @a @b (a :: a) (a :: b) :: a where Foo3 a b = Case_0123456789876543210 a b (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a b) type Foo2 :: a -> Maybe a -> a - type family Foo2 (a :: a) (a :: Maybe a) :: a where + type family Foo2 @a (a :: a) (a :: Maybe a) :: a where Foo2 d _ = Case_0123456789876543210 d (Let0123456789876543210Scrutinee_0123456789876543210Sym1 d) type Foo1 :: a -> Maybe a -> a - type family Foo1 (a :: a) (a :: Maybe a) :: a where + type family Foo1 @a (a :: a) (a :: Maybe a) :: a where Foo1 d x = Case_0123456789876543210 d x x sFoo5 :: (forall (t :: a). Sing t -> Sing (Apply Foo5Sym0 t :: a) :: Type) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden index e2f4f777..cd3f1ce5 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Classes.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Classes.golden @@ -107,7 +107,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ConstSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ConstSym1KindInference ()) type ConstSym2 :: a -> b -> a - type family ConstSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family ConstSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where ConstSym2 a0123456789876543210 a0123456789876543210 = Const a0123456789876543210 a0123456789876543210 type FooCompare :: Foo -> Foo -> Ordering type family FooCompare (a :: Foo) (a :: Foo) :: Ordering where @@ -116,7 +116,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations FooCompare B B = GTSym0 FooCompare B A = EQSym0 type Const :: a -> b -> a - type family Const (a :: a) (a :: b) :: a where + type family Const @a @b (a :: a) (a :: b) :: a where Const x _ = x type MycompareSym0 :: forall a. (~>) a ((~>) a Ordering) data MycompareSym0 :: (~>) a ((~>) a Ordering) @@ -135,7 +135,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (MycompareSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MycompareSym1KindInference ()) type MycompareSym2 :: forall a. a -> a -> Ordering - type family MycompareSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where + type family MycompareSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where MycompareSym2 a0123456789876543210 a0123456789876543210 = Mycompare a0123456789876543210 a0123456789876543210 type (<=>@#@$) :: forall a. (~>) a ((~>) a Ordering) data (<=>@#@$) :: (~>) a ((~>) a Ordering) @@ -156,11 +156,11 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) (:<=>@#@$$###) ()) infix 4 <=>@#@$$ type (<=>@#@$$$) :: forall a. a -> a -> Ordering - type family (<=>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where + type family (<=>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where (<=>@#@$$$) a0123456789876543210 a0123456789876543210 = (<=>) a0123456789876543210 a0123456789876543210 infix 4 <=>@#@$$$ type TFHelper_0123456789876543210 :: a -> a -> Ordering - type family TFHelper_0123456789876543210 (a :: a) (a :: a) :: Ordering where + type family TFHelper_0123456789876543210 @a (a :: a) (a :: a) :: Ordering where TFHelper_0123456789876543210 a_0123456789876543210 a_0123456789876543210 = Apply (Apply MycompareSym0 a_0123456789876543210) a_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) a Ordering) data TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) a Ordering) @@ -181,7 +181,7 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: a -> a -> Ordering - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where + type family TFHelper_0123456789876543210Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 class PMyOrd a where type family Mycompare (arg :: a) (arg :: a) :: Ordering diff --git a/singletons-base/tests/compile-and-dump/Singletons/Contains.golden b/singletons-base/tests/compile-and-dump/Singletons/Contains.golden index fb891871..21ec20df 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Contains.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Contains.golden @@ -24,10 +24,10 @@ Singletons/Contains.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ContainsSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ContainsSym1KindInference ()) type ContainsSym2 :: a -> [a] -> Bool - type family ContainsSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: [a]) :: Bool where + type family ContainsSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: [a]) :: Bool where ContainsSym2 a0123456789876543210 a0123456789876543210 = Contains a0123456789876543210 a0123456789876543210 type Contains :: a -> [a] -> Bool - type family Contains (a :: a) (a :: [a]) :: Bool where + type family Contains @a (a :: a) (a :: [a]) :: Bool where Contains _ '[] = FalseSym0 Contains elt ('(:) h t) = Apply (Apply (||@#@$) (Apply (Apply (==@#@$) elt) h)) (Apply (Apply ContainsSym0 elt) t) sContains :: diff --git a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden index 10819f78..2c24a1dd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/DataValues.golden @@ -33,7 +33,7 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (PairSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) PairSym1KindInference ()) type PairSym2 :: forall a b. a -> b -> Pair a b - type family PairSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where + type family PairSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where PairSym2 a0123456789876543210 a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210 type family AListSym0 where AListSym0 = AList @@ -53,7 +53,7 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0) type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Pair a b -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210 @a @b (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 p_0123456789876543210 (Pair arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) @@ -86,7 +86,7 @@ Singletons/DataValues.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Pair a b -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a @b (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Pair a b) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/Error.golden b/singletons-base/tests/compile-and-dump/Singletons/Error.golden index b2ba3b3f..9514f886 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Error.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Error.golden @@ -16,10 +16,10 @@ Singletons/Error.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings HeadSym0 where suppressUnusedWarnings = snd ((,) HeadSym0KindInference ()) type HeadSym1 :: [a] -> a - type family HeadSym1 (a0123456789876543210 :: [a]) :: a where + type family HeadSym1 @a (a0123456789876543210 :: [a]) :: a where HeadSym1 a0123456789876543210 = Head a0123456789876543210 type Head :: [a] -> a - type family Head (a :: [a]) :: a where + type family Head @a (a :: [a]) :: a where Head ('(:) a _) = a Head '[] = Apply ErrorSym0 "head: empty list" sHead :: diff --git a/singletons-base/tests/compile-and-dump/Singletons/Fixity.golden b/singletons-base/tests/compile-and-dump/Singletons/Fixity.golden index 8af0f88e..7fb4b5d4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Fixity.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Fixity.golden @@ -34,11 +34,11 @@ Singletons/Fixity.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) (:====@#@$$###) ()) infix 4 ====@#@$$ type (====@#@$$$) :: a -> a -> a - type family (====@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where + type family (====@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (====@#@$$$) a0123456789876543210 a0123456789876543210 = (====) a0123456789876543210 a0123456789876543210 infix 4 ====@#@$$$ type (====) :: a -> a -> a - type family (====) (a :: a) (a :: a) :: a where + type family (====) @a (a :: a) (a :: a) :: a where (====) a _ = a type (<=>@#@$) :: forall a. (~>) a ((~>) a Ordering) data (<=>@#@$) :: (~>) a ((~>) a Ordering) @@ -59,7 +59,7 @@ Singletons/Fixity.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) (:<=>@#@$$###) ()) infix 4 <=>@#@$$ type (<=>@#@$$$) :: forall a. a -> a -> Ordering - type family (<=>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where + type family (<=>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where (<=>@#@$$$) a0123456789876543210 a0123456789876543210 = (<=>) a0123456789876543210 a0123456789876543210 infix 4 <=>@#@$$$ class PMyOrd a where diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden b/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden index d547d718..e6173c3f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunDeps.golden @@ -32,7 +32,7 @@ Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MethSym0 where suppressUnusedWarnings = snd ((,) MethSym0KindInference ()) type MethSym1 :: forall a. a -> a - type family MethSym1 (a0123456789876543210 :: a) :: a where + type family MethSym1 @a (a0123456789876543210 :: a) :: a where MethSym1 a0123456789876543210 = Meth a0123456789876543210 type L2rSym0 :: forall a b. (~>) a b data L2rSym0 :: (~>) a b @@ -43,7 +43,7 @@ Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings L2rSym0 where suppressUnusedWarnings = snd ((,) L2rSym0KindInference ()) type L2rSym1 :: forall a b. a -> b - type family L2rSym1 (a0123456789876543210 :: a) :: b where + type family L2rSym1 @a @b (a0123456789876543210 :: a) :: b where L2rSym1 a0123456789876543210 = L2r a0123456789876543210 class PFD a b | a -> b where type family Meth (arg :: a) :: a diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden index 66bcf471..dfa7da96 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden @@ -47,7 +47,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkT1Sym3KindInference ()) type MkT1Sym4 :: forall x a. x -> a -> Maybe a -> Maybe (Maybe a) -> T x a - type family MkT1Sym4 (a0123456789876543210 :: x) (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe (Maybe a)) :: T x a where + type family MkT1Sym4 @x @a (a0123456789876543210 :: x) (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe (Maybe a)) :: T x a where MkT1Sym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = MkT1 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type MkT2Sym0 :: forall x a. (~>) (Maybe x) (T x a) data MkT2Sym0 :: (~>) (Maybe x) (T x a) @@ -58,7 +58,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkT2Sym0 where suppressUnusedWarnings = snd ((,) MkT2Sym0KindInference ()) type MkT2Sym1 :: forall x a. Maybe x -> T x a - type family MkT2Sym1 (a0123456789876543210 :: Maybe x) :: T x a where + type family MkT2Sym1 @x @a (a0123456789876543210 :: Maybe x) :: T x a where MkT2Sym1 a0123456789876543210 = MkT2 a0123456789876543210 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 @@ -141,7 +141,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type family Lambda_0123456789876543210Sym3 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 type Fmap_0123456789876543210 :: (~>) a b -> T x a -> T x b - type family Fmap_0123456789876543210 (a :: (~>) a b) (a :: T x a) :: T x b where + type family Fmap_0123456789876543210 @a @b @x (a :: (~>) a b) (a :: T x a) :: T x b where Fmap_0123456789876543210 _f_0123456789876543210 (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply FmapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply FmapSym0 _f_0123456789876543210)) a_0123456789876543210) Fmap_0123456789876543210 _f_0123456789876543210 (MkT2 a_0123456789876543210) = Apply MkT2Sym0 (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) a_0123456789876543210) a_0123456789876543210) type Fmap_0123456789876543210Sym0 :: (~>) ((~>) a b) ((~>) (T x a) (T x b)) @@ -164,7 +164,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Fmap_0123456789876543210Sym1KindInference ()) 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 + type family Fmap_0123456789876543210Sym2 @a @b @x (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: T x a) :: T x b where Fmap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Fmap_0123456789876543210 a0123456789876543210 a0123456789876543210 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 @@ -299,7 +299,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type family Lambda_0123456789876543210Sym3 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 type TFHelper_0123456789876543210 :: a -> T x b -> T x a - type family TFHelper_0123456789876543210 (a :: a) (a :: T x b) :: T x a where + type family TFHelper_0123456789876543210 @a @x @b (a :: a) (a :: T x b) :: T x a where TFHelper_0123456789876543210 _z_0123456789876543210 (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210)) (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210)) (Apply (Apply (<$@#@$) _z_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply (<$@#@$) _z_0123456789876543210)) a_0123456789876543210) TFHelper_0123456789876543210 _z_0123456789876543210 (MkT2 a_0123456789876543210) = Apply MkT2Sym0 (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) type TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) (T x b) (T x a)) @@ -321,7 +321,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: a -> T x b -> T x a - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: T x b) :: T x a where + type family TFHelper_0123456789876543210Sym2 @a @x @b (a0123456789876543210 :: a) (a0123456789876543210 :: T x b) :: T x a where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PFunctor (T x) where type Fmap a a = Apply (Apply Fmap_0123456789876543210Sym0 a) a @@ -407,7 +407,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations type family Lambda_0123456789876543210Sym3 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 where Lambda_0123456789876543210Sym3 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n_01234567898765432100123456789876543210 type FoldMap_0123456789876543210 :: (~>) a m -> T x a -> m - type family FoldMap_0123456789876543210 (a :: (~>) a m) (a :: T x a) :: m where + type family FoldMap_0123456789876543210 @a @m @x (a :: (~>) a m) (a :: T x a) :: m where FoldMap_0123456789876543210 _f_0123456789876543210 (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) = Apply (Apply MappendSym0 (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply (Apply FoldMapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FoldMapSym0 (Apply FoldMapSym0 _f_0123456789876543210)) a_0123456789876543210))) FoldMap_0123456789876543210 _f_0123456789876543210 (MkT2 a_0123456789876543210) = Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) a_0123456789876543210) a_0123456789876543210 type FoldMap_0123456789876543210Sym0 :: (~>) ((~>) a m) ((~>) (T x a) m) @@ -429,7 +429,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) FoldMap_0123456789876543210Sym1KindInference ()) type FoldMap_0123456789876543210Sym2 :: (~>) a m -> T x a -> m - type family FoldMap_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a m) (a0123456789876543210 :: T x a) :: m where + type family FoldMap_0123456789876543210Sym2 @a @m @x (a0123456789876543210 :: (~>) a m) (a0123456789876543210 :: T x a) :: m where FoldMap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = FoldMap_0123456789876543210 a0123456789876543210 a0123456789876543210 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 @@ -765,7 +765,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations Lambda_0123456789876543210Sym5 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 = Lambda_0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 n1_01234567898765432100123456789876543210 n2_01234567898765432100123456789876543210 type Foldr_0123456789876543210 :: (~>) a ((~>) b b) -> b -> T x a -> b - type family Foldr_0123456789876543210 (a :: (~>) a ((~>) b b)) (a :: b) (a :: T x a) :: b where + type family Foldr_0123456789876543210 @a @b @x (a :: (~>) a ((~>) b b)) (a :: b) (a :: T x a) :: b where Foldr_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) = Apply (Apply (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) (Apply (Apply _f_0123456789876543210 a_0123456789876543210) (Apply (Apply (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) (Apply (Apply (Apply (Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) _z_0123456789876543210))) Foldr_0123456789876543210 _f_0123456789876543210 _z_0123456789876543210 (MkT2 a_0123456789876543210) = Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 _f_0123456789876543210) _z_0123456789876543210) a_0123456789876543210) a_0123456789876543210) _z_0123456789876543210 type Foldr_0123456789876543210Sym0 :: (~>) ((~>) a ((~>) b b)) ((~>) b ((~>) (T x a) b)) @@ -799,14 +799,14 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Foldr_0123456789876543210Sym2KindInference ()) type Foldr_0123456789876543210Sym3 :: (~>) a ((~>) b b) -> b -> T x a -> b - type family Foldr_0123456789876543210Sym3 (a0123456789876543210 :: (~>) a ((~>) b b)) (a0123456789876543210 :: b) (a0123456789876543210 :: T x a) :: b where + type family Foldr_0123456789876543210Sym3 @a @b @x (a0123456789876543210 :: (~>) a ((~>) b b)) (a0123456789876543210 :: b) (a0123456789876543210 :: T x a) :: b where Foldr_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Foldr_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PFoldable (T x) where type FoldMap a a = Apply (Apply FoldMap_0123456789876543210Sym0 a) a type Foldr a a a = Apply (Apply (Apply Foldr_0123456789876543210Sym0 a) a) a type Traverse_0123456789876543210 :: (~>) a (f b) -> T x a -> f (T x b) - type family Traverse_0123456789876543210 (a :: (~>) a (f b)) (a :: T x a) :: f (T x b) where + type family Traverse_0123456789876543210 @a @f @b @x (a :: (~>) a (f b)) (a :: T x a) :: f (T x b) where Traverse_0123456789876543210 _f_0123456789876543210 (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) = Apply (Apply (<*>@#@$) (Apply (Apply (<*>@#@$) (Apply (Apply (Apply LiftA2Sym0 MkT1Sym0) (Apply PureSym0 a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210))) (Apply (Apply TraverseSym0 _f_0123456789876543210) a_0123456789876543210))) (Apply (Apply TraverseSym0 (Apply TraverseSym0 _f_0123456789876543210)) a_0123456789876543210) Traverse_0123456789876543210 _f_0123456789876543210 (MkT2 a_0123456789876543210) = Apply (Apply FmapSym0 MkT2Sym0) (Apply PureSym0 a_0123456789876543210) type Traverse_0123456789876543210Sym0 :: (~>) ((~>) a (f b)) ((~>) (T x a) (f (T x b))) @@ -830,13 +830,13 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Traverse_0123456789876543210Sym1KindInference ()) type Traverse_0123456789876543210Sym2 :: (~>) a (f b) -> T x a -> f (T x b) - type family Traverse_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a (f b)) (a0123456789876543210 :: T x a) :: f (T x b) where + type family Traverse_0123456789876543210Sym2 @a @f @b @x (a0123456789876543210 :: (~>) a (f b)) (a0123456789876543210 :: T x a) :: f (T x b) where 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_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 + type family Fmap_0123456789876543210 @a @b (a :: (~>) a b) (a :: Empty a) :: Empty b where Fmap_0123456789876543210 _ v_0123456789876543210 = Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210 type Fmap_0123456789876543210Sym0 :: (~>) ((~>) a b) ((~>) (Empty a) (Empty b)) data Fmap_0123456789876543210Sym0 :: (~>) ((~>) a b) ((~>) (Empty a) (Empty b)) @@ -858,11 +858,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Fmap_0123456789876543210Sym1KindInference ()) type Fmap_0123456789876543210Sym2 :: (~>) a b -> Empty a -> Empty b - type family Fmap_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Empty a) :: Empty b where + type family Fmap_0123456789876543210Sym2 @a @b (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Empty a) :: Empty b where Fmap_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Fmap_0123456789876543210 a0123456789876543210 a0123456789876543210 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 + type family TFHelper_0123456789876543210 @a @b (a :: a) (a :: Empty b) :: Empty a where TFHelper_0123456789876543210 _ v_0123456789876543210 = Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) (Empty b) (Empty a)) data TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) (Empty b) (Empty a)) @@ -884,13 +884,13 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: a -> Empty b -> Empty a - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Empty b) :: Empty a where + type family TFHelper_0123456789876543210Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: Empty b) :: Empty a where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PFunctor Empty where type Fmap a a = Apply (Apply Fmap_0123456789876543210Sym0 a) a type (<$) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type FoldMap_0123456789876543210 :: (~>) a m -> Empty a -> m - type family FoldMap_0123456789876543210 (a :: (~>) a m) (a :: Empty a) :: m where + type family FoldMap_0123456789876543210 @a @m (a :: (~>) a m) (a :: Empty a) :: m where FoldMap_0123456789876543210 _ _ = MemptySym0 type FoldMap_0123456789876543210Sym0 :: (~>) ((~>) a m) ((~>) (Empty a) m) data FoldMap_0123456789876543210Sym0 :: (~>) ((~>) a m) ((~>) (Empty a) m) @@ -912,14 +912,14 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) FoldMap_0123456789876543210Sym1KindInference ()) type FoldMap_0123456789876543210Sym2 :: (~>) a m -> Empty a -> m - type family FoldMap_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a m) (a0123456789876543210 :: Empty a) :: m where + type family FoldMap_0123456789876543210Sym2 @a @m (a0123456789876543210 :: (~>) a m) (a0123456789876543210 :: Empty a) :: m where 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_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 + type family Traverse_0123456789876543210 @a @f @b (a :: (~>) a (f b)) (a :: Empty a) :: f (Empty b) where Traverse_0123456789876543210 _ v_0123456789876543210 = Apply PureSym0 (Case_0123456789876543210 v_0123456789876543210 v_0123456789876543210) type Traverse_0123456789876543210Sym0 :: (~>) ((~>) a (f b)) ((~>) (Empty a) (f (Empty b))) data Traverse_0123456789876543210Sym0 :: (~>) ((~>) a (f b)) ((~>) (Empty a) (f (Empty b))) @@ -942,7 +942,7 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Traverse_0123456789876543210Sym1KindInference ()) type Traverse_0123456789876543210Sym2 :: (~>) a (f b) -> Empty a -> f (Empty b) - type family Traverse_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a (f b)) (a0123456789876543210 :: Empty a) :: f (Empty b) where + type family Traverse_0123456789876543210Sym2 @a @f @b (a0123456789876543210 :: (~>) a (f b)) (a0123456789876543210 :: Empty a) :: f (Empty b) where Traverse_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Traverse_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PTraversable Empty where type Traverse a a = Apply (Apply Traverse_0123456789876543210Sym0 a) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden index 1ea1dfce..d6775a52 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/HigherOrder.golden @@ -49,7 +49,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings LeftSym0 where suppressUnusedWarnings = snd ((,) LeftSym0KindInference ()) type LeftSym1 :: forall a b. a -> Either a b - type family LeftSym1 (a0123456789876543210 :: a) :: Either a b where + type family LeftSym1 @a @b (a0123456789876543210 :: a) :: Either a b where LeftSym1 a0123456789876543210 = Left a0123456789876543210 type RightSym0 :: forall a b. (~>) b (Either a b) data RightSym0 :: (~>) b (Either a b) @@ -60,7 +60,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings RightSym0 where suppressUnusedWarnings = snd ((,) RightSym0KindInference ()) type RightSym1 :: forall a b. b -> Either a b - type family RightSym1 (a0123456789876543210 :: b) :: Either a b where + type family RightSym1 @a @b (a0123456789876543210 :: b) :: Either a b where RightSym1 a0123456789876543210 = Right a0123456789876543210 type family Case_0123456789876543210 n0123456789876543210 b0123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 t where Case_0123456789876543210 n b a_0123456789876543210 a_0123456789876543210 'True = Apply SuccSym0 (Apply SuccSym0 n) @@ -204,7 +204,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FooSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FooSym2KindInference ()) type FooSym3 :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> a -> b - type family FooSym3 (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: a) :: b where + type family FooSym3 @a @b (a0123456789876543210 :: (~>) ((~>) a b) ((~>) a b)) (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: a) :: b where FooSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 a0123456789876543210 type ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c])) data ZipWithSym0 :: (~>) ((~>) a ((~>) b c)) ((~>) [a] ((~>) [b] [c])) @@ -231,7 +231,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ZipWithSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ZipWithSym2KindInference ()) type ZipWithSym3 :: (~>) a ((~>) b c) -> [a] -> [b] -> [c] - type family ZipWithSym3 (a0123456789876543210 :: (~>) a ((~>) b c)) (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [c] where + type family ZipWithSym3 @a @b @c (a0123456789876543210 :: (~>) a ((~>) b c)) (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [c] where ZipWithSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ZipWith a0123456789876543210 a0123456789876543210 a0123456789876543210 type LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b)) data LiftMaybeSym0 :: (~>) ((~>) a b) ((~>) (Maybe a) (Maybe b)) @@ -250,7 +250,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (LiftMaybeSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) LiftMaybeSym1KindInference ()) type LiftMaybeSym2 :: (~>) a b -> Maybe a -> Maybe b - type family LiftMaybeSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where + type family LiftMaybeSym2 @a @b (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Maybe a) :: Maybe b where LiftMaybeSym2 a0123456789876543210 a0123456789876543210 = LiftMaybe a0123456789876543210 a0123456789876543210 type MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b]) data MapSym0 :: (~>) ((~>) a b) ((~>) [a] [b]) @@ -269,7 +269,7 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (MapSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MapSym1KindInference ()) type MapSym2 :: (~>) a b -> [a] -> [b] - type family MapSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: [a]) :: [b] where + type family MapSym2 @a @b (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: [a]) :: [b] where MapSym2 a0123456789876543210 a0123456789876543210 = Map a0123456789876543210 a0123456789876543210 type Etad :: [Nat] -> [Bool] -> [Nat] type family Etad (a :: [Nat]) (a :: [Bool]) :: [Nat] where @@ -278,20 +278,20 @@ Singletons/HigherOrder.hs:(0,0)-(0,0): Splicing declarations type family Splunge (a :: [Nat]) (a :: [Bool]) :: [Nat] where Splunge ns bs = Apply (Apply (Apply ZipWithSym0 (Apply (Apply Lambda_0123456789876543210Sym0 ns) bs)) ns) bs type Foo :: (~>) ((~>) a b) ((~>) a b) -> (~>) a b -> a -> b - type family Foo (a :: (~>) ((~>) a b) ((~>) a b)) (a :: (~>) a b) (a :: a) :: b where + type family Foo @a @b (a :: (~>) ((~>) a b) ((~>) a b)) (a :: (~>) a b) (a :: a) :: b where Foo f g a = Apply (Apply f g) a type ZipWith :: (~>) a ((~>) b c) -> [a] -> [b] -> [c] - type family ZipWith (a :: (~>) a ((~>) b c)) (a :: [a]) (a :: [b]) :: [c] where + type family ZipWith @a @b @c (a :: (~>) a ((~>) b c)) (a :: [a]) (a :: [b]) :: [c] where ZipWith f ('(:) x xs) ('(:) y ys) = Apply (Apply (:@#@$) (Apply (Apply f x) y)) (Apply (Apply (Apply ZipWithSym0 f) xs) ys) ZipWith _ '[] '[] = NilSym0 ZipWith _ ('(:) _ _) '[] = NilSym0 ZipWith _ '[] ('(:) _ _) = NilSym0 type LiftMaybe :: (~>) a b -> Maybe a -> Maybe b - type family LiftMaybe (a :: (~>) a b) (a :: Maybe a) :: Maybe b where + type family LiftMaybe @a @b (a :: (~>) a b) (a :: Maybe a) :: Maybe b where LiftMaybe f ('Just x) = Apply JustSym0 (Apply f x) LiftMaybe _ 'Nothing = NothingSym0 type Map :: (~>) a b -> [a] -> [b] - type family Map (a :: (~>) a b) (a :: [a]) :: [b] where + type family Map @a @b (a :: (~>) a b) (a :: [a]) :: [b] where Map _ '[] = NilSym0 Map f ('(:) h t) = Apply (Apply (:@#@$) (Apply f h)) (Apply (Apply MapSym0 f) t) sEtad :: diff --git a/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden b/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden index aaedca51..9a0449f5 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LambdaCase.golden @@ -130,7 +130,7 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo3Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo3Sym1KindInference ()) type Foo3Sym2 :: a -> b -> a - type family Foo3Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo3Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo3Sym2 a0123456789876543210 a0123456789876543210 = Foo3 a0123456789876543210 a0123456789876543210 type Foo2Sym0 :: (~>) a ((~>) (Maybe a) a) data Foo2Sym0 :: (~>) a ((~>) (Maybe a) a) @@ -149,7 +149,7 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo2Sym1KindInference ()) type Foo2Sym2 :: a -> Maybe a -> a - type family Foo2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where + type family Foo2Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where Foo2Sym2 a0123456789876543210 a0123456789876543210 = Foo2 a0123456789876543210 a0123456789876543210 type Foo1Sym0 :: (~>) a ((~>) (Maybe a) a) data Foo1Sym0 :: (~>) a ((~>) (Maybe a) a) @@ -168,16 +168,16 @@ Singletons/LambdaCase.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo1Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo1Sym1KindInference ()) type Foo1Sym2 :: a -> Maybe a -> a - type family Foo1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where + type family Foo1Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe a) :: a where Foo1Sym2 a0123456789876543210 a0123456789876543210 = Foo1 a0123456789876543210 a0123456789876543210 type Foo3 :: a -> b -> a - type family Foo3 (a :: a) (a :: b) :: a where + type family Foo3 @a @b (a :: a) (a :: b) :: a where Foo3 a b = Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) b) (Apply (Apply Tuple2Sym0 a) b) type Foo2 :: a -> Maybe a -> a - type family Foo2 (a :: a) (a :: Maybe a) :: a where + type family Foo2 @a (a :: a) (a :: Maybe a) :: a where Foo2 d _ = Apply (Apply Lambda_0123456789876543210Sym0 d) (Apply JustSym0 d) type Foo1 :: a -> Maybe a -> a - type family Foo1 (a :: a) (a :: Maybe a) :: a where + type family Foo1 @a (a :: a) (a :: Maybe a) :: a where Foo1 d x = Apply (Apply (Apply Lambda_0123456789876543210Sym0 d) x) x sFoo3 :: (forall (t :: a) (t :: b). diff --git a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden index ada73a02..987639c7 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Lambdas.golden @@ -57,7 +57,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FooSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FooSym1KindInference ()) type FooSym2 :: forall a b. a -> b -> Foo a b - type family FooSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Foo a b where + type family FooSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Foo a b where FooSym2 a0123456789876543210 a0123456789876543210 = Foo a0123456789876543210 a0123456789876543210 type family Case_0123456789876543210 arg_01234567898765432100123456789876543210 x0123456789876543210 t where Case_0123456789876543210 arg_0123456789876543210 x (Foo a _) = a @@ -377,7 +377,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo8Sym0 where suppressUnusedWarnings = snd ((,) Foo8Sym0KindInference ()) type Foo8Sym1 :: Foo a b -> a - type family Foo8Sym1 (a0123456789876543210 :: Foo a b) :: a where + type family Foo8Sym1 @a @b (a0123456789876543210 :: Foo a b) :: a where Foo8Sym1 a0123456789876543210 = Foo8 a0123456789876543210 type Foo7Sym0 :: (~>) a ((~>) b b) data Foo7Sym0 :: (~>) a ((~>) b b) @@ -396,7 +396,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo7Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo7Sym1KindInference ()) type Foo7Sym2 :: a -> b -> b - type family Foo7Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family Foo7Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Foo7Sym2 a0123456789876543210 a0123456789876543210 = Foo7 a0123456789876543210 a0123456789876543210 type Foo6Sym0 :: (~>) a ((~>) b a) data Foo6Sym0 :: (~>) a ((~>) b a) @@ -415,7 +415,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo6Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo6Sym1KindInference ()) type Foo6Sym2 :: a -> b -> a - type family Foo6Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo6Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo6Sym2 a0123456789876543210 a0123456789876543210 = Foo6 a0123456789876543210 a0123456789876543210 type Foo5Sym0 :: (~>) a ((~>) b b) data Foo5Sym0 :: (~>) a ((~>) b b) @@ -434,7 +434,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo5Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo5Sym1KindInference ()) type Foo5Sym2 :: a -> b -> b - type family Foo5Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family Foo5Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Foo5Sym2 a0123456789876543210 a0123456789876543210 = Foo5 a0123456789876543210 a0123456789876543210 type Foo4Sym0 :: (~>) a ((~>) b ((~>) c a)) data Foo4Sym0 :: (~>) a ((~>) b ((~>) c a)) @@ -461,7 +461,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo4Sym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo4Sym2KindInference ()) type Foo4Sym3 :: a -> b -> c -> a - type family Foo4Sym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: a where + type family Foo4Sym3 @a @b @c (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) :: a where Foo4Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = Foo4 a0123456789876543210 a0123456789876543210 a0123456789876543210 type Foo3Sym0 :: (~>) a a data Foo3Sym0 :: (~>) a a @@ -472,7 +472,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo3Sym0 where suppressUnusedWarnings = snd ((,) Foo3Sym0KindInference ()) type Foo3Sym1 :: a -> a - type family Foo3Sym1 (a0123456789876543210 :: a) :: a where + type family Foo3Sym1 @a (a0123456789876543210 :: a) :: a where Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210 type Foo2Sym0 :: (~>) a ((~>) b a) data Foo2Sym0 :: (~>) a ((~>) b a) @@ -491,7 +491,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo2Sym1KindInference ()) type Foo2Sym2 :: a -> b -> a - type family Foo2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo2Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo2Sym2 a0123456789876543210 a0123456789876543210 = Foo2 a0123456789876543210 a0123456789876543210 type Foo1Sym0 :: (~>) a ((~>) b a) data Foo1Sym0 :: (~>) a ((~>) b a) @@ -510,7 +510,7 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo1Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo1Sym1KindInference ()) type Foo1Sym2 :: a -> b -> a - type family Foo1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo1Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo1Sym2 a0123456789876543210 a0123456789876543210 = Foo1 a0123456789876543210 a0123456789876543210 type Foo0Sym0 :: (~>) a ((~>) b a) data Foo0Sym0 :: (~>) a ((~>) b a) @@ -529,34 +529,34 @@ Singletons/Lambdas.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo0Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo0Sym1KindInference ()) type Foo0Sym2 :: a -> b -> a - type family Foo0Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo0Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo0Sym2 a0123456789876543210 a0123456789876543210 = Foo0 a0123456789876543210 a0123456789876543210 type Foo8 :: Foo a b -> a - type family Foo8 (a :: Foo a b) :: a where + type family Foo8 @a @b (a :: Foo a b) :: a where Foo8 x = Apply (Apply Lambda_0123456789876543210Sym0 x) x type Foo7 :: a -> b -> b - type family Foo7 (a :: a) (a :: b) :: b where + type family Foo7 @a @b (a :: a) (a :: b) :: b where Foo7 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) (Apply (Apply Tuple2Sym0 x) y) type Foo6 :: a -> b -> a - type family Foo6 (a :: a) (a :: b) :: a where + type family Foo6 @a @b (a :: a) (a :: b) :: a where Foo6 a b = Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a) b) a) b type Foo5 :: a -> b -> b - type family Foo5 (a :: a) (a :: b) :: b where + type family Foo5 @a @b (a :: a) (a :: b) :: b where Foo5 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) y type Foo4 :: a -> b -> c -> a - type family Foo4 (a :: a) (a :: b) (a :: c) :: a where + type family Foo4 @a @b @c (a :: a) (a :: b) (a :: c) :: a where Foo4 x y z = Apply (Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) z) y) z type Foo3 :: a -> a - type family Foo3 (a :: a) :: a where + type family Foo3 @a (a :: a) :: a where Foo3 x = Apply (Apply Lambda_0123456789876543210Sym0 x) x type Foo2 :: a -> b -> a - type family Foo2 (a :: a) (a :: b) :: a where + type family Foo2 @a @b (a :: a) (a :: b) :: a where Foo2 x y = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) y type Foo1 :: a -> b -> a - type family Foo1 (a :: a) (a :: b) :: a where + type family Foo1 @a @b (a :: a) (a :: b) :: a where Foo1 x a_0123456789876543210 = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) a_0123456789876543210) a_0123456789876543210 type Foo0 :: a -> b -> a - type family Foo0 (a :: a) (a :: b) :: a where + type family Foo0 @a @b (a :: a) (a :: b) :: a where Foo0 a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210) a_0123456789876543210) a_0123456789876543210 sFoo8 :: (forall (t :: Foo a b). diff --git a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden index 2e8ac33d..2dd2d1d8 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/LetStatements.golden @@ -589,7 +589,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo13_Sym0 where suppressUnusedWarnings = snd ((,) Foo13_Sym0KindInference ()) type Foo13_Sym1 :: a -> a - type family Foo13_Sym1 (a0123456789876543210 :: a) :: a where + type family Foo13_Sym1 @a (a0123456789876543210 :: a) :: a where Foo13_Sym1 a0123456789876543210 = Foo13_ a0123456789876543210 type Foo13Sym0 :: forall a. (~>) a a data Foo13Sym0 :: (~>) a a @@ -600,7 +600,7 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo13Sym0 where suppressUnusedWarnings = snd ((,) Foo13Sym0KindInference ()) type Foo13Sym1 :: forall a. a -> a - type family Foo13Sym1 (a0123456789876543210 :: a) :: a where + type family Foo13Sym1 @a (a0123456789876543210 :: a) :: a where Foo13Sym1 a0123456789876543210 = Foo13 a0123456789876543210 type Foo12Sym0 :: (~>) Nat Nat data Foo12Sym0 :: (~>) Nat Nat @@ -730,10 +730,10 @@ Singletons/LetStatements.hs:(0,0)-(0,0): Splicing declarations type family Foo14 (a :: Nat) :: (Nat, Nat) where Foo14 x = Apply (Apply Tuple2Sym0 (Let0123456789876543210ZSym1 x)) (Let0123456789876543210YSym1 x) type Foo13_ :: a -> a - type family Foo13_ (a :: a) :: a where + type family Foo13_ @a (a :: a) :: a where Foo13_ y = y type Foo13 :: forall a. a -> a - type family Foo13 (a :: a) :: a where + type family Foo13 @a (a :: a) :: a where Foo13 @a (x :: a) = Apply Foo13_Sym0 (Let0123456789876543210BarSym2 a x) type Foo12 :: Nat -> Nat type family Foo12 (a :: Nat) :: Nat where diff --git a/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden b/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden index 301ed2ba..2a9a04c4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Maybe.golden @@ -8,7 +8,7 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations = Nothing | Just a deriving (Eq, Show) type NothingSym0 :: forall a. Maybe a - type family NothingSym0 :: Maybe a where + type family NothingSym0 @a :: Maybe a where NothingSym0 = Nothing type JustSym0 :: forall a. (~>) a (Maybe a) data JustSym0 :: (~>) a (Maybe a) @@ -19,10 +19,10 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings JustSym0 where suppressUnusedWarnings = snd ((,) JustSym0KindInference ()) type JustSym1 :: forall a. a -> Maybe a - type family JustSym1 (a0123456789876543210 :: a) :: Maybe a where + type family JustSym1 @a (a0123456789876543210 :: a) :: Maybe a where JustSym1 a0123456789876543210 = Just a0123456789876543210 type TFHelper_0123456789876543210 :: Maybe a -> Maybe a -> Bool - type family TFHelper_0123456789876543210 (a :: Maybe a) (a :: Maybe a) :: Bool where + type family TFHelper_0123456789876543210 @a (a :: Maybe a) (a :: Maybe a) :: Bool where TFHelper_0123456789876543210 Nothing Nothing = TrueSym0 TFHelper_0123456789876543210 Nothing (Just _) = FalseSym0 TFHelper_0123456789876543210 (Just _) Nothing = FalseSym0 @@ -47,13 +47,13 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Maybe a -> Maybe a -> Bool - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe a) :: Bool where + type family TFHelper_0123456789876543210Sym2 @a (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe a) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (Maybe a) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Maybe a -> GHC.Types.Symbol -> GHC.Types.Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Maybe a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where + type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: Maybe a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210 _ Nothing a_0123456789876543210 = Apply (Apply ShowStringSym0 "Nothing") a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (Just arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Just ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Maybe a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) @@ -87,7 +87,7 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Maybe a -> GHC.Types.Symbol -> GHC.Types.Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Maybe a) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a @@ -169,12 +169,14 @@ Singletons/Maybe.hs:(0,0)-(0,0): Splicing declarations instance Eq (SMaybe (z :: Maybe a)) where (==) _ _ = True instance SDecide a => - Data.Type.Equality.TestEquality (SMaybe :: Maybe a -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SMaybe :: Maybe a + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => - Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SMaybe :: Maybe a + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Data.Singletons.ShowSing.ShowSing a => Show (SMaybe (z :: Maybe a)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Nat.golden b/singletons-base/tests/compile-and-dump/Singletons/Nat.golden index c296d2fa..6380764d 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Nat.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Nat.golden @@ -304,12 +304,14 @@ Singletons/Nat.hs:(0,0)-(0,0): Splicing declarations instance Eq (SNat (z :: Nat)) where (==) _ _ = True instance SDecide Nat => - Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => - Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SNat (z :: Nat)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden index 623fd8ba..2abd0838 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/OrdDeriving.golden @@ -75,7 +75,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ASym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ASym3KindInference ()) type ASym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d - type family ASym4 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where + type family ASym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where ASym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = A a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type BSym0 :: forall a b @@ -115,7 +115,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (BSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BSym3KindInference ()) type BSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d - type family BSym4 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where + type family BSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where BSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = B a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type CSym0 :: forall a b @@ -155,7 +155,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (CSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) CSym3KindInference ()) type CSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d - type family CSym4 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where + type family CSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where CSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = C a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type DSym0 :: forall a b @@ -195,7 +195,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (DSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) DSym3KindInference ()) type DSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d - type family DSym4 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where + type family DSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where DSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = D a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type ESym0 :: forall a b @@ -235,7 +235,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ESym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ESym3KindInference ()) type ESym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d - type family ESym4 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where + type family ESym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where ESym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = E a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type FSym0 :: forall a b @@ -275,7 +275,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FSym3KindInference ()) type FSym4 :: forall a b c d. a -> b -> c -> d -> Foo a b c d - type family FSym4 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where + type family FSym4 @a @b @c @d (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: c) (a0123456789876543210 :: d) :: Foo a b c d where FSym4 a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 = F a0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 type TFHelper_0123456789876543210 :: Nat -> Nat -> Bool type family TFHelper_0123456789876543210 (a :: Nat) (a :: Nat) :: Bool where @@ -337,7 +337,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type TFHelper_0123456789876543210 :: Foo a b c d -> Foo a b c d -> Bool - type family TFHelper_0123456789876543210 (a :: Foo a b c d) (a :: Foo a b c d) :: Bool where + type family TFHelper_0123456789876543210 @a @b @c @d (a :: Foo a b c d) (a :: Foo a b c d) :: Bool where TFHelper_0123456789876543210 (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210))) TFHelper_0123456789876543210 (A _ _ _ _) (B _ _ _ _) = FalseSym0 TFHelper_0123456789876543210 (A _ _ _ _) (C _ _ _ _) = FalseSym0 @@ -395,13 +395,13 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Foo a b c d -> Foo a b c d -> Bool - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Foo a b c d) (a0123456789876543210 :: Foo a b c d) :: Bool where + type family TFHelper_0123456789876543210Sym2 @a @b @c @d (a0123456789876543210 :: Foo a b c d) (a0123456789876543210 :: Foo a b c d) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (Foo a b c d) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Foo a b c d -> Foo a b c d -> Ordering - type family Compare_0123456789876543210 (a :: Foo a b c d) (a :: Foo a b c d) :: Ordering where + type family Compare_0123456789876543210 @a @b @c @d (a :: Foo a b c d) (a :: Foo a b c d) :: Ordering where Compare_0123456789876543210 (A a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (A b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (B a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (B b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) Compare_0123456789876543210 (C a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) (C b_0123456789876543210 b_0123456789876543210 b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)))) @@ -459,7 +459,7 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Compare_0123456789876543210Sym1KindInference ()) type Compare_0123456789876543210Sym2 :: Foo a b c d -> Foo a b c d -> Ordering - type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Foo a b c d) (a0123456789876543210 :: Foo a b c d) :: Ordering where + type family Compare_0123456789876543210Sym2 @a @b @c @d (a0123456789876543210 :: Foo a b c d) (a0123456789876543210 :: Foo a b c d) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd (Foo a b c d) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a @@ -1119,12 +1119,14 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance Eq (SNat (z :: Nat)) where (==) _ _ = True instance SDecide Nat => - Data.Type.Equality.TestEquality (SNat :: Nat -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SNat :: Nat + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide Nat => - Data.Type.Coercion.TestCoercion (SNat :: Nat -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SNat :: Nat + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance (SDecide a, SDecide b, SDecide c, SDecide d) => SDecide (Foo a b c d) where @@ -1233,12 +1235,14 @@ Singletons/OrdDeriving.hs:(0,0)-(0,0): Splicing declarations instance Eq (SFoo (z :: Foo a b c d)) where (==) _ _ = True instance (SDecide a, SDecide b, SDecide c, SDecide d) => - Data.Type.Equality.TestEquality (SFoo :: Foo a b c d -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SFoo :: Foo a b c d + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance (SDecide a, SDecide b, SDecide c, SDecide d) => - Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SFoo :: Foo a b c d + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SNat (z :: Nat)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden index 859b86f9..d602065c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden @@ -33,7 +33,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (PairSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) PairSym1KindInference ()) type PairSym2 :: forall a b. a -> b -> Pair a b - type family PairSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where + type family PairSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where PairSym2 a0123456789876543210 a0123456789876543210 = Pair a0123456789876543210 a0123456789876543210 type family AListSym0 where AListSym0 = AList @@ -53,7 +53,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations Pr = Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) (Apply (Apply (:@#@$) ZeroSym0) NilSym0) type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Pair a b -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210 @a @b (a :: GHC.Num.Natural.Natural) (a :: Pair a b) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 p_0123456789876543210 (Pair arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Pair ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Pair a b) ((~>) Symbol Symbol)) @@ -86,7 +86,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Pair a b -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a @b (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Pair a b) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Pair a b) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a @@ -368,18 +368,18 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings SillySym0 where suppressUnusedWarnings = snd ((,) SillySym0KindInference ()) type SillySym1 :: a -> () - type family SillySym1 (a0123456789876543210 :: a) :: () where + type family SillySym1 @a (a0123456789876543210 :: a) :: () where SillySym1 a0123456789876543210 = Silly a0123456789876543210 - type Foo2Sym0 :: (~>) (a, b) a - data Foo2Sym0 :: (~>) (a, b) a + type Foo2Sym0 :: (~>) ((#,#) a b) a + data Foo2Sym0 :: (~>) ((#,#) a b) a where Foo2Sym0KindInference :: SameKind (Apply Foo2Sym0 arg) (Foo2Sym1 arg) => Foo2Sym0 a0123456789876543210 type instance Apply Foo2Sym0 a0123456789876543210 = Foo2 a0123456789876543210 instance SuppressUnusedWarnings Foo2Sym0 where suppressUnusedWarnings = snd ((,) Foo2Sym0KindInference ()) - type Foo2Sym1 :: (a, b) -> a - type family Foo2Sym1 (a0123456789876543210 :: (a, b)) :: a where + type Foo2Sym1 :: (#,#) a b -> a + type family Foo2Sym1 @a @b (a0123456789876543210 :: (#,#) a b) :: a where Foo2Sym1 a0123456789876543210 = Foo2 a0123456789876543210 type Foo1Sym0 :: (~>) (a, b) a data Foo1Sym0 :: (~>) (a, b) a @@ -390,7 +390,8 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo1Sym0 where suppressUnusedWarnings = snd ((,) Foo1Sym0KindInference ()) type Foo1Sym1 :: (a, b) -> a - type family Foo1Sym1 (a0123456789876543210 :: (a, b)) :: a where + type family Foo1Sym1 @a @b (a0123456789876543210 :: (a, + b)) :: a where Foo1Sym1 a0123456789876543210 = Foo1 a0123456789876543210 type family BlimySym0 where BlimySym0 = Blimy @@ -423,14 +424,14 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations type family X_0123456789876543210Sym0 where X_0123456789876543210Sym0 = X_0123456789876543210 type Silly :: a -> () - type family Silly (a :: a) :: () where + type family Silly @a (a :: a) :: () where Silly x = Case_0123456789876543210 x x - type Foo2 :: (a, b) -> a - type family Foo2 (a :: (a, b)) :: a where + type Foo2 :: (#,#) a b -> a + type family Foo2 @a @b (a :: (#,#) a b) :: a where Foo2 '(x, y) = Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y) type Foo1 :: (a, b) -> a - type family Foo1 (a :: (a, b)) :: a where + type family Foo1 @a @b (a :: (a, b)) :: a where Foo1 '(x, y) = Apply (Apply (Apply Lambda_0123456789876543210Sym0 x) y) y type family Blimy where @@ -466,7 +467,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations sSilly :: (forall (t :: a). Sing t -> Sing (Apply SillySym0 t :: ()) :: Type) sFoo2 :: - (forall (t :: (a, b)). + (forall (t :: (#,#) a b). Sing t -> Sing (Apply Foo2Sym0 t :: a) :: Type) sFoo1 :: (forall (t :: (a, b)). @@ -594,7 +595,24 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations sX_0123456789876543210 = sPr instance SingI (SillySym0 :: (~>) a ()) where sing = singFun1 @SillySym0 sSilly - instance SingI (Foo2Sym0 :: (~>) (a, b) a) where + instance SingI (Foo2Sym0 :: (~>) ((#,#) a b) a) where sing = singFun1 @Foo2Sym0 sFoo2 instance SingI (Foo1Sym0 :: (~>) (a, b) a) where sing = singFun1 @Foo1Sym0 sFoo1 +Singletons/PatternMatching.hs:0:0: error: [GHC-83865] + • Couldn't match a lifted type with an unlifted type + Expected kind ‘Type’, + but ‘(#,#) a b’ has kind ‘TYPE + (GHC.Types.TupleRep + ((:) + @GHC.Types.RuntimeRep + GHC.Types.LiftedRep + ((:) + @GHC.Types.RuntimeRep + GHC.Types.LiftedRep + ('[] @GHC.Types.RuntimeRep))))’ + • In a standalone kind signature for ‘Foo2’: (#,#) a b -> a + | +19 | $(singletons [d| + | ^^^^^^^^^^^^^^^... + diff --git a/singletons-base/tests/compile-and-dump/Singletons/PolyKinds.golden b/singletons-base/tests/compile-and-dump/Singletons/PolyKinds.golden index 8b2123cf..b0ace7b4 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PolyKinds.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PolyKinds.golden @@ -14,7 +14,7 @@ Singletons/PolyKinds.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FffSym0 where suppressUnusedWarnings = snd ((,) FffSym0KindInference ()) type FffSym1 :: forall k (a :: k). Proxy (a :: k) -> () - type family FffSym1 (a0123456789876543210 :: Proxy (a :: k)) :: () where + type family FffSym1 @k @(a :: k) (a0123456789876543210 :: Proxy (a :: k)) :: () where FffSym1 a0123456789876543210 = Fff a0123456789876543210 class PCls (a :: k) where type family Fff (arg :: Proxy (a :: k)) :: () diff --git a/singletons-base/tests/compile-and-dump/Singletons/PolyKindsApp.golden b/singletons-base/tests/compile-and-dump/Singletons/PolyKindsApp.golden index 3ffcbbe9..0be0542f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PolyKindsApp.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PolyKindsApp.golden @@ -7,7 +7,8 @@ Singletons/PolyKindsApp.hs:(0,0)-(0,0): Splicing declarations fff :: (a :: k -> Type) (b :: k) type FffSym0 :: forall k (a :: k -> Type) (b :: k). (a :: k -> Type) (b :: k) - type family FffSym0 :: (a :: k -> Type) (b :: k) where + type family FffSym0 @k @(a :: k -> Type) @(b :: k) :: (a :: k + -> Type) (b :: k) where FffSym0 = Fff class PCls (a :: k -> Type) where type family Fff :: (a :: k -> Type) (b :: k) diff --git a/singletons-base/tests/compile-and-dump/Singletons/Records.golden b/singletons-base/tests/compile-and-dump/Singletons/Records.golden index 757c3ca1..cddbbfb9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Records.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Records.golden @@ -20,7 +20,7 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (MkRecordSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MkRecordSym1KindInference ()) type MkRecordSym2 :: forall a. a -> Bool -> Record a - type family MkRecordSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Bool) :: Record a where + type family MkRecordSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Bool) :: Record a where MkRecordSym2 a0123456789876543210 a0123456789876543210 = MkRecord a0123456789876543210 a0123456789876543210 type Field2Sym0 :: forall a. (~>) (Record a) Bool data Field2Sym0 :: (~>) (Record a) Bool @@ -31,7 +31,7 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Field2Sym0 where suppressUnusedWarnings = snd ((,) Field2Sym0KindInference ()) type Field2Sym1 :: forall a. Record a -> Bool - type family Field2Sym1 (a0123456789876543210 :: Record a) :: Bool where + type family Field2Sym1 @a (a0123456789876543210 :: Record a) :: Bool where Field2Sym1 a0123456789876543210 = Field2 a0123456789876543210 type Field1Sym0 :: forall a. (~>) (Record a) a data Field1Sym0 :: (~>) (Record a) a @@ -42,13 +42,13 @@ Singletons/Records.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Field1Sym0 where suppressUnusedWarnings = snd ((,) Field1Sym0KindInference ()) type Field1Sym1 :: forall a. Record a -> a - type family Field1Sym1 (a0123456789876543210 :: Record a) :: a where + type family Field1Sym1 @a (a0123456789876543210 :: Record a) :: a where Field1Sym1 a0123456789876543210 = Field1 a0123456789876543210 type Field2 :: forall a. Record a -> Bool - type family Field2 (a :: Record a) :: Bool where + type family Field2 @a (a :: Record a) :: Bool where Field2 @a (MkRecord _ field :: Record a) = field type Field1 :: forall a. Record a -> a - type family Field1 (a :: Record a) :: a where + type family Field1 @a (a :: Record a) :: a where Field1 @a (MkRecord field _ :: Record a) = field sField2 :: forall a (t :: Record a). Sing t diff --git a/singletons-base/tests/compile-and-dump/Singletons/ReturnFunc.golden b/singletons-base/tests/compile-and-dump/Singletons/ReturnFunc.golden index 143b10b4..538618ab 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/ReturnFunc.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/ReturnFunc.golden @@ -30,7 +30,7 @@ Singletons/ReturnFunc.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (IdFooSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) IdFooSym1KindInference ()) type IdFooSym2 :: c -> a -> a - type family IdFooSym2 (a0123456789876543210 :: c) (a0123456789876543210 :: a) :: a where + type family IdFooSym2 @c @a (a0123456789876543210 :: c) (a0123456789876543210 :: a) :: a where IdFooSym2 a0123456789876543210 a0123456789876543210 = IdFoo a0123456789876543210 a0123456789876543210 type IdSym0 :: (~>) a a data IdSym0 :: (~>) a a @@ -41,7 +41,7 @@ Singletons/ReturnFunc.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings IdSym0 where suppressUnusedWarnings = snd ((,) IdSym0KindInference ()) type IdSym1 :: a -> a - type family IdSym1 (a0123456789876543210 :: a) :: a where + type family IdSym1 @a (a0123456789876543210 :: a) :: a where IdSym1 a0123456789876543210 = Id a0123456789876543210 type ReturnFuncSym0 :: (~>) Nat ((~>) Nat Nat) data ReturnFuncSym0 :: (~>) Nat ((~>) Nat Nat) @@ -63,10 +63,10 @@ Singletons/ReturnFunc.hs:(0,0)-(0,0): Splicing declarations type family ReturnFuncSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Nat where ReturnFuncSym2 a0123456789876543210 a0123456789876543210 = ReturnFunc a0123456789876543210 a0123456789876543210 type IdFoo :: c -> a -> a - type family IdFoo (a :: c) (a :: a) :: a where + type family IdFoo @c @a (a :: c) (a :: a) :: a where IdFoo _ a_0123456789876543210 = Apply IdSym0 a_0123456789876543210 type Id :: a -> a - type family Id (a :: a) :: a where + type family Id @a (a :: a) :: a where Id x = x type ReturnFunc :: Nat -> Nat -> Nat type family ReturnFunc (a :: Nat) (a :: Nat) :: Nat where diff --git a/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden index 607fa0e6..8c855cb8 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/ShowDeriving.golden @@ -44,7 +44,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (MkFoo2aSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MkFoo2aSym1KindInference ()) type MkFoo2aSym2 :: forall a. a -> a -> Foo2 a - type family MkFoo2aSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where + type family MkFoo2aSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where MkFoo2aSym2 a0123456789876543210 a0123456789876543210 = MkFoo2a a0123456789876543210 a0123456789876543210 type MkFoo2bSym0 :: forall a. (~>) a ((~>) a (Foo2 a)) data MkFoo2bSym0 :: (~>) a ((~>) a (Foo2 a)) @@ -65,7 +65,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkFoo2bSym1KindInference ()) infixl 5 `MkFoo2bSym1` type MkFoo2bSym2 :: forall a. a -> a -> Foo2 a - type family MkFoo2bSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where + type family MkFoo2bSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where MkFoo2bSym2 a0123456789876543210 a0123456789876543210 = MkFoo2b a0123456789876543210 a0123456789876543210 infixl 5 `MkFoo2bSym2` type (:*:@#@$) :: forall a. (~>) a ((~>) a (Foo2 a)) @@ -87,7 +87,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) (::*:@#@$$###) ()) infixl 5 :*:@#@$$ type (:*:@#@$$$) :: forall a. a -> a -> Foo2 a - type family (:*:@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where + type family (:*:@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where (:*:@#@$$$) a0123456789876543210 a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210 infixl 5 :*:@#@$$$ type (:&:@#@$) :: forall a. (~>) a ((~>) a (Foo2 a)) @@ -109,7 +109,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) (::&:@#@$$###) ()) infixl 5 :&:@#@$$ type (:&:@#@$$$) :: forall a. a -> a -> Foo2 a - type family (:&:@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where + type family (:&:@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Foo2 a where (:&:@#@$$$) a0123456789876543210 a0123456789876543210 = (:&:) a0123456789876543210 a0123456789876543210 infixl 5 :&:@#@$$$ type MkFoo3Sym0 :: (~>) Bool ((~>) Bool Foo3) @@ -200,7 +200,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Foo2 a -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Foo2 a) (a :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: Foo2 a) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 p_0123456789876543210 (MkFoo2a arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "MkFoo2a ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (MkFoo2b argL_0123456789876543210 argR_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 5))) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 6)) argL_0123456789876543210)) (Apply (Apply (.@#@$) (Apply ShowStringSym0 " `MkFoo2b` ")) (Apply (Apply ShowsPrecSym0 (FromInteger 6)) argR_0123456789876543210)))) a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 ((:*:) arg_0123456789876543210 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "(:*:) ")) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210)) (Apply (Apply (.@#@$) ShowSpaceSym0) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))))) a_0123456789876543210 @@ -236,7 +236,7 @@ Singletons/ShowDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Foo2 a -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Foo2 a) (a0123456789876543210 :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Foo2 a) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Foo2 a) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden index 08799f53..a9867bef 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/StandaloneDeriving.golden @@ -44,7 +44,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) (::*:@#@$$###) ()) infixl 6 :*:@#@$$ type (:*:@#@$$$) :: forall a b. a -> b -> T a b - type family (:*:@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: T a b where + type family (:*:@#@$$$) @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: T a b where (:*:@#@$$$) a0123456789876543210 a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210 infixl 6 :*:@#@$$$ type S1Sym0 :: S @@ -54,7 +54,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations type family S2Sym0 :: S where S2Sym0 = S2 type TFHelper_0123456789876543210 :: T a () -> T a () -> Bool - type family TFHelper_0123456789876543210 (a :: T a ()) (a :: T a ()) :: Bool where + type family TFHelper_0123456789876543210 @a (a :: T a ()) (a :: T a ()) :: Bool where TFHelper_0123456789876543210 ((:*:) a_0123456789876543210 a_0123456789876543210) ((:*:) b_0123456789876543210 b_0123456789876543210) = Apply (Apply (&&@#@$) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210) type TFHelper_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Bool) data TFHelper_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Bool) @@ -76,12 +76,12 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: T a () -> T a () -> Bool - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: T a ()) (a0123456789876543210 :: T a ()) :: Bool where + type family TFHelper_0123456789876543210Sym2 @a (a0123456789876543210 :: T a ()) (a0123456789876543210 :: T a ()) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (T a ()) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: T a () -> T a () -> Ordering - type family Compare_0123456789876543210 (a :: T a ()) (a :: T a ()) :: Ordering where + type family Compare_0123456789876543210 @a (a :: T a ()) (a :: T a ()) :: Ordering where Compare_0123456789876543210 ((:*:) a_0123456789876543210 a_0123456789876543210) ((:*:) b_0123456789876543210 b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0)) type Compare_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Ordering) data Compare_0123456789876543210Sym0 :: (~>) (T a ()) ((~>) (T a ()) Ordering) @@ -104,13 +104,13 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Compare_0123456789876543210Sym1KindInference ()) type Compare_0123456789876543210Sym2 :: T a () -> T a () -> Ordering - type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: T a ()) (a0123456789876543210 :: T a ()) :: Ordering where + type family Compare_0123456789876543210Sym2 @a (a0123456789876543210 :: T a ()) (a0123456789876543210 :: T a ()) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd (T a ()) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> T a () -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: T a ()) (a :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: T a ()) (a :: Symbol) :: Symbol where ShowsPrec_0123456789876543210 p_0123456789876543210 ((:*:) argL_0123456789876543210 argR_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 6))) (Apply (Apply (.@#@$) (Apply (Apply ShowsPrecSym0 (FromInteger 7)) argL_0123456789876543210)) (Apply (Apply (.@#@$) (Apply ShowStringSym0 " :*: ")) (Apply (Apply ShowsPrecSym0 (FromInteger 7)) argR_0123456789876543210)))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol)) data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (T a ()) ((~>) Symbol Symbol)) @@ -143,7 +143,7 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> T a () -> Symbol -> Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: T a ()) (a0123456789876543210 :: Symbol) :: Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: T a ()) (a0123456789876543210 :: Symbol) :: Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (T a ()) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a @@ -513,12 +513,14 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations instance Eq (ST (z :: T a ())) where (==) _ _ = True instance SDecide a => - Data.Type.Equality.TestEquality (ST :: T a () -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (ST :: T a () + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => - Data.Type.Coercion.TestCoercion (ST :: T a () -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (ST :: T a () + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance SDecide S where (%~) SS1 SS1 = Proved Refl @@ -527,11 +529,13 @@ Singletons/StandaloneDeriving.hs:(0,0)-(0,0): Splicing declarations (%~) SS2 SS2 = Proved Refl instance Eq (SS (z :: S)) where (==) _ _ = True - instance Data.Type.Equality.TestEquality (SS :: S -> Type) where - Data.Type.Equality.testEquality + instance GHC.Internal.Data.Type.Equality.TestEquality (SS :: S + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (SS :: S -> Type) where - Data.Type.Coercion.testCoercion + instance GHC.Internal.Data.Type.Coercion.TestCoercion (SS :: S + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (ST (z :: T a ())) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/Star.golden b/singletons-base/tests/compile-and-dump/Singletons/Star.golden index 8ce9824e..683eb463 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/Star.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/Star.golden @@ -257,11 +257,13 @@ Singletons/Star.hs:0:0:: Splicing declarations instance Eq (SRep (z :: Type)) where (==) _ _ = True instance (SDecide Type, SDecide Nat) => - Data.Type.Equality.TestEquality (SRep :: Type -> Type) where - Data.Type.Equality.testEquality = decideEquality + GHC.Internal.Data.Type.Equality.TestEquality (SRep :: Type + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = decideEquality instance (SDecide Type, SDecide Nat) => - Data.Type.Coercion.TestCoercion (SRep :: Type -> Type) where - Data.Type.Coercion.testCoercion = decideCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SRep :: Type + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = decideCoercion instance (SEq Type, SEq Nat) => SEq Type where (%==) :: forall (t1 :: Type) (t2 :: Type). Sing t1 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T136b.golden b/singletons-base/tests/compile-and-dump/Singletons/T136b.golden index 5c54728f..2985b700 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T136b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T136b.golden @@ -14,7 +14,7 @@ Singletons/T136b.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MethSym0 where suppressUnusedWarnings = snd ((,) MethSym0KindInference ()) type MethSym1 :: forall a. a -> a - type family MethSym1 (a0123456789876543210 :: a) :: a where + type family MethSym1 @a (a0123456789876543210 :: a) :: a where MethSym1 a0123456789876543210 = Meth a0123456789876543210 class PC a where type family Meth (arg :: a) :: a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T145.golden b/singletons-base/tests/compile-and-dump/Singletons/T145.golden index 84a3c687..e54515d7 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T145.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T145.golden @@ -22,7 +22,7 @@ Singletons/T145.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ColSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ColSym1KindInference ()) type ColSym2 :: forall f a. f a -> a -> Bool - type family ColSym2 (a0123456789876543210 :: f a) (a0123456789876543210 :: a) :: Bool where + type family ColSym2 @f @a (a0123456789876543210 :: f a) (a0123456789876543210 :: a) :: Bool where ColSym2 a0123456789876543210 a0123456789876543210 = Col a0123456789876543210 a0123456789876543210 class PColumn (f :: Type -> Type) where type family Col (arg :: f a) (arg :: a) :: Bool diff --git a/singletons-base/tests/compile-and-dump/Singletons/T150.golden b/singletons-base/tests/compile-and-dump/Singletons/T150.golden index 9a1156fd..7da2cf48 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T150.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T150.golden @@ -71,7 +71,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations HCons :: x -> (HList xs) -> HList ('(:) x xs) data Obj :: Type where Obj :: a -> Obj type FZSym0 :: Fin ('Succ n) - type family FZSym0 :: Fin ('Succ n) where + type family FZSym0 @n :: Fin ('Succ n) where FZSym0 = FZ type FSSym0 :: (~>) (Fin n) (Fin ('Succ n)) data FSSym0 :: (~>) (Fin n) (Fin ('Succ n)) @@ -82,7 +82,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FSSym0 where suppressUnusedWarnings = snd ((,) FSSym0KindInference ()) type FSSym1 :: Fin n -> Fin ('Succ n) - type family FSSym1 (a0123456789876543210 :: Fin n) :: Fin ('Succ n) where + type family FSSym1 @n (a0123456789876543210 :: Fin n) :: Fin ('Succ n) where FSSym1 a0123456789876543210 = FS a0123456789876543210 type MkFoo1Sym0 :: Foo Bool type family MkFoo1Sym0 :: Foo Bool where @@ -91,7 +91,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations type family MkFoo2Sym0 :: Foo Ordering where MkFoo2Sym0 = MkFoo2 type VNilSym0 :: Vec 'Zero a - type family VNilSym0 :: Vec 'Zero a where + type family VNilSym0 @a :: Vec 'Zero a where VNilSym0 = VNil type VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a)) data VConsSym0 :: (~>) a ((~>) (Vec n a) (Vec ('Succ n) a)) @@ -110,10 +110,10 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (VConsSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) VConsSym1KindInference ()) type VConsSym2 :: a -> Vec n a -> Vec ('Succ n) a - type family VConsSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Vec n a) :: Vec ('Succ n) a where + type family VConsSym2 @a @n (a0123456789876543210 :: a) (a0123456789876543210 :: Vec n a) :: Vec ('Succ n) a where VConsSym2 a0123456789876543210 a0123456789876543210 = VCons a0123456789876543210 a0123456789876543210 type ReflexiveSym0 :: Equal a a - type family ReflexiveSym0 :: Equal a a where + type family ReflexiveSym0 @a :: Equal a a where ReflexiveSym0 = Reflexive type HNilSym0 :: HList '[] type family HNilSym0 :: HList '[] where @@ -135,7 +135,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (HConsSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) HConsSym1KindInference ()) type HConsSym2 :: x -> HList xs -> HList ('(:) x xs) - type family HConsSym2 (a0123456789876543210 :: x) (a0123456789876543210 :: HList xs) :: HList ('(:) x xs) where + type family HConsSym2 @x @xs (a0123456789876543210 :: x) (a0123456789876543210 :: HList xs) :: HList ('(:) x xs) where HConsSym2 a0123456789876543210 a0123456789876543210 = HCons a0123456789876543210 a0123456789876543210 type ObjSym0 :: (~>) a Obj data ObjSym0 :: (~>) a Obj @@ -146,7 +146,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ObjSym0 where suppressUnusedWarnings = snd ((,) ObjSym0KindInference ()) type ObjSym1 :: a -> Obj - type family ObjSym1 (a0123456789876543210 :: a) :: Obj where + type family ObjSym1 @a (a0123456789876543210 :: a) :: Obj where ObjSym1 a0123456789876543210 = Obj a0123456789876543210 type family Case_0123456789876543210 n0123456789876543210 t where type TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c)) @@ -166,7 +166,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (TransitivitySym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) TransitivitySym1KindInference ()) type TransitivitySym2 :: Equal a b -> Equal b c -> Equal a c - type family TransitivitySym2 (a0123456789876543210 :: Equal a b) (a0123456789876543210 :: Equal b c) :: Equal a c where + type family TransitivitySym2 @a @b @c (a0123456789876543210 :: Equal a b) (a0123456789876543210 :: Equal b c) :: Equal a c where TransitivitySym2 a0123456789876543210 a0123456789876543210 = Transitivity a0123456789876543210 a0123456789876543210 type SymmetrySym0 :: (~>) (Equal a b) (Equal b a) data SymmetrySym0 :: (~>) (Equal a b) (Equal b a) @@ -177,7 +177,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings SymmetrySym0 where suppressUnusedWarnings = snd ((,) SymmetrySym0KindInference ()) type SymmetrySym1 :: Equal a b -> Equal b a - type family SymmetrySym1 (a0123456789876543210 :: Equal a b) :: Equal b a where + type family SymmetrySym1 @a @b (a0123456789876543210 :: Equal a b) :: Equal b a where SymmetrySym1 a0123456789876543210 = Symmetry a0123456789876543210 type MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b)) data MapVecSym0 :: (~>) ((~>) a b) ((~>) (Vec n a) (Vec n b)) @@ -196,7 +196,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (MapVecSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MapVecSym1KindInference ()) type MapVecSym2 :: (~>) a b -> Vec n a -> Vec n b - type family MapVecSym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Vec n a) :: Vec n b where + type family MapVecSym2 @a @b @n (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: Vec n a) :: Vec n b where MapVecSym2 a0123456789876543210 a0123456789876543210 = MapVec a0123456789876543210 a0123456789876543210 type (!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a) data (!@#@$) :: (~>) (Vec n a) ((~>) (Fin n) a) @@ -215,7 +215,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((!@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:!@#@$$###) ()) type (!@#@$$$) :: Vec n a -> Fin n -> a - type family (!@#@$$$) (a0123456789876543210 :: Vec n a) (a0123456789876543210 :: Fin n) :: a where + type family (!@#@$$$) @n @a (a0123456789876543210 :: Vec n a) (a0123456789876543210 :: Fin n) :: a where (!@#@$$$) a0123456789876543210 a0123456789876543210 = (!) a0123456789876543210 a0123456789876543210 type TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a) data TailVecSym0 :: (~>) (Vec ('Succ n) a) (Vec n a) @@ -226,7 +226,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings TailVecSym0 where suppressUnusedWarnings = snd ((,) TailVecSym0KindInference ()) type TailVecSym1 :: Vec ('Succ n) a -> Vec n a - type family TailVecSym1 (a0123456789876543210 :: Vec ('Succ n) a) :: Vec n a where + type family TailVecSym1 @n @a (a0123456789876543210 :: Vec ('Succ n) a) :: Vec n a where TailVecSym1 a0123456789876543210 = TailVec a0123456789876543210 type HeadVecSym0 :: (~>) (Vec ('Succ n) a) a data HeadVecSym0 :: (~>) (Vec ('Succ n) a) a @@ -237,28 +237,28 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings HeadVecSym0 where suppressUnusedWarnings = snd ((,) HeadVecSym0KindInference ()) type HeadVecSym1 :: Vec ('Succ n) a -> a - type family HeadVecSym1 (a0123456789876543210 :: Vec ('Succ n) a) :: a where + type family HeadVecSym1 @n @a (a0123456789876543210 :: Vec ('Succ n) a) :: a where HeadVecSym1 a0123456789876543210 = HeadVec a0123456789876543210 type Transitivity :: Equal a b -> Equal b c -> Equal a c - type family Transitivity (a :: Equal a b) (a :: Equal b c) :: Equal a c where + type family Transitivity @a @b @c (a :: Equal a b) (a :: Equal b c) :: Equal a c where Transitivity Reflexive Reflexive = ReflexiveSym0 type Symmetry :: Equal a b -> Equal b a - type family Symmetry (a :: Equal a b) :: Equal b a where + type family Symmetry @a @b (a :: Equal a b) :: Equal b a where Symmetry Reflexive = ReflexiveSym0 type MapVec :: (~>) a b -> Vec n a -> Vec n b - type family MapVec (a :: (~>) a b) (a :: Vec n a) :: Vec n b where + type family MapVec @a @b @n (a :: (~>) a b) (a :: Vec n a) :: Vec n b where MapVec _ VNil = VNilSym0 MapVec f (VCons x xs) = Apply (Apply VConsSym0 (Apply f x)) (Apply (Apply MapVecSym0 f) xs) type (!) :: Vec n a -> Fin n -> a - type family (!) (a :: Vec n a) (a :: Fin n) :: a where + type family (!) @n @a (a :: Vec n a) (a :: Fin n) :: a where (!) (VCons x _) FZ = x (!) (VCons _ xs) (FS n) = Apply (Apply (!@#@$) xs) n (!) VNil n = Case_0123456789876543210 n n type TailVec :: Vec ('Succ n) a -> Vec n a - type family TailVec (a :: Vec ('Succ n) a) :: Vec n a where + type family TailVec @n @a (a :: Vec ('Succ n) a) :: Vec n a where TailVec (VCons _ xs) = xs type HeadVec :: Vec ('Succ n) a -> a - type family HeadVec (a :: Vec ('Succ n) a) :: a where + type family HeadVec @n @a (a :: Vec ('Succ n) a) :: a where HeadVec (VCons x _) = x sTransitivity :: (forall (t :: Equal a b) (t :: Equal b c). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T160.golden b/singletons-base/tests/compile-and-dump/Singletons/T160.golden index 563abd1c..e98fe501 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T160.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T160.golden @@ -32,10 +32,10 @@ Singletons/T160.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FooSym0 where suppressUnusedWarnings = snd ((,) FooSym0KindInference ()) type FooSym1 :: a -> a - type family FooSym1 (a0123456789876543210 :: a) :: a where + type family FooSym1 @a (a0123456789876543210 :: a) :: a where FooSym1 a0123456789876543210 = Foo a0123456789876543210 type Foo :: a -> a - type family Foo (a :: a) :: a where + type family Foo @a (a :: a) :: a where Foo x = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) sFoo :: (forall (t :: a). @@ -60,7 +60,6 @@ Singletons/T160.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun1 @ShowTypeSym0 SShowType) sX)) instance (SNum a, SEq a) => SingI (FooSym0 :: (~>) a a) where sing = singFun1 @FooSym0 sFoo - Singletons/T160.hs:0:0: error: [GHC-64725] • 1 • In the expression: Refl @@ -68,3 +67,4 @@ Singletons/T160.hs:0:0: error: [GHC-64725] | 13 | f = Refl | ^^^^ + diff --git a/singletons-base/tests/compile-and-dump/Singletons/T163.golden b/singletons-base/tests/compile-and-dump/Singletons/T163.golden index 2c8777e0..433ca640 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T163.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T163.golden @@ -11,7 +11,7 @@ Singletons/T163.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings LSym0 where suppressUnusedWarnings = snd ((,) LSym0KindInference ()) type LSym1 :: forall a b. a -> (+) a b - type family LSym1 (a0123456789876543210 :: a) :: (+) a b where + type family LSym1 @a @b (a0123456789876543210 :: a) :: (+) a b where LSym1 a0123456789876543210 = L a0123456789876543210 type RSym0 :: forall a b. (~>) b ((+) a b) data RSym0 :: (~>) b ((+) a b) @@ -22,7 +22,7 @@ Singletons/T163.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings RSym0 where suppressUnusedWarnings = snd ((,) RSym0KindInference ()) type RSym1 :: forall a b. b -> (+) a b - type family RSym1 (a0123456789876543210 :: b) :: (+) a b where + type family RSym1 @a @b (a0123456789876543210 :: b) :: (+) a b where RSym1 a0123456789876543210 = R a0123456789876543210 data (%+) :: forall a b. (+) a b -> Type where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T166.golden b/singletons-base/tests/compile-and-dump/Singletons/T166.golden index 29f30832..10431dd1 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T166.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T166.golden @@ -31,7 +31,7 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FoosPrecSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FoosPrecSym2KindInference ()) type FoosPrecSym3 :: forall a. Natural -> a -> [Bool] -> [Bool] - type family FoosPrecSym3 (a0123456789876543210 :: Natural) (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where + type family FoosPrecSym3 @a (a0123456789876543210 :: Natural) (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where FoosPrecSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = FoosPrec a0123456789876543210 a0123456789876543210 a0123456789876543210 type FooSym0 :: forall a. (~>) a [Bool] data FooSym0 :: (~>) a [Bool] @@ -42,7 +42,7 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FooSym0 where suppressUnusedWarnings = snd ((,) FooSym0KindInference ()) type FooSym1 :: forall a. a -> [Bool] - type family FooSym1 (a0123456789876543210 :: a) :: [Bool] where + type family FooSym1 @a (a0123456789876543210 :: a) :: [Bool] where FooSym1 a0123456789876543210 = Foo a0123456789876543210 type family Lambda_0123456789876543210 x0123456789876543210 s where Lambda_0123456789876543210 x s = Apply (Apply (Apply FoosPrecSym0 (FromInteger 0)) x) s @@ -65,7 +65,7 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations type family Lambda_0123456789876543210Sym2 x0123456789876543210 s0123456789876543210 where Lambda_0123456789876543210Sym2 x0123456789876543210 s0123456789876543210 = Lambda_0123456789876543210 x0123456789876543210 s0123456789876543210 type Foo_0123456789876543210 :: a -> [Bool] - type family Foo_0123456789876543210 (a :: a) :: [Bool] where + type family Foo_0123456789876543210 @a (a :: a) :: [Bool] where Foo_0123456789876543210 x = Apply Lambda_0123456789876543210Sym0 x type Foo_0123456789876543210Sym0 :: (~>) a [Bool] data Foo_0123456789876543210Sym0 :: (~>) a [Bool] @@ -77,7 +77,7 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Foo_0123456789876543210Sym0KindInference ()) type Foo_0123456789876543210Sym1 :: a -> [Bool] - type family Foo_0123456789876543210Sym1 (a0123456789876543210 :: a) :: [Bool] where + type family Foo_0123456789876543210Sym1 @a (a0123456789876543210 :: a) :: [Bool] where Foo_0123456789876543210Sym1 a0123456789876543210 = Foo_0123456789876543210 a0123456789876543210 class PFoo a where type family FoosPrec (arg :: Natural) (arg :: a) (arg :: [Bool]) :: [Bool] @@ -140,7 +140,6 @@ Singletons/T166.hs:(0,0)-(0,0): Splicing declarations = singFun1 @(FoosPrecSym2 (d :: Natural) (d :: a)) (sFoosPrec s s) instance SFoo a => SingI (FooSym0 :: (~>) a [Bool]) where sing = singFun1 @FooSym0 sFoo - Singletons/T166.hs:0:0: error: [GHC-83865] • Expecting one more argument to ‘Apply Lambda_0123456789876543210Sym0 x’ Expected kind ‘[Bool]’, @@ -152,3 +151,4 @@ Singletons/T166.hs:0:0: error: [GHC-83865] | 6 | $(singletonsOnly [d| | ^^^^^^^^^^^^^^^^^^^... + diff --git a/singletons-base/tests/compile-and-dump/Singletons/T167.golden b/singletons-base/tests/compile-and-dump/Singletons/T167.golden index 3056dcd7..56ed9a83 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T167.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T167.golden @@ -34,7 +34,7 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FoosPrecSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FoosPrecSym2KindInference ()) type FoosPrecSym3 :: forall a. Natural -> a -> [Bool] -> [Bool] - type family FoosPrecSym3 (a0123456789876543210 :: Natural) (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where + type family FoosPrecSym3 @a (a0123456789876543210 :: Natural) (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where FoosPrecSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = FoosPrec a0123456789876543210 a0123456789876543210 a0123456789876543210 type FooListSym0 :: forall a. (~>) a ((~>) [Bool] [Bool]) data FooListSym0 :: (~>) a ((~>) [Bool] [Bool]) @@ -53,10 +53,10 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FooListSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FooListSym1KindInference ()) type FooListSym2 :: forall a. a -> [Bool] -> [Bool] - type family FooListSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where + type family FooListSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where FooListSym2 a0123456789876543210 a0123456789876543210 = FooList a0123456789876543210 a0123456789876543210 type FooList_0123456789876543210 :: a -> [Bool] -> [Bool] - type family FooList_0123456789876543210 (a :: a) (a :: [Bool]) :: [Bool] where + type family FooList_0123456789876543210 @a (a :: a) (a :: [Bool]) :: [Bool] where FooList_0123456789876543210 a_0123456789876543210 a_0123456789876543210 = Apply (Apply UndefinedSym0 a_0123456789876543210) a_0123456789876543210 type FooList_0123456789876543210Sym0 :: (~>) a ((~>) [Bool] [Bool]) data FooList_0123456789876543210Sym0 :: (~>) a ((~>) [Bool] [Bool]) @@ -77,7 +77,7 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) FooList_0123456789876543210Sym1KindInference ()) type FooList_0123456789876543210Sym2 :: a -> [Bool] -> [Bool] - type family FooList_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where + type family FooList_0123456789876543210Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: [Bool]) :: [Bool] where FooList_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = FooList_0123456789876543210 a0123456789876543210 a0123456789876543210 class PFoo a where type family FoosPrec (arg :: Natural) (arg :: a) (arg :: [Bool]) :: [Bool] @@ -85,7 +85,7 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations type FooList a a = Apply (Apply FooList_0123456789876543210Sym0 a) a type FoosPrec_0123456789876543210 :: Natural -> [a] -> [Bool] -> [Bool] - type family FoosPrec_0123456789876543210 (a :: Natural) (a :: [a]) (a :: [Bool]) :: [Bool] where + type family FoosPrec_0123456789876543210 @a (a :: Natural) (a :: [a]) (a :: [Bool]) :: [Bool] where FoosPrec_0123456789876543210 _ a_0123456789876543210 a_0123456789876543210 = Apply (Apply FooListSym0 a_0123456789876543210) a_0123456789876543210 type FoosPrec_0123456789876543210Sym0 :: (~>) Natural ((~>) [a] ((~>) [Bool] [Bool])) data FoosPrec_0123456789876543210Sym0 :: (~>) Natural ((~>) [a] ((~>) [Bool] [Bool])) @@ -118,7 +118,7 @@ Singletons/T167.hs:(0,0)-(0,0): Splicing declarations = snd ((,) FoosPrec_0123456789876543210Sym2KindInference ()) type FoosPrec_0123456789876543210Sym3 :: Natural -> [a] -> [Bool] -> [Bool] - type family FoosPrec_0123456789876543210Sym3 (a0123456789876543210 :: Natural) (a0123456789876543210 :: [a]) (a0123456789876543210 :: [Bool]) :: [Bool] where + type family FoosPrec_0123456789876543210Sym3 @a (a0123456789876543210 :: Natural) (a0123456789876543210 :: [a]) (a0123456789876543210 :: [Bool]) :: [Bool] where FoosPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = FoosPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PFoo [a] where type FoosPrec a a a = Apply (Apply (Apply FoosPrec_0123456789876543210Sym0 a) a) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T175.golden b/singletons-base/tests/compile-and-dump/Singletons/T175.golden index 58b7f83a..d4b22ccc 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T175.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T175.golden @@ -19,24 +19,24 @@ Singletons/T175.hs:(0,0)-(0,0): Splicing declarations quux2 :: Bar2 a => a quux2 = baz type Quux2Sym0 :: a - type family Quux2Sym0 :: a where + type family Quux2Sym0 @a :: a where Quux2Sym0 = Quux2 type Quux2 :: a - type family Quux2 :: a where + type family Quux2 @a :: a where Quux2 = BazSym0 type BazSym0 :: forall a. a - type family BazSym0 :: a where + type family BazSym0 @a :: a where BazSym0 = Baz class PFoo a where type family Baz :: a type Quux1Sym0 :: forall a. a - type family Quux1Sym0 :: a where + type family Quux1Sym0 @a :: a where Quux1Sym0 = Quux1 type Quux1_0123456789876543210 :: a - type family Quux1_0123456789876543210 :: a where + type family Quux1_0123456789876543210 @a :: a where Quux1_0123456789876543210 = BazSym0 type Quux1_0123456789876543210Sym0 :: a - type family Quux1_0123456789876543210Sym0 :: a where + type family Quux1_0123456789876543210Sym0 @a :: a where Quux1_0123456789876543210Sym0 = Quux1_0123456789876543210 class PBar1 a where type family Quux1 :: a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T176.golden b/singletons-base/tests/compile-and-dump/Singletons/T176.golden index b0670af1..1d7c9521 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T176.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T176.golden @@ -53,7 +53,7 @@ Singletons/T176.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Quux2Sym0 where suppressUnusedWarnings = snd ((,) Quux2Sym0KindInference ()) type Quux2Sym1 :: a -> a - type family Quux2Sym1 (a0123456789876543210 :: a) :: a where + type family Quux2Sym1 @a (a0123456789876543210 :: a) :: a where Quux2Sym1 a0123456789876543210 = Quux2 a0123456789876543210 type Quux1Sym0 :: (~>) a a data Quux1Sym0 :: (~>) a a @@ -64,13 +64,13 @@ Singletons/T176.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Quux1Sym0 where suppressUnusedWarnings = snd ((,) Quux1Sym0KindInference ()) type Quux1Sym1 :: a -> a - type family Quux1Sym1 (a0123456789876543210 :: a) :: a where + type family Quux1Sym1 @a (a0123456789876543210 :: a) :: a where Quux1Sym1 a0123456789876543210 = Quux1 a0123456789876543210 type Quux2 :: a -> a - type family Quux2 (a :: a) :: a where + type family Quux2 @a (a :: a) :: a where Quux2 x = Apply (Apply Bar2Sym0 x) Baz2Sym0 type Quux1 :: a -> a - type family Quux1 (a :: a) :: a where + type family Quux1 @a (a :: a) :: a where Quux1 x = Apply (Apply Bar1Sym0 x) (Apply Lambda_0123456789876543210Sym0 x) type Bar1Sym0 :: forall a b. (~>) a ((~>) ((~>) a b) b) data Bar1Sym0 :: (~>) a ((~>) ((~>) a b) b) @@ -89,10 +89,10 @@ Singletons/T176.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Bar1Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Bar1Sym1KindInference ()) type Bar1Sym2 :: forall a b. a -> (~>) a b -> b - type family Bar1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: (~>) a b) :: b where + type family Bar1Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: (~>) a b) :: b where Bar1Sym2 a0123456789876543210 a0123456789876543210 = Bar1 a0123456789876543210 a0123456789876543210 type Baz1Sym0 :: forall a. a - type family Baz1Sym0 :: a where + type family Baz1Sym0 @a :: a where Baz1Sym0 = Baz1 class PFoo1 a where type family Bar1 (arg :: a) (arg :: (~>) a b) :: b @@ -114,10 +114,10 @@ Singletons/T176.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Bar2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Bar2Sym1KindInference ()) type Bar2Sym2 :: forall a b. a -> b -> b - type family Bar2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family Bar2Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Bar2Sym2 a0123456789876543210 a0123456789876543210 = Bar2 a0123456789876543210 a0123456789876543210 type Baz2Sym0 :: forall a. a - type family Baz2Sym0 :: a where + type family Baz2Sym0 @a :: a where Baz2Sym0 = Baz2 class PFoo2 a where type family Bar2 (arg :: a) (arg :: b) :: b diff --git a/singletons-base/tests/compile-and-dump/Singletons/T178.golden b/singletons-base/tests/compile-and-dump/Singletons/T178.golden index 60f6fa7a..755aab69 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T178.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T178.golden @@ -244,13 +244,13 @@ Singletons/T178.hs:(0,0)-(0,0): Splicing declarations (%~) SMany SMany = Proved Refl instance Eq (SOcc (z :: Occ)) where (==) _ _ = True - instance Data.Type.Equality.TestEquality (SOcc :: Occ - -> Type) where - Data.Type.Equality.testEquality + instance GHC.Internal.Data.Type.Equality.TestEquality (SOcc :: Occ + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (SOcc :: Occ - -> Type) where - Data.Type.Coercion.testCoercion + instance GHC.Internal.Data.Type.Coercion.TestCoercion (SOcc :: Occ + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SOcc (z :: Occ)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/T183.golden b/singletons-base/tests/compile-and-dump/Singletons/T183.golden index 1f358258..909d4623 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T183.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T183.golden @@ -204,7 +204,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo9Sym0 where suppressUnusedWarnings = snd ((,) Foo9Sym0KindInference ()) type Foo9Sym1 :: a -> a - type family Foo9Sym1 (a0123456789876543210 :: a) :: a where + type family Foo9Sym1 @a (a0123456789876543210 :: a) :: a where Foo9Sym1 a0123456789876543210 = Foo9 a0123456789876543210 type Foo8Sym0 :: forall a. (~>) (Maybe a) (Maybe a) data Foo8Sym0 :: (~>) (Maybe a) (Maybe a) @@ -215,7 +215,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo8Sym0 where suppressUnusedWarnings = snd ((,) Foo8Sym0KindInference ()) type Foo8Sym1 :: forall a. Maybe a -> Maybe a - type family Foo8Sym1 (a0123456789876543210 :: Maybe a) :: Maybe a where + type family Foo8Sym1 @a (a0123456789876543210 :: Maybe a) :: Maybe a where Foo8Sym1 a0123456789876543210 = Foo8 a0123456789876543210 type Foo7Sym0 :: (~>) a ((~>) b a) data Foo7Sym0 :: (~>) a ((~>) b a) @@ -234,7 +234,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Foo7Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Foo7Sym1KindInference ()) type Foo7Sym2 :: a -> b -> a - type family Foo7Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Foo7Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Foo7Sym2 a0123456789876543210 a0123456789876543210 = Foo7 a0123456789876543210 a0123456789876543210 type Foo6Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a)) data Foo6Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a)) @@ -245,7 +245,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo6Sym0 where suppressUnusedWarnings = snd ((,) Foo6Sym0KindInference ()) type Foo6Sym1 :: Maybe (Maybe a) -> Maybe (Maybe a) - type family Foo6Sym1 (a0123456789876543210 :: Maybe (Maybe a)) :: Maybe (Maybe a) where + type family Foo6Sym1 @a (a0123456789876543210 :: Maybe (Maybe a)) :: Maybe (Maybe a) where Foo6Sym1 a0123456789876543210 = Foo6 a0123456789876543210 type Foo5Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a)) data Foo5Sym0 :: (~>) (Maybe (Maybe a)) (Maybe (Maybe a)) @@ -256,7 +256,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo5Sym0 where suppressUnusedWarnings = snd ((,) Foo5Sym0KindInference ()) type Foo5Sym1 :: Maybe (Maybe a) -> Maybe (Maybe a) - type family Foo5Sym1 (a0123456789876543210 :: Maybe (Maybe a)) :: Maybe (Maybe a) where + type family Foo5Sym1 @a (a0123456789876543210 :: Maybe (Maybe a)) :: Maybe (Maybe a) where Foo5Sym1 a0123456789876543210 = Foo5 a0123456789876543210 type Foo4Sym0 :: (~>) (a, b) (b, a) data Foo4Sym0 :: (~>) (a, b) (b, a) @@ -267,8 +267,8 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo4Sym0 where suppressUnusedWarnings = snd ((,) Foo4Sym0KindInference ()) type Foo4Sym1 :: (a, b) -> (b, a) - type family Foo4Sym1 (a0123456789876543210 :: (a, b)) :: (b, - a) where + type family Foo4Sym1 @a @b (a0123456789876543210 :: (a, b)) :: (b, + a) where Foo4Sym1 a0123456789876543210 = Foo4 a0123456789876543210 type Foo3Sym0 :: forall a. (~>) (Maybe a) a data Foo3Sym0 :: (~>) (Maybe a) a @@ -279,7 +279,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo3Sym0 where suppressUnusedWarnings = snd ((,) Foo3Sym0KindInference ()) type Foo3Sym1 :: forall a. Maybe a -> a - type family Foo3Sym1 (a0123456789876543210 :: Maybe a) :: a where + type family Foo3Sym1 @a (a0123456789876543210 :: Maybe a) :: a where Foo3Sym1 a0123456789876543210 = Foo3 a0123456789876543210 type Foo2Sym0 :: forall a. (~>) (Maybe a) a data Foo2Sym0 :: (~>) (Maybe a) a @@ -290,7 +290,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo2Sym0 where suppressUnusedWarnings = snd ((,) Foo2Sym0KindInference ()) type Foo2Sym1 :: forall a. Maybe a -> a - type family Foo2Sym1 (a0123456789876543210 :: Maybe a) :: a where + type family Foo2Sym1 @a (a0123456789876543210 :: Maybe a) :: a where Foo2Sym1 a0123456789876543210 = Foo2 a0123456789876543210 type Foo1Sym0 :: (~>) (Maybe a) a data Foo1Sym0 :: (~>) (Maybe a) a @@ -301,7 +301,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Foo1Sym0 where suppressUnusedWarnings = snd ((,) Foo1Sym0KindInference ()) type Foo1Sym1 :: Maybe a -> a - type family Foo1Sym1 (a0123456789876543210 :: Maybe a) :: a where + type family Foo1Sym1 @a (a0123456789876543210 :: Maybe a) :: a where Foo1Sym1 a0123456789876543210 = Foo1 a0123456789876543210 data GSym0 a0123456789876543210 where @@ -340,32 +340,32 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations type family F1Sym1 a0123456789876543210 where F1Sym1 a0123456789876543210 = F1 a0123456789876543210 type Foo9 :: a -> a - type family Foo9 (a :: a) :: a where + type family Foo9 @a (a :: a) :: a where Foo9 (x :: a) = Apply (Apply (Let0123456789876543210GSym2 a x) x) Tuple0Sym0 type Foo8 :: forall a. Maybe a -> Maybe a - type family Foo8 (a :: Maybe a) :: Maybe a where + type family Foo8 @a (a :: Maybe a) :: Maybe a where Foo8 @a ('Just (wild_0123456789876543210 :: a) :: Maybe a :: Maybe a) = Let0123456789876543210XSym2 a wild_0123456789876543210 Foo8 @a ('Nothing :: Maybe a :: Maybe a) = Let0123456789876543210XSym1 a type Foo7 :: a -> b -> a - type family Foo7 (a :: a) (a :: b) :: a where + type family Foo7 @a @b (a :: a) (a :: b) :: a where Foo7 (x :: a) (wild_0123456789876543210 :: b) = x :: a type Foo6 :: Maybe (Maybe a) -> Maybe (Maybe a) - type family Foo6 (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where + type family Foo6 @a (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where Foo6 ('Just x :: Maybe (Maybe a)) = Case_0123456789876543210 a x (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a x) type Foo5 :: Maybe (Maybe a) -> Maybe (Maybe a) - type family Foo5 (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where + type family Foo5 @a (a :: Maybe (Maybe a)) :: Maybe (Maybe a) where Foo5 ('Just ('Just (x :: a) :: Maybe a) :: Maybe (Maybe a)) = Apply JustSym0 (Apply JustSym0 (x :: a) :: Maybe a) :: Maybe (Maybe a) type Foo4 :: (a, b) -> (b, a) - type family Foo4 (a :: (a, b)) :: (b, a) where + type family Foo4 @a @b (a :: (a, b)) :: (b, a) where Foo4 a_0123456789876543210 = Apply (Apply Lambda_0123456789876543210Sym0 a_0123456789876543210) a_0123456789876543210 type Foo3 :: forall a. Maybe a -> a - type family Foo3 (a :: Maybe a) :: a where + type family Foo3 @a (a :: Maybe a) :: a where Foo3 @a ('Just x :: Maybe a) = x :: a type Foo2 :: forall a. Maybe a -> a - type family Foo2 (a :: Maybe a) :: a where + type family Foo2 @a (a :: Maybe a) :: a where Foo2 @a ('Just x :: Maybe a :: Maybe a) = x :: a type Foo1 :: Maybe a -> a - type family Foo1 (a :: Maybe a) :: a where + type family Foo1 @a (a :: Maybe a) :: a where Foo1 ('Just x :: Maybe a) = x :: a type family G a where G x = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T184.golden b/singletons-base/tests/compile-and-dump/Singletons/T184.golden index e9469d65..85828518 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T184.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T184.golden @@ -289,8 +289,8 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (CartProdSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) CartProdSym1KindInference ()) type CartProdSym2 :: [a] -> [b] -> [(a, b)] - type family CartProdSym2 (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [(a, - b)] where + type family CartProdSym2 @a @b (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [(a, + b)] where CartProdSym2 a0123456789876543210 a0123456789876543210 = CartProd a0123456789876543210 a0123456789876543210 type Zip'Sym0 :: (~>) [a] ((~>) [b] [(a, b)]) data Zip'Sym0 :: (~>) [a] ((~>) [b] [(a, b)]) @@ -309,8 +309,8 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Zip'Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Zip'Sym1KindInference ()) type Zip'Sym2 :: [a] -> [b] -> [(a, b)] - type family Zip'Sym2 (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [(a, - b)] where + type family Zip'Sym2 @a @b (a0123456789876543210 :: [a]) (a0123456789876543210 :: [b]) :: [(a, + b)] where Zip'Sym2 a0123456789876543210 a0123456789876543210 = Zip' a0123456789876543210 a0123456789876543210 type BoogieSym0 :: (~>) (Maybe a) ((~>) (Maybe Bool) (Maybe a)) data BoogieSym0 :: (~>) (Maybe a) ((~>) (Maybe Bool) (Maybe a)) @@ -329,19 +329,19 @@ Singletons/T184.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (BoogieSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BoogieSym1KindInference ()) type BoogieSym2 :: Maybe a -> Maybe Bool -> Maybe a - type family BoogieSym2 (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe Bool) :: Maybe a where + type family BoogieSym2 @a (a0123456789876543210 :: Maybe a) (a0123456789876543210 :: Maybe Bool) :: Maybe a where BoogieSym2 a0123456789876543210 a0123456789876543210 = Boogie a0123456789876543210 a0123456789876543210 type Trues :: [Bool] -> [Bool] type family Trues (a :: [Bool]) :: [Bool] where Trues xs = Apply (Apply (>>=@#@$) xs) (Apply Lambda_0123456789876543210Sym0 xs) type CartProd :: [a] -> [b] -> [(a, b)] - type family CartProd (a :: [a]) (a :: [b]) :: [(a, b)] where + type family CartProd @a @b (a :: [a]) (a :: [b]) :: [(a, b)] where CartProd xs ys = Apply (Apply (>>=@#@$) xs) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys) type Zip' :: [a] -> [b] -> [(a, b)] - type family Zip' (a :: [a]) (a :: [b]) :: [(a, b)] where + type family Zip' @a @b (a :: [a]) (a :: [b]) :: [(a, b)] where Zip' xs ys = Apply (Apply (>>=@#@$) (Apply (Apply MzipSym0 (Apply (Apply (>>=@#@$) xs) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys))) (Apply (Apply (>>=@#@$) ys) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys)))) (Apply (Apply Lambda_0123456789876543210Sym0 xs) ys) type Boogie :: Maybe a -> Maybe Bool -> Maybe a - type family Boogie (a :: Maybe a) (a :: Maybe Bool) :: Maybe a where + type family Boogie @a (a :: Maybe a) (a :: Maybe Bool) :: Maybe a where Boogie ma mb = Apply (Apply (>>=@#@$) ma) (Apply (Apply Lambda_0123456789876543210Sym0 ma) mb) sTrues :: (forall (t :: [Bool]). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T187.golden b/singletons-base/tests/compile-and-dump/Singletons/T187.golden index e708a989..7578015f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T187.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T187.golden @@ -85,13 +85,13 @@ Singletons/T187.hs:(0,0)-(0,0): Splicing declarations (%~) x _ = Proved (case x of {}) instance Eq (SEmpty (z :: Empty)) where (==) _ _ = True - instance Data.Type.Equality.TestEquality (SEmpty :: Empty - -> Type) where - Data.Type.Equality.testEquality + instance GHC.Internal.Data.Type.Equality.TestEquality (SEmpty :: Empty + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (SEmpty :: Empty - -> Type) where - Data.Type.Coercion.testCoercion + instance GHC.Internal.Data.Type.Coercion.TestCoercion (SEmpty :: Empty + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SEmpty (z :: Empty)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/T190.golden b/singletons-base/tests/compile-and-dump/Singletons/T190.golden index 9c808a64..56464bcf 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T190.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T190.golden @@ -224,11 +224,13 @@ Singletons/T190.hs:0:0:: Splicing declarations (%~) ST ST = Proved Refl instance Eq (ST (z :: T)) where (==) _ _ = True - instance Data.Type.Equality.TestEquality (ST :: T -> Type) where - Data.Type.Equality.testEquality + instance GHC.Internal.Data.Type.Equality.TestEquality (ST :: T + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (ST :: T -> Type) where - Data.Type.Coercion.testCoercion + instance GHC.Internal.Data.Type.Coercion.TestCoercion (ST :: T + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (ST (z :: T)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/T197b.golden b/singletons-base/tests/compile-and-dump/Singletons/T197b.golden index 413c4151..4c9b22e8 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T197b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T197b.golden @@ -26,7 +26,7 @@ Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((:*:@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (::*:@#@$$###) ()) type (:*:@#@$$$) :: forall a b. a -> b -> (:*:) a b - type family (:*:@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (:*:) a b where + type family (:*:@#@$$$) @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: (:*:) a b where (:*:@#@$$$) a0123456789876543210 a0123456789876543210 = (:*:) a0123456789876543210 a0123456789876543210 type MkPairSym0 :: forall a b. (~>) a ((~>) b (Pair a b)) data MkPairSym0 :: (~>) a ((~>) b (Pair a b)) @@ -47,7 +47,7 @@ Singletons/T197b.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkPairSym1KindInference ()) infixr 9 `MkPairSym1` type MkPairSym2 :: forall a b. a -> b -> Pair a b - type family MkPairSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where + type family MkPairSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Pair a b where MkPairSym2 a0123456789876543210 a0123456789876543210 = MkPair a0123456789876543210 a0123456789876543210 infixr 9 `MkPairSym2` infixr 9 `SMkPair` diff --git a/singletons-base/tests/compile-and-dump/Singletons/T204.golden b/singletons-base/tests/compile-and-dump/Singletons/T204.golden index cd59b4fd..dd7bcd1f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T204.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T204.golden @@ -32,7 +32,7 @@ Singletons/T204.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((:%@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (::%@#@$$###) ()) type (:%@#@$$$) :: forall a. a -> a -> Ratio1 a - type family (:%@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ratio1 a where + type family (:%@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ratio1 a where (:%@#@$$$) a0123456789876543210 a0123456789876543210 = (:%) a0123456789876543210 a0123456789876543210 type (:%%@#@$) :: forall a. (~>) a ((~>) a (Ratio2 a)) data (:%%@#@$) :: (~>) a ((~>) a (Ratio2 a)) @@ -51,7 +51,7 @@ Singletons/T204.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((:%%@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (::%%@#@$$###) ()) type (:%%@#@$$$) :: forall a. a -> a -> Ratio2 a - type family (:%%@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ratio2 a where + type family (:%%@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ratio2 a where (:%%@#@$$$) a0123456789876543210 a0123456789876543210 = (:%%) a0123456789876543210 a0123456789876543210 data SRatio1 :: forall a. Ratio1 a -> GHC.Types.Type where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T209.golden b/singletons-base/tests/compile-and-dump/Singletons/T209.golden index 8474a88d..c5714a09 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T209.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T209.golden @@ -45,10 +45,10 @@ Singletons/T209.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (MSym2 a0123456789876543210 a0123456789876543210) where suppressUnusedWarnings = snd ((,) MSym2KindInference ()) type MSym3 :: a -> b -> Bool -> Bool - type family MSym3 (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: Bool) :: Bool where + type family MSym3 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) (a0123456789876543210 :: Bool) :: Bool where MSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = M a0123456789876543210 a0123456789876543210 a0123456789876543210 type M :: a -> b -> Bool -> Bool - type family M (a :: a) (a :: b) (a :: Bool) :: Bool where + type family M @a @b (a :: a) (a :: b) (a :: Bool) :: Bool where M _ _ x = x class PC a b instance PC Bool Hm diff --git a/singletons-base/tests/compile-and-dump/Singletons/T249.golden b/singletons-base/tests/compile-and-dump/Singletons/T249.golden index 6631c53a..5f349806 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T249.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T249.golden @@ -16,7 +16,7 @@ Singletons/T249.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkFoo1Sym0 where suppressUnusedWarnings = snd ((,) MkFoo1Sym0KindInference ()) type MkFoo1Sym1 :: forall a. a -> Foo1 a - type family MkFoo1Sym1 (a0123456789876543210 :: a) :: Foo1 a where + type family MkFoo1Sym1 @a (a0123456789876543210 :: a) :: Foo1 a where MkFoo1Sym1 a0123456789876543210 = MkFoo1 a0123456789876543210 type MkFoo2Sym0 :: (~>) x (Foo2 x) data MkFoo2Sym0 :: (~>) x (Foo2 x) @@ -27,7 +27,7 @@ Singletons/T249.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkFoo2Sym0 where suppressUnusedWarnings = snd ((,) MkFoo2Sym0KindInference ()) type MkFoo2Sym1 :: x -> Foo2 x - type family MkFoo2Sym1 (a0123456789876543210 :: x) :: Foo2 x where + type family MkFoo2Sym1 @x (a0123456789876543210 :: x) :: Foo2 x where MkFoo2Sym1 a0123456789876543210 = MkFoo2 a0123456789876543210 type MkFoo3Sym0 :: forall x. (~>) x (Foo3 x) data MkFoo3Sym0 :: (~>) x (Foo3 x) @@ -38,7 +38,7 @@ Singletons/T249.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkFoo3Sym0 where suppressUnusedWarnings = snd ((,) MkFoo3Sym0KindInference ()) type MkFoo3Sym1 :: forall x. x -> Foo3 x - type family MkFoo3Sym1 (a0123456789876543210 :: x) :: Foo3 x where + type family MkFoo3Sym1 @x (a0123456789876543210 :: x) :: Foo3 x where MkFoo3Sym1 a0123456789876543210 = MkFoo3 a0123456789876543210 data SFoo1 :: forall a. Foo1 a -> Type where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T271.golden b/singletons-base/tests/compile-and-dump/Singletons/T271.golden index 7656a3c4..52870d77 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T271.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T271.golden @@ -24,7 +24,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) ConstantSym0KindInference ()) type ConstantSym1 :: forall (a :: Type) (b :: Type). a -> Constant a b - type family ConstantSym1 (a0123456789876543210 :: a) :: Constant a b where + type family ConstantSym1 @(a :: Type) @(b :: Type) (a0123456789876543210 :: a) :: Constant a b where ConstantSym1 a0123456789876543210 = Constant a0123456789876543210 type IdentitySym0 :: (~>) a (Identity a) data IdentitySym0 :: (~>) a (Identity a) @@ -35,11 +35,11 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings IdentitySym0 where suppressUnusedWarnings = snd ((,) IdentitySym0KindInference ()) type IdentitySym1 :: a -> Identity a - type family IdentitySym1 (a0123456789876543210 :: a) :: Identity a where + type family IdentitySym1 @a (a0123456789876543210 :: a) :: Identity a where IdentitySym1 a0123456789876543210 = Identity a0123456789876543210 type TFHelper_0123456789876543210 :: Constant a b -> Constant a b -> Bool - type family TFHelper_0123456789876543210 (a :: Constant a b) (a :: Constant a b) :: Bool where + type family TFHelper_0123456789876543210 @a @b (a :: Constant a b) (a :: Constant a b) :: Bool where TFHelper_0123456789876543210 (Constant a_0123456789876543210) (Constant b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) (Constant a b) ((~>) (Constant a b) Bool) data TFHelper_0123456789876543210Sym0 :: (~>) (Constant a b) ((~>) (Constant a b) Bool) @@ -62,13 +62,13 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Constant a b -> Constant a b -> Bool - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Constant a b) (a0123456789876543210 :: Constant a b) :: Bool where + type family TFHelper_0123456789876543210Sym2 @a @b (a0123456789876543210 :: Constant a b) (a0123456789876543210 :: Constant a b) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (Constant a b) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Constant a b -> Constant a b -> Ordering - type family Compare_0123456789876543210 (a :: Constant a b) (a :: Constant a b) :: Ordering where + type family Compare_0123456789876543210 @a @b (a :: Constant a b) (a :: Constant a b) :: Ordering where Compare_0123456789876543210 (Constant a_0123456789876543210) (Constant b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0) type Compare_0123456789876543210Sym0 :: (~>) (Constant a b) ((~>) (Constant a b) Ordering) data Compare_0123456789876543210Sym0 :: (~>) (Constant a b) ((~>) (Constant a b) Ordering) @@ -91,13 +91,13 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Compare_0123456789876543210Sym1KindInference ()) type Compare_0123456789876543210Sym2 :: Constant a b -> Constant a b -> Ordering - type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Constant a b) (a0123456789876543210 :: Constant a b) :: Ordering where + type family Compare_0123456789876543210Sym2 @a @b (a0123456789876543210 :: Constant a b) (a0123456789876543210 :: Constant a b) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd (Constant a b) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a type TFHelper_0123456789876543210 :: Identity a -> Identity a -> Bool - type family TFHelper_0123456789876543210 (a :: Identity a) (a :: Identity a) :: Bool where + type family TFHelper_0123456789876543210 @a (a :: Identity a) (a :: Identity a) :: Bool where TFHelper_0123456789876543210 (Identity a_0123456789876543210) (Identity b_0123456789876543210) = Apply (Apply (==@#@$) a_0123456789876543210) b_0123456789876543210 type TFHelper_0123456789876543210Sym0 :: (~>) (Identity a) ((~>) (Identity a) Bool) data TFHelper_0123456789876543210Sym0 :: (~>) (Identity a) ((~>) (Identity a) Bool) @@ -120,13 +120,13 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: Identity a -> Identity a -> Bool - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: Identity a) (a0123456789876543210 :: Identity a) :: Bool where + type family TFHelper_0123456789876543210Sym2 @a (a0123456789876543210 :: Identity a) (a0123456789876543210 :: Identity a) :: Bool where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PEq (Identity a) where type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a type Compare_0123456789876543210 :: Identity a -> Identity a -> Ordering - type family Compare_0123456789876543210 (a :: Identity a) (a :: Identity a) :: Ordering where + type family Compare_0123456789876543210 @a (a :: Identity a) (a :: Identity a) :: Ordering where Compare_0123456789876543210 (Identity a_0123456789876543210) (Identity b_0123456789876543210) = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) (Apply (Apply (:@#@$) (Apply (Apply CompareSym0 a_0123456789876543210) b_0123456789876543210)) NilSym0) type Compare_0123456789876543210Sym0 :: (~>) (Identity a) ((~>) (Identity a) Ordering) data Compare_0123456789876543210Sym0 :: (~>) (Identity a) ((~>) (Identity a) Ordering) @@ -149,7 +149,7 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations = snd ((,) Compare_0123456789876543210Sym1KindInference ()) type Compare_0123456789876543210Sym2 :: Identity a -> Identity a -> Ordering - type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: Identity a) (a0123456789876543210 :: Identity a) :: Ordering where + type family Compare_0123456789876543210Sym2 @a (a0123456789876543210 :: Identity a) (a0123456789876543210 :: Identity a) :: Ordering where Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210 instance POrd (Identity a) where type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a @@ -249,14 +249,14 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations instance Eq (SConstant (z :: Constant a b)) where (==) _ _ = True instance SDecide a => - Data.Type.Equality.TestEquality (SConstant :: Constant a b - -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SConstant :: Constant a b + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => - Data.Type.Coercion.TestCoercion (SConstant :: Constant a b - -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SConstant :: Constant a b + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance SDecide a => SDecide (Identity a) where (%~) (SIdentity a) (SIdentity b) @@ -267,14 +267,14 @@ Singletons/T271.hs:(0,0)-(0,0): Splicing declarations instance Eq (SIdentity (z :: Identity a)) where (==) _ _ = True instance SDecide a => - Data.Type.Equality.TestEquality (SIdentity :: Identity a - -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SIdentity :: Identity a + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance SDecide a => - Data.Type.Coercion.TestCoercion (SIdentity :: Identity a - -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SIdentity :: Identity a + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SConstant (z :: Constant a b)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/T287.golden b/singletons-base/tests/compile-and-dump/Singletons/T287.golden index d8000518..f1e0b444 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T287.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T287.golden @@ -27,7 +27,7 @@ Singletons/T287.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((<<>>@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (:<<>>@#@$$###) ()) type (<<>>@#@$$$) :: forall a. a -> a -> a - type family (<<>>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where + type family (<<>>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<<>>@#@$$$) a0123456789876543210 a0123456789876543210 = (<<>>) a0123456789876543210 a0123456789876543210 class PS a where type family (<<>>) (arg :: a) (arg :: a) :: a @@ -61,7 +61,7 @@ Singletons/T287.hs:(0,0)-(0,0): Splicing declarations Lambda_0123456789876543210Sym3 f0123456789876543210 g0123456789876543210 x0123456789876543210 = Lambda_0123456789876543210 f0123456789876543210 g0123456789876543210 x0123456789876543210 type TFHelper_0123456789876543210 :: (~>) a b -> (~>) a b -> (~>) a b - type family TFHelper_0123456789876543210 (a :: (~>) a b) (a :: (~>) a b) :: (~>) a b where + type family TFHelper_0123456789876543210 @a @b (a :: (~>) a b) (a :: (~>) a b) :: (~>) a b where TFHelper_0123456789876543210 f g = Apply (Apply Lambda_0123456789876543210Sym0 f) g type TFHelper_0123456789876543210Sym0 :: (~>) ((~>) a b) ((~>) ((~>) a b) ((~>) a b)) data TFHelper_0123456789876543210Sym0 :: (~>) ((~>) a b) ((~>) ((~>) a b) ((~>) a b)) @@ -84,7 +84,7 @@ Singletons/T287.hs:(0,0)-(0,0): Splicing declarations = snd ((,) TFHelper_0123456789876543210Sym1KindInference ()) type TFHelper_0123456789876543210Sym2 :: (~>) a b -> (~>) a b -> (~>) a b - type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: (~>) a b) :: (~>) a b where + type family TFHelper_0123456789876543210Sym2 @a @b (a0123456789876543210 :: (~>) a b) (a0123456789876543210 :: (~>) a b) :: (~>) a b where TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210 instance PS ((~>) a b) where type (<<>>) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T296.golden b/singletons-base/tests/compile-and-dump/Singletons/T296.golden index a99af46d..50264af2 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T296.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T296.golden @@ -21,7 +21,7 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations in z in x type MyProxySym0 :: forall (a :: Type). MyProxy a - type family MyProxySym0 :: MyProxy a where + type family MyProxySym0 @(a :: Type) :: MyProxy a where MyProxySym0 = MyProxy data Let0123456789876543210ZSym0 a0123456789876543210 where @@ -56,10 +56,10 @@ Singletons/T296.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FSym0 where suppressUnusedWarnings = snd ((,) FSym0KindInference ()) type FSym1 :: forall a. MyProxy a -> MyProxy a - type family FSym1 (a0123456789876543210 :: MyProxy a) :: MyProxy a where + type family FSym1 @a (a0123456789876543210 :: MyProxy a) :: MyProxy a where FSym1 a0123456789876543210 = F a0123456789876543210 type F :: forall a. MyProxy a -> MyProxy a - type family F (a :: MyProxy a) :: MyProxy a where + type family F @a (a :: MyProxy a) :: MyProxy a where F @a (MyProxy :: MyProxy a) = Let0123456789876543210XSym1 a sF :: forall a (t :: MyProxy a). Sing t diff --git a/singletons-base/tests/compile-and-dump/Singletons/T297.golden b/singletons-base/tests/compile-and-dump/Singletons/T297.golden index e33a7c9f..1190d364 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T297.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T297.golden @@ -19,13 +19,13 @@ Singletons/T297.hs:(0,0)-(0,0): Splicing declarations in z in x type MyProxySym0 :: forall (a :: Type). MyProxy a - type family MyProxySym0 :: MyProxy a where + type family MyProxySym0 @(a :: Type) :: MyProxy a where MyProxySym0 = MyProxy type Let0123456789876543210ZSym0 :: MyProxy a - type family Let0123456789876543210ZSym0 :: MyProxy a where + type family Let0123456789876543210ZSym0 @a :: MyProxy a where Let0123456789876543210ZSym0 = Let0123456789876543210Z type Let0123456789876543210Z :: MyProxy a - type family Let0123456789876543210Z :: MyProxy a where + type family Let0123456789876543210Z @a :: MyProxy a where Let0123456789876543210Z = MyProxySym0 type family Let0123456789876543210XSym0 where Let0123456789876543210XSym0 = Let0123456789876543210X diff --git a/singletons-base/tests/compile-and-dump/Singletons/T312.golden b/singletons-base/tests/compile-and-dump/Singletons/T312.golden index 1cc43ad6..62fe053a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T312.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T312.golden @@ -36,7 +36,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (BarSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BarSym1KindInference ()) type BarSym2 :: forall a b. a -> b -> b - type family BarSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family BarSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where BarSym2 a0123456789876543210 a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 type BazSym0 :: forall a b. (~>) a ((~>) b b) data BazSym0 :: (~>) a ((~>) b b) @@ -55,10 +55,10 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (BazSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) BazSym1KindInference ()) type BazSym2 :: forall a b. a -> b -> b - type family BazSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family BazSym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where BazSym2 a0123456789876543210 a0123456789876543210 = Baz a0123456789876543210 a0123456789876543210 type Bar_0123456789876543210 :: a -> b -> b - type family Bar_0123456789876543210 (a :: a) (a :: b) :: b where + type family Bar_0123456789876543210 @a @b (a :: a) (a :: b) :: b where Bar_0123456789876543210 _ x = x type Bar_0123456789876543210Sym0 :: (~>) a ((~>) b b) data Bar_0123456789876543210Sym0 :: (~>) a ((~>) b b) @@ -79,7 +79,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Bar_0123456789876543210Sym1KindInference ()) type Bar_0123456789876543210Sym2 :: a -> b -> b - type family Bar_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family Bar_0123456789876543210Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Bar_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Bar_0123456789876543210 a0123456789876543210 a0123456789876543210 data Let0123456789876543210HSym0 a_01234567898765432100123456789876543210 where @@ -118,7 +118,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations type family Let0123456789876543210H a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 (a :: c) (a :: b) :: b where Let0123456789876543210H a_0123456789876543210 a_0123456789876543210 (_ :: c) (x :: b) = x type Baz_0123456789876543210 :: a -> b -> b - type family Baz_0123456789876543210 (a :: a) (a :: b) :: b where + type family Baz_0123456789876543210 @a @b (a :: a) (a :: b) :: b where Baz_0123456789876543210 a_0123456789876543210 a_0123456789876543210 = Apply (Apply (Let0123456789876543210HSym2 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) a_0123456789876543210 type Baz_0123456789876543210Sym0 :: (~>) a ((~>) b b) data Baz_0123456789876543210Sym0 :: (~>) a ((~>) b b) @@ -139,7 +139,7 @@ Singletons/T312.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Baz_0123456789876543210Sym1KindInference ()) type Baz_0123456789876543210Sym2 :: a -> b -> b - type family Baz_0123456789876543210Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where + type family Baz_0123456789876543210Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: b where Baz_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Baz_0123456789876543210 a0123456789876543210 a0123456789876543210 class PFoo a where type family Bar (arg :: a) (arg :: b) :: b diff --git a/singletons-base/tests/compile-and-dump/Singletons/T316.golden b/singletons-base/tests/compile-and-dump/Singletons/T316.golden index a75bd5f3..574ded2e 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T316.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T316.golden @@ -34,9 +34,9 @@ Singletons/T316.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ReplaceAllGTypesSym2KindInference ()) type ReplaceAllGTypesSym3 :: (~>) a ((~>) Type a) -> [Type] -> [a] -> [a] - type family ReplaceAllGTypesSym3 (a0123456789876543210 :: (~>) a ((~>) Type a)) (a0123456789876543210 :: [Type]) (a0123456789876543210 :: [a]) :: [a] where + type family ReplaceAllGTypesSym3 @a (a0123456789876543210 :: (~>) a ((~>) Type a)) (a0123456789876543210 :: [Type]) (a0123456789876543210 :: [a]) :: [a] where ReplaceAllGTypesSym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ReplaceAllGTypes a0123456789876543210 a0123456789876543210 a0123456789876543210 type ReplaceAllGTypes :: (~>) a ((~>) Type a) -> [Type] -> [a] -> [a] - type family ReplaceAllGTypes (a :: (~>) a ((~>) Type a)) (a :: [Type]) (a :: [a]) :: [a] where + type family ReplaceAllGTypes @a (a :: (~>) a ((~>) Type a)) (a :: [Type]) (a :: [a]) :: [a] where ReplaceAllGTypes f types as = Apply (Apply (Apply ZipWithSym0 f) as) types diff --git a/singletons-base/tests/compile-and-dump/Singletons/T326.golden b/singletons-base/tests/compile-and-dump/Singletons/T326.golden index 7d0f4d6b..4a9a89e3 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T326.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T326.golden @@ -20,7 +20,7 @@ Singletons/T326.hs:0:0:: Splicing declarations suppressUnusedWarnings = snd ((,) (:<%>@#@$$###) ()) infixl 9 <%>@#@$$ type (<%>@#@$$$) :: forall a. a -> a -> a - type family (<%>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where + type family (<%>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%>) a0123456789876543210 a0123456789876543210 infixl 9 <%>@#@$$$ type PC1 :: Type -> Constraint @@ -49,7 +49,7 @@ Singletons/T326.hs:0:0:: Splicing declarations suppressUnusedWarnings = snd ((,) (:<%%>@#@$$###) ()) infixl 9 <%%>@#@$$ type (<%%>@#@$$$) :: forall a. a -> a -> a - type family (<%%>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where + type family (<%%>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: a where (<%%>@#@$$$) a0123456789876543210 a0123456789876543210 = (<%%>) a0123456789876543210 a0123456789876543210 infixl 9 <%%>@#@$$$ type PC2 :: Type -> Constraint diff --git a/singletons-base/tests/compile-and-dump/Singletons/T353.golden b/singletons-base/tests/compile-and-dump/Singletons/T353.golden index 7b27978c..a7bc9230 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T353.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T353.golden @@ -59,7 +59,8 @@ Singletons/T353.hs:0:0:: Splicing declarations (f :: k -> Type) (g :: k -> Type) (p :: k). f p -> g p -> Prod f g p - type family MkProdSym2 (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod f g p where + type family MkProdSym2 @k @(f :: k -> Type) @(g :: k + -> Type) @(p :: k) (a0123456789876543210 :: f p) (a0123456789876543210 :: g p) :: Prod f g p where MkProdSym2 a0123456789876543210 a0123456789876543210 = 'MkProd a0123456789876543210 a0123456789876543210 Singletons/T353.hs:0:0:: Splicing declarations genDefunSymbols [''Foo] @@ -86,5 +87,5 @@ Singletons/T353.hs:0:0:: Splicing declarations suppressUnusedWarnings = snd ((,) MkFooSym1KindInference ()) type MkFooSym2 :: forall k k (a :: k) (b :: k). Proxy a -> Proxy b -> Foo a b - type family MkFooSym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo a b where + type family MkFooSym2 @k @k @(a :: k) @(b :: k) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: Foo a b where MkFooSym2 a0123456789876543210 a0123456789876543210 = 'MkFoo a0123456789876543210 a0123456789876543210 diff --git a/singletons-base/tests/compile-and-dump/Singletons/T358.golden b/singletons-base/tests/compile-and-dump/Singletons/T358.golden index 40f6cc9b..e9c8b5b0 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T358.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T358.golden @@ -26,7 +26,7 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations method2a _ = [] method2b _ = [] type Method1Sym0 :: forall f a. f a - type family Method1Sym0 :: f a where + type family Method1Sym0 @f @a :: f a where Method1Sym0 = Method1 class PC1 (f :: k -> Type) where type family Method1 :: f a @@ -39,7 +39,7 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Method2aSym0 where suppressUnusedWarnings = snd ((,) Method2aSym0KindInference ()) type Method2aSym1 :: forall b a. b -> a - type family Method2aSym1 (a0123456789876543210 :: b) :: a where + type family Method2aSym1 @b @a (a0123456789876543210 :: b) :: a where Method2aSym1 a0123456789876543210 = Method2a a0123456789876543210 type Method2bSym0 :: forall b a. (~>) b a data Method2bSym0 :: (~>) b a @@ -50,21 +50,21 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Method2bSym0 where suppressUnusedWarnings = snd ((,) Method2bSym0KindInference ()) type Method2bSym1 :: forall b a. b -> a - type family Method2bSym1 (a0123456789876543210 :: b) :: a where + type family Method2bSym1 @b @a (a0123456789876543210 :: b) :: a where Method2bSym1 a0123456789876543210 = Method2b a0123456789876543210 class PC2 a where type family Method2a (arg :: b) :: a type family Method2b (arg :: b) :: a type Method1_0123456789876543210 :: [a] - type family Method1_0123456789876543210 :: [a] where + type family Method1_0123456789876543210 @a :: [a] where Method1_0123456789876543210 = NilSym0 type Method1_0123456789876543210Sym0 :: [a] - type family Method1_0123456789876543210Sym0 :: [a] where + type family Method1_0123456789876543210Sym0 @a :: [a] where Method1_0123456789876543210Sym0 = Method1_0123456789876543210 instance PC1 [] where type Method1 = Method1_0123456789876543210Sym0 type Method2a_0123456789876543210 :: b -> [a] - type family Method2a_0123456789876543210 (a :: b) :: [a] where + type family Method2a_0123456789876543210 @b @a (a :: b) :: [a] where Method2a_0123456789876543210 _ = NilSym0 type Method2a_0123456789876543210Sym0 :: (~>) b [a] data Method2a_0123456789876543210Sym0 :: (~>) b [a] @@ -76,10 +76,10 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Method2a_0123456789876543210Sym0KindInference ()) type Method2a_0123456789876543210Sym1 :: b -> [a] - type family Method2a_0123456789876543210Sym1 (a0123456789876543210 :: b) :: [a] where + type family Method2a_0123456789876543210Sym1 @b @a (a0123456789876543210 :: b) :: [a] where Method2a_0123456789876543210Sym1 a0123456789876543210 = Method2a_0123456789876543210 a0123456789876543210 type Method2b_0123456789876543210 :: b -> [a] - type family Method2b_0123456789876543210 (a :: b) :: [a] where + type family Method2b_0123456789876543210 @b @a (a :: b) :: [a] where Method2b_0123456789876543210 _ = NilSym0 type Method2b_0123456789876543210Sym0 :: (~>) b [a] data Method2b_0123456789876543210Sym0 :: (~>) b [a] @@ -91,7 +91,7 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) Method2b_0123456789876543210Sym0KindInference ()) type Method2b_0123456789876543210Sym1 :: b -> [a] - type family Method2b_0123456789876543210Sym1 (a0123456789876543210 :: b) :: [a] where + type family Method2b_0123456789876543210Sym1 @b @a (a0123456789876543210 :: b) :: [a] where Method2b_0123456789876543210Sym1 a0123456789876543210 = Method2b_0123456789876543210 a0123456789876543210 instance PC2 [a] where type Method2a a = Apply Method2a_0123456789876543210Sym0 a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T367.golden b/singletons-base/tests/compile-and-dump/Singletons/T367.golden index 5a8cd5b2..434eeedf 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T367.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T367.golden @@ -22,10 +22,10 @@ Singletons/T367.hs:(0,0)-(0,0): Splicing declarations Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings = snd ((,) Const'Sym1KindInference ()) type Const'Sym2 :: a -> b -> a - type family Const'Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family Const'Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where Const'Sym2 a0123456789876543210 a0123456789876543210 = Const' a0123456789876543210 a0123456789876543210 type Const' :: a -> b -> a - type family Const' (a :: a) (a :: b) :: a where + type family Const' @a @b (a :: a) (a :: b) :: a where Const' x _ = x sConst' :: (forall (t :: a) (t :: b). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T371.golden b/singletons-base/tests/compile-and-dump/Singletons/T371.golden index c0799cf9..2b1ffead 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T371.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T371.golden @@ -14,7 +14,7 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations = Y1 | Y2 (X a) deriving Show type X1Sym0 :: forall (a :: Type). X a - type family X1Sym0 :: X a where + type family X1Sym0 @(a :: Type) :: X a where X1Sym0 = X1 type X2Sym0 :: forall (a :: Type). (~>) (Y a) (X a) data X2Sym0 :: (~>) (Y a) (X a) @@ -25,10 +25,10 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings X2Sym0 where suppressUnusedWarnings = snd ((,) X2Sym0KindInference ()) type X2Sym1 :: forall (a :: Type). Y a -> X a - type family X2Sym1 (a0123456789876543210 :: Y a) :: X a where + type family X2Sym1 @(a :: Type) (a0123456789876543210 :: Y a) :: X a where X2Sym1 a0123456789876543210 = X2 a0123456789876543210 type Y1Sym0 :: forall (a :: Type). Y a - type family Y1Sym0 :: Y a where + type family Y1Sym0 @(a :: Type) :: Y a where Y1Sym0 = Y1 type Y2Sym0 :: forall (a :: Type). (~>) (X a) (Y a) data Y2Sym0 :: (~>) (X a) (Y a) @@ -39,11 +39,11 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Y2Sym0 where suppressUnusedWarnings = snd ((,) Y2Sym0KindInference ()) type Y2Sym1 :: forall (a :: Type). X a -> Y a - type family Y2Sym1 (a0123456789876543210 :: X a) :: Y a where + type family Y2Sym1 @(a :: Type) (a0123456789876543210 :: X a) :: Y a where Y2Sym1 a0123456789876543210 = Y2 a0123456789876543210 type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> X a -> GHC.Types.Symbol -> GHC.Types.Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: X a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where + type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: X a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210 _ X1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "X1") a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (X2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "X2 ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (X a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) @@ -77,13 +77,13 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> X a -> GHC.Types.Symbol -> GHC.Types.Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: X a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: X a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (X a) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural -> Y a -> GHC.Types.Symbol -> GHC.Types.Symbol - type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: Y a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where + type family ShowsPrec_0123456789876543210 @a (a :: GHC.Num.Natural.Natural) (a :: Y a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210 _ Y1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "Y1") a_0123456789876543210 ShowsPrec_0123456789876543210 p_0123456789876543210 (Y2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Y2 ")) (Apply (Apply ShowsPrecSym0 (FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210 type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) (Y a) ((~>) GHC.Types.Symbol GHC.Types.Symbol)) @@ -117,7 +117,7 @@ Singletons/T371.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ()) type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural -> Y a -> GHC.Types.Symbol -> GHC.Types.Symbol - type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Y a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where + type family ShowsPrec_0123456789876543210Sym3 @a (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: Y a) (a0123456789876543210 :: GHC.Types.Symbol) :: GHC.Types.Symbol where ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210 instance PShow (Y a) where type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378a.golden b/singletons-base/tests/compile-and-dump/Singletons/T378a.golden index 3e4eb043..fc11f828 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T378a.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T378a.golden @@ -19,16 +19,16 @@ Singletons/T378a.hs:(0,0)-(0,0): Splicing declarations Proxy3 :: forall a. Proxy a Proxy4 :: forall k (a :: k). Proxy a type Proxy1Sym0 :: Proxy a - type family Proxy1Sym0 :: Proxy a where + type family Proxy1Sym0 @a :: Proxy a where Proxy1Sym0 = Proxy1 type Proxy2Sym0 :: Proxy (a :: k) - type family Proxy2Sym0 :: Proxy (a :: k) where + type family Proxy2Sym0 @k @(a :: k) :: Proxy (a :: k) where Proxy2Sym0 = Proxy2 type Proxy3Sym0 :: forall a. Proxy a - type family Proxy3Sym0 :: Proxy a where + type family Proxy3Sym0 @a :: Proxy a where Proxy3Sym0 = Proxy3 type Proxy4Sym0 :: forall k (a :: k). Proxy a - type family Proxy4Sym0 :: Proxy a where + type family Proxy4Sym0 @k @(a :: k) :: Proxy a where Proxy4Sym0 = Proxy4 type ConstBASym0 :: forall b a. (~>) a ((~>) b a) data ConstBASym0 :: (~>) a ((~>) b a) @@ -47,10 +47,10 @@ Singletons/T378a.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (ConstBASym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) ConstBASym1KindInference ()) type ConstBASym2 :: forall b a. a -> b -> a - type family ConstBASym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family ConstBASym2 @b @a (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where ConstBASym2 a0123456789876543210 a0123456789876543210 = ConstBA a0123456789876543210 a0123456789876543210 type ConstBA :: forall b a. a -> b -> a - type family ConstBA (a :: a) (a :: b) :: a where + type family ConstBA @b @a (a :: a) (a :: b) :: a where ConstBA @b @a (x :: a) (_ :: b) = x sConstBA :: forall b a (t :: a) (t :: b). Sing t diff --git a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden index bf234afd..a207ce8f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T378b.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T378b.golden @@ -71,7 +71,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (FSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) FSym1KindInference ()) type FSym2 :: forall b a. a -> b -> () - type family FSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: () where + type family FSym2 @b @a (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: () where FSym2 a0123456789876543210 a0123456789876543210 = F a0123456789876543210 a0123456789876543210 type NatMinus :: Nat -> Nat -> Nat type family NatMinus (a :: Nat) (a :: Nat) :: Nat where @@ -79,7 +79,7 @@ Singletons/T378b.hs:(0,0)-(0,0): Splicing declarations NatMinus ('Succ a) ('Succ b) = Apply (Apply NatMinusSym0 a) b NatMinus ('Succ wild_0123456789876543210) 'Zero = Let0123456789876543210ASym1 wild_0123456789876543210 type F :: forall b a. a -> b -> () - type family F (a :: a) (a :: b) :: () where + type family F @b @a (a :: a) (a :: b) :: () where F @b @a (_ :: a) (_ :: b) = Tuple0Sym0 type PC :: forall b a. a -> b -> Constraint class PC x y diff --git a/singletons-base/tests/compile-and-dump/Singletons/T410.golden b/singletons-base/tests/compile-and-dump/Singletons/T410.golden index 8427a2be..44b259a6 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T410.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T410.golden @@ -29,7 +29,7 @@ Singletons/T410.hs:(0,0)-(0,0): Splicing declarations Data.Singletons.TH.SuppressUnusedWarnings.suppressUnusedWarnings = snd ((,) EqualsSym1KindInference ()) type EqualsSym2 :: forall a. a -> a -> Bool - type family EqualsSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Bool where + type family EqualsSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Bool where EqualsSym2 a0123456789876543210 a0123456789876543210 = Equals a0123456789876543210 a0123456789876543210 class PEq a where type family Equals (arg :: a) (arg :: a) :: Bool diff --git a/singletons-base/tests/compile-and-dump/Singletons/T412.golden b/singletons-base/tests/compile-and-dump/Singletons/T412.golden index a82f6e43..b757f4e1 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T412.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T412.golden @@ -83,7 +83,7 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkD1Sym1KindInference ()) infixr 5 `MkD1Sym1` type MkD1Sym2 :: forall a b. a -> b -> D1 a b - type family MkD1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D1 a b where + type family MkD1Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D1 a b where MkD1Sym2 a0123456789876543210 a0123456789876543210 = MkD1 a0123456789876543210 a0123456789876543210 infixr 5 `MkD1Sym2` type D1BSym0 :: forall a b. (~>) (D1 a b) b @@ -96,7 +96,7 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) D1BSym0KindInference ()) infixr 5 `D1BSym0` type D1BSym1 :: forall a b. D1 a b -> b - type family D1BSym1 (a0123456789876543210 :: D1 a b) :: b where + type family D1BSym1 @a @b (a0123456789876543210 :: D1 a b) :: b where D1BSym1 a0123456789876543210 = D1B a0123456789876543210 infixr 5 `D1BSym1` type D1ASym0 :: forall a b. (~>) (D1 a b) a @@ -109,14 +109,14 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) D1ASym0KindInference ()) infixr 5 `D1ASym0` type D1ASym1 :: forall a b. D1 a b -> a - type family D1ASym1 (a0123456789876543210 :: D1 a b) :: a where + type family D1ASym1 @a @b (a0123456789876543210 :: D1 a b) :: a where D1ASym1 a0123456789876543210 = D1A a0123456789876543210 infixr 5 `D1ASym1` type D1B :: forall a b. D1 a b -> b - type family D1B (a :: D1 a b) :: b where + type family D1B @a @b (a :: D1 a b) :: b where D1B @a @b (MkD1 _ field :: D1 a b) = field type D1A :: forall a b. D1 a b -> a - type family D1A (a :: D1 a b) :: a where + type family D1A @a @b (a :: D1 a b) :: a where D1A @a @b (MkD1 field _ :: D1 a b) = field infixr 5 `D1B` infixr 5 `D1A` @@ -140,7 +140,7 @@ Singletons/T412.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) M1Sym1KindInference ()) infix 6 `M1Sym1` type M1Sym2 :: forall a b. a -> b -> Bool - type family M1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where + type family M1Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where M1Sym2 a0123456789876543210 a0123456789876543210 = M1 a0123456789876543210 a0123456789876543210 infix 6 `M1Sym2` class PC1 a b where @@ -220,7 +220,7 @@ Singletons/T412.hs:0:0:: Splicing declarations suppressUnusedWarnings = snd ((,) M2Sym1KindInference ()) infix 6 `M2Sym1` type M2Sym2 :: forall a b. a -> b -> Bool - type family M2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where + type family M2Sym2 @a @b (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: Bool where M2Sym2 a0123456789876543210 a0123456789876543210 = M2 a0123456789876543210 a0123456789876543210 infix 6 `M2Sym2` type PC2 :: Type -> Type -> Constraint @@ -308,7 +308,7 @@ Singletons/T412.hs:0:0:: Splicing declarations suppressUnusedWarnings = snd ((,) MkD2Sym1KindInference ()) infixr 5 `MkD2Sym1` type MkD2Sym2 :: forall (a :: Type) (b :: Type). a -> b -> D2 a b - type family MkD2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 a b where + type family MkD2Sym2 @(a :: Type) @(b :: Type) (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: D2 a b where MkD2Sym2 a0123456789876543210 a0123456789876543210 = 'MkD2 a0123456789876543210 a0123456789876543210 infixr 5 `MkD2Sym2` infixr 5 `D2A` @@ -322,7 +322,7 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings D2BSym0 where suppressUnusedWarnings = snd ((,) D2BSym0KindInference ()) type D2BSym1 :: forall (a :: Type) (b :: Type). D2 a b -> b - type family D2BSym1 (a0123456789876543210 :: D2 a b) :: b where + type family D2BSym1 @(a :: Type) @(b :: Type) (a0123456789876543210 :: D2 a b) :: b where D2BSym1 a0123456789876543210 = D2B a0123456789876543210 type D2ASym0 :: forall (a :: Type) (b :: Type). (~>) (D2 a b) a data D2ASym0 :: (~>) (D2 a b) a @@ -333,13 +333,13 @@ Singletons/T412.hs:0:0:: Splicing declarations instance SuppressUnusedWarnings D2ASym0 where suppressUnusedWarnings = snd ((,) D2ASym0KindInference ()) type D2ASym1 :: forall (a :: Type) (b :: Type). D2 a b -> a - type family D2ASym1 (a0123456789876543210 :: D2 a b) :: a where + type family D2ASym1 @(a :: Type) @(b :: Type) (a0123456789876543210 :: D2 a b) :: a where D2ASym1 a0123456789876543210 = D2A a0123456789876543210 type D2B :: forall (a :: Type) (b :: Type). D2 a b -> b - type family D2B (a :: D2 a b) :: b where + type family D2B @(a :: Type) @(b :: Type) (a :: D2 a b) :: b where D2B @a @b ('MkD2 _ field :: D2 a b) = field type D2A :: forall (a :: Type) (b :: Type). D2 a b -> a - type family D2A (a :: D2 a b) :: a where + type family D2A @(a :: Type) @(b :: Type) (a :: D2 a b) :: a where D2A @a @b ('MkD2 field _ :: D2 a b) = field sD2B :: forall (a :: Type) (b :: Type) (t :: D2 a b). Sing t diff --git a/singletons-base/tests/compile-and-dump/Singletons/T433.golden b/singletons-base/tests/compile-and-dump/Singletons/T433.golden index 3a7cff36..f1f52791 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T433.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T433.golden @@ -192,7 +192,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Id8Sym0 where suppressUnusedWarnings = snd ((,) Id8Sym0KindInference ()) type Id8Sym1 :: a -> a - type family Id8Sym1 (a0123456789876543210 :: a) :: a where + type family Id8Sym1 @a (a0123456789876543210 :: a) :: a where Id8Sym1 a0123456789876543210 = Id8 a0123456789876543210 data Id7Sym0 a0123456789876543210 where @@ -212,7 +212,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Id6Sym0 where suppressUnusedWarnings = snd ((,) Id6Sym0KindInference ()) type Id6Sym1 :: a -> a - type family Id6Sym1 (a0123456789876543210 :: a) :: a where + type family Id6Sym1 @a (a0123456789876543210 :: a) :: a where Id6Sym1 a0123456789876543210 = Id6 a0123456789876543210 type Id5Sym0 :: forall a. (~>) a a data Id5Sym0 :: (~>) a a @@ -223,7 +223,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Id5Sym0 where suppressUnusedWarnings = snd ((,) Id5Sym0KindInference ()) type Id5Sym1 :: forall a. a -> a - type family Id5Sym1 (a0123456789876543210 :: a) :: a where + type family Id5Sym1 @a (a0123456789876543210 :: a) :: a where Id5Sym1 a0123456789876543210 = Id5 a0123456789876543210 type Id4Sym0 :: forall a. (~>) a a data Id4Sym0 :: (~>) a a @@ -234,7 +234,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Id4Sym0 where suppressUnusedWarnings = snd ((,) Id4Sym0KindInference ()) type Id4Sym1 :: forall a. a -> a - type family Id4Sym1 (a0123456789876543210 :: a) :: a where + type family Id4Sym1 @a (a0123456789876543210 :: a) :: a where Id4Sym1 a0123456789876543210 = Id4 a0123456789876543210 type Id3Sym0 :: (~>) a a data Id3Sym0 :: (~>) a a @@ -245,7 +245,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Id3Sym0 where suppressUnusedWarnings = snd ((,) Id3Sym0KindInference ()) type Id3Sym1 :: a -> a - type family Id3Sym1 (a0123456789876543210 :: a) :: a where + type family Id3Sym1 @a (a0123456789876543210 :: a) :: a where Id3Sym1 a0123456789876543210 = Id3 a0123456789876543210 type Id2Sym0 :: forall a. (~>) a a data Id2Sym0 :: (~>) a a @@ -256,7 +256,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Id2Sym0 where suppressUnusedWarnings = snd ((,) Id2Sym0KindInference ()) type Id2Sym1 :: forall a. a -> a - type family Id2Sym1 (a0123456789876543210 :: a) :: a where + type family Id2Sym1 @a (a0123456789876543210 :: a) :: a where Id2Sym1 a0123456789876543210 = Id2 a0123456789876543210 type FooSym0 :: forall a. (~>) a () data FooSym0 :: (~>) a () @@ -267,7 +267,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FooSym0 where suppressUnusedWarnings = snd ((,) FooSym0KindInference ()) type FooSym1 :: forall a. a -> () - type family FooSym1 (a0123456789876543210 :: a) :: () where + type family FooSym1 @a (a0123456789876543210 :: a) :: () where FooSym1 a0123456789876543210 = Foo a0123456789876543210 data FSym0 a0123456789876543210 where @@ -295,7 +295,7 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Konst2Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Konst2Sym1KindInference ()) type Konst2Sym2 :: a -> Maybe Bool -> a - type family Konst2Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe Bool) :: a where + type family Konst2Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Maybe Bool) :: a where Konst2Sym2 a0123456789876543210 a0123456789876543210 = Konst2 a0123456789876543210 a0123456789876543210 type Konst1Sym0 :: (~>) a ((~>) Bool a) data Konst1Sym0 :: (~>) a ((~>) Bool a) @@ -314,36 +314,36 @@ Singletons/T433.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (Konst1Sym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) Konst1Sym1KindInference ()) type Konst1Sym2 :: a -> Bool -> a - type family Konst1Sym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Bool) :: a where + type family Konst1Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: Bool) :: a where Konst1Sym2 a0123456789876543210 a0123456789876543210 = Konst1 a0123456789876543210 a0123456789876543210 type Id8 :: a -> a - type family Id8 (a :: a) :: a where + type family Id8 @a (a :: a) :: a where Id8 x = Apply (Apply (Let0123456789876543210GSym1 x) x) TrueSym0 type family Id7 a where Id7 (x :: b) = Let0123456789876543210GSym2 b x type Id6 :: a -> a - type family Id6 (a :: a) :: a where + type family Id6 @a (a :: a) :: a where Id6 (x :: b) = Let0123456789876543210GSym2 b x type Id5 :: forall a. a -> a - type family Id5 (a :: a) :: a where + type family Id5 @a (a :: a) :: a where Id5 @a (a_0123456789876543210 :: a) = Apply (Let0123456789876543210GSym2 a a_0123456789876543210) a_0123456789876543210 type Id4 :: forall a. a -> a - type family Id4 (a :: a) :: a where + type family Id4 @a (a :: a) :: a where Id4 @a (x :: a :: a) = Apply IdSym0 (x :: a) type Id3 :: a -> a - type family Id3 (a :: a) :: a where + type family Id3 @a (a :: a) :: a where Id3 (x :: b) = Apply IdSym0 (x :: b) type Id2 :: forall a. a -> a - type family Id2 (a :: a) :: a where + type family Id2 @a (a :: a) :: a where Id2 @a (x :: a) = Apply IdSym0 (x :: a) type Foo :: forall a. a -> () - type family Foo (a :: a) :: () where + type family Foo @a (a :: a) :: () where Foo @a (x :: a) = Apply (Apply ConstSym0 Tuple0Sym0) (NothingSym0 :: Maybe a) type family F a where F local = Let0123456789876543210GSym1 local type Konst2 :: a -> Maybe Bool -> a - type family Konst2 (a :: a) (a :: Maybe Bool) :: a where + type family Konst2 @a (a :: a) (a :: Maybe Bool) :: a where Konst2 x _ = x type Konst1 :: a -> Bool -> a - type family Konst1 (a :: a) (a :: Bool) :: a where + type family Konst1 @a (a :: a) (a :: Bool) :: a where Konst1 x _ = x diff --git a/singletons-base/tests/compile-and-dump/Singletons/T443.golden b/singletons-base/tests/compile-and-dump/Singletons/T443.golden index e3a8d57d..da26b7ec 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T443.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T443.golden @@ -27,7 +27,7 @@ Singletons/T443.hs:(0,0)-(0,0): Splicing declarations type family SSym1 (a0123456789876543210 :: Nat) :: Nat where SSym1 a0123456789876543210 = S a0123456789876543210 type VNilSym0 :: Vec Z a - type family VNilSym0 :: Vec Z a where + type family VNilSym0 @a :: Vec Z a where VNilSym0 = VNil type (:>@#@$) :: (~>) a ((~>) (Vec n a) (Vec (S n) a)) data (:>@#@$) :: (~>) a ((~>) (Vec n a) (Vec (S n) a)) @@ -46,7 +46,7 @@ Singletons/T443.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings ((:>@#@$$) a0123456789876543210) where suppressUnusedWarnings = snd ((,) (::>@#@$$###) ()) type (:>@#@$$$) :: a -> Vec n a -> Vec (S n) a - type family (:>@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: Vec n a) :: Vec (S n) a where + type family (:>@#@$$$) @a @n (a0123456789876543210 :: a) (a0123456789876543210 :: Vec n a) :: Vec (S n) a where (:>@#@$$$) a0123456789876543210 a0123456789876543210 = (:>) a0123456789876543210 a0123456789876543210 type TailSym0 :: (~>) (Vec (S n) a) (Vec n a) data TailSym0 :: (~>) (Vec (S n) a) (Vec n a) @@ -57,7 +57,7 @@ Singletons/T443.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings TailSym0 where suppressUnusedWarnings = snd ((,) TailSym0KindInference ()) type TailSym1 :: Vec (S n) a -> Vec n a - type family TailSym1 (a0123456789876543210 :: Vec (S n) a) :: Vec n a where + type family TailSym1 @n @a (a0123456789876543210 :: Vec (S n) a) :: Vec n a where TailSym1 a0123456789876543210 = Tail a0123456789876543210 type HeadSym0 :: (~>) (Vec (S n) a) a data HeadSym0 :: (~>) (Vec (S n) a) a @@ -68,13 +68,13 @@ Singletons/T443.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings HeadSym0 where suppressUnusedWarnings = snd ((,) HeadSym0KindInference ()) type HeadSym1 :: Vec (S n) a -> a - type family HeadSym1 (a0123456789876543210 :: Vec (S n) a) :: a where + type family HeadSym1 @n @a (a0123456789876543210 :: Vec (S n) a) :: a where HeadSym1 a0123456789876543210 = Head a0123456789876543210 type Tail :: Vec (S n) a -> Vec n a - type family Tail (a :: Vec (S n) a) :: Vec n a where + type family Tail @n @a (a :: Vec (S n) a) :: Vec n a where Tail ((:>) _ field) = field type Head :: Vec (S n) a -> a - type family Head (a :: Vec (S n) a) :: a where + type family Head @n @a (a :: Vec (S n) a) :: a where Head ((:>) field _) = field sTail :: (forall (t :: Vec (S n) a). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T450.golden b/singletons-base/tests/compile-and-dump/Singletons/T450.golden index 2d6296c4..5823fff1 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T450.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T450.golden @@ -128,7 +128,7 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) PMkFunctionSym0KindInference ()) type PMkFunctionSym1 :: forall (a :: Type) (b :: Type). (~>) a b -> PFunction a b - type family PMkFunctionSym1 (a0123456789876543210 :: (~>) a b) :: PFunction a b where + type family PMkFunctionSym1 @(a :: Type) @(b :: Type) (a0123456789876543210 :: (~>) a b) :: PFunction a b where PMkFunctionSym1 a0123456789876543210 = 'PMkFunction a0123456789876543210 type SFunction :: forall (a :: Type) (b :: Type). PFunction a b -> Type @@ -176,11 +176,11 @@ Singletons/T450.hs:(0,0)-(0,0): Splicing declarations = snd ((,) ComposeFunctionSym1KindInference ()) type ComposeFunctionSym2 :: PFunction b c -> PFunction a b -> PFunction a c - type family ComposeFunctionSym2 (a0123456789876543210 :: PFunction b c) (a0123456789876543210 :: PFunction a b) :: PFunction a c where + type family ComposeFunctionSym2 @b @c @a (a0123456789876543210 :: PFunction b c) (a0123456789876543210 :: PFunction a b) :: PFunction a c where ComposeFunctionSym2 a0123456789876543210 a0123456789876543210 = ComposeFunction a0123456789876543210 a0123456789876543210 type ComposeFunction :: PFunction b c -> PFunction a b -> PFunction a c - type family ComposeFunction (a :: PFunction b c) (a :: PFunction a b) :: PFunction a c where + type family ComposeFunction @b @c @a (a :: PFunction b c) (a :: PFunction a b) :: PFunction a c where ComposeFunction ('PMkFunction (f :: (~>) b c)) ('PMkFunction (g :: (~>) a b)) = Apply PMkFunctionSym0 (Apply (Apply (.@#@$) f) g :: (~>) a c) sComposeFunction :: (forall (t :: PFunction b c) (t :: PFunction a b). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T470.golden b/singletons-base/tests/compile-and-dump/Singletons/T470.golden index 745d4b85..32d3ad92 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T470.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T470.golden @@ -23,7 +23,7 @@ Singletons/T470.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkT1Sym0 where suppressUnusedWarnings = snd ((,) MkT1Sym0KindInference ()) type MkT1Sym1 :: a -> T a - type family MkT1Sym1 (a0123456789876543210 :: a) :: T a where + type family MkT1Sym1 @a (a0123456789876543210 :: a) :: T a where MkT1Sym1 a0123456789876543210 = MkT1 a0123456789876543210 type MkT2Sym0 :: (~>) Void (T a) data MkT2Sym0 :: (~>) Void (T a) @@ -34,7 +34,7 @@ Singletons/T470.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkT2Sym0 where suppressUnusedWarnings = snd ((,) MkT2Sym0KindInference ()) type MkT2Sym1 :: Void -> T a - type family MkT2Sym1 (a0123456789876543210 :: Void) :: T a where + type family MkT2Sym1 @a (a0123456789876543210 :: Void) :: T a where MkT2Sym1 a0123456789876543210 = MkT2 a0123456789876543210 type MkSSym0 :: (~>) Bool S data MkSSym0 :: (~>) Bool S @@ -88,9 +88,9 @@ Singletons/T470.hs:(0,0)-(0,0): Splicing declarations liftSing = SMkS instance SingI (MkSSym0 :: (~>) Bool S) where sing = singFun1 @MkSSym0 SMkS - Singletons/T470.hs:0:0: warning: [GHC-39584] {-# UNPACK #-} pragmas are ignored by `singletons-th`. | 6 | $(singletons [d| | ^^^^^^^^^^^^^^^... + diff --git a/singletons-base/tests/compile-and-dump/Singletons/T489.golden b/singletons-base/tests/compile-and-dump/Singletons/T489.golden index 4cb48bc2..0a2f1c9c 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T489.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T489.golden @@ -33,14 +33,14 @@ Singletons/T489.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings BlahSym0 where suppressUnusedWarnings = snd ((,) BlahSym0KindInference ()) type BlahSym1 :: Maybe a -> [a] - type family BlahSym1 (a0123456789876543210 :: Maybe a) :: [a] where + type family BlahSym1 @a (a0123456789876543210 :: Maybe a) :: [a] where BlahSym1 a0123456789876543210 = Blah a0123456789876543210 type Flurmp :: Maybe () -> () type family Flurmp (a :: Maybe ()) :: () where Flurmp ('Nothing @_) = Tuple0Sym0 Flurmp ('Just '()) = Tuple0Sym0 type Blah :: Maybe a -> [a] - type family Blah (a :: Maybe a) :: [a] where + type family Blah @a (a :: Maybe a) :: [a] where Blah ('Just @a x) = Apply (Apply (:@#@$) (x :: a)) NilSym0 Blah ('Nothing @a) = NilSym0 :: [a] sFlurmp :: diff --git a/singletons-base/tests/compile-and-dump/Singletons/T511.golden b/singletons-base/tests/compile-and-dump/Singletons/T511.golden index 76153f65..616de8ae 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T511.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T511.golden @@ -1,4 +1,3 @@ - Singletons/T511.hs:0:0: error: [GHC-39584] Q monad failure | 7 | $(singletons [d| @@ -6,8 +5,9 @@ Singletons/T511.hs:0:0: error: [GHC-39584] Q monad failure Singletons/T511.hs:0:0: error: [GHC-39584] `singletons-th` does not support partial applications of (->) - In the type: Data.Proxy.Proxy (->) + In the type: GHC.Internal.Data.Proxy.Proxy (->) | 7 | $(singletons [d| | ^^^^^^^^^^^^^^^... + diff --git a/singletons-base/tests/compile-and-dump/Singletons/T536.golden b/singletons-base/tests/compile-and-dump/Singletons/T536.golden index 54d2386b..4f7c21b9 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T536.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T536.golden @@ -76,24 +76,26 @@ Singletons/T536.hs:(0,0)-(0,0): Splicing declarations Data.Singletons.Decide.SDecide PMessage where (Data.Singletons.Decide.%~) (SMkMessage a) (SMkMessage b) = case (Data.Singletons.Decide.%~) a b of - Data.Singletons.Decide.Proved Data.Type.Equality.Refl - -> Data.Singletons.Decide.Proved Data.Type.Equality.Refl + Data.Singletons.Decide.Proved GHC.Internal.Data.Type.Equality.Refl + -> Data.Singletons.Decide.Proved + GHC.Internal.Data.Type.Equality.Refl Data.Singletons.Decide.Disproved contra -> Data.Singletons.Decide.Disproved (\ refl -> case refl of - Data.Type.Equality.Refl -> contra Data.Type.Equality.Refl) + GHC.Internal.Data.Type.Equality.Refl + -> contra GHC.Internal.Data.Type.Equality.Refl) instance Eq (SMessage (z :: PMessage)) where (==) _ _ = True instance Data.Singletons.Decide.SDecide Text => - Data.Type.Equality.TestEquality (SMessage :: PMessage - -> Type) where - Data.Type.Equality.testEquality + GHC.Internal.Data.Type.Equality.TestEquality (SMessage :: PMessage + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality instance Data.Singletons.Decide.SDecide Text => - Data.Type.Coercion.TestCoercion (SMessage :: PMessage - -> Type) where - Data.Type.Coercion.testCoercion + GHC.Internal.Data.Type.Coercion.TestCoercion (SMessage :: PMessage + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion deriving instance Data.Singletons.ShowSing.ShowSing Text => Show (SMessage (z :: PMessage)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T555.golden b/singletons-base/tests/compile-and-dump/Singletons/T555.golden index 4388f18a..922e3c6a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T555.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T555.golden @@ -190,13 +190,13 @@ Singletons/T555.hs:(0,0)-(0,0): Splicing declarations (%~) SQuaternion SQuaternion = Proved Refl instance Eq (SMyPropKind (z :: MyPropKind)) where (==) _ _ = True - instance Data.Type.Equality.TestEquality (SMyPropKind :: MyPropKind - -> Type) where - Data.Type.Equality.testEquality + instance GHC.Internal.Data.Type.Equality.TestEquality (SMyPropKind :: MyPropKind + -> Type) where + GHC.Internal.Data.Type.Equality.testEquality = Data.Singletons.Decide.decideEquality - instance Data.Type.Coercion.TestCoercion (SMyPropKind :: MyPropKind - -> Type) where - Data.Type.Coercion.testCoercion + instance GHC.Internal.Data.Type.Coercion.TestCoercion (SMyPropKind :: MyPropKind + -> Type) where + GHC.Internal.Data.Type.Coercion.testCoercion = Data.Singletons.Decide.decideCoercion instance Ord (SMyPropKind (z :: MyPropKind)) where compare _ _ = EQ diff --git a/singletons-base/tests/compile-and-dump/Singletons/T567.golden b/singletons-base/tests/compile-and-dump/Singletons/T567.golden index 6e2fca69..c80b261b 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T567.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T567.golden @@ -20,16 +20,16 @@ Singletons/T567.hs:(0,0)-(0,0): Splicing declarations type D4 :: forall k. forall (a :: k) -> Proxy a -> Type data D4 (x :: j) (p :: Proxy x) = MkD4 type MkD1Sym0 :: forall x p. D1 x p - type family MkD1Sym0 :: D1 x p where + type family MkD1Sym0 @x @p :: D1 x p where MkD1Sym0 = MkD1 type MkD2Sym0 :: forall j (x :: j) p. D2 x p - type family MkD2Sym0 :: D2 x p where + type family MkD2Sym0 @j @(x :: j) @p :: D2 x p where MkD2Sym0 = MkD2 type MkD3Sym0 :: forall x (p :: Proxy x). D3 x p - type family MkD3Sym0 :: D3 x p where + type family MkD3Sym0 @x @(p :: Proxy x) :: D3 x p where MkD3Sym0 = MkD3 type MkD4Sym0 :: forall j (x :: j) (p :: Proxy x). D4 x p - type family MkD4Sym0 :: D4 x p where + type family MkD4Sym0 @j @(x :: j) @(p :: Proxy x) :: D4 x p where MkD4Sym0 = MkD4 type SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type data SD1 :: forall k (x :: k) (p :: Proxy x). D1 x p -> Type diff --git a/singletons-base/tests/compile-and-dump/Singletons/T571.golden b/singletons-base/tests/compile-and-dump/Singletons/T571.golden index 9d01608b..890f34cb 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T571.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T571.golden @@ -14,10 +14,10 @@ Singletons/T571.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings FSym0 where suppressUnusedWarnings = snd ((,) FSym0KindInference ()) type FSym1 :: a -> a - type family FSym1 (a0123456789876543210 :: a) :: a where + type family FSym1 @a (a0123456789876543210 :: a) :: a where FSym1 a0123456789876543210 = F a0123456789876543210 type F :: a -> a - type family F (a :: a) :: a where + type family F @a (a :: a) :: a where F x = x sF :: (forall (t :: a). Sing t -> Sing (Apply FSym0 t :: a) :: Type) @@ -48,10 +48,10 @@ Singletons/T571.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (GSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) GSym1KindInference ()) type GSym2 :: (~>) a a -> a -> a - type family GSym2 (a0123456789876543210 :: (~>) a a) (a0123456789876543210 :: a) :: a where + type family GSym2 @a (a0123456789876543210 :: (~>) a a) (a0123456789876543210 :: a) :: a where GSym2 a0123456789876543210 a0123456789876543210 = G a0123456789876543210 a0123456789876543210 type G :: (~>) a a -> a -> a - type family G (a :: (~>) a a) (a :: a) :: a where + type family G @a (a :: (~>) a a) (a :: a) :: a where G f x = Apply f x sG :: (forall (t :: (~>) a a) (t :: a). diff --git a/singletons-base/tests/compile-and-dump/Singletons/T585.golden b/singletons-base/tests/compile-and-dump/Singletons/T585.golden index 5f1d563b..6ec5166a 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T585.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T585.golden @@ -22,10 +22,10 @@ Singletons/T585.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings (KonstSym1 a0123456789876543210) where suppressUnusedWarnings = snd ((,) KonstSym1KindInference ()) type KonstSym2 :: forall a {b}. a -> b -> a - type family KonstSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where + type family KonstSym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: b) :: a where KonstSym2 a0123456789876543210 a0123456789876543210 = Konst a0123456789876543210 a0123456789876543210 type Konst :: forall a {b}. a -> b -> a - type family Konst (a :: a) (a :: b) :: a where + type family Konst @a (a :: a) (a :: b) :: a where Konst @a (x :: a) (_ :: b) = x sKonst :: forall a {b} (t :: a) (t :: b). Sing t diff --git a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden index 9d827b84..4d357738 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden @@ -19,7 +19,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations type instance Apply BarSym0 a0123456789876543210 = BarSym1 a0123456789876543210 instance SuppressUnusedWarnings BarSym0 where suppressUnusedWarnings - = Data.Tuple.snd ((,) BarSym0KindInference ()) + = GHC.Internal.Data.Tuple.snd ((,) BarSym0KindInference ()) type BarSym1 :: Bool -> (~>) Bool Foo data BarSym1 (a0123456789876543210 :: Bool) :: (~>) Bool Foo where @@ -28,7 +28,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations type instance Apply (BarSym1 a0123456789876543210) a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 instance SuppressUnusedWarnings (BarSym1 a0123456789876543210) where suppressUnusedWarnings - = Data.Tuple.snd ((,) BarSym1KindInference ()) + = GHC.Internal.Data.Tuple.snd ((,) BarSym1KindInference ()) type BarSym2 :: Bool -> Bool -> Foo type family BarSym2 (a0123456789876543210 :: Bool) (a0123456789876543210 :: Bool) :: Foo where BarSym2 a0123456789876543210 a0123456789876543210 = Bar a0123456789876543210 a0123456789876543210 @@ -159,7 +159,8 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations ISym0 a0123456789876543210 type instance Apply ISym0 a0123456789876543210 = I a0123456789876543210 instance SuppressUnusedWarnings ISym0 where - suppressUnusedWarnings = Data.Tuple.snd ((,) ISym0KindInference ()) + suppressUnusedWarnings + = GHC.Internal.Data.Tuple.snd ((,) ISym0KindInference ()) type ISym1 :: Bool -> Bool type family ISym1 (a0123456789876543210 :: Bool) :: Bool where ISym1 a0123456789876543210 = I a0123456789876543210 @@ -170,7 +171,8 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations HSym0 a0123456789876543210 type instance Apply HSym0 a0123456789876543210 = H a0123456789876543210 instance SuppressUnusedWarnings HSym0 where - suppressUnusedWarnings = Data.Tuple.snd ((,) HSym0KindInference ()) + suppressUnusedWarnings + = GHC.Internal.Data.Tuple.snd ((,) HSym0KindInference ()) type HSym1 :: Bool -> Bool type family HSym1 (a0123456789876543210 :: Bool) :: Bool where HSym1 a0123456789876543210 = H a0123456789876543210 @@ -183,7 +185,8 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations GSym0 a0123456789876543210 type instance Apply GSym0 a0123456789876543210 = G a0123456789876543210 instance SuppressUnusedWarnings GSym0 where - suppressUnusedWarnings = Data.Tuple.snd ((,) GSym0KindInference ()) + suppressUnusedWarnings + = GHC.Internal.Data.Tuple.snd ((,) GSym0KindInference ()) type GSym1 :: Bool -> Bool type family GSym1 (a0123456789876543210 :: Bool) :: Bool where GSym1 a0123456789876543210 = G a0123456789876543210 @@ -194,7 +197,8 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations FSym0 a0123456789876543210 type instance Apply FSym0 a0123456789876543210 = F a0123456789876543210 instance SuppressUnusedWarnings FSym0 where - suppressUnusedWarnings = Data.Tuple.snd ((,) FSym0KindInference ()) + suppressUnusedWarnings + = GHC.Internal.Data.Tuple.snd ((,) FSym0KindInference ()) type FSym1 :: Bool -> Bool type family FSym1 (a0123456789876543210 :: Bool) :: Bool where FSym1 a0123456789876543210 = F a0123456789876543210 @@ -210,7 +214,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations type instance Apply NotSym0 a0123456789876543210 = Not a0123456789876543210 instance SuppressUnusedWarnings NotSym0 where suppressUnusedWarnings - = Data.Tuple.snd ((,) NotSym0KindInference ()) + = GHC.Internal.Data.Tuple.snd ((,) NotSym0KindInference ()) type NotSym1 :: Bool -> Bool type family NotSym1 (a0123456789876543210 :: Bool) :: Bool where NotSym1 a0123456789876543210 = Not a0123456789876543210 @@ -222,9 +226,9 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations type instance Apply IdSym0 a0123456789876543210 = Id a0123456789876543210 instance SuppressUnusedWarnings IdSym0 where suppressUnusedWarnings - = Data.Tuple.snd ((,) IdSym0KindInference ()) + = GHC.Internal.Data.Tuple.snd ((,) IdSym0KindInference ()) type IdSym1 :: a -> a - type family IdSym1 (a0123456789876543210 :: a) :: a where + type family IdSym1 @a (a0123456789876543210 :: a) :: a where IdSym1 a0123456789876543210 = Id a0123456789876543210 type OtherwiseSym0 :: Bool type family OtherwiseSym0 :: Bool where @@ -268,7 +272,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations Not 'True = FalseSym0 Not 'False = TrueSym0 type Id :: a -> a - type family Id (a :: a) :: a where + type family Id @a (a :: a) :: a where Id x = x type Otherwise :: Bool type family Otherwise :: Bool where @@ -301,14 +305,14 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations (forall (t :: a). Sing t -> Sing (Apply IdSym0 t :: a) :: Type) sOtherwise :: (Sing (OtherwiseSym0 :: Bool) :: Type) sM - = GHC.Base.id + = GHC.Internal.Base.id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SCons _ (SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) SNil) -> sY_0123456789876543210) sL - = GHC.Base.id + = GHC.Internal.Base.id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) @@ -325,13 +329,13 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun1 @IdSym0 sId) SFalse)) SNil) sK - = GHC.Base.id + = GHC.Internal.Base.id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SBar _ (sY_0123456789876543210 :: Sing y_0123456789876543210) -> sY_0123456789876543210) sJ - = GHC.Base.id + = GHC.Internal.Base.id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SBar (sY_0123456789876543210 :: Sing y_0123456789876543210) _ @@ -342,7 +346,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations (applySing (singFun1 @HSym0 sH) SFalse) sI (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing - (GHC.Base.id + (GHC.Internal.Base.id @(Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of STuple2 _ (sY_0123456789876543210 :: Sing y_0123456789876543210) @@ -350,7 +354,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations sA_0123456789876543210 sH (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing - (GHC.Base.id + (GHC.Internal.Base.id @(Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of STuple2 (sY_0123456789876543210 :: Sing y_0123456789876543210) _ @@ -362,7 +366,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations (singFun1 @GSym0 sG) sG (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing - (GHC.Base.id + (GHC.Internal.Base.id @(Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SCons _ @@ -371,7 +375,7 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations sA_0123456789876543210 sF (sA_0123456789876543210 :: Sing a_0123456789876543210) = applySing - (GHC.Base.id + (GHC.Internal.Base.id @(Sing (Case_0123456789876543210 a_0123456789876543210 X_0123456789876543210Sym0)) (case sX_0123456789876543210 of SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden index eb25b21d..6e390106 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TypeAbstractions.golden @@ -107,7 +107,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkD1Sym1KindInference ()) type MkD1Sym2 :: forall j k (a :: j) (b :: k). Proxy a -> Proxy b -> D1 @j @k a b - type family MkD1Sym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D1 @j @k a b where + type family MkD1Sym2 @j @k @(a :: j) @(b :: k) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D1 @j @k a b where MkD1Sym2 a0123456789876543210 a0123456789876543210 = MkD1 a0123456789876543210 a0123456789876543210 type MkD2Sym0 :: forall x y @@ -131,7 +131,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkD2Sym1KindInference ()) type MkD2Sym2 :: forall x y (a :: x) (b :: y). Proxy a -> Proxy b -> D2 @x @y a b - type family MkD2Sym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D2 @x @y a b where + type family MkD2Sym2 @x @y @(a :: x) @(b :: y) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D2 @x @y a b where MkD2Sym2 a0123456789876543210 a0123456789876543210 = MkD2 a0123456789876543210 a0123456789876543210 type MkD3Sym0 :: forall j (a :: j) @@ -155,7 +155,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations suppressUnusedWarnings = snd ((,) MkD3Sym1KindInference ()) type MkD3Sym2 :: forall j (a :: j) k (b :: k). Proxy a -> Proxy b -> D3 @j a @k b - type family MkD3Sym2 (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D3 @j a @k b where + type family MkD3Sym2 @j @(a :: j) @k @(b :: k) (a0123456789876543210 :: Proxy a) (a0123456789876543210 :: Proxy b) :: D3 @j a @k b where MkD3Sym2 a0123456789876543210 a0123456789876543210 = MkD3 a0123456789876543210 a0123456789876543210 type MkD4Sym0 :: forall a. (~>) a (D4 @a) data MkD4Sym0 :: (~>) a (D4 @a) @@ -166,7 +166,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings MkD4Sym0 where suppressUnusedWarnings = snd ((,) MkD4Sym0KindInference ()) type MkD4Sym1 :: forall a. a -> D4 @a - type family MkD4Sym1 (a0123456789876543210 :: a) :: D4 @a where + type family MkD4Sym1 @a (a0123456789876543210 :: a) :: D4 @a where MkD4Sym1 a0123456789876543210 = MkD4 a0123456789876543210 type Meth1Sym0 :: forall a b. (~>) (Proxy a) (Proxy b) data Meth1Sym0 :: (~>) (Proxy a) (Proxy b) @@ -177,7 +177,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Meth1Sym0 where suppressUnusedWarnings = snd ((,) Meth1Sym0KindInference ()) type Meth1Sym1 :: forall a b. Proxy a -> Proxy b - type family Meth1Sym1 (a0123456789876543210 :: Proxy a) :: Proxy b where + type family Meth1Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where Meth1Sym1 a0123456789876543210 = Meth1 a0123456789876543210 type PC1 :: forall j k. j -> k -> Constraint class PC1 @j @k (a :: j) (b :: k) where @@ -191,7 +191,7 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Meth2Sym0 where suppressUnusedWarnings = snd ((,) Meth2Sym0KindInference ()) type Meth2Sym1 :: forall a b. Proxy a -> Proxy b - type family Meth2Sym1 (a0123456789876543210 :: Proxy a) :: Proxy b where + type family Meth2Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where Meth2Sym1 a0123456789876543210 = Meth2 a0123456789876543210 type PC2 :: forall j k. j -> k -> Constraint class PC2 @x @y (a :: x) (b :: y) where @@ -205,13 +205,13 @@ Singletons/TypeAbstractions.hs:(0,0)-(0,0): Splicing declarations instance SuppressUnusedWarnings Meth3Sym0 where suppressUnusedWarnings = snd ((,) Meth3Sym0KindInference ()) type Meth3Sym1 :: forall a b. Proxy a -> Proxy b - type family Meth3Sym1 (a0123456789876543210 :: Proxy a) :: Proxy b where + type family Meth3Sym1 @a @b (a0123456789876543210 :: Proxy a) :: Proxy b where Meth3Sym1 a0123456789876543210 = Meth3 a0123456789876543210 type PC3 :: forall j. j -> forall k. k -> Constraint class PC3 @j (a :: j) @k (b :: k) where type family Meth3 (arg :: Proxy a) :: Proxy b type Meth4Sym0 :: forall a. a - type family Meth4Sym0 :: a where + type family Meth4Sym0 @a :: a where Meth4Sym0 = Meth4 type PC4 :: forall (a :: Type). Constraint class PC4 @a where