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.
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
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
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
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
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
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
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
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

0 comments on commit 2fbce8b

Please sign in to comment.