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

[Adam Chlipala]

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.