Skip to content

Commit

Permalink
Draft: singletons-base: Accept GHC 9.10 golden test output
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
RyanGlScott committed May 4, 2024
1 parent 27537b0 commit 2fbce8b
Show file tree
Hide file tree
Showing 74 changed files with 518 additions and 472 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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) =>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion singletons-base/tests/compile-and-dump/Promote/T361.golden
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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).
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand Down
12 changes: 6 additions & 6 deletions singletons-base/tests/compile-and-dump/Singletons/Classes.golden
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 ::
Expand Down
Loading

0 comments on commit 2fbce8b

Please sign in to comment.