[Ur] First-Class Polymorphism example

[Marc Weber]

http://impredicative.com/ur/tutorial/tlc.html
shows this example:

  type nat = t :: Type -> t -> (t -> t) -> t
  val zero : nat = fn [t :: Type] (z : t) (s : t -> t) => z
  fun succ (n : nat) : nat = fn [t :: Type] (z : t) (s : t -> t) => s (n [t] z s)

  val one = succ zero
  val two = succ one
  val three = succ two

  three [int] 0 (plus 1)
  == 3

  three [string] "" (strcat "!")
  == "!!!"

Eg the succ function has t in its return type and in it n:nat arg.
So should urweb be able to deduce type of t automatically? Should it be
possible to replace the explicit :: by an implicit t ::: Type ?

Trying to do so I get some unification errors - is it because I removed
some [t] like args incorrectly?

Marc Weber