Singletons/T555.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| data MyPropKind
            = Location | Quaternion
            deriving (Eq, Ord, Show) |]
  ======>
    data MyPropKind
      = Location | Quaternion
      deriving (Eq, Ord, Show)
    type LocationSym0 :: MyPropKind
    type family LocationSym0 :: MyPropKind where
      LocationSym0 = Location
    type QuaternionSym0 :: MyPropKind
    type family QuaternionSym0 :: MyPropKind where
      QuaternionSym0 = Quaternion
    type TFHelper_0123456789876543210 :: MyPropKind
                                         -> MyPropKind -> Bool
    type family TFHelper_0123456789876543210 (a :: MyPropKind) (a :: MyPropKind) :: Bool where
      TFHelper_0123456789876543210 Location Location = TrueSym0
      TFHelper_0123456789876543210 Location Quaternion = FalseSym0
      TFHelper_0123456789876543210 Quaternion Location = FalseSym0
      TFHelper_0123456789876543210 Quaternion Quaternion = TrueSym0
    type TFHelper_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind Bool)
    data TFHelper_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind Bool)
      where
        TFHelper_0123456789876543210Sym0KindInference :: SameKind (Apply TFHelper_0123456789876543210Sym0 arg) (TFHelper_0123456789876543210Sym1 arg) =>
                                                         TFHelper_0123456789876543210Sym0 a0123456789876543210
    type instance Apply TFHelper_0123456789876543210Sym0 a0123456789876543210 = TFHelper_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings TFHelper_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) TFHelper_0123456789876543210Sym0KindInference ())
    type TFHelper_0123456789876543210Sym1 :: MyPropKind
                                             -> (~>) MyPropKind Bool
    data TFHelper_0123456789876543210Sym1 (a0123456789876543210 :: MyPropKind) :: (~>) MyPropKind Bool
      where
        TFHelper_0123456789876543210Sym1KindInference :: SameKind (Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) arg) (TFHelper_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                         TFHelper_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (TFHelper_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (TFHelper_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) TFHelper_0123456789876543210Sym1KindInference ())
    type TFHelper_0123456789876543210Sym2 :: MyPropKind
                                             -> MyPropKind -> Bool
    type family TFHelper_0123456789876543210Sym2 (a0123456789876543210 :: MyPropKind) (a0123456789876543210 :: MyPropKind) :: Bool where
      TFHelper_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = TFHelper_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PEq MyPropKind where
      type (==) a a = Apply (Apply TFHelper_0123456789876543210Sym0 a) a
    type Compare_0123456789876543210 :: MyPropKind
                                        -> MyPropKind -> Ordering
    type family Compare_0123456789876543210 (a :: MyPropKind) (a :: MyPropKind) :: Ordering where
      Compare_0123456789876543210 Location Location = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 Quaternion Quaternion = Apply (Apply (Apply FoldlSym0 (<>@#@$)) EQSym0) NilSym0
      Compare_0123456789876543210 Location Quaternion = LTSym0
      Compare_0123456789876543210 Quaternion Location = GTSym0
    type Compare_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind Ordering)
    data Compare_0123456789876543210Sym0 :: (~>) MyPropKind ((~>) MyPropKind Ordering)
      where
        Compare_0123456789876543210Sym0KindInference :: SameKind (Apply Compare_0123456789876543210Sym0 arg) (Compare_0123456789876543210Sym1 arg) =>
                                                        Compare_0123456789876543210Sym0 a0123456789876543210
    type instance Apply Compare_0123456789876543210Sym0 a0123456789876543210 = Compare_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings Compare_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) Compare_0123456789876543210Sym0KindInference ())
    type Compare_0123456789876543210Sym1 :: MyPropKind
                                            -> (~>) MyPropKind Ordering
    data Compare_0123456789876543210Sym1 (a0123456789876543210 :: MyPropKind) :: (~>) MyPropKind Ordering
      where
        Compare_0123456789876543210Sym1KindInference :: SameKind (Apply (Compare_0123456789876543210Sym1 a0123456789876543210) arg) (Compare_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                        Compare_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (Compare_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (Compare_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) Compare_0123456789876543210Sym1KindInference ())
    type Compare_0123456789876543210Sym2 :: MyPropKind
                                            -> MyPropKind -> Ordering
    type family Compare_0123456789876543210Sym2 (a0123456789876543210 :: MyPropKind) (a0123456789876543210 :: MyPropKind) :: Ordering where
      Compare_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 = Compare_0123456789876543210 a0123456789876543210 a0123456789876543210
    instance POrd MyPropKind where
      type Compare a a = Apply (Apply Compare_0123456789876543210Sym0 a) a
    type ShowsPrec_0123456789876543210 :: GHC.Num.Natural.Natural
                                          -> MyPropKind -> Symbol -> Symbol
    type family ShowsPrec_0123456789876543210 (a :: GHC.Num.Natural.Natural) (a :: MyPropKind) (a :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210 _ Location a_0123456789876543210 = Apply (Apply ShowStringSym0 "Location") a_0123456789876543210
      ShowsPrec_0123456789876543210 _ Quaternion a_0123456789876543210 = Apply (Apply ShowStringSym0 "Quaternion") a_0123456789876543210
    type ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) Symbol Symbol))
    data ShowsPrec_0123456789876543210Sym0 :: (~>) GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) Symbol Symbol))
      where
        ShowsPrec_0123456789876543210Sym0KindInference :: SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd ((,) ShowsPrec_0123456789876543210Sym0KindInference ())
    type ShowsPrec_0123456789876543210Sym1 :: GHC.Num.Natural.Natural
                                              -> (~>) MyPropKind ((~>) Symbol Symbol)
    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Num.Natural.Natural) :: (~>) MyPropKind ((~>) Symbol Symbol)
      where
        ShowsPrec_0123456789876543210Sym1KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) ShowsPrec_0123456789876543210Sym1KindInference ())
    type ShowsPrec_0123456789876543210Sym2 :: GHC.Num.Natural.Natural
                                              -> MyPropKind -> (~>) Symbol Symbol
    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: MyPropKind) :: (~>) Symbol Symbol
      where
        ShowsPrec_0123456789876543210Sym2KindInference :: SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
                                                          ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) ShowsPrec_0123456789876543210Sym2KindInference ())
    type ShowsPrec_0123456789876543210Sym3 :: GHC.Num.Natural.Natural
                                              -> MyPropKind -> Symbol -> Symbol
    type family ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Num.Natural.Natural) (a0123456789876543210 :: MyPropKind) (a0123456789876543210 :: Symbol) :: Symbol where
      ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
    instance PShow MyPropKind where
      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
    data SMyPropKind :: MyPropKind -> Type
      where
        SLocation :: SMyPropKind (Location :: MyPropKind)
        SQuaternion :: SMyPropKind (Quaternion :: MyPropKind)
    type instance Sing @MyPropKind = SMyPropKind
    instance SingKind MyPropKind where
      type Demote MyPropKind = MyPropKind
      fromSing SLocation = Location
      fromSing SQuaternion = Quaternion
      toSing Location = SomeSing SLocation
      toSing Quaternion = SomeSing SQuaternion
    instance SEq MyPropKind where
      (%==) ::
        forall (t1 :: MyPropKind) (t2 :: MyPropKind). Sing t1
                                                      -> Sing t2
                                                         -> Sing (Apply (Apply ((==@#@$) :: TyFun MyPropKind ((~>) MyPropKind Bool)
                                                                                            -> Type) t1) t2)
      (%==) SLocation SLocation = STrue
      (%==) SLocation SQuaternion = SFalse
      (%==) SQuaternion SLocation = SFalse
      (%==) SQuaternion SQuaternion = STrue
    instance SOrd MyPropKind where
      sCompare ::
        forall (t1 :: MyPropKind) (t2 :: MyPropKind). Sing t1
                                                      -> Sing t2
                                                         -> Sing (Apply (Apply (CompareSym0 :: TyFun MyPropKind ((~>) MyPropKind Ordering)
                                                                                               -> Type) t1) t2)
      sCompare SLocation SLocation
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare SQuaternion SQuaternion
        = applySing
            (applySing
               (applySing (singFun3 @FoldlSym0 sFoldl) (singFun2 @(<>@#@$) (%<>)))
               SEQ)
            SNil
      sCompare SLocation SQuaternion = SLT
      sCompare SQuaternion SLocation = SGT
    instance SShow MyPropKind where
      sShowsPrec ::
        forall (t1 :: GHC.Num.Natural.Natural)
               (t2 :: MyPropKind)
               (t3 :: Symbol). Sing t1
                               -> Sing t2
                                  -> Sing t3
                                     -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Num.Natural.Natural ((~>) MyPropKind ((~>) Symbol Symbol))
                                                                                    -> Type) t1) t2) t3)
      sShowsPrec
        _
        SLocation
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Location"))
            sA_0123456789876543210
      sShowsPrec
        _
        SQuaternion
        (sA_0123456789876543210 :: Sing a_0123456789876543210)
        = applySing
            (applySing
               (singFun2 @ShowStringSym0 sShowString) (sing :: Sing "Quaternion"))
            sA_0123456789876543210
    instance SDecide MyPropKind where
      (%~) SLocation SLocation = Proved Refl
      (%~) SLocation SQuaternion = Disproved (\ x -> case x of {})
      (%~) SQuaternion SLocation = Disproved (\ x -> case x of {})
      (%~) SQuaternion SQuaternion = Proved Refl
    instance Data.Type.Equality.TestEquality (SMyPropKind :: MyPropKind
                                                             -> Type) where
      Data.Type.Equality.testEquality
        = Data.Singletons.Decide.decideEquality
    instance Data.Type.Coercion.TestCoercion (SMyPropKind :: MyPropKind
                                                             -> Type) where
      Data.Type.Coercion.testCoercion
        = Data.Singletons.Decide.decideCoercion
    deriving instance Show (SMyPropKind (z :: MyPropKind))
    instance SingI Location where
      sing = SLocation
    instance SingI Quaternion where
      sing = SQuaternion