packages feed

singletons-1.1: tests/compile-and-dump/Singletons/Records.ghc78.template

Singletons/Records.hs:0:0: Splicing declarations
    singletons
      [d| data Record a = MkRecord {field1 :: a, field2 :: Bool} |]
  ======>
    Singletons/Records.hs:(0,0)-(0,0)
    data Record a = MkRecord {field1 :: a, field2 :: Bool}
    type Field1Sym1 (t :: Record a) = Field1 t
    instance SuppressUnusedWarnings Field1Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Field1Sym0KindInference GHC.Tuple.())
    data Field1Sym0 (l :: TyFun (Record a) a)
      = forall arg. KindOf (Apply Field1Sym0 arg) ~ KindOf (Field1Sym1 arg) =>
        Field1Sym0KindInference
    type instance Apply Field1Sym0 l = Field1Sym1 l
    type Field2Sym1 (t :: Record a) = Field2 t
    instance SuppressUnusedWarnings Field2Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Field2Sym0KindInference GHC.Tuple.())
    data Field2Sym0 (l :: TyFun (Record a) Bool)
      = forall arg. KindOf (Apply Field2Sym0 arg) ~ KindOf (Field2Sym1 arg) =>
        Field2Sym0KindInference
    type instance Apply Field2Sym0 l = Field2Sym1 l
    type family Field1 (a :: Record a) :: a where
      Field1 (MkRecord field z) = field
    type family Field2 (a :: Record a) :: Bool where
      Field2 (MkRecord z field) = field
    type MkRecordSym2 (t :: a) (t :: Bool) = MkRecord t t
    instance SuppressUnusedWarnings MkRecordSym1 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) MkRecordSym1KindInference GHC.Tuple.())
    data MkRecordSym1 (l :: a) (l :: TyFun Bool (Record a))
      = forall arg. KindOf (Apply (MkRecordSym1 l) arg) ~ KindOf (MkRecordSym2 l arg) =>
        MkRecordSym1KindInference
    type instance Apply (MkRecordSym1 l) l = MkRecordSym2 l l
    instance SuppressUnusedWarnings MkRecordSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) MkRecordSym0KindInference GHC.Tuple.())
    data MkRecordSym0 (l :: TyFun a (TyFun Bool (Record a) -> *))
      = forall arg. KindOf (Apply MkRecordSym0 arg) ~ KindOf (MkRecordSym1 arg) =>
        MkRecordSym0KindInference
    type instance Apply MkRecordSym0 l = MkRecordSym1 l
    data instance Sing (z :: Record a)
      = forall (n :: a) (n :: Bool). z ~ MkRecord n n =>
        SMkRecord {sField1 :: Sing n, sField2 :: Sing n}
    type SRecord (z :: Record a) = Sing z
    instance SingKind (KProxy :: KProxy a) =>
             SingKind (KProxy :: KProxy (Record a)) where
      type DemoteRep (KProxy :: KProxy (Record a)) = Record (DemoteRep (KProxy :: KProxy a))
      fromSing (SMkRecord b b) = MkRecord (fromSing b) (fromSing b)
      toSing (MkRecord b b)
        = case
              GHC.Tuple.(,)
                (toSing b :: SomeSing (KProxy :: KProxy a))
                (toSing b :: SomeSing (KProxy :: KProxy Bool))
          of {
            GHC.Tuple.(,) (SomeSing c) (SomeSing c)
              -> SomeSing (SMkRecord c c) }
    instance (SingI n, SingI n) =>
             SingI (MkRecord (n :: a) (n :: Bool)) where
      sing = SMkRecord sing sing