Make the Con and Con' patterns produce evidence

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



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.

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


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

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

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.



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.