TypeHoles: errors, warnings, and deferring

[Sean Leather]

(I'm starting a new thread to focus on just this issue.)

On Thu, Oct 4, 2012 at 11:33 AM, Simon Peyton-Jones wrote:

>   (2) There is a strange case where an error is not reported for a
> missing type class instance, even though there is no (apparent) relation
> between the missing instance and the hole. (This also relates to
> the connection to `undefined', but less directly.)
>
> **
>
> ** **
>
> Yes; GHC classifies type errors into two groups:****
>
> **·         **insoluble (eg Int~Bool) are definitely wrong****
>
> **·         **unsolved (eg Eq a) might be ok if (say) the context changed*
> ***
>
> If there are any insolubles (anywhere), error messages about unsolved
> constraints are suppressed.  This is usually good; it focuses your
> attention on definite errors first.  Let’s call the suppressed errors
> “suppressed erorrs”.****
>
> ** **
>
> Now, holes are classified as “insoluble” at the moment, and that’s why all
> other unsolved errors are suppressed.****
>
> ** **
>
> ** **
>
> At the moment, if you way –XTypeHoles you get only a *warning *even
> though it’s really an error.  Moreover it’s weird that the * warning*suppresses other
> *error* messages.****
>
> ** **
>
> So I propose to change it so that –XTypeHoles gives an error message (for
> holes); and you can use –fdefer-type-errors to defer it.****
>
> ** **
>
> In doing this I also realised that with –fdefer-type-errors you only get
> warnings for the things that would previously have been errors; you don’t
> get warnings for “supressed errors”.  And that’s arguably bad, since you
> don’t know about all the errors you are deferring to runtime.  So I’ve
> changed it so that with –fdefer-type-errors you get **all** errors as
> warnings (no supression).
>

How do we report holes? As errors or warnings? What happens to other type
errors and warnings?

The following is the "ideal" approach that Thijs and I propose:

   1. A hole report is a warning.
   2. Any type error "caused" by a hole is also a warning.
   3. All other type errors are treated normally (e.g. errors are not
   deferred unless -fdefer-type-errors is used, insoluble errors suppress
   unsolved, and errors suppress warnings).


This approach provides the greatest convenience, the most useful
information, and the least surprise:

   - *Convenience*: You don't need -fdefer-type-errors when working with
   holes. One of our goals was to allow you to focus on the holes while
   trusting the program to be well-typed. Consequently, you use
   -fdefer-type-errors only if you want *all* errors to be deferred.
   - *Information*: You get more information by including the type errors
   caused by the hole. For example, the type of the hole in `show _` (e.g.
   `a0'), is not that useful on its own, but the additional warning of the
   missing instance (`Show a0`) is quite useful. If you were to suppress this
   warning, we would be missing crucial evidence for what you could use to
   fill the hole.
   - *Surprise*: If you replace a hole with `undefined' in the current
   implementation, you would be surprised by suddenly seeing new errors that
   you might not expect. If all of those errors were instead treated as
   warnings with the hole present, you would know what to expect.


We think the only type errors that fit the category of "being caused by a
hole" are unsolved constraints. That includes `show _' plus even examples
such as the following:

> f :: a -> a
> f x = x _

Currently, this only prints the hole warning, presumably because there are
no constraints on `a'.

Note that determining the unsolved constraints caused by a hole may be an
approximation. For example, consider the following code:

> data T a = T a
> instance Show (T Int) -- flexible instance
> g = show (T _)

We can see that the hole is the "cause" for the unsolved constraint, but
the type of the hole (`a0') is not in the top level of the constraint
(`Show (T a0)'). It may be that this remains an unsolved error. I think
that's acceptable.

You could view our description of a hole as an `undefined' with
locally-deferred type errors. This is clearly treating a hole as a
different sort of error. It doesn't seem to immediately fit into one of the
two groups: insoluble and unsolved. A hole warning doesn't suppress other
errors, but it could cause some unsolved errors to become warnings. I don't
think a hole will lead to any insoluble errors. If that's true, perhaps it
should not be considered insoluble itself. Perhaps a hole could be
considered a special form of unsolved error.

I'm not sure if our proposal fits nicely into GHC's design, but we think it
provides the best approach from a user's perspective.

Regards,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20121005/8aa60df1/attachment.htm>