Right to left, inner expressions to outer expressions ('type inference')
Left to right, outer expressions to inner expressions ('type implication' / 'type constraints')
There are scenarios where these mechanisms could be applied but currently aren't and there are two different implementations of the second mechanism that should be unified, because currently type information doesn't propagate if the producer is using one implementation and the consumer expects the other
Producers of type implications:
Overload resolution produces type implications - where a single overload unambiguously matches the supplied argument types, even if some types are unknown or partially unknown, overload resolution will propose that overload and supply implied actual types for all arguments
Consumers of type implications:
Function literal arguments without explicit types will be assigned the type implied by the actual argument type of any matching overload. In this example, the argument of filter is already known to be int -> bool. The lambda argument n initially has unknown type, but a type implication of int -> bool is passed down into the lambda from the overload resolution for filter, and n picks up the type int from here
[1, 2, ,3 ,4] | .filter(n => n % 2 ==0)
Producers of type constraints:
Local variable definitions with explicit types and initializers. The explicit type is passed into the initializer as a type constraint.
Return statements in functions of non-void return type. The function return type is passed into the return statement expression as a type constraint
Expression body of functions of non-void return type. The function return type is passed into the expression body as a type constraint
Consumers of type constraints:
letin expressions - Any type constraint passed into a letin expression is propagated into its expression
if expressions - If expressions apply any supplied constraint to their branch expressions, in preference to inferring a common type. They also propagate any type constraint into their branches.
List literals - List literals use any type constraint as their element type, in preference to inferring a common type. The currently do not propagate any type constraint into their branches, but they arguably should.
Type constraints and type implications should be unified:
[ ] Overload resolution should be changed to produce type constraints instead of implications
[ ] Function literal argument type inference should be changed to consume type constraints instead of implications
[ ] Error messages may need to be clarified in the case where type constraints are not met for function literal arguments (should be reported as the compiler failing to correctly infer argument type, rather than misleadingly reporting that the user has supplied a value of incorrect type)
Type constraints could be produced in additional places:
[ ] Left side of assignment statements. This is awkward to implement, because the left side expects to be given an evaluated right side to consume. However, we could try to speculatively load the left side (rather than assign to it) in order to determine its type. If that succeeds, then push the resulting type into the right side as a constraint. If it fails, discard any errors and don't set any constraint. Destructuring would need to be handled differently - we'd need to create a tuple type corresponding to the left side pattern, but discard it if the right hand side is not a tuple literal (or something else comprised of only tuple literals like a list literal or if expression)
[ ] List literal element types. This would require a speculative first walk to determine LUB, and then a second actual walk where the element type determined by LUB is applied to each element as a type constraint. I think this is a requirement for supporting #1166 for tuple literals within a list literal)
Type inference in ghūl works in two directions:
There are scenarios where these mechanisms could be applied but currently aren't and there are two different implementations of the second mechanism that should be unified, because currently type information doesn't propagate if the producer is using one implementation and the consumer expects the other
Producers of type implications:
Consumers of type implications:
filter
is already known to beint -> bool
. The lambda argumentn
initially has unknown type, but a type implication ofint -> bool
is passed down into the lambda from the overload resolution forfilter
, andn
picks up the typeint
from hereProducers of type constraints:
Consumers of type constraints:
let
in
expressions - Any type constraint passed into alet
in
expression is propagated into its expressionif
expressions -If
expressions apply any supplied constraint to their branch expressions, in preference to inferring a common type. They also propagate any type constraint into their branches.Type constraints and type implications should be unified:
Type constraints could be produced in additional places: