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.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
