If a variable or function is declared with a type signature it is currently unified against the type of the right hand side expression instead of simply checked for equality. This means that the following snippet:
foo (x: a) : a = x + 1
Type checks despite the actual inferred type of foo being Int a -> Int a. To fix this, we'll need to check for type equality if a type signature is already present, and fallback to unification only if it is not. When checking type equality we'll need to be careful to call follow_all_bindings on each type to ensure any type variable links are already followed, otherwise they can fail the equality check on otherwise equal types.
I'm marking this "good first issue" mostly for those already familiar with Hindley Milner type systems as it only requires learning part of Ante's type checking pass.
If a variable or function is declared with a type signature it is currently unified against the type of the right hand side expression instead of simply checked for equality. This means that the following snippet:
Type checks despite the actual inferred type of
foo
beingInt a -> Int a
. To fix this, we'll need to check for type equality if a type signature is already present, and fallback to unification only if it is not. When checking type equality we'll need to be careful to callfollow_all_bindings
on each type to ensure any type variable links are already followed, otherwise they can fail the equality check on otherwise equal types.I'm marking this "good first issue" mostly for those already familiar with Hindley Milner type systems as it only requires learning part of Ante's type checking pass.