DataValues.ghc76.template

Singletons/DataValues.hs:0:0: Splicing declarations
    singletons
      [d| pr = Pair (Succ Zero) ([Zero])
          complex = Pair (Pair (Just Zero) Zero) False
          tuple = (False, Just Zero, True)
          aList = [Zero, Succ Zero, Succ (Succ Zero)]
          
          data Pair a b
            = Pair a b
            deriving (Show) |]
  ======>
    Singletons/DataValues.hs:(0,0)-(0,0)
    data Pair a b
      = Pair a b
      deriving (Show)
    pr = Pair (Succ Zero) [Zero]
    complex = Pair (Pair (Just Zero) Zero) False
    tuple = (False, Just Zero, True)
    aList = [Zero, Succ Zero, Succ (Succ Zero)]
    type PairTyCtor = Pair
    data PairTyCtorSym1 (l :: *) (l :: TyFun * *)
    data PairTyCtorSym0 (k :: TyFun * (TyFun * * -> *))
    type instance Apply (PairTyCtorSym1 a) a = PairTyCtor a a
    type instance Apply PairTyCtorSym0 a = PairTyCtorSym1 a
    data PairSym1 (l :: a) (l :: TyFun b (Pair a b))
    data PairSym0 (k :: TyFun a (TyFun b (Pair a b) -> *))
    type instance Apply (PairSym1 a) a = Pair a a
    type instance Apply PairSym0 a = PairSym1 a
    type Pr =
        Apply (Apply PairSym0 (Apply SuccSym0 ZeroSym0)) '[ZeroSym0]
    type PrSym0 = Pr
    type Complex =
        Apply (Apply PairSym0 (Apply (Apply PairSym0 (Apply JustSym0 ZeroSym0)) ZeroSym0)) FalseSym0
    type ComplexSym0 = Complex
    type Tuple = '(FalseSym0, Apply JustSym0 ZeroSym0, TrueSym0)
    type TupleSym0 = Tuple
    type AList =
        '[ZeroSym0,
          Apply SuccSym0 ZeroSym0,
          Apply SuccSym0 (Apply SuccSym0 ZeroSym0)]
    type AListSym0 = AList
    data instance Sing (z :: Pair a b)
      = forall (n :: a) (n :: b). z ~ Pair n n => SPair (Sing n) (Sing n)
    type SPair (z :: Pair a b) = Sing z
    instance (SingKind (KProxy :: KProxy a),
              SingKind (KProxy :: KProxy b)) =>
             SingKind (KProxy :: KProxy (Pair a b)) where
      type instance DemoteRep (KProxy :: KProxy (Pair a b)) =
          Pair (DemoteRep (KProxy :: KProxy a)) (DemoteRep (KProxy :: KProxy b))
      fromSing (SPair b b) = Pair (fromSing b) (fromSing b)
      toSing (Pair b b)
        = case
              (toSing b :: SomeSing (KProxy :: KProxy a), 
               toSing b :: SomeSing (KProxy :: KProxy b))
          of {
            (SomeSing c, SomeSing c) -> SomeSing (SPair c c) }
    instance (SingI n, SingI n) => SingI (Pair (n :: a) (n :: b)) where
      sing = SPair sing sing
    sPr = SPair (SSucc SZero) (SCons SZero SNil)
    sComplex = SPair (SPair (SJust SZero) SZero) SFalse
    sTuple = STuple3 SFalse (SJust SZero) STrue
    sAList
      = SCons
          SZero (SCons (SSucc SZero) (SCons (SSucc (SSucc SZero)) SNil))