IUCompilerCourse / python-student-support-code

Support for for students (Python)
MIT License
57 stars 38 forks source link

typechecking of closures is bogus #10

Open AndrewTolmach opened 1 year ago

AndrewTolmach commented 1 year ago

Currently, type_check_Llambda.py treats the type of a closure as being the type of the corresponding tuple. But this makes it impossible to obtain type equality for two lambdas that have closures with different shapes. Indeed, it is well-known that type-checking closure-converted code requires existential types.

This problem has been masked partly because the test suite doesn't contain any triggers, and partly because type_check_Ltup.py currently fails to compare tuples properly (it doesn't check that they have the same length).

A test file that demonstrates the problem is:

def p() -> Callable[[int], int]:
    b = True
    x = 42
    f : Callable[[int], int] = lambda z: z if b else 1
    g : Callable[[int], int] = lambda w: w if x == 42 else 1
    return f if True else g
print(p()(42))