Make the Con and Con' patterns produce evidence
ClosedPublic

Authored by dfeuer on Oct 29 2017, 10:07 PM.

Details

Summary

Matching with the Con and Con' patterns can reveal evidence
that the type in question is *not* an application. This can help
the pattern checker.

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
dfeuer created this revision.Oct 29 2017, 10:07 PM
bgamari requested changes to this revision.Oct 29 2017, 10:28 PM

Yes, this seems reasonable to me. Just a small suggestion

libraries/base/Data/Typeable/Internal.hs
460

YesApp and NoApp sound a bit odd. Perhaps call these IsApp and IsCon.

This revision now requires changes to proceed.Oct 29 2017, 10:28 PM
austin resigned from this revision.Nov 9 2017, 5:44 PM
dfeuer updated this revision to Diff 14705.Nov 15 2017, 9:32 PM

Rebase; rename constructors

dfeuer marked an inline comment as done.Nov 15 2017, 9:33 PM
dfeuer added inline comments.Nov 15 2017, 11:26 PM
libraries/base/Data/Typeable/Internal.hs
459

This may produce fairly poor errors when users include bad Con patterns. I haven't yet found a way to use TypeError to get good error messages that doesn't also confuse the pattern checker. What I can do is use a custom type rather than Bool as the result of IsApplication. I suppose I could (disgustingly) embed a message in the name of one of the constructors....

bgamari added inline comments.Nov 22 2017, 9:52 AM
libraries/base/Data/Typeable/Internal.hs
459

How poor is poor? Let's not try to solve a problem that we don't have.

bgamari requested changes to this revision.Dec 1 2017, 11:46 AM

@dfeuer is going to try to quickly improve the error messages produced by this.

This revision now requires changes to proceed.Dec 1 2017, 11:46 AM
dfeuer updated this revision to Diff 14870.Dec 1 2017, 2:56 PM

Improve error message for redundant Con/Con'

bgamari accepted this revision.Dec 1 2017, 3:03 PM

Assuming it validates this looks good to me.

libraries/base/Data/Typeable/Internal.hs
466

Clever.

This revision is now accepted and ready to land.Dec 1 2017, 3:03 PM
This revision was automatically updated to reflect the committed changes.