En la parte anterior definimos la función compatible? tal que solo ignora los modificadores en top level, es decir, si al recibir el mtype ignora su modificador, pero los tipos subyacentes los compara por igualdad.

Por esto, el siguiente programa es rechazado por typecheck:

{with {apply1 {fun {f : {Num -> Num}} -> Num : {f 1}}}
      {with {id {fun {x : {lazy Num}} -> Num : x}}
            {apply1 id}}}

Ya que el tipo {lazy Num} → Num no es compatible con Num → Num. Sin embargo, si suponemos la existencia de una función

La implementación de estrategias de evaluación realizada en la parte anterior tiene algunos problemas. En particular, para evitar errores de adaptación, implementamos un chequeo más estricto respecto a los modificadores de tipo en los argumentos/valores de retorno de las funciones.

En esta parte de la tarea, queremos implementar un ajuste de orden superior, que permita compatibilizar los tipos de entrada y salida de las funciones.