singletons-1.0: tests/compile-and-dump/Singletons/Operators.ghc78.template

Singletons/Operators.hs:0:0: Splicing declarations
    singletons
      [d| child :: Foo -> Foo
          child FLeaf = FLeaf
          child (a :+: _) = a
          (+) :: Nat -> Nat -> Nat
          Zero + m = m
          (Succ n) + m = Succ (n + m)
          
          data Foo
            where
              FLeaf :: Foo
              :+: :: Foo -> Foo -> Foo |]
  ======>
    Singletons/Operators.hs:(0,0)-(0,0)
    data Foo = FLeaf | (:+:) Foo Foo
    child :: Foo -> Foo
    child FLeaf = FLeaf
    child (a :+: _) = a
    (+) :: Nat -> Nat -> Nat
    (+) Zero m = m
    (+) (Succ n) m = Succ (n + m)
    type FLeafSym0 = FLeaf
    type (:+:$$$) (t :: Foo) (t :: Foo) = (:+:) t t
    instance SuppressUnusedWarnings (:+:$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:+:$$###) GHC.Tuple.())
    data (:+:$$) (l :: Foo) (l :: TyFun Foo Foo)
      = forall arg. (GHC.Types.~) (KindOf (Apply ((:+:$$) l) arg)) (KindOf ((:+:$$$) l arg)) =>
        (:+:$$###)
    type instance Apply ((:+:$$) l) l = (:+:$$$) l l
    instance SuppressUnusedWarnings (:+:$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:+:$###) GHC.Tuple.())
    data (:+:$) (l :: TyFun Foo (TyFun Foo Foo -> *))
      = forall arg. (GHC.Types.~) (KindOf (Apply (:+:$) arg)) (KindOf ((:+:$$) arg)) =>
        (:+:$###)
    type instance Apply (:+:$) l = (:+:$$) l
    type (:+$$$) (t :: Nat) (t :: Nat) = (:+) t t
    instance SuppressUnusedWarnings (:+$$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:+$$###) GHC.Tuple.())
    data (:+$$) (l :: Nat) (l :: TyFun Nat Nat)
      = forall arg. (GHC.Types.~) (KindOf (Apply ((:+$$) l) arg)) (KindOf ((:+$$$) l arg)) =>
        (:+$$###)
    type instance Apply ((:+$$) l) l = (:+$$$) l l
    instance SuppressUnusedWarnings (:+$) where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) (:+$###) GHC.Tuple.())
    data (:+$) (l :: TyFun Nat (TyFun Nat Nat -> *))
      = forall arg. (GHC.Types.~) (KindOf (Apply (:+$) arg)) (KindOf ((:+$$) arg)) =>
        (:+$###)
    type instance Apply (:+$) l = (:+$$) l
    type ChildSym1 (t :: Foo) = Child t
    instance SuppressUnusedWarnings ChildSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) ChildSym0KindInference GHC.Tuple.())
    data ChildSym0 (l :: TyFun Foo Foo)
      = forall arg. (GHC.Types.~) (KindOf (Apply ChildSym0 arg)) (KindOf (ChildSym1 arg)) =>
        ChildSym0KindInference
    type instance Apply ChildSym0 l = ChildSym1 l
    type family (:+) (a :: Nat) (a :: Nat) :: Nat where
      (:+) Zero m = m
      (:+) (Succ n) m = Apply SuccSym0 (Apply (Apply (:+$) n) m)
    type family Child (a :: Foo) :: Foo where
      Child FLeaf = FLeafSym0
      Child ((:+:) a z) = a
    (%:+) ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t)
    sChild :: forall (t :: Foo). Sing t -> Sing (Apply ChildSym0 t)
    (%:+) SZero sM
      = let
          lambda ::
            forall m. ((GHC.Types.~) t ZeroSym0, (GHC.Types.~) t m) =>
            Sing m -> Sing (Apply (Apply (:+$) ZeroSym0) m)
          lambda m = m
        in lambda sM
    (%:+) (SSucc sN) sM
      = let
          lambda ::
            forall n m. ((GHC.Types.~) t (Apply SuccSym0 n),
                         (GHC.Types.~) t m) =>
            Sing n -> Sing m -> Sing (Apply (Apply (:+$) (Apply SuccSym0 n)) m)
          lambda n m
            = applySing
                (singFun1 (Proxy :: Proxy SuccSym0) SSucc)
                (applySing (applySing (singFun2 (Proxy :: Proxy (:+$)) (%:+)) n) m)
        in lambda sN sM
    sChild SFLeaf
      = let
          lambda ::
            (GHC.Types.~) t FLeafSym0 => Sing (Apply ChildSym0 FLeafSym0)
          lambda = SFLeaf
        in lambda
    sChild ((:%+:) sA _)
      = let
          lambda ::
            forall a wild. (GHC.Types.~) t (Apply (Apply (:+:$) a) wild) =>
            Sing a -> Sing (Apply ChildSym0 (Apply (Apply (:+:$) a) wild))
          lambda a = a
        in lambda sA
    data instance Sing (z :: Foo)
      = (GHC.Types.~) z FLeaf => SFLeaf |
        forall (n :: Foo) (n :: Foo). (GHC.Types.~) z ((:+:) n n) =>
        (:%+:) (Sing n) (Sing n)
    type SFoo (z :: Foo) = Sing z
    instance SingKind (KProxy :: KProxy Foo) where
      type DemoteRep (KProxy :: KProxy Foo) = Foo
      fromSing SFLeaf = FLeaf
      fromSing ((:%+:) b b) = (:+:) (fromSing b) (fromSing b)
      toSing FLeaf = SomeSing SFLeaf
      toSing ((:+:) b b)
        = case
              GHC.Tuple.(,)
                (toSing b :: SomeSing (KProxy :: KProxy Foo))
                (toSing b :: SomeSing (KProxy :: KProxy Foo))
          of {
            GHC.Tuple.(,) (SomeSing c) (SomeSing c) -> SomeSing ((:%+:) c c) }
    instance SingI FLeaf where
      sing = SFLeaf
    instance (SingI n, SingI n) =>
             SingI ((:+:) (n :: Foo) (n :: Foo)) where
      sing = (:%+:) sing sing