singletons-2.7: tests/compile-and-dump/Singletons/T204.golden
Singletons/T204.hs:(0,0)-(0,0): Splicing declarations
let
sing_data_con_name :: Name -> Name
sing_data_con_name n
= case nameBase n of
':' : '%' : rest -> mkName $ ":^%" ++ rest
_ -> singledDataConName defaultOptions n
in
withOptions
defaultOptions {singledDataConName = sing_data_con_name}
$ singletons
$ lift
[d| data Ratio1 a = a :% a
data Ratio2 a = a :%% a |]
======>
data Ratio1 a = a :% a
data Ratio2 a = a :%% a
type (:%@#@$) :: forall a. (~>) a ((~>) a (Ratio1 a))
data (:%@#@$) a0123456789876543210
where
(::%@#@$###) :: SameKind (Apply (:%@#@$) arg) ((:%@#@$$) arg) =>
(:%@#@$) a0123456789876543210
type instance Apply (:%@#@$) a0123456789876543210 = (:%@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:%@#@$) where
suppressUnusedWarnings = snd (((,) (::%@#@$###)) ())
type (:%@#@$$) :: forall a. a -> (~>) a (Ratio1 a)
data (:%@#@$$) a0123456789876543210 a0123456789876543210
where
(::%@#@$$###) :: SameKind (Apply ((:%@#@$$) a0123456789876543210) arg) ((:%@#@$$$) a0123456789876543210 arg) =>
(:%@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:%@#@$$) a0123456789876543210) a0123456789876543210 = (:%@#@$$$) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:%@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (::%@#@$$###)) ())
type (:%@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) =
(:%) a0123456789876543210 a0123456789876543210 :: Ratio1 a
type (:%%@#@$) :: forall a. (~>) a ((~>) a (Ratio2 a))
data (:%%@#@$) a0123456789876543210
where
(::%%@#@$###) :: SameKind (Apply (:%%@#@$) arg) ((:%%@#@$$) arg) =>
(:%%@#@$) a0123456789876543210
type instance Apply (:%%@#@$) a0123456789876543210 = (:%%@#@$$) a0123456789876543210
instance SuppressUnusedWarnings (:%%@#@$) where
suppressUnusedWarnings = snd (((,) (::%%@#@$###)) ())
type (:%%@#@$$) :: forall a. a -> (~>) a (Ratio2 a)
data (:%%@#@$$) a0123456789876543210 a0123456789876543210
where
(::%%@#@$$###) :: SameKind (Apply ((:%%@#@$$) a0123456789876543210) arg) ((:%%@#@$$$) a0123456789876543210 arg) =>
(:%%@#@$$) a0123456789876543210 a0123456789876543210
type instance Apply ((:%%@#@$$) a0123456789876543210) a0123456789876543210 = (:%%@#@$$$) a0123456789876543210 a0123456789876543210
instance SuppressUnusedWarnings ((:%%@#@$$) a0123456789876543210) where
suppressUnusedWarnings = snd (((,) (::%%@#@$$###)) ())
type (:%%@#@$$$) (a0123456789876543210 :: a) (a0123456789876543210 :: a) =
(:%%) a0123456789876543210 a0123456789876543210 :: Ratio2 a
data SRatio1 :: forall a. Ratio1 a -> GHC.Types.Type
where
(:^%) :: forall a (n :: a) (n :: a).
(Sing n) -> (Sing n) -> SRatio1 ((:%) n n :: Ratio1 a)
type instance Sing @(Ratio1 a) = SRatio1
instance SingKind a => SingKind (Ratio1 a) where
type Demote (Ratio1 a) = Ratio1 (Demote a)
fromSing ((:^%) b b) = ((:%) (fromSing b)) (fromSing b)
toSing ((:%) (b :: Demote a) (b :: Demote a))
= case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing a) of {
(,) (SomeSing c) (SomeSing c) -> SomeSing (((:^%) c) c) }
data SRatio2 :: forall a. Ratio2 a -> GHC.Types.Type
where
(:^%%) :: forall a (n :: a) (n :: a).
(Sing n) -> (Sing n) -> SRatio2 ((:%%) n n :: Ratio2 a)
type instance Sing @(Ratio2 a) = SRatio2
instance SingKind a => SingKind (Ratio2 a) where
type Demote (Ratio2 a) = Ratio2 (Demote a)
fromSing ((:^%%) b b) = ((:%%) (fromSing b)) (fromSing b)
toSing ((:%%) (b :: Demote a) (b :: Demote a))
= case ((,) (toSing b :: SomeSing a)) (toSing b :: SomeSing a) of {
(,) (SomeSing c) (SomeSing c) -> SomeSing (((:^%%) c) c) }
instance (SingI n, SingI n) => SingI ((:%) (n :: a) (n :: a)) where
sing = ((:^%) sing) sing
instance SingI ((:%@#@$) :: (~>) a ((~>) a (Ratio1 a))) where
sing = (singFun2 @(:%@#@$)) (:^%)
instance SingI d =>
SingI ((:%@#@$$) (d :: a) :: (~>) a (Ratio1 a)) where
sing = (singFun1 @((:%@#@$$) (d :: a))) ((:^%) (sing @d))
instance (SingI n, SingI n) =>
SingI ((:%%) (n :: a) (n :: a)) where
sing = ((:^%%) sing) sing
instance SingI ((:%%@#@$) :: (~>) a ((~>) a (Ratio2 a))) where
sing = (singFun2 @(:%%@#@$)) (:^%%)
instance SingI d =>
SingI ((:%%@#@$$) (d :: a) :: (~>) a (Ratio2 a)) where
sing = (singFun1 @((:%%@#@$$) (d :: a))) ((:^%%) (sing @d))