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 (t :: Nat) = Succ t
    instance SuppressUnusedWarnings SuccSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) SuccSym0KindInference) GHC.Tuple.())
    data SuccSym0 (l :: TyFun Nat Nat)
      = forall arg. SameKind (Apply SuccSym0 arg) (SuccSym1 arg) =>
        SuccSym0KindInference
    type instance Apply SuccSym0 l = Succ l
    data instance Sing (z :: Nat)
      where
        SZero :: Sing Zero
        SSucc :: forall (n :: Nat). (Sing (n :: Nat)) -> Sing (Succ n)
    type SNat = (Sing :: Nat -> Type)
    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
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 GHC.Types.[] = [n]
    insert n (h GHC.Types.: t)
      = if (leq n) h then
            (n GHC.Types.: (h GHC.Types.: t))
        else
            (h GHC.Types.: ((insert n) t))
    insertionSort :: [Nat] -> [Nat]
    insertionSort GHC.Types.[] = []
    insertionSort (h GHC.Types.: t) = (insert h) (insertionSort t)
    type Let0123456789876543210Scrutinee_0123456789876543210Sym3 t t t =
        Let0123456789876543210Scrutinee_0123456789876543210 t t t
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym2 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference)
               GHC.Tuple.())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l l
      = forall arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym3 l l arg) =>
        Let0123456789876543210Scrutinee_0123456789876543210Sym2KindInference
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l) l = Let0123456789876543210Scrutinee_0123456789876543210 l l l
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym1 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference)
               GHC.Tuple.())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym1 l l
      = forall arg. SameKind (Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 l) arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym2 l arg) =>
        Let0123456789876543210Scrutinee_0123456789876543210Sym1KindInference
    type instance Apply (Let0123456789876543210Scrutinee_0123456789876543210Sym1 l) l = Let0123456789876543210Scrutinee_0123456789876543210Sym2 l l
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            ((GHC.Tuple.(,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
               GHC.Tuple.())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 l
      = forall arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 l = Let0123456789876543210Scrutinee_0123456789876543210Sym1 l
    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 LeqSym2 (t :: Nat) (t :: Nat) = Leq t t
    instance SuppressUnusedWarnings LeqSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) LeqSym1KindInference) GHC.Tuple.())
    data LeqSym1 (l :: Nat) (l :: TyFun Nat Bool)
      = forall arg. SameKind (Apply (LeqSym1 l) arg) (LeqSym2 l arg) =>
        LeqSym1KindInference
    type instance Apply (LeqSym1 l) l = Leq l l
    instance SuppressUnusedWarnings LeqSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) LeqSym0KindInference) GHC.Tuple.())
    data LeqSym0 (l :: TyFun Nat (TyFun Nat Bool -> Type))
      = forall arg. SameKind (Apply LeqSym0 arg) (LeqSym1 arg) =>
        LeqSym0KindInference
    type instance Apply LeqSym0 l = LeqSym1 l
    type InsertSym2 (t :: Nat) (t :: [Nat]) = Insert t t
    instance SuppressUnusedWarnings InsertSym1 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) InsertSym1KindInference) GHC.Tuple.())
    data InsertSym1 (l :: Nat) (l :: TyFun [Nat] [Nat])
      = forall arg. SameKind (Apply (InsertSym1 l) arg) (InsertSym2 l arg) =>
        InsertSym1KindInference
    type instance Apply (InsertSym1 l) l = Insert l l
    instance SuppressUnusedWarnings InsertSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) InsertSym0KindInference) GHC.Tuple.())
    data InsertSym0 (l :: TyFun Nat (TyFun [Nat] [Nat] -> Type))
      = forall arg. SameKind (Apply InsertSym0 arg) (InsertSym1 arg) =>
        InsertSym0KindInference
    type instance Apply InsertSym0 l = InsertSym1 l
    type InsertionSortSym1 (t :: [Nat]) = InsertionSort t
    instance SuppressUnusedWarnings InsertionSortSym0 where
      suppressUnusedWarnings
        = snd ((GHC.Tuple.(,) InsertionSortSym0KindInference) GHC.Tuple.())
    data InsertionSortSym0 (l :: TyFun [Nat] [Nat])
      = forall arg. SameKind (Apply InsertionSortSym0 arg) (InsertionSortSym1 arg) =>
        InsertionSortSym0KindInference
    type instance Apply InsertionSortSym0 l = InsertionSort l
    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
    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 InsertionSort (a :: [Nat]) :: [Nat] where
      InsertionSort '[] = '[]
      InsertionSort ((:) h t) = Apply (Apply InsertSym0 h) (Apply InsertionSortSym0 t)
    sLeq ::
      forall (t :: Nat) (t :: Nat).
      Sing t -> Sing t -> Sing (Apply (Apply LeqSym0 t) t :: Bool)
    sInsert ::
      forall (t :: Nat) (t :: [Nat]).
      Sing t -> Sing t -> Sing (Apply (Apply InsertSym0 t) t :: [Nat])
    sInsertionSort ::
      forall (t :: [Nat]).
      Sing t -> Sing (Apply InsertionSortSym0 t :: [Nat])
    sLeq SZero _ = STrue
    sLeq (SSucc _) SZero = SFalse
    sLeq (SSucc (sA :: Sing a)) (SSucc (sB :: Sing b))
      = (applySing ((applySing ((singFun2 @LeqSym0) sLeq)) sA)) sB
    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  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) ::
              Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t) :: [Nat])
    sInsertionSort SNil = SNil
    sInsertionSort (SCons (sH :: Sing h) (sT :: Sing t))
      = (applySing ((applySing ((singFun2 @InsertSym0) sInsert)) sH))
          ((applySing ((singFun1 @InsertionSortSym0) sInsertionSort)) sT)