Natural.golden

Singletons/Natural.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| addAge :: Age -> Age -> Age
          addAge (MkAge (x :: Natural)) (MkAge (y :: Natural))
            = MkAge (x + y :: Natural)
          
          newtype Age = MkAge Natural |]
  ======>
    newtype Age = MkAge Natural
    addAge :: Age -> Age -> Age
    addAge (MkAge (x :: Natural)) (MkAge (y :: Natural))
      = MkAge ((x + y) :: Natural)
    type MkAgeSym0 :: (~>) Natural Age
    data MkAgeSym0 :: (~>) Natural Age
      where
        MkAgeSym0KindInference :: SameKind (Apply MkAgeSym0 arg) (MkAgeSym1 arg) =>
                                  MkAgeSym0 a0123456789876543210
    type instance Apply @Natural @Age MkAgeSym0 a0123456789876543210 = MkAge a0123456789876543210
    instance SuppressUnusedWarnings MkAgeSym0 where
      suppressUnusedWarnings = snd ((,) MkAgeSym0KindInference ())
    type MkAgeSym1 :: Natural -> Age
    type family MkAgeSym1 (a0123456789876543210 :: Natural) :: Age where
      MkAgeSym1 a0123456789876543210 = MkAge a0123456789876543210
    type AddAgeSym0 :: (~>) Age ((~>) Age Age)
    data AddAgeSym0 :: (~>) Age ((~>) Age Age)
      where
        AddAgeSym0KindInference :: SameKind (Apply AddAgeSym0 arg) (AddAgeSym1 arg) =>
                                   AddAgeSym0 a0123456789876543210
    type instance Apply @Age @((~>) Age Age) AddAgeSym0 a0123456789876543210 = AddAgeSym1 a0123456789876543210
    instance SuppressUnusedWarnings AddAgeSym0 where
      suppressUnusedWarnings = snd ((,) AddAgeSym0KindInference ())
    type AddAgeSym1 :: Age -> (~>) Age Age
    data AddAgeSym1 (a0123456789876543210 :: Age) :: (~>) Age Age
      where
        AddAgeSym1KindInference :: SameKind (Apply (AddAgeSym1 a0123456789876543210) arg) (AddAgeSym2 a0123456789876543210 arg) =>
                                   AddAgeSym1 a0123456789876543210 a0123456789876543210
    type instance Apply @Age @Age (AddAgeSym1 a0123456789876543210) a0123456789876543210 = AddAge a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (AddAgeSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) AddAgeSym1KindInference ())
    type AddAgeSym2 :: Age -> Age -> Age
    type family AddAgeSym2 (a0123456789876543210 :: Age) (a0123456789876543210 :: Age) :: Age where
      AddAgeSym2 a0123456789876543210 a0123456789876543210 = AddAge a0123456789876543210 a0123456789876543210
    type AddAge :: Age -> Age -> Age
    type family AddAge (a :: Age) (a :: Age) :: Age where
      AddAge (MkAge (x :: Natural)) (MkAge (y :: Natural)) = Apply MkAgeSym0 (Apply (Apply (+@#@$) x) y :: Natural)
    sAddAge ::
      (forall (t :: Age) (t :: Age).
       Sing t -> Sing t -> Sing (AddAge t t :: Age) :: Type)
    sAddAge (SMkAge (sX :: Sing x)) (SMkAge (sY :: Sing y))
      = (\cases
           (_ :: Sing (x :: Natural)) (_ :: Sing (y :: Natural))
             -> applySing
                  (singFun1 @MkAgeSym0 SMkAge)
                  (applySing (applySing (singFun2 @(+@#@$) (%+)) sX) sY ::
                     Sing (Apply (Apply (+@#@$) x) y :: Natural)))
          (sX :: Sing x) (sY :: Sing y)
    instance SingI (AddAgeSym0 :: (~>) Age ((~>) Age Age)) where
      sing = singFun2 @AddAgeSym0 sAddAge
    instance SingI d =>
             SingI (AddAgeSym1 (d :: Age) :: (~>) Age Age) where
      sing = singFun1 @(AddAgeSym1 (d :: Age)) (sAddAge (sing @d))
    instance SingI1 (AddAgeSym1 :: Age -> (~>) Age Age) where
      liftSing (s :: Sing (d :: Age))
        = singFun1 @(AddAgeSym1 (d :: Age)) (sAddAge s)
    data SAge :: Age -> Type
      where
        SMkAge :: forall (n :: Natural). (Sing n) -> SAge (MkAge n :: Age)
    type instance Sing @Age = SAge
    instance SingKind Age where
      type Demote Age = Age
      fromSing (SMkAge b) = MkAge (fromSing b)
      toSing (MkAge (b :: Demote Natural))
        = (\cases (SomeSing c) -> SomeSing (SMkAge c))
            (toSing b :: SomeSing Natural)
    instance SingI n => SingI (MkAge (n :: Natural)) where
      sing = SMkAge sing
    instance SingI1 MkAge where
      liftSing = SMkAge
    instance SingI (MkAgeSym0 :: (~>) Natural Age) where
      sing = singFun1 @MkAgeSym0 SMkAge