InsertionSort/InsertionSortImp.hs:0:0: Splicing declarations
    singletons [d| data Nat = Zero | Succ Nat |]
  ======>
    InsertionSort/InsertionSortImp.hs:(0,0)-(0,0)
    data Nat = Zero | Succ Nat
    data instance Sing (z :: Nat)
      = z ~ Zero => SZero |
        forall (n :: Nat). z ~ Succ n => SSucc (Sing n)
    type SNat (z :: Nat) = Sing z
    instance SingKind (KProxy :: KProxy Nat) where
      type DemoteRep (KProxy :: KProxy Nat) = Nat
      fromSing SZero = Zero
      fromSing (SSucc b) = Succ (fromSing b)
      toSing Zero = SomeSing SZero
      toSing (Succ b)
        = case toSing b :: SomeSing (KProxy :: KProxy 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: 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) |]
  ======>
    InsertionSort/InsertionSortImp.hs:(0,0)-(0,0)
    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 family Leq (a :: Nat) (a :: Nat) :: Bool where
      Leq Zero z = True
      Leq (Succ z) Zero = False
      Leq (Succ a) (Succ b) = Leq a b
    type family Insert (a :: Nat) (a :: [Nat]) :: [Nat] where
      Insert n GHC.Types.[] = '[n]
      Insert n ((GHC.Types.:) h t) = If (Leq n h) ((GHC.Types.:) n ((GHC.Types.:) h t)) ((GHC.Types.:) h (Insert n t))
    type family InsertionSort (a :: [Nat]) :: [Nat] where
      InsertionSort GHC.Types.[] = '[]
      InsertionSort ((GHC.Types.:) h t) = Insert h (InsertionSort t)
    sLeq ::
      forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Leq t t)
    sLeq SZero _ = STrue
    sLeq (SSucc _) SZero = SFalse
    sLeq (SSucc a) (SSucc b) = sLeq a b
    sInsert ::
      forall (t :: Nat) (t :: [Nat]).
      Sing t -> Sing t -> Sing (Insert t t)
    sInsert n SNil = SCons n SNil
    sInsert n (SCons h t)
      = sIf (sLeq n h) (SCons n (SCons h t)) (SCons h (sInsert n t))
    sInsertionSort ::
      forall (t :: [Nat]). Sing t -> Sing (InsertionSort t)
    sInsertionSort SNil = SNil
    sInsertionSort (SCons h t) = sInsert h (sInsertionSort t)