Fixes on instance member function type checking

[rodrigogribeiro]

• Fixes the instance member function type checking.
• Updates test cases and stdlib code which had instances which were wrongly accepted by the type checker.

[d-xo]

when checking instances this is not necessary.

why?

[rodrigogribeiro]

Let's consider the following function:

forall a . function id() : ((a) -> a) {
    return lam(x) {return x ; } ;
}

This will be desugared into the following function and unique type for the lambda:

function lambda_impl3 (x<$2> : $2) -> $2 {
   return x<$2>;
}

data t_lambda_impl34 ($2) = t_lambda_impl34;

After generating these new definitions, function id will be

forall $2 . function id() -> t_lambda_impl34($2) {
   return t_lambda_impl34;
}

Note that id's type has changed and if we unify the return type of id with its annotated type, we get a unnecessary type error. The implementation avoid this error by determining when we have a type change in the function, using the following condition:

let tynames = tyconNames t1'
changeTy <- or <$> mapM isUniqueTyName tynames

which basically checks if the inferred type for function body (t1') changed during the inference.

However, when we discovered the problem in instance member function signature checking (which was accepting functions with a type most general than its expected type), I fixed this problem that make me discover another one: the lack of unification on the return type in invokable instances for functions like id
are making the compiler incorrectly reject them. The fix consists in, when checking instance member functions, we should unify arguments, even if it mentions unique type names. Because of that, I changed the condition to:

let tynames = tyconNames t1'
changeTy <- or <$> mapM isUniqueTyName tynames 
let rt2 = if changeTy && incl then t1' else rt1'

The incl argument is always false in calls to tcFunDef, in this way, we get the right value for rt2 and unificaion succeeds, as it should.

I know that his is not the best solution for this... This is one of the reasons that I believe that we should not do desugaring during type inference.