{-

data Tick t a = Tick a
type T w a = T {v|v=w} a

pure :: x -> T 0 a
pure x = Tick x

</> :: t1 t2 -> T t1 (a -> b) -> T t2 a -> T (t1 + t2) b
Tick f </> Tick x = Tick (f x)

(++) :: xs:[a] -> ys:[a] -> T (len xs) {v|v=len xs + len ys}
[] ++ ys = pure ys
(x:xs') ++ ys = pure (x:) </> (xs' ++ ys)

(<*>) as forall a, b. t1:Int ~> t2: Int ~>
         Tick {v | v = t1} (a -> b)
      -> Tick {v | v = t2} a
      -> Tick {v | v = t1 + t2} b
Tick f <*> Tick x = Tick (f x)

(>>=) as forall a, b. t1:Int ~> t2: Int ~>
         Tick {v | v = t1} a
      -> (a -> Tick {v | v = t2} b)
      -> Tick {v | v = t1 + t2} b

step as forall a. t1:Int ~>
     -> m: Int
     -> Tick {v | v = t1} a
     -> Tick {v | v = t1 + m} a
step m (Tick x) = Tick x

(</>) as forall a, b. t1:Int ~> t2:Int
      -> Tick {v | v = t1} (a -> b)
      -> Tick {v | v = t2} a
      -> Tick {v | v = t1 + t2 + 1} b
(</>) = (<*>)

(++) :: forall a.
     -> xs: [a]
     -> ys: [a]
     -> Tick {v | v = length xs} {v | v = length xs + length ys}
[] ++ ys = pure ys
(x:xs') ++ ys = pure (x:) </> (xs' ++ ys)

reverse :: xs:[a] -> Tick {v | v = ((length xs * length xs) / 2) + ((length xs + 1) / 2)} [a]
reverse [] = pure []
reverse (x:xs) = reverse xs >>= (++ [x])
-}

measure mNil :: List [>Int] -> Bool
measure mCons :: List [>Int] -> Bool
measure mLength :: List [>Int] -> Int
measure not :: Bool -> Bool

empty as x:(List >Int) -> {v: Bool | (v == mNil x) /\ (v == not (mCons x)) /\ (v == (mLength x == 0))}
empty = (0)

nil as {v: List >Int | (mNil v) /\ (mLength v = 0) /\ (not (mCons v))}
nil = (0)

cons as x:Int -> xs:(List >Int) -> {v: List >Int | (mCons v) /\ (mLength v = mLength xs + 1) /\ (not (mNil v))}
cons = (0)

first as {v: List >Int | mCons v} -> Int
first = (0)

rest as rs:{v: List >Int | mCons v} -> {v: List >Int | mLength v == mLength rs - 1 }
rest = (0)

pure as rforall a. x:a -> Tick >{v:Int | v == 0} >a
pure = (0)

ap as rforall a, b. t1:Int ~> t2:Int ~>
  (Tick >{v:Int | v == t1} >x:a -> b) ->
  Tick >{v:Int | v == t2} >a ->
  Tick >{v:Int | v == t1 + t2 + 1} >b
ap = (0)

ap0 as rforall a, b. t10:Int ~> t20:Int ~>
  (Tick >{v:Int | v == t10} >x:a -> b) ->
  Tick >{v:Int | v == t20} >a ->
  Tick >{v:Int | v == t10 + t20} >b
ap0 = (0)

append :: xs:(List >Int) -> ys:(List >Int) ->
  Tick >{v:Int | v = mLength xs} >{v: List >Int | mLength v = (mLength xs) + (mLength ys)}
append = \xs -> \ys ->
  if empty xs
    then pure ys
    else (ap (pure (\rest -> cons (first xs) rest)) (append (rest xs) ys))

mapA :: n:Int ~>
  (x:Int -> Tick >{v:Int | v == n} >Int) ->
  xs:(List >Int) ->
  Tick >{v:Int | v == n * (mLength xs)} >(List >Int)
mapA = \f xs ->
  if empty xs
    then pure nil
    else (ap0 (ap0 (pure cons) (f (first xs))) (mapA f (rest xs)))