InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations
    singletons [d| data Nat = Zero | Succ Nat |]
  ======>
    data Nat = Zero | Succ Nat
    type ZeroSym0 = Zero
    type SuccSym1 (t0123456789876543210 :: Nat) =
        Succ t0123456789876543210
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings = snd (((,) SuccSym0KindInference) ())
    data SuccSym0 :: (~>) Nat Nat
      where
        SuccSym0KindInference :: forall t0123456789876543210
                                        arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
                                 SuccSym0 t0123456789876543210
    type instance Apply SuccSym0 t0123456789876543210 = Succ t0123456789876543210
    data SNat :: Nat -> Type
      where
        SZero :: SNat Zero
        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> SNat (Succ n)
    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 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)
    type Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 t0123456789876543210 =
        Let0123456789876543210Scrutinee_0123456789876543210 n0123456789876543210 h0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym2 h0123456789876543210 n0123456789876543210) where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference :: forall n0123456789876543210
                                                                                       h0123456789876543210
                                                                                       t0123456789876543210
                                                                                       arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n0123456789876543210 h0123456789876543210 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym2 n0123456789876543210 h0123456789876543210 t0123456789876543210
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 h0123456789876543210 n0123456789876543210) t0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 h0123456789876543210 n0123456789876543210 t0123456789876543210
    instance SuppressUnusedWarnings (Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210) where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210 h0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference :: forall n0123456789876543210
                                                                                       h0123456789876543210
                                                                                       arg. 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_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: forall n0123456789876543210
                                                                                       arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 n0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 n0123456789876543210
    type family Let0123456789876543210Scrutinee_0123456789876543210 n h t where
      Let0123456789876543210Scrutinee_0123456789876543210 n h t = Apply (Apply LeqSym0 n) h
    type family Case_0123456789876543210 n h t 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 InsertionSortSym1 (a0123456789876543210 :: [Nat]) =
        InsertionSort a0123456789876543210
    instance SuppressUnusedWarnings InsertionSortSym0 where
      suppressUnusedWarnings
        = snd (((,) InsertionSortSym0KindInference) ())
    data InsertionSortSym0 :: (~>) [Nat] [Nat]
      where
        InsertionSortSym0KindInference :: forall a0123456789876543210
                                                 arg. SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
                                          InsertionSortSym0 a0123456789876543210
    type instance Apply InsertionSortSym0 a0123456789876543210 = InsertionSort a0123456789876543210
    type InsertSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: [Nat]) =
        Insert a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (InsertSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) InsertSym1KindInference) ())
    data InsertSym1 (a0123456789876543210 :: Nat) :: (~>) [Nat] [Nat]
      where
        InsertSym1KindInference :: forall a0123456789876543210
                                          a0123456789876543210
                                          arg. SameKind (Apply (InsertSym1 a0123456789876543210) arg) (InsertSym2 a0123456789876543210 arg) =>
                                   InsertSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (InsertSym1 a0123456789876543210) a0123456789876543210 = Insert a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings InsertSym0 where
      suppressUnusedWarnings = snd (((,) InsertSym0KindInference) ())
    data InsertSym0 :: (~>) Nat ((~>) [Nat] [Nat])
      where
        InsertSym0KindInference :: forall a0123456789876543210
                                          arg. SameKind (Apply InsertSym0 arg) (InsertSym1 arg) =>
                                   InsertSym0 a0123456789876543210
    type instance Apply InsertSym0 a0123456789876543210 = InsertSym1 a0123456789876543210
    type LeqSym2 (a0123456789876543210 :: Nat) (a0123456789876543210 :: Nat) =
        Leq a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings (LeqSym1 a0123456789876543210) where
      suppressUnusedWarnings = snd (((,) LeqSym1KindInference) ())
    data LeqSym1 (a0123456789876543210 :: Nat) :: (~>) Nat Bool
      where
        LeqSym1KindInference :: forall a0123456789876543210
                                       a0123456789876543210
                                       arg. SameKind (Apply (LeqSym1 a0123456789876543210) arg) (LeqSym2 a0123456789876543210 arg) =>
                                LeqSym1 a0123456789876543210 a0123456789876543210
    type instance Apply (LeqSym1 a0123456789876543210) a0123456789876543210 = Leq a0123456789876543210 a0123456789876543210
    instance SuppressUnusedWarnings LeqSym0 where
      suppressUnusedWarnings = snd (((,) LeqSym0KindInference) ())
    data LeqSym0 :: (~>) Nat ((~>) Nat Bool)
      where
        LeqSym0KindInference :: forall a0123456789876543210
                                       arg. SameKind (Apply LeqSym0 arg) (LeqSym1 arg) =>
                                LeqSym0 a0123456789876543210
    type instance Apply LeqSym0 a0123456789876543210 = LeqSym1 a0123456789876543210
    type family InsertionSort (a :: [Nat]) :: [Nat] where
      InsertionSort '[] = '[]
      InsertionSort ('(:) h t) = Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
    type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
      Insert n '[] = Apply (Apply (:@#@$) n) '[]
      Insert n ('(:) h t) = Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)
    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])
    sInsert ::
      forall (t :: Nat) (t :: [Nat]).
      Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
    sLeq ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
    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) :: [Nat])))
            (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 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))