Support typechecking of type literals in backpack
ClosedPublic

Authored by ppk on Jul 10 2018, 8:24 AM.

Details

Summary

Backpack is unable to type check signatures that expect a data which
is a type level literal. This was reported in issue Trac #15138. These
commits are a fix for this. It also includes a minimal test case that
was mentioned in the issue.

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.
ppk created this revision.Jul 10 2018, 8:24 AM
ppk added a comment.Jul 12 2018, 3:35 AM

I noticed that there are some new line ugliness. Will add a commit for that.

ppk updated this revision to Diff 17278.Jul 12 2018, 3:39 AM
  • some newline cleanups.
bgamari accepted this revision.Jul 12 2018, 10:06 AM

Looks reasonable to me. Thanks!

This revision is now accepted and ready to land.Jul 12 2018, 10:06 AM
ppk added a comment.Jul 12 2018, 10:34 PM

Do you want me to do a commit sqashing. I think I can give better commit messages ?

ppk added a comment.Jul 12 2018, 10:41 PM

There is one clarification that I still need so may be you can just hold on before you merge. The function in question seems to be used both for hs-boot files and hsig files. The very next guard in the function check whether the function is for hsig and there is a comment there saying that it does not work with hsboot. Since I do not understand the code fully, can you confirm whether I should add such a check for this clause also

ppk added a subscriber: ezyang.Jul 14 2018, 11:14 AM

@ezyang I managed to fix this issue of Nats and Backpack. Can you have a look as there is somethings regarding hs-boot and hsig files here that are not clear to me.

ezyang accepted this revision.Jul 14 2018, 4:14 PM

Two nits:

  1. Shouldn't be enabled for hs-boot files (it's probably harmless, but we'd have to reason about it carefully first)
  2. Use a function like this in Type.hs https://lpaste.net/8942558089970712576

But I'd be happy to take this in for 8.6 without the nits.

ppk added a comment.Jul 14 2018, 5:03 PM

@ezyang Okey I will make the changes you suggested in a couple of days.

ppk updated this revision to Diff 17337.Jul 16 2018, 1:08 AM
  • allow type literal for data declaration spec only in hsig files.
  • added the test isLitTy to the Types module
  • simplify typecheck with isLitTy.
ppk updated this revision to Diff 17338.Jul 16 2018, 1:11 AM
  • typo in description of isLitTy.
ppk added a comment.Jul 16 2018, 11:10 AM

The windows build failed due to some strange problems. Shall I restart the build ?

bgamari added a comment.EditedJul 16 2018, 6:57 PM

Hmm, that is indeed quite peculiar. I've restarted it.

ppk added a comment.Jul 17 2018, 10:50 PM

I guess this is finally ready to merge. If there is anything pending please let me know @bgamari @ezyang.

In D4951#137103, @ppk wrote:

I guess this is finally ready to merge. If there is anything pending please let me know @bgamari @ezyang.

It looks like there are a few failing tests still:

TEST="bkpfail23 bkpfail25 bkpfail26 bkpfail27 bkpfail46"

I looked them over and they look like legitimate failures.

bgamari requested changes to this revision.Jul 27 2018, 2:28 PM
This revision now requires changes to proceed.Jul 27 2018, 2:28 PM
ppk added a subscriber: simonpj.Jul 28 2018, 2:18 AM

@ezyang can you have a look at the backpack tests that are failing. In light of what @simonpj says about the witness; it could be pretty serious

ppk added a comment.Jul 29 2018, 10:15 PM

It looks like there are a few failing tests still:

TEST="bkpfail23 bkpfail25 bkpfail26 bkpfail27 bkpfail46"

I looked them over and they look like legitimate failures.

@bgamari @ezyang. I am surprised that the tests now pass. How did that happen ? What changed ?
If everything is okey let me know. We still need to address the issue that @simonpj raised.

If everything is okey let me know. We still need to address the issue that @simonpj raised.

What issue did I raise? I don't see anything on the ticket or in the Phab log.I recall writing stuff about KnonwNat but isn't that a separate patch? Confused...

ppk added a comment.Jul 30 2018, 3:09 AM

If everything is okey let me know. We still need to address the issue that @simonpj raised.

What issue did I raise? I don't see anything on the ticket or in the Phab log.I recall writing stuff about KnonwNat but isn't that a separate patch? Confused...

Sorry the culprit is me. I was the one who was confused all along. Yeah I commented on the wrong phab.

In D4951#138039, @ppk wrote:

If everything is okey let me know. We still need to address the issue that @simonpj raised.

It looks to me like they are still failing, no?

ppk updated this revision to Diff 17555.Aug 2 2018, 4:34 AM
  • testsuite: Added test for Trac #15379.
  • hand-written instances only rejected when not in boot/sig files.
  • testsuite: T15379 updated with instances of KnownSymbol and Typeable.
  • allow instances of builtin classes only in hsig and not hboot
  • testsuite: update the stdout for T15379.
  • delay on-the-fly generation of instances for KnownNat and friends.
  1. Updating D4951: support typechecking of type literals in backpack fixes Trac #15138 #

I reorded the checks and now it succeeds all but bkpfail25.

ppk updated this revision to Diff 17556.Aug 2 2018, 4:47 AM

rebased with what is available on D4951.

ppk updated this revision to Diff 17557.Aug 2 2018, 4:48 AM

Sorry Wrong commits unknowingly pushed here.

bgamari requested changes to this revision.Aug 2 2018, 8:20 AM

I think your problems stem from the issue I point out inline.

compiler/typecheck/TcRnDriver.hs
1033

Did the or 'data bit get truncated?

1040

Shouldn't this be matching on Just True? We want to know not only that the unit's definition is a type synonym (the Just) but also that its RHS is a literal (the True).

This revision now requires changes to proceed.Aug 2 2018, 8:20 AM
bgamari added inline comments.Aug 2 2018, 8:22 AM
compiler/typecheck/TcRnDriver.hs
1040

I believe this is the reason why bkpfail46 is getting broken by your patch.

bgamari retitled this revision from support typechecking of type literals in backpack fixes #15138 to Support typechecking of type literals in backpack.Aug 2 2018, 8:22 AM
bgamari added inline comments.Aug 2 2018, 8:25 AM
compiler/typecheck/TcRnDriver.hs
1040

Ahh, isLitTy also returns a Maybe. Then perhaps you want Just _ <- synTyConDefn_maybe tc2 >>= isLitTy . snd.

ppk updated this revision to Diff 17561.Aug 2 2018, 9:57 AM
  • fixup: the just bug.
  • doc: fixup

Fixing the Just bug.

bgamari accepted this revision.Aug 6 2018, 5:28 PM

Looks good to me. Thanks @ppk!

This revision is now accepted and ready to land.Aug 6 2018, 5:28 PM
Closed by commit rGHC7d771987c276: Support typechecking of type literals in backpack (authored by Piyush P Kurur <ppk@cse.iitk.ac.in>, committed by bgamari). · Explain WhyAug 7 2018, 2:55 PM
This revision was automatically updated to reflect the committed changes.