Home My Page Projects Code Snippets Project Openings SML/NJ Bugs
Summary Activity Tracker Lists

[#220] Incorrect error message for equality-type failure?

Date:
2019-04-19 14:40
Priority:
3
State:
Closed
Submitted by:
Bug Submitter (webuser)
Assigned to:
David MacQueen (dbm)
Machine Architecture:
x86
Operating System:
Linux
Component:
Compiler
Resolution:
Fixed
Severity:
Minor
OS Version:
Debian 9
SML/NJ Version:
110.85
Keywords:
URL:
Transcript (of reproduction):
$ cat ullman-ex5.23.sml fun simpleMap F ys = if ys = nil then nil else let val x = hd ys val xs = tl ys in F(x) :: simpleMap F xs end ; simpleMap (fn x => x*x) [1.0, 2.0, 3.0] ; $ sml ullman-ex5.23.sml Standard ML of New Jersey v110.85 [built: Mon Feb 25 15:10:48 2019] [opening ullman-ex5.23.sml] ullman-ex5.23.sml:2.9 Warning: calling polyEqual val simpleMap = fn : (''a -> 'b) -> ''a list -> 'b list ullman-ex5.23.sml:11.1-11.40 Error: operator and operand do not agree [overload conflict] operator domain: [* ty] list operand: real list in expression: (simpleMap (fn x => <exp> * <exp>)) (1.0 :: 2.0 :: 3.0 :: nil)
Source (for reproduction):
fun simpleMap F ys = if ys = nil then nil else let val x = hd ys val xs = tl ys in F(x) :: simpleMap F xs end ; simpleMap (fn x => x*x) [1.0, 2.0, 3.0] ;
Summary:
Incorrect error message for equality-type failure?

Detailed description
What appears to be an equality type error results in an error message
complaining about incorrect overloading of *.

The sample code is a version of map that tests whether the argument list is
empty using the = operator. Thus the list must be an equality type, and in
fact the map function is correctly typed as

(''a -> 'b) -> ''a list -> 'b list

But when the map function is used to map fn x => x*x over a real list, the
complaint is that real is not a [* ty].

My understanding is that the problem is not with fn x => x*x, because the
overloading is not resolved to a default type until a top-level declaration.
Indeed, if I change ys = nil to null ys in simpleMap, no type errors are
reported.


Submitted via web form by Norman Danner <ndanner@wesleyan.edu>

Comments:

Message  ↓
Date: 2020-04-09 21:49
Sender: David MacQueen

Here 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?

Attached Files:

Changes

Field Old Value Date By
status_idOpen2020-04-21 16:48jhr
close_dateNone2020-04-21 16:48jhr
ResolutionNone2020-04-21 16:48jhr
Transcript (of reproduction)$ cat ullman-ex5.23.sml fun simpleMap F ys = if ys = nil then nil else let val x = hd ys val xs = tl ys in F(x) :: simpleMap F xs end ; simpleMap (fn x => x*x) [1.0, 2.0, 3.0] ; $ sml ullman-ex5.23.sml Standard ML of New Jersey v110.85 [built: Mon Feb 25 15:10:48 2019] [opening ullman-ex5.23.sml] ullman-ex5.23.sml:2.9 Warning: calling polyEqual val simpleMap = fn : (''a -> 'b) -> ''a list -> 'b list ullman-ex5.23.sml:11.1-11.40 Error: operator and operand do not agree [overload conflict] operator domain: [* ty] list operand: real list in expression: (simpleMap (fn x => <exp> * <exp>)) (1.0 :: 2.0 :: 3.0 :: nil) 2019-04-23 12:19jhr
Source (for reproduction)fun simpleMap F ys = if ys = nil then nil else let val x = hd ys val xs = tl ys in F(x) :: simpleMap F xs end ; simpleMap (fn x => x*x) [1.0, 2.0, 3.0] ; 2019-04-23 12:19jhr
assigned_tonone2019-04-23 12:19jhr
detailsWhat appears to be an equality type error results in an error message complaining about incorrect overloading of *. The sample code is a version of map that tests whether the argument list is empty using the = operator. Thus the list must be an equality type, and in fact the map function is correctly typed as (''a -> 'b) -> ''a list -> 'b list But when the map function is used to map fn x => x*x over a real list, the complaint is that real is not a [* ty]. My understanding is that the problem is not with fn x => x*x, because the overloading is not resolved to a default type until a top-level declaration. Indeed, if I change ys = nil to null ys in simpleMap, no type errors are reported. Submitted via web form by Norman Danner <ndanner@wesleyan.edu> 2019-04-23 12:19jhr