typecheck: Disallow users to write instances of KnownNat and KnownSym
ClosedPublic

Authored by sjorn3 on Dec 24 2016, 10:45 AM.

Details

Summary

As noted in Trac #12837, these classes are special and the user should not be able to define their own instances.

Test Plan

Validate

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.
sjorn3 updated this revision to Diff 10180.Dec 24 2016, 10:45 AM
sjorn3 retitled this revision from to compiler: fix trac issue #12837.
sjorn3 updated this object.
sjorn3 edited the test plan for this revision. (Show Details)
sjorn3 added a comment.EditedDec 24 2016, 10:54 AM

It may be beneficial to define rejectedClassNames (or similar) in PrelNames, and then import that instead of a potentially long list of imported class names.

mpickering requested changes to this revision.Dec 24 2016, 11:00 AM
mpickering added a reviewer: mpickering.
mpickering added a subscriber: mpickering.

Thanks @sjorn3 . I added Adam as a reviewer, could you please edit the differential title and description to describe the change you have made? The commit message is based on this information. so it is best to be a bit more descriptive.

Perhaps something like "Disallow users to write instances for KnownNat and KnownSymbol" and make sure to reference the ticket in the description.

This revision now requires changes to proceed.Dec 24 2016, 11:00 AM

I think that should do it, let me know if that's what you were after.

goldfire accepted this revision.Dec 28 2016, 9:47 AM
goldfire added a reviewer: goldfire.
goldfire added a subscriber: goldfire.

This patch solves the problem well and fits with existing code in the area. Thanks, @sjorn3 !

However, the existing code in the area is not as well organized as it could be. Perhaps we can improve. The problem is that TcInstDcls.tcClsInstDecl calls the doClsInstErrorChecks function edited here. That function starts out by calling TcHsType.tcHsClsInstType, which calls TcValidity.checkValidInstance which calls TcValidity.checkValidInstHead. That last function prevents hand-written instances of the so-called abstract classes, which are (~), (~~), and Coercible. However, we really should add Typeable, KnownNat, and KnownSymbol to this list and then move the check that's in doClsInstErrorChecks to checkValidInstHead. It's just painful to have two separate checks for the same sort of problem.

I propose this logic: doClsInstErrorChecks does the checks that depend on the body of the instance (currently, this would just be the no-bindings-in-boot-files check) and checkVAlidInstHead does the checks that depend on the type (or other bits in the instance head). According to this logic, the abstract-class check moves.

Of course, I'm asking here just to clean up some existing mess and am happy to mark the current patch for acceptance as is, if you'd prefer to get the patch in. Thanks again!

bgamari retitled this revision from compiler: fix trac issue #12837 to typecheck: Disallow users to write instances of KnownNat and KnownSym.Dec 28 2016, 2:16 PM
bgamari updated this object.
bgamari edited the test plan for this revision. (Show Details)
bgamari edited edge metadata.
bgamari updated the Trac tickets for this revision.
bgamari requested changes to this revision.Dec 28 2016, 2:19 PM
bgamari edited edge metadata.

@sjorn3, great work. Regarding @goldfire's proposed refactoring I would be perfectly happy to merge this as-is so long as a regression test is added. See the Wiki for details on how to add a new testcase.

Thanks for the comments @goldfire and @bgamari, and for the help @mpickering.

Regarding the refactoring, for now I'd rather just get the patch in as I have exams coming up (last on the 10th) and need to focus on them, but would be happy to give it a go once they're done with.

I'll take a look at writing a regression test tomorrow evening, thanks again.

mpickering accepted this revision.Dec 29 2016, 2:22 PM
mpickering edited edge metadata.
sjorn3 updated this revision to Diff 10215.Dec 31 2016, 5:17 PM
sjorn3 edited edge metadata.

Added a regression test for the changes.

This comment was removed by sjorn3.
sjorn3 updated this revision to Diff 10216.Dec 31 2016, 5:27 PM
sjorn3 edited edge metadata.

Fixing the diff to the right commit

Got a bit muddled there, sorry about that. I think this should be about right @bgamari but I'd better wait to see if it passes.

This revision was automatically updated to reflect the committed changes.

I committed this for you Sean, thanks for the patch. The tests were failing due to another problem which has since been fixed.

sjorn3 added a comment.Jan 2 2017, 5:30 PM

Thanks Matt, should I set this to resolved on track?

adamgundry edited edge metadata.Jan 3 2017, 10:22 AM

Thanks very much @sjorn3 for taking this on, and to the others for the review. Sorry I missed this earlier due to the holiday.

In D2898#84650, @sjorn3 wrote:

Thanks Matt, should I set this to resolved on track?

No need, it has been committed and the Trac ticket has been closed.