Karn Kallio wrote:
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?
Include the return type, like this:
fun rev2 [e ::: Type] (xs : list e) (ys : list e) : list e =
case xs of
[] => ys
| x :: xs => rev2 xs (x :: ys)
To elaborate on why adding the return type helps:
This error message comes when type inference requires performing
substitution for a type variable found in a type that itself contains a
unification variable. Since we don't yet know which type the
unification variable will be replaced with, we don't know how to perform
substitution in it. There are approaches to handling this in a general
way, but I've avoided that complexity in the Ur/Web compilers to date.
Instead, I have an error signaled when there is not enough information
to be sure of computing a substitution soundly.
In this concrete example, the blocking unification variable was the one
standing for the return type of the reverse function. We know this type
may contain the parameter [e], but, without further information, we
don't know precisely which spots within the resolved type we will need
to drop the concrete choice of [e] into.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
