Date: 2020-04-09 21:49 Sender: David MacQueenHere is a simpler test case:
- (fn x => (x = x; x * x)) 1.0;
stdIn:1.2-2.15 Error: operator and operand do not agree [overload conflict]
operator domain: [* ty]
operand: real
in expression:
(fn x => (<exp> = <exp>; <exp> * <exp>)) 1.0
The problem here is that the equality operation imposes a constraint that the type of x (as a metavariable or unification variable in the type inference algorithm) must be an equality type (i.e. the type metavariable has an equality attribute). The x*x subexpression means that that metavariable is instantiated to a special form of metavariable used for overloading resolution, which can only be instantiated to a limited set of ground types (like int, real). But the equality attribute is propagated with this instantiation, so
we now we have a type metavariable that is both an overloading resolution variable (for operation *) and an equality metavariable, which can only be instantiated to an equality type. When this is unified with type real, there is an error caused by the fact that real is not an equality variable.
So a solution of the bug could be to
(a) print the metavariable more accurately, as, e.g. [=,*-ty] to represent the two constraining attributes of the metavariable, and
(b) have the type error message make clear that the failure is due to real not being an equality type, instead of saying it is an “overload” conflict) (since real is a valid instantiation of the overloaded type of *
Of course, (a) would accomplish (b) indirectly (if we get rid of the “overload conflict” annotation.
This error situation can be revisited in the general rewrite of the type checker.
One notational issue or problem is how I am now printing type metavariables in error messages (they should never occur when printing the actual types resulting from type inference). There are various conventions. By default, they can be printed as ‘X (like a type variable but capitalized), and ‘’X can be used to denote a metavariable with the equality attribute (where X is a completely arbitrary name). I am using [* ty] to denote an _overloading resolution_ metavariable deriving from the overloaded “*” operator. So what is the best way to represent a metavariable which has the equality attribute and also is an overloading resolution metavariable? |