[MLton] funny error message

[Stephen Weeks]

> Ok, here is a pretty minimal example that produces the bad error
> message.

Now all is clear.  Here are the type schemes for flatmap and flatten
as determined by type inference on the structure.

  flatmap: forall 'a. ('a -> X stream) -> ('a stream -> X stream)
  flatten: X stream stream -> X stream

Here, X indicates a single unspecified type (not a generalizable type
variable).

The signature requires the type schemes for flatmap and flatten to be
the following.

  flatmap: forall 'a, 'b. ('a -> 'b stream) -> ('a stream -> 'b stream)
  flatten: forall 'a. 'a stream stream -> 'a stream

When matching, MLton first tries to match flatmap in the structure
against the signature.  This is done by instantiating flatmap in the
structure with a fresh unknown type, Y, and unifying the resulting
type

  (Y -> X stream) -> (Y stream -> X stream)

with the type of flatmap needed for the signature

  ('a -> 'b stream) -> ('a stream -> 'b stream)

The unification causes X = 'b and Y = 'a.  At this point the type of
flatmap becomes

  flatten: forall 'a. ('a -> 'b stream) -> ('a stream -> 'b stream)

Because 'b is not in the type scheme, MLton reports the following
error.

  Variable type in structure disagrees with signature.
    variable: flatmap
    unable to generalize: 'b
    signature: ('a -> 'b stream) -> ('a stream -> 'b stream)

If we stopped here, all would be well.  But, since MLton likes to
report as many errors as possible, it continues by comparing the type
of flatten in the structure

  flatten: 'b stream stream -> 'b stream

with the type scheme in the signature

  flatten: forall 'a. 'a stream stream -> 'a stream

In this case, there is nothing to instantiate, since the type in the
structure is a monotype, so MLton simply unifies

  'b stream stream -> 'b stream

with
  
  'a stream stream -> 'a stream

This gives the error that you saw

  Variable type in structure disagrees with signature.
    variable: flatten
    structure: ['a] stream stream -> ['a] stream
    signature: ['b] stream stream -> ['b] stream

The names for the tyvars appear switched because MLton chooses those
names at the last possible minute and only for printing an error
message.  The tyvars are really just distinct objects inside.

In short, the problem is a spurious error due to the prior error.  As
a reminder, it is always best to read errors from first to last, since
later errors may be spurious.

There are two ways I could see fixing this bug.

1. During the matching of flatmap, we could avoid unifying X because
   we know that it is not generalizable due to its occurrence in
   flatten.  We would still report the "unable to generalize" error on
   flatmap.  The matching of flatten would automatically do the right
   thing. 

2. We could allow the matching of flatmap to proceed, but notice
   during the matching of flatten that there are ungeneralized type
   variables.

(1) seems better because the type error for both flatten and flatmap
will be the same, while (2) will cause there to be a different error
for flatten.

I'm not sure how viable either of these really is, but I'll think
about it.  I'd like to hear other ideas too.