robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
84 stars 2 forks source link

Type mismatch errors don’t indicate the overall type being checked #76

Open robrix opened 5 years ago

robrix commented 5 years ago

This mostly matters in the context of dependent unification (cf #63): TypeMismatch errors are thrown for the individual subtypes that don’t unify, which may be arbitrary leaves of some much larger type. We should throw errors which include the overall types, and ideally highlighting the incompatible portions à la Elm.