When we type infer, we check to see that there are enough known types around to choose a rule. However, with user help we can implement a no-score type inference, allowing for even stronger inference.
Essentially, even if the user gives us that an operation is, for example d_0, we can only infer types if one is already known. But we know that this operator can only have a very specific src/tgt, so even if they were both :infer, we could guess that these types must be Form0 and Form1 respectively.
Implementing this may require two sets of rules for each op set that may then be combined together. One will have untyped generic names, like d, that require scoring and one will have typed names, like d_0, that can use the aggressive inference above.
When we type infer, we check to see that there are enough known types around to choose a rule. However, with user help we can implement a no-score type inference, allowing for even stronger inference.
Essentially, even if the user gives us that an operation is, for example
d_0, we can only infer types if one is already known. But we know that this operator can only have a very specific src/tgt, so even if they were both:infer, we could guess that these types must beForm0andForm1respectively.Implementing this may require two sets of rules for each op set that may then be combined together. One will have untyped generic names, like
d, that require scoring and one will have typed names, liked_0, that can use the aggressive inference above.