In the model linking phase it will be good to enforce types of expressions, and annotate nodes with types. We might not need a separate type checker then.
The current implementation of type inference (besides being unfinished) is way to general. We just need untyped (unit-less) built-in numeric type for constants, and allow local unification with typed values. In absence of type variables and named type-less constants, this should suffice to soundly type check. If we introduce named typeless constants one day, then the worst thing that can happen is that the unit of the constant will be dynamic depending on the context (but most likely we will make named constants typed).
So kill the current implementation of inference and make it simpler.
wasowski
commented
6 years ago
In the model linking phase it will be good to enforce types of expressions, and annotate nodes with types. We might not need a separate type checker then.
The current implementation of type inference (besides being unfinished) is way to general. We just need untyped (unit-less) built-in numeric type for constants, and allow local unification with typed values. In absence of type variables and named type-less constants, this should suffice to soundly type check. If we introduce named typeless constants one day, then the worst thing that can happen is that the unit of the constant will be dynamic depending on the context (but most likely we will make named constants typed).
So kill the current implementation of inference and make it simpler.