{-# LANGUAGE GADTs, TypeInType, RankNTypes, TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
 
import Data.Type.Equality
import Data.Functor.Compose
 
-- A natural number type (that can be promoted to the type level)
data Nat = Z | S Nat
 
-- A List of length 'n' holding values of type 'a'
data List a n where
  Nil  :: List a Z
  Cons :: a -> List a m -> List a (S m)
 
type family (+) (a :: Nat) (b :: Nat) :: Nat where
  Z + n = n
  S m + n = S (m + n)
 
foldlVec :: forall p a m.
            (forall n. a -> p n -> p (S n)) ->
            p Z ->
            List a m -> p m
foldlVec pS pZ Nil         = pZ
foldlVec pS pZ (Cons x xs) = getCompose $ foldlVec pSS pSZ xs
  where
    pSS :: forall n. a -> Compose p S n -> Compose p S (S n)
    pSS = \x -> Compose . pS x . getCompose
    pSZ = Compose $ pS x pZ
 
newtype Aux a m n = Aux { getAux :: (a, List a (n + S m)) }
 
aux :: Ord a => List a n -> a -> List a m -> List a (n + S m)
aux xs prev acc = snd . getAux $ foldlVec step init xs where
  init = Aux (prev, Cons prev acc)
  step hd (Aux (prev', acc')) = Aux (hd, Cons (max hd prev') acc')
 
main = return ()

ey0jIExBTkdVQUdFIEdBRFRzLCBUeXBlSW5UeXBlLCBSYW5rTlR5cGVzLCBUeXBlT3BlcmF0b3JzLCBUeXBlRmFtaWxpZXMsIFR5cGVBcHBsaWNhdGlvbnMsIEFsbG93QW1iaWd1b3VzVHlwZXMgIy19CnstIyBMQU5HVUFHRSBTY29wZWRUeXBlVmFyaWFibGVzICMtfQoKaW1wb3J0IERhdGEuVHlwZS5FcXVhbGl0eQppbXBvcnQgRGF0YS5GdW5jdG9yLkNvbXBvc2UKCi0tIEEgbmF0dXJhbCBudW1iZXIgdHlwZSAodGhhdCBjYW4gYmUgcHJvbW90ZWQgdG8gdGhlIHR5cGUgbGV2ZWwpCmRhdGEgTmF0ID0gWiB8IFMgTmF0CgotLSBBIExpc3Qgb2YgbGVuZ3RoICduJyBob2xkaW5nIHZhbHVlcyBvZiB0eXBlICdhJwpkYXRhIExpc3QgYSBuIHdoZXJlCiAgTmlsICA6OiBMaXN0IGEgWgogIENvbnMgOjogYSAtPiBMaXN0IGEgbSAtPiBMaXN0IGEgKFMgbSkKCnR5cGUgZmFtaWx5ICgrKSAoYSA6OiBOYXQpIChiIDo6IE5hdCkgOjogTmF0IHdoZXJlCiAgWiArIG4gPSBuCiAgUyBtICsgbiA9IFMgKG0gKyBuKQoKZm9sZGxWZWMgOjogZm9yYWxsIHAgYSBtLgogICAgICAgICAgICAoZm9yYWxsIG4uIGEgLT4gcCBuIC0+IHAgKFMgbikpIC0+CiAgICAgICAgICAgIHAgWiAtPgogICAgICAgICAgICBMaXN0IGEgbSAtPiBwIG0KZm9sZGxWZWMgcFMgcFogTmlsICAgICAgICAgPSBwWgpmb2xkbFZlYyBwUyBwWiAoQ29ucyB4IHhzKSA9IGdldENvbXBvc2UgJCBmb2xkbFZlYyBwU1MgcFNaIHhzCiAgd2hlcmUKICAgIHBTUyA6OiBmb3JhbGwgbi4gYSAtPiBDb21wb3NlIHAgUyBuIC0+IENvbXBvc2UgcCBTIChTIG4pCiAgICBwU1MgPSBceCAtPiBDb21wb3NlIC4gcFMgeCAuIGdldENvbXBvc2UKICAgIHBTWiA9IENvbXBvc2UgJCBwUyB4IHBaCgpuZXd0eXBlIEF1eCBhIG0gbiA9IEF1eCB7IGdldEF1eCA6OiAoYSwgTGlzdCBhIChuICsgUyBtKSkgfQoKYXV4IDo6IE9yZCBhID0+IExpc3QgYSBuIC0+IGEgLT4gTGlzdCBhIG0gLT4gTGlzdCBhIChuICsgUyBtKQphdXggeHMgcHJldiBhY2MgPSBzbmQgLiBnZXRBdXggJCBmb2xkbFZlYyBzdGVwIGluaXQgeHMgd2hlcmUKICBpbml0ID0gQXV4IChwcmV2LCBDb25zIHByZXYgYWNjKQogIHN0ZXAgaGQgKEF1eCAocHJldicsIGFjYycpKSA9IEF1eCAoaGQsIENvbnMgKG1heCBoZCBwcmV2JykgYWNjJykKCm1haW4gPSByZXR1cm4gKCk=