Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support scoped type variables in class/instance declarations #591

Merged
merged 2 commits into from
Jun 6, 2024
Merged

Support scoped type variables in class/instance declarations #591

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
fa8e376
Simplify singling of instance method types
RyanGlScott May 12, 2024
076e70d
Support scoped type variables in class/instance declarations
RyanGlScott May 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -634,7 +634,6 @@ instance POrd Bool where
type Compare 'True 'True = 'EQ

instance SOrd Bool where
sCompare :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (Compare x y)
sCompare SFalse SFalse = SEQ
sCompare SFalse STrue = SLT
sCompare STrue SFalse = SGT
Expand Down
1 change: 1 addition & 0 deletions singletons-base/tests/SingletonsBaseTestSuite.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,7 @@ tests =
, compileAndDumpStdTest "T563"
, compileAndDumpStdTest "T567"
, compileAndDumpStdTest "T571"
, compileAndDumpStdTest "T581"
, compileAndDumpStdTest "T585"
, compileAndDumpStdTest "TypeAbstractions"
],
Expand Down
36 changes: 0 additions & 36 deletions singletons-base/tests/compile-and-dump/GradingClient/Database.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,11 +92,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
toSing (Succ (b :: Demote Nat))
= case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
instance SEq Nat => SEq Nat where
(%==) ::
forall (t1 :: Nat) (t2 :: Nat). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Nat ((~>) Nat Bool)
-> Type) t1) t2)
(%==) SZero SZero = STrue
(%==) SZero (SSucc _) = SFalse
(%==) (SSucc _) SZero = SFalse
Expand All @@ -107,11 +102,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210
instance SOrd Nat => SOrd Nat where
sCompare ::
forall (t1 :: Nat) (t2 :: Nat). Sing t1
-> Sing t2
-> Sing (Apply (Apply (CompareSym0 :: TyFun Nat ((~>) Nat Ordering)
-> Type) t1) t2)
sCompare SZero SZero
= applySing
(applySing
Expand Down Expand Up @@ -1626,11 +1616,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
= case toSing b :: SomeSing [Attribute] of
SomeSing c -> SomeSing (SSch c)
instance (SEq U, SEq Nat) => SEq U where
(%==) ::
forall (t1 :: U) (t2 :: U). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun U ((~>) U Bool)
-> Type) t1) t2)
(%==) SBOOL SBOOL = STrue
(%==) SBOOL SSTRING = SFalse
(%==) SBOOL SNAT = SFalse
Expand Down Expand Up @@ -1661,14 +1646,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(applySing (singFun2 @(==@#@$) (%==)) sA_0123456789876543210)
sB_0123456789876543210)
instance (SShow U, SShow Nat) => SShow U where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: U)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) U ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SBOOL
Expand Down Expand Up @@ -1728,14 +1705,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
sArg_0123456789876543210)))))
sA_0123456789876543210
instance SShow AChar where
sShowsPrec ::
forall (t1 :: GHC.Num.Natural.Natural)
(t2 :: AChar)
(t3 :: Symbol). Sing t1
-> Sing t2
-> Sing t3
-> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) AChar ((~>) Symbol Symbol))
-> Type) t1) t2) t3)
sShowsPrec
_
SCA
Expand Down Expand Up @@ -1945,11 +1914,6 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations
(singFun2 @ShowStringSym0 sShowString) (sing :: Sing "CZ"))
sA_0123456789876543210
instance SEq AChar where
(%==) ::
forall (t1 :: AChar) (t2 :: AChar). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun AChar ((~>) AChar Bool)
-> Type) t1) t2)
(%==) SCA SCA = STrue
(%==) SCA SCB = SFalse
(%==) SCA SCC = SFalse
Expand Down
34 changes: 12 additions & 22 deletions singletons-base/tests/compile-and-dump/Singletons/BoundedDeriving.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,31 +115,31 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
instance PBounded Foo2 where
type MinBound = MinBound_0123456789876543210Sym0
type MaxBound = MaxBound_0123456789876543210Sym0
type MinBound_0123456789876543210 :: Foo3 a
type MinBound_0123456789876543210 :: forall a. Foo3 a
type family MinBound_0123456789876543210 @a :: Foo3 a where
MinBound_0123456789876543210 = Apply Foo3Sym0 MinBoundSym0
type MinBound_0123456789876543210Sym0 :: Foo3 a
MinBound_0123456789876543210 @a = Apply Foo3Sym0 MinBoundSym0
type MinBound_0123456789876543210Sym0 :: forall a. Foo3 a
type family MinBound_0123456789876543210Sym0 @a :: Foo3 a where
MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210
type MaxBound_0123456789876543210 :: Foo3 a
type MaxBound_0123456789876543210 :: forall a. Foo3 a
type family MaxBound_0123456789876543210 @a :: Foo3 a where
MaxBound_0123456789876543210 = Apply Foo3Sym0 MaxBoundSym0
type MaxBound_0123456789876543210Sym0 :: Foo3 a
MaxBound_0123456789876543210 @a = Apply Foo3Sym0 MaxBoundSym0
type MaxBound_0123456789876543210Sym0 :: forall a. Foo3 a
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 MinBound_0123456789876543210 :: forall a b. Foo4 a b
type family MinBound_0123456789876543210 @a @b :: Foo4 a b where
MinBound_0123456789876543210 = Foo41Sym0
type MinBound_0123456789876543210Sym0 :: Foo4 a b
MinBound_0123456789876543210 @a @b = Foo41Sym0
type MinBound_0123456789876543210Sym0 :: forall a b. Foo4 a b
type family MinBound_0123456789876543210Sym0 @a @b :: Foo4 a b where
MinBound_0123456789876543210Sym0 = MinBound_0123456789876543210
type MaxBound_0123456789876543210 :: Foo4 a b
type MaxBound_0123456789876543210 :: forall a b. Foo4 a b
type family MaxBound_0123456789876543210 @a @b :: Foo4 a b where
MaxBound_0123456789876543210 = Foo42Sym0
type MaxBound_0123456789876543210Sym0 :: Foo4 a b
MaxBound_0123456789876543210 @a @b = Foo42Sym0
type MaxBound_0123456789876543210Sym0 :: forall a b. Foo4 a b
type family MaxBound_0123456789876543210Sym0 @a @b :: Foo4 a b where
MaxBound_0123456789876543210Sym0 = MaxBound_0123456789876543210
instance PBounded (Foo4 a b) where
Expand Down Expand Up @@ -220,28 +220,18 @@ Singletons/BoundedDeriving.hs:(0,0)-(0,0): Splicing declarations
of
(,) (SomeSing c) (SomeSing c) -> SomeSing (SPair c c)
instance SBounded Foo1 where
sMinBound :: Sing (MinBoundSym0 :: Foo1)
sMaxBound :: Sing (MaxBoundSym0 :: Foo1)
sMinBound = SFoo1
sMaxBound = SFoo1
instance SBounded Foo2 where
sMinBound :: Sing (MinBoundSym0 :: Foo2)
sMaxBound :: Sing (MaxBoundSym0 :: Foo2)
sMinBound = SA
sMaxBound = SE
instance SBounded a => SBounded (Foo3 a) where
sMinBound :: Sing (MinBoundSym0 :: Foo3 a)
sMaxBound :: Sing (MaxBoundSym0 :: Foo3 a)
sMinBound = applySing (singFun1 @Foo3Sym0 SFoo3) sMinBound
sMaxBound = applySing (singFun1 @Foo3Sym0 SFoo3) sMaxBound
instance SBounded (Foo4 a b) where
sMinBound :: Sing (MinBoundSym0 :: Foo4 a b)
sMaxBound :: Sing (MaxBoundSym0 :: Foo4 a b)
sMinBound = SFoo41
sMaxBound = SFoo42
instance SBounded Bool => SBounded Pair where
sMinBound :: Sing (MinBoundSym0 :: Pair)
sMaxBound :: Sing (MaxBoundSym0 :: Pair)
sMinBound
= applySing
(applySing (singFun2 @PairSym0 SPair) sMinBound) sMinBound
Expand Down
37 changes: 7 additions & 30 deletions singletons-base/tests/compile-and-dump/Singletons/Classes.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -159,10 +159,10 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
type family (<=>@#@$$$) @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where
(<=>@#@$$$) a0123456789876543210 a0123456789876543210 = (<=>) a0123456789876543210 a0123456789876543210
infix 4 <=>@#@$$$
type TFHelper_0123456789876543210 :: a -> a -> Ordering
type TFHelper_0123456789876543210 :: forall a. a -> a -> Ordering
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)
TFHelper_0123456789876543210 @a (a_0123456789876543210 :: a) (a_0123456789876543210 :: a) = Apply (Apply MycompareSym0 a_0123456789876543210) a_0123456789876543210
type TFHelper_0123456789876543210Sym0 :: forall a. (~>) a ((~>) a Ordering)
data TFHelper_0123456789876543210Sym0 :: (~>) a ((~>) a Ordering)
where
TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
Expand All @@ -171,7 +171,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
type TFHelper_0123456789876543210Sym1 :: a -> (~>) a Ordering
type TFHelper_0123456789876543210Sym1 :: forall a. a
-> (~>) a Ordering
data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: a) :: (~>) a Ordering
where
TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
Expand All @@ -180,7 +181,8 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
suppressUnusedWarnings
= snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
type TFHelper_0123456789876543210Sym2 :: a -> a -> Ordering
type TFHelper_0123456789876543210Sym2 :: forall a. a
-> a -> Ordering
type family TFHelper_0123456789876543210Sym2 @a (a0123456789876543210 :: a) (a0123456789876543210 :: a) :: Ordering where
TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
class PMyOrd a where
Expand Down Expand Up @@ -376,31 +378,16 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
(singFun2 @MycompareSym0 sMycompare) sA_0123456789876543210)
sA_0123456789876543210
instance SMyOrd Nat where
sMycompare ::
(forall (t :: Nat) (t :: Nat).
Sing t
-> Sing t
-> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
sMycompare SZero SZero = SEQ
sMycompare SZero (SSucc _) = SLT
sMycompare (SSucc _) SZero = SGT
sMycompare (SSucc (sN :: Sing n)) (SSucc (sM :: Sing m))
= applySing (applySing (singFun2 @MycompareSym0 sMycompare) sM) sN
instance SMyOrd () where
sMycompare ::
(forall (t :: ()) (t :: ()).
Sing t
-> Sing t
-> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
sMycompare _ (sA_0123456789876543210 :: Sing a_0123456789876543210)
= applySing
(applySing (singFun2 @ConstSym0 sConst) SEQ) sA_0123456789876543210
instance SMyOrd Foo where
sMycompare ::
(forall (t :: Foo) (t :: Foo).
Sing t
-> Sing t
-> Sing (Apply (Apply MycompareSym0 t) t :: Ordering) :: Type)
sMycompare
(sA_0123456789876543210 :: Sing a_0123456789876543210)
(sA_0123456789876543210 :: Sing a_0123456789876543210)
Expand All @@ -409,11 +396,6 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
(singFun2 @FooCompareSym0 sFooCompare) sA_0123456789876543210)
sA_0123456789876543210
instance SEq Foo2 where
(%==) ::
forall (t1 :: Foo2) (t2 :: Foo2). Sing t1
-> Sing t2
-> Sing (Apply (Apply ((==@#@$) :: TyFun Foo2 ((~>) Foo2 Bool)
-> Type) t1) t2)
(%==) SF SF = STrue
(%==) SG SG = STrue
(%==) SF SG = SFalse
Expand Down Expand Up @@ -596,11 +578,6 @@ Singletons/Classes.hs:(0,0)-(0,0): Splicing declarations
= case toSing b :: SomeSing Nat' of
SomeSing c -> SomeSing (SSucc' c)
instance SMyOrd Nat' where
sMycompare ::
forall (t :: Nat') (t :: Nat'). Sing t
-> Sing t
-> Sing (Apply (Apply (MycompareSym0 :: TyFun Nat' ((~>) Nat' Ordering)
-> Type) t) t)
sMycompare SZero' SZero' = SEQ
sMycompare SZero' (SSucc' _) = SLT
sMycompare (SSucc' _) SZero' = SGT
Expand Down
5 changes: 0 additions & 5 deletions singletons-base/tests/compile-and-dump/Singletons/Classes2.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,11 +74,6 @@ Singletons/Classes2.hs:(0,0)-(0,0): Splicing declarations
= case toSing b :: SomeSing NatFoo of
SomeSing c -> SomeSing (SSuccFoo c)
instance SMyOrd NatFoo where
sMycompare ::
forall (t1 :: NatFoo) (t2 :: NatFoo). Sing t1
-> Sing t2
-> Sing (Apply (Apply (MycompareSym0 :: TyFun NatFoo ((~>) NatFoo Ordering)
-> Type) t1) t2)
sMycompare SZeroFoo SZeroFoo = SEQ
sMycompare SZeroFoo (SSuccFoo _) = SLT
sMycompare (SSuccFoo _) SZeroFoo = SGT
Expand Down
Loading