Records.golden

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 MkRecordSym0 :: forall a. (~>) a ((~>) Bool (Record a))
    data MkRecordSym0 :: (~>) a ((~>) Bool (Record a))
      where
        MkRecordSym0KindInference :: SameKind (Apply MkRecordSym0 arg) (MkRecordSym1 arg) =>
                                     MkRecordSym0 a0123456789876543210
    type instance Apply MkRecordSym0 a0123456789876543210 = MkRecordSym1 a0123456789876543210
    instance SuppressUnusedWarnings MkRecordSym0 where
      suppressUnusedWarnings = snd ((,) MkRecordSym0KindInference ())
    type MkRecordSym1 :: forall a. a -> (~>) Bool (Record a)
    data MkRecordSym1 (a0123456789876543210 :: a) :: (~>) Bool (Record a)
      where
        MkRecordSym1KindInference :: SameKind (Apply (MkRecordSym1 a0123456789876543210) arg) (MkRecordSym2 a0123456789876543210 arg) =>
                                     MkRecordSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (MkRecordSym1 a0123456789876543210) a0123456789876543210 = MkRecord a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (MkRecordSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) MkRecordSym1KindInference ())
    type MkRecordSym2 :: forall a. a -> Bool -> Record a
    type family MkRecordSym2 (a0123456789876543210 :: a) (a0123456789876543210 :: Bool) :: Record a where
      MkRecordSym2 a0123456789876543210 a0123456789876543210 = MkRecord a0123456789876543210 a0123456789876543210
    type Field2Sym0 :: forall a. (~>) (Record a) Bool
    data Field2Sym0 :: (~>) (Record a) Bool
      where
        Field2Sym0KindInference :: SameKind (Apply Field2Sym0 arg) (Field2Sym1 arg) =>
                                   Field2Sym0 a0123456789876543210
    type instance Apply Field2Sym0 a0123456789876543210 = Field2 a0123456789876543210
    instance SuppressUnusedWarnings Field2Sym0 where
      suppressUnusedWarnings = snd ((,) Field2Sym0KindInference ())
    type Field2Sym1 :: forall a. Record a -> Bool
    type family Field2Sym1 (a0123456789876543210 :: Record a) :: Bool where
      Field2Sym1 a0123456789876543210 = Field2 a0123456789876543210
    type Field1Sym0 :: forall a. (~>) (Record a) a
    data Field1Sym0 :: (~>) (Record a) a
      where
        Field1Sym0KindInference :: SameKind (Apply Field1Sym0 arg) (Field1Sym1 arg) =>
                                   Field1Sym0 a0123456789876543210
    type instance Apply Field1Sym0 a0123456789876543210 = Field1 a0123456789876543210
    instance SuppressUnusedWarnings Field1Sym0 where
      suppressUnusedWarnings = snd ((,) Field1Sym0KindInference ())
    type Field1Sym1 :: forall a. Record a -> a
    type family Field1Sym1 (a0123456789876543210 :: Record a) :: a where
      Field1Sym1 a0123456789876543210 = Field1 a0123456789876543210
    type Field2 :: forall a. Record a -> Bool
    type family Field2 (a :: Record a) :: Bool where
      Field2 (MkRecord _ field) = field
    type Field1 :: forall a. Record a -> a
    type family Field1 (a :: Record a) :: a where
      Field1 (MkRecord field _) = field
    sField2 ::
      forall a (t :: Record a). Sing t
                                -> Sing (Apply Field2Sym0 t :: Bool)
    sField1 ::
      forall a (t :: Record a). Sing t -> Sing (Apply Field1Sym0 t :: a)
    sField2 (SMkRecord _ (sField :: Sing field)) = sField
    sField1 (SMkRecord (sField :: Sing field) _) = sField
    instance SingI (Field2Sym0 :: (~>) (Record a) Bool) where
      sing = singFun1 @Field2Sym0 sField2
    instance SingI (Field1Sym0 :: (~>) (Record a) a) where
      sing = singFun1 @Field1Sym0 sField1
    data SRecord :: forall a. Record a -> Type
      where
        SMkRecord :: forall a (n :: a) (n :: Bool).
                     (Sing n) -> (Sing n) -> SRecord (MkRecord n n :: Record a)
    type instance Sing @(Record a) = SRecord
    instance SingKind a => SingKind (Record a) where
      type Demote (Record a) = Record (Demote a)
      fromSing (SMkRecord b b) = MkRecord (fromSing b) (fromSing b)
      toSing (MkRecord (b :: Demote a) (b :: Demote Bool))
        = case (,) (toSing b :: SomeSing a) (toSing b :: SomeSing Bool) of
            (,) (SomeSing c) (SomeSing c) -> SomeSing (SMkRecord c c)
    instance (SingI n, SingI n) =>
             SingI (MkRecord (n :: a) (n :: Bool)) where
      sing = SMkRecord sing sing
    instance SingI n => SingI1 (MkRecord (n :: a)) where
      liftSing = SMkRecord sing
    instance SingI2 MkRecord where
      liftSing2 = SMkRecord
    instance SingI (MkRecordSym0 :: (~>) a ((~>) Bool (Record a))) where
      sing = singFun2 @MkRecordSym0 SMkRecord
    instance SingI d =>
             SingI (MkRecordSym1 (d :: a) :: (~>) Bool (Record a)) where
      sing = singFun1 @(MkRecordSym1 (d :: a)) (SMkRecord (sing @d))
    instance SingI1 (MkRecordSym1 :: a -> (~>) Bool (Record a)) where
      liftSing (s :: Sing (d :: a))
        = singFun1 @(MkRecordSym1 (d :: a)) (SMkRecord s)