Singletons/Records.hs:(0,0)-(0,0): Splicing declarations singletons [d| data Record a = MkRecord {field1 :: a, field2 :: Bool} |] ======> data Record a = MkRecord {field1 :: a, field2 :: Bool} type Field1Sym1 (t :: Record a0123456789) = Field1 t instance SuppressUnusedWarnings Field1Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Field1Sym0KindInference GHC.Tuple.()) data Field1Sym0 (l :: TyFun (Record a0123456789) a0123456789) = forall arg. KindOf (Apply Field1Sym0 arg) ~ KindOf (Field1Sym1 arg) => Field1Sym0KindInference type instance Apply Field1Sym0 l = Field1Sym1 l type Field2Sym1 (t :: Record a0123456789) = Field2 t instance SuppressUnusedWarnings Field2Sym0 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) Field2Sym0KindInference GHC.Tuple.()) data Field2Sym0 (l :: TyFun (Record a0123456789) 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_0123456789) = field type family Field2 (a :: Record a) :: Bool where Field2 (MkRecord _z_0123456789 field) = field type MkRecordSym2 (t :: a0123456789) (t :: Bool) = MkRecord t t instance SuppressUnusedWarnings MkRecordSym1 where suppressUnusedWarnings _ = snd (GHC.Tuple.(,) MkRecordSym1KindInference GHC.Tuple.()) data MkRecordSym1 (l :: a0123456789) (l :: TyFun Bool (Record a0123456789)) = 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 a0123456789 (TyFun Bool (Record a0123456789) -> *)) = 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 :: a), sField2 :: Sing (n :: Bool)} type SRecord = (Sing :: Record a -> *) 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