[Ur] Unexpected type error: "Substitution in constructor is blocked by a too-deep unification variable"

[Vag Vagoff]

Hi!

Why rev1 is ok and rev2-4 throws "Substitution in constructor is blocked by a too-deep unification variable" while types seems to be ok?

fun rev1 [e ::: Type] (xs : list e) (ys : list e) =
     let
	fun rev1' xs ys =
	    case xs of
		[] => ys
	      | x :: xs => rev1' xs (x :: ys)
     in
	rev1' xs ys
     end

fun rev2 [e ::: Type] (xs : list e) (ys : list e) =
     case xs of
	[] => ys
       | x :: xs => rev2 xs (x :: ys)

fun rev3 [e ::: Type] (xs : list e) (ys : list e) =
     case xs of
	[] => ys
       | x :: xs => @rev3 [e] xs (x :: ys)

fun rev4 [e ::: Type] (xs : list e) (ys : list e) =
     case xs of
	[] => ys
       | x :: xs => @@rev4 [e] xs (x :: ys)

Vag.