Type checker crashes when checking invalid function calls

[kyouko-taiga]

Minimal example

fun f() {}
fun g() {
  f(x: 0) 
}

The error is caused by the way constraints for a function call are solved. The above program will create the following constraints:

τf == () -> ()
τf == (x: τ0) -> τ1
τ2 <: τ0
τ2 ⊏ ExpressibleByIntLiteral

Because the number of parameters do not match, the solver won't create any additional constraint on τ0 when it solves τf == (x: τ0) -> τ1. Hence, it will eventually have to solve τ2 <: τ0 by guessing τ2 == τ0, causing τ0 to be bound to Int.

As a result, trying to reify (x: τ0) -> τ1 will violate FunType's invariant, as τ0 won't be bound to a parameter type.