import language.higherKinds
import language.implicitConversions

sealed trait Nat {
  type +[N <: Nat] <: Nat
  def +[N <: Nat](n: N): +[N]
}

sealed trait _0 extends Nat {
  type +[N <: Nat] = N
  def +[N <: Nat](n: N) = n
}

case object _0 extends _0

case class S[N <: Nat](n: N) extends Nat {
  type +[M <: Nat] = S[N# + [M]]
  def +[M <: Nat](m: M) = S(n + m)
}

trait Monoid[M] extends MonoidLow[M] {
  type Zero <: M
  type Append[A <: M, B <: M] <: M
  def zero: Zero
  def append[A <: M, B <: M](a1: A, a2: B): Append[A, B]
}

trait MonoidLow[M] { self: Monoid[M] =>
  def leftIdentity[A <: M](a: Append[Zero, A]): A
  def rightIdentity[A <: M](a: Append[A, Zero]): A
  def associativity[A <: M, B <: M, C <: M](a: Append[A, Append[B, C]]): Append[Append[A, B], C]
}

object NatInstance extends Monoid[Nat] {
  type Zero = _0
  type Append[A <: Nat, B <: Nat] = A# + [B]
  def zero = _0
  def append[A <: Nat, B <: Nat](a: A, b: B) = a + b
  def leftIdentity[A <: Nat](a: Append[Zero, A]) = a
  implicit def rightIdentity[A <: Nat](a: Append[A, Zero]) = a
  implicit def associativity[A <: Nat, B <: Nat, C <: Nat](a: Append[A, Append[B, C]]) = a
}