Implement support for user-defined type errors.

Authored by yav on Sep 9 2015, 11:37 AM.



Implements Lennart's idea from the Haskell Symposium.
Users may use the special type function TypeError, which is
similar to error at the value level.

See Trac ticket, and wiki page

Test Plan


Diff Detail

rGHC Glasgow Haskell Compiler
Automatic diff as part of commit; lint not applicable.
Automatic diff as part of commit; unit tests not applicable.
yav retitled this revision from to Implement support for user-defined type errors..Sep 9 2015, 11:37 AM
yav updated this object.
yav edited the test plan for this revision. (Show Details)
yav added reviewers: simonpj, austin, hvr.

Is there a specification of this feature anywhere? For example, should the expression id :: TypeError "blah" -> TypeError "blah" type-check? Is it ever possible to get a Core program with TypeError in it? Should we check this in Lint?

Thanks for jumping in with this! I think it will be useful.

1144 ↗(On Diff #4132)

Why do this?


I think having custom treatment here obscures things rather than improves them.

yav added a comment.Sep 9 2015, 1:45 PM

Is there a specification of this feature anywhere? For example, should the expression id :: TypeError "blah" -> TypeError "blah" type-check? Is it ever possible to get a Core program with TypeError in it? Should we check this in Lint?

Thanks for jumping in with this! I think it will be useful.

I think of instances like:

instance TypeError (Text "something") => Show (a -> b) where ...
type instance F a = TypeError (Text "something")

almost as a special language constructs (e.g., the first one has some similarities with the fails instances from the work on instance chains). Anyway, implementing them with a type function (as Lennart suggested) seems fairly natural and easy. It does have the unfortunate side-effect of allowing you to write TypeError in places where it doesn't really make sense to do so (e.g., writing it directly in a type signature, or as a field of a datatype).

In terms of semantics, TypeError has the same semantics as any other partial type-level function and is basically the same thing as Any with an annotation on it. The intention is that there should be no instance of TypeError, so maybe we should declare it is a closed TypeFamily with no equations? I think that with the current implementation, TypeError may appear in Core, and while I don't think that's every useful, it is also not any more unsafe than any other partial function.

1144 ↗(On Diff #4132)

When a type function is about to reduce to TypeError, we emit a special constraint: it is also TypeError, but at kind Constraint. You may think of this constraint as being similar to a CHoleCan, in that it will never be solved---it is just there so that we can report the type error later.

The code here ensure that GHC does not short-cut this process and reduce to TypeError directly.


If you don't do this, you get a really ugly error message when a type error appears somewhere in a GHC message. For example, currently you'd get something like this:

   The record { a: Int, B: Char } does not have field C
    When checking that 'example' has the inferred type
        example :: (type error)

If we don't do the special rendering of type errors, then where you see (type error) you get a big ugly type describing the same type error as the nicely rendered version above. It would looks something like TypeError (Text "The record " :<>: Text "{ " :<>: Text "a" ...)

Yeah, not entirely sure what's going on with this yet. Some basic stuff, but I'll do another pass when there's a spec. :)


Comments plz!




More seriously, are these just "This is a bug case", or "I don't know if this can happen" case? Because either way we should probably make it clear what's going on.


Comments! Also, s/{-kind-}// please - might as well not mention kinds-without-data if it's not even in yet.

yav added a comment.Sep 10 2015, 5:42 PM

I don't think cases marked with ?? can happen, but they might if we were to add more combinators to the ErrorMessage kind, and we forgot to update this code. Rather than panic-ing while we are reporting a type error, I figured it is better to simply render the type as is, which would result in a less pretty error message, but at least nothing will crash in strange ways.


This is just a comment, intended to indicate that ErrorMessage is only intended to be used as a kind and it doesn't really make sense at the value levels. I think that removing the comment would make things less clear, not more so.

See also some questions added to the wiki page.


I would favor panicking in cases we believe should never happen. We want the panic and the ensuing bug report, I think.

1144 ↗(On Diff #4132)

But won't the custom TypeError processing happen regardless? This is a case of reducing to TypeError, not reducing a use of TypeError.

1295 ↗(On Diff #4132)

What happens here if we have a Given TypeError constraint? See more on the wiki page.


I see your point. Perhaps then have TypeError ... printed out, so that users know that the error relates to TypeError? The current output could be confusing to the uninitiated.

Is there anything that will prevent the error from being emitted multiple times? One idea would be to have TypeError reduce to Any but emit the error (as an insoluble) along the way.

yav added a comment.Sep 11 2015, 12:43 AM

When I emit the custom type error, I treat it as "very important" (see "custom_error" in reportWanteds, in TcErrors) so as soon as GHC sees a custom one, it reports it and then stops, so it does not report more errors. I figured since the most common use of this feature is DSLs, it might be better to first fix all custom errors one at a time, without having to worry about many errors at once.

austin requested changes to this revision.Sep 11 2015, 3:30 AM
austin added inline comments.

Yes, I agree with @goldfire, which is what I was going to get at. I would much rather have these cases panic, so that we don't forget this in the future. And if these names for ErrorMessage and this case statement needs to be in sync, we should mention that in a Note and in the panic message IMO, for a more informative bug report.

Default fall through cases are eeevil.


OK, but in that case, mention it in the documentation for ErrorMessage instead - otherwise a user won't get any indication this is the case, because they'd have to view the source anyway to see it.

I guess my complaint is that if the syntax is there when I read it, it alludes to some sort of Haskell that maybe does/might/can/did exist - but we don't know what it is yet and it's "not enabled", which feels weird. Types-are-kinds are going to happen sooner than later too, so ErrorMessage would need this anyway in lieu of the real syntax (in fact a lot of questions like this about many APIs opens up when types-are-kinds, but you get the drift).

It doesn't matter that much ultimately, but I do want the docs at least. Perhaps instead we should just note that "When we can declare only new kinds without declaring data, this should only be a kind" in a note to the side, as a TODO. I feel like we really might want to do a pass on the libraries for things like this, but that's a totally separate discussion.

This revision now requires changes to proceed.Sep 11 2015, 3:30 AM
simonpj updated the Trac tickets for this revision.Sep 11 2015, 3:45 AM
simonpj updated this object.

See comments on the wiki page.

1295 ↗(On Diff #4132)

I'm somewhat inclined to have a Ct data constructor here, along the lines of CHoleCan. But that's a fairly narrow engineering issue.

In D1236#34478, @simonpj wrote:

See comments on the wiki page.

I don't. Did you mean to add some? The edit to the wiki page I see you've made is just formatting.

bgamari requested changes to this revision.Oct 28 2015, 6:46 AM

Looks good other than the comments above.


Absolutely, please fail instead of the current behavior.


I would agree that needs some proper Haddock documentation.

yav updated this revision to Diff 4766.Oct 29 2015, 3:46 PM

Implements latest discussion.

yav updated this revision to Diff 4768.Oct 29 2015, 3:55 PM
  • Add Haddoc documentation.

Looks pretty good to me. Any test cases?

Thanks, Iavor.

yav updated this revision to Diff 4885.Nov 2 2015, 11:49 AM

Implement more aggressive reporting of custom type errors.

bgamari requested changes to this revision.Nov 11 2015, 4:33 AM

It's getting close. One comment inline. Otherwise this looks pretty good to me.


Indeed, the current (type error) text really isn't specific enough. Perhaps TypeError or user-defined type error would be better?

This revision now requires changes to proceed.Nov 11 2015, 4:33 AM
goldfire requested changes to this revision.Nov 11 2015, 8:03 AM

This still needs test cases.

yav updated this revision to Diff 5046.Nov 11 2015, 3:54 PM
  • Report a custom type error if a class parameter is (type error).
  • Refactor to avoid code duplication; rendering is now a pure function.
  • Move custom printing of TypeError with custom printing of tycons.
  • Move recognition of TypeError msg to Type.hs
  • Remove unused imports
  • Move custom rendering for ErrorMessage to Type.hs
  • Check that inferred and user-specified types od not mention TypeError directly
  • Change the rendering of user-defined type errors to (TypeError ...)
  • Add some tests.
bgamari accepted this revision.Nov 16 2015, 9:46 AM

Looks good to me as well. Thanks @yav!

This revision was automatically updated to reflect the committed changes.