Records.ghc84.template

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 a0123456789876543210) = Field1 t
    instance SuppressUnusedWarnings Field1Sym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) Field1Sym0KindInference) GHC.Tuple.())
    data Field1Sym0 (l :: TyFun (Record a0123456789876543210) a0123456789876543210)
      = forall arg. SameKind (Apply Field1Sym0 arg) (Field1Sym1 arg) =>
        Field1Sym0KindInference
    type instance Apply Field1Sym0 l = Field1 l
    type Field2Sym1 (t :: Record a0123456789876543210) = Field2 t
    instance SuppressUnusedWarnings Field2Sym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) Field2Sym0KindInference) GHC.Tuple.())
    data Field2Sym0 (l :: TyFun (Record a0123456789876543210) Bool)
      = forall arg. SameKind (Apply Field2Sym0 arg) (Field2Sym1 arg) =>
        Field2Sym0KindInference
    type instance Apply Field2Sym0 l = Field2 l
    type family Field1 (a :: Record a) :: a where
      Field1 (MkRecord field _) = field
    type family Field2 (a :: Record a) :: Bool where
      Field2 (MkRecord _ field) = field
    type MkRecordSym2 (t :: a0123456789876543210) (t :: Bool) =
        MkRecord t t
    instance SuppressUnusedWarnings MkRecordSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) MkRecordSym1KindInference) GHC.Tuple.())
    data MkRecordSym1 (l :: a0123456789876543210) (l :: TyFun Bool (Record a0123456789876543210))
      = forall arg. SameKind (Apply (MkRecordSym1 l) arg) (MkRecordSym2 l arg) =>
        MkRecordSym1KindInference
    type instance Apply (MkRecordSym1 l) l = MkRecord l l
    instance SuppressUnusedWarnings MkRecordSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) MkRecordSym0KindInference) GHC.Tuple.())
    data MkRecordSym0 (l :: TyFun a0123456789876543210 (TyFun Bool (Record a0123456789876543210)
                                                        -> GHC.Types.Type))
      = forall arg. SameKind (Apply MkRecordSym0 arg) (MkRecordSym1 arg) =>
        MkRecordSym0KindInference
    type instance Apply MkRecordSym0 l = MkRecordSym1 l
    data instance Sing (z :: Record a)
      where
        SMkRecord :: forall (n :: a) (n :: Bool).
                     {sField1 :: (Sing (n :: a)), sField2 :: (Sing (n :: Bool))}
                     -> Sing (MkRecord n n)
    type SRecord = (Sing :: Record a -> GHC.Types.Type)
    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
              (GHC.Tuple.(,) (toSing b :: SomeSing a))
                (toSing b :: SomeSing 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