Operators.ghc84.template

Singletons/Operators.hs:(0,0)-(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 |]
  ======>
    data Foo
      where
        FLeaf :: Foo
        (:+:) :: Foo -> 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. SameKind (Apply ((:+:@#@$$) l) arg) ((:+:@#@$$$) 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 -> GHC.Types.Type))
      = forall arg. SameKind (Apply (:+:@#@$) arg) ((:+:@#@$$) 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. SameKind (Apply ((+@#@$$) l) arg) ((+@#@$$$) 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 -> GHC.Types.Type))
      = forall arg. SameKind (Apply (+@#@$) arg) ((+@#@$$) 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. SameKind (Apply ChildSym0 arg) (ChildSym1 arg) =>
        ChildSym0KindInference
    type instance Apply ChildSym0 l = Child 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 _) = a
    (%+) ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t :: Nat)
    sChild ::
      forall (t :: Foo). Sing t -> Sing (Apply ChildSym0 t :: Foo)
    (%+) SZero (sM :: Sing m) = sM
    (%+) (SSucc (sN :: Sing n)) (sM :: Sing m)
      = (applySing ((singFun1 @SuccSym0) SSucc))
          ((applySing ((applySing ((singFun2 @(+@#@$)) (%+))) sN)) sM)
    sChild SFLeaf = SFLeaf
    sChild ((:%+:) (sA :: Sing a) _) = sA
    data instance Sing (z :: Foo)
      where
        SFLeaf :: Sing FLeaf
        (:%+:) :: forall (n :: Foo) (n :: Foo).
                  (Sing (n :: Foo)) -> (Sing (n :: Foo)) -> Sing ((:+:) n n)
    type SFoo = (Sing :: Foo -> GHC.Types.Type)
    instance SingKind Foo where
      type Demote Foo = Foo
      fromSing SFLeaf = FLeaf
      fromSing ((:%+:) b b) = ((:+:) (fromSing b)) (fromSing b)
      toSing FLeaf = SomeSing SFLeaf
      toSing ((:+:) (b :: Demote Foo) (b :: Demote Foo))
        = case
              (GHC.Tuple.(,) (toSing b :: SomeSing Foo))
                (toSing b :: SomeSing 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