headers
Sean Leather | 5 Oct 2012 14:55
Picon

TypeHoles: errors, warnings, and deferring

(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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Permalink | Reply |

Gmane