Typechecking error: was throwing away information

[amosr]

I broke case expressions when I rewrote the generateP constraint generation function. The case typechecking was typechecking the scrutinee and getting its type, as well as keeping the substitution (the things you learned while typechecking). And it was sending the substitution downwards, but when it returned the new substitution upwards, I forgot to include the scrutinee part.

Num t0; v : (Bool, t0) |- case (fst v) | True -> False | False -> True end 

when you typecheck the scrutinee, you introduce new type variables t1 and t2 for the arguments to fst, before unifying them with the type of v. So you learn that t1 = Bool and t2 = t0. But if you don't return the substitution upwards, you forget the fact that t2 = t0, and end up with the annotated program saying that the (fst : (Bool,t2) -> Bool), which gets defaulted to unit at the top-level.

Anyway this fixes it.

! @jystic @tranma /jury approved @jystic

[jacobstanley]

:avocado:

[tranma]

cool