Algoritmo de Unificación
Cuando se llama a una función o a un procedimiento, hay que unificar los tipos esperados por los mismos con los tipos actuales de las expresiones pasadas como argumento.
fun f(a : T, b : T) ret r : bool
where (T : Ord)
r := a < b
end fun
...
var b : bool
b := f(1, 2)
En la implementación hay una cuestión pendiente a resolver, y es la llamada de métodos con la constante null como argumento. En el sistema de tipos, este valor posee el tipo puntero polimórfico, por lo que no se puede inferir un tipo para el argumento con el que coincide. Un ejemplo posible, es el siguiente:
fun p(p : pointer of T) ret r : T
r := #p
end fun
...
var b : bool
b := p(null)
¿Cual debería ser el tipo de retorno de la función? ¿Bool? ¿Polimórfico? Debido a esta dificultad, actualmente no se permite la llamada de funciones o procedimientos con argumentos null (63fc35c9). Obviamente, esto es solo una solución temporal para asegurar el correcto funcionamiento del algoritmo de unificación implementado.