InsertionSortImp.golden

InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
    singletons [d| data Nat = Zero | Succ Nat |]
  ======>
    data Nat = Zero | Succ Nat
    type ZeroSym0 :: Nat
    type family ZeroSym0 :: Nat where
      ZeroSym0 = Zero
    type SuccSym0 :: (~>) Nat Nat
    data SuccSym0 :: (~>) Nat Nat
      where
        SuccSym0KindInference :: SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                 SuccSym0 a0123456789876543210
    type instance Apply SuccSym0 a0123456789876543210 = Succ a0123456789876543210
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings = snd ((,) SuccSym0KindInference ())
    type SuccSym1 :: Nat -> Nat
    type family SuccSym1 (a0123456789876543210 :: Nat) :: Nat where
      SuccSym1 a0123456789876543210 = Succ a0123456789876543210
    data SNat :: Nat -> Type
      where
        SZero :: SNat (Zero :: Nat)
        SSucc :: forall (n :: Nat). (Sing n) -> SNat (Succ n :: Nat)
    type instance Sing @Nat = SNat
    instance SingKind Nat where
      type Demote Nat = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ (b :: Demote Nat))
        = case toSing b :: SomeSing Nat of SomeSing c -> SomeSing (SSucc c)
    instance SingI Zero where
      sing = SZero
    instance SingI n => SingI (Succ (n :: Nat)) where
      sing = SSucc sing
    instance SingI1 Succ where
      liftSing = SSucc
    instance SingI (SuccSym0 :: (~>) Nat Nat) where
      sing = singFun1 @SuccSym0 SSucc
InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| leq :: Nat -> Nat -> Bool
          leq Zero _ = True
          leq (Succ _) Zero = False
          leq (Succ a) (Succ b) = leq a b
          insert :: Nat -> [Nat] -> [Nat]
          insert n [] = [n]
          insert n (h : t)
            = if leq n h then (n : h : t) else h : (insert n t)
          insertionSort :: [Nat] -> [Nat]
          insertionSort [] = []
          insertionSort (h : t) = insert h (insertionSort t) |]
  ======>
    leq :: Nat -> Nat -> Bool
    leq Zero _ = True
    leq (Succ _) Zero = False
    leq (Succ a) (Succ b) = leq a b
    insert :: Nat -> [Nat] -> [Nat]
    insert n [] = [n]
    insert n (h : t)
      = if leq n h then (n : (h : t)) else (h : insert n t)
    insertionSort :: [Nat] -> [Nat]
    insertionSort [] = []
    insertionSort (h : t) = insert h (insertionSort t)
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((,)
               Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) h0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
      suppressUnusedWarnings
        = snd
            ((,)
               Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) where
      suppressUnusedWarnings
        = snd
            ((,)
               Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
               ())
    type family Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
      Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
    type family Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 where
      Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
    type family Case_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210 t where
      Case_0123456789876543210 n h t 'True = Apply (Apply (:@#@$) n) (Apply (Apply (:@#@$) h) t)
      Case_0123456789876543210 n h t 'False = Apply (Apply (:@#@$) h) (Apply (Apply InsertSym0 n) t)
    type InsertionSortSym0 :: (~>) [Nat] [Nat]
    data InsertionSortSym0 :: (~>) [Nat] [Nat]
      where
        InsertionSortSym0KindInference :: SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
                                          InsertionSortSym0 a0123456789876543210
    type instance Apply InsertionSortSym0 a0123456789876543210 = InsertionSort a0123456789876543210
    instance SuppressUnusedWarnings InsertionSortSym0 where
      suppressUnusedWarnings
        = snd ((,) InsertionSortSym0KindInference ())
    type InsertionSortSym1 :: [Nat] -> [Nat]
    type family InsertionSortSym1 (a0123456789876543210 :: [Nat]) :: [Nat] where
      InsertionSortSym1 a0123456789876543210 = InsertionSort a0123456789876543210
    type InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])
    data InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])
      where
        InsertSym0KindInference :: SameKind (Apply InsertSym0 arg) (InsertSym1 arg) =>
                                   InsertSym0 a0123456789876543210
    type instance Apply InsertSym0 a0123456789876543210 = InsertSym1 a0123456789876543210
    instance SuppressUnusedWarnings InsertSym0 where
      suppressUnusedWarnings = snd ((,) InsertSym0KindInference ())
    type InsertSym1 :: Nat -> (~>) [Nat] [Nat]
    data InsertSym1 (a0123456789876543210 :: Nat) :: (~>) [Nat] [Nat]
      where
        InsertSym1KindInference :: SameKind (Apply (InsertSym1 a0123456789876543210) arg) (InsertSym2 a0123456789876543210 arg) =>
                                   InsertSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (InsertSym1 a0123456789876543210) a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (InsertSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) InsertSym1KindInference ())
    type InsertSym2 :: Nat -> [Nat] -> [Nat]
    type family InsertSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: [Nat]) :: [Nat] where
      InsertSym2 a0123456789876543210 a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
    type LeqSym0 :: (~>) Nat ((~>) Nat Bool)
    data LeqSym0 :: (~>) Nat ((~>) Nat Bool)
      where
        LeqSym0KindInference :: SameKind (Apply LeqSym0 arg) (LeqSym1 arg) =>
                                LeqSym0 a0123456789876543210
    type instance Apply LeqSym0 a0123456789876543210 = LeqSym1 a0123456789876543210
    instance SuppressUnusedWarnings LeqSym0 where
      suppressUnusedWarnings = snd ((,) LeqSym0KindInference ())
    type LeqSym1 :: Nat -> (~>) Nat Bool
    data LeqSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool
      where
        LeqSym1KindInference :: SameKind (Apply (LeqSym1 a0123456789876543210) arg) (LeqSym2 a0123456789876543210 arg) =>
                                LeqSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (LeqSym1 a0123456789876543210) a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (LeqSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd ((,) LeqSym1KindInference ())
    type LeqSym2 :: Nat -> Nat -> Bool
    type family LeqSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) :: Bool where
      LeqSym2 a0123456789876543210 a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
    type InsertionSort :: [Nat] -> [Nat]
    type family InsertionSort (a :: [Nat]) :: [Nat] where
      InsertionSort '[] = NilSym0
      InsertionSort ('(:) h t) = Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
    type Insert :: Nat -> [Nat] -> [Nat]
    type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
      Insert n '[] = Apply (Apply (:@#@$) n) NilSym0
      Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
    type Leq :: Nat -> Nat -> Bool
    type family Leq (a :: Nat) (a :: Nat) :: Bool where
      Leq 'Zero _ = TrueSym0
      Leq ('Succ _) 'Zero = FalseSym0
      Leq ('Succ a) ('Succ b) = Apply (Apply LeqSym0 a) b
    sInsertionSort ::
      (forall (t :: [Nat]).
       Sing t -> Sing (Apply InsertionSortSym0 t :: [Nat]) :: Type)
    sInsert ::
      (forall (t :: Nat) (t :: [Nat]).
       Sing t
       -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat]) :: Type)
    sLeq ::
      (forall (t :: Nat) (t :: Nat).
       Sing t
       -> Sing t -> Sing (Apply (Apply LeqSym0 t) t :: Bool) :: Type)
    sInsertionSort SNil = SNil
    sInsertionSort (SCons (sH :: Sing h) (sT :: Sing t))
      = applySing
          (applySing (singFun2 @InsertSym0 sInsert) sH)
          (applySing (singFun1 @InsertionSortSym0 sInsertionSort) sT)
    sInsert (sN :: Sing n) SNil
      = applySing (applySing (singFun2 @(:@#@$) SCons) sN) SNil
    sInsert (sN :: Sing n) (SCons (sH :: Sing h) (sT :: Sing t))
      = let
          sScrutinee_0123456789876543210 ::
            Sing @_ (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
          sScrutinee_0123456789876543210
            = applySing (applySing (singFun2 @LeqSym0 sLeq) sN) sH
        in
          id
            @(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)))
            (case sScrutinee_0123456789876543210 of
               STrue
                 -> applySing
                      (applySing (singFun2 @(:@#@$) SCons) sN)
                      (applySing (applySing (singFun2 @(:@#@$) SCons) sH) sT)
               SFalse
                 -> applySing
                      (applySing (singFun2 @(:@#@$) SCons) sH)
                      (applySing (applySing (singFun2 @InsertSym0 sInsert) sN) sT))
    sLeq SZero _ = STrue
    sLeq (SSucc _) SZero = SFalse
    sLeq (SSucc (sA :: Sing a)) (SSucc (sB :: Sing b))
      = applySing (applySing (singFun2 @LeqSym0 sLeq) sA) sB
    instance SingI (InsertionSortSym0 :: (~>) [Nat] [Nat]) where
      sing = singFun1 @InsertionSortSym0 sInsertionSort
    instance SingI (InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])) where
      sing = singFun2 @InsertSym0 sInsert
    instance SingI d =>
             SingI (InsertSym1 (d :: Nat) :: (~>) [Nat] [Nat]) where
      sing = singFun1 @(InsertSym1 (d :: Nat)) (sInsert (sing @d))
    instance SingI1 (InsertSym1 :: Nat -> (~>) [Nat] [Nat]) where
      liftSing (s :: Sing (d :: Nat))
        = singFun1 @(InsertSym1 (d :: Nat)) (sInsert s)
    instance SingI (LeqSym0 :: (~>) Nat ((~>) Nat Bool)) where
      sing = singFun2 @LeqSym0 sLeq
    instance SingI d =>
             SingI (LeqSym1 (d :: Nat) :: (~>) Nat Bool) where
      sing = singFun1 @(LeqSym1 (d :: Nat)) (sLeq (sing @d))
    instance SingI1 (LeqSym1 :: Nat -> (~>) Nat Bool) where
      liftSing (s :: Sing (d :: Nat))
        = singFun1 @(LeqSym1 (d :: Nat)) (sLeq s)