Bizarre (printing of?) type error

[blerner]

The following program, when typechecked and run (on either CPO or pyret-horizon):

fun f(x :: Number) -> Number:
  x
end
g :: Function<String, String> = f

yields the following weird error message:

Type checking failed because of a type inconsistency. The type constraint Any<String, String> was incompatible with the type constraint (Number -> Number)

What on earth is an Any<String, String>?

[mkolosick]

I think Function is aliased to top which prints as Any. Is Function just for binary functions or how is it supposed to work?

[blerner]

Function is the type of all functions -- it's blatantly imprecise, and (I'm guessing) not terribly useful from a static type-checking perspective. But what's weirder about it is allowing the two type arguments -- why should Any/top/Function accept any type arguments at all?

[mkolosick]

It would seem that I am not checking that a type application makes sense upon reading annotations.

[blerner]

Well, a :: List<String, String> = empty does indeed yield a useful (though ugly) message that List<String, String> is inconsistent with List<?-1>, so you do clearly do some arity checking...

[mkolosick]

Yeah there's code in there to do this sort of thing. I just need to use it in at least one more place.