How to exclude nonsensical types without relying on type inference?

Question

I've been working on a type validator for Javascript to enable gradual typing for a language that was originally designed for dynamic types.

Type validation means there is only type checking of terms with explicit type annotations but no inference. Unfortunately, such an approach is unsound, because it allows to type programs as the following:

foo :: ([a] -> [a]) -> [b] -> [c] -> ([b], [c])
foo f xs ys = undefined
-- foo f xs ys = (f xs, f ys)

rev :: [d] -> [d]
rev xs = undefined
-- rev = foldl (flip (:)) []    

r = foo rev ['a', 'b'] [True, False]

This type checks, because type inference is bypassed. However, r has no value, because the function application requires a higher-ranked type. While Haskell terminates the program as soon as r's evaluation is enforced, in Javascript such a program would be valid, even though my type validator should reject it.

My first idea was to analyze the type annotation and to check if function arguments are compatible with one of the other arguments, but such an approach feels off.

Is there a more principled way to rule such types out without relying on type inference?

Answer 1

The goal is to rule out nonsensical type annotations without inferring from terms to types, because checking definitions is not part of my type validator (it is to hard considering JS' complex syntax).

What I cannot guarantee is that an explicit type annotation matches a given expression. However, I should be able to rule such type annotations out that have no inhabitants at all.

I don't have any experience with proof theory but I guess sequent calculus comes close to what I need. Here is an attempt to apply it to the problem at hand:

([a] -> [a]) -> [b] -> [c] -> ([b], [c])

f: [a] -> [a]
x: [b]
y: [c]
------------
goal: ([b], [c])

apply f
----------
subgoal: [a]

ABORT

Maybe someone with more experience can tell, if I am on the right track.