Support builtin classes like KnownNat in backpack
ClosedPublic

Authored by ppk on Jul 19 2018, 7:54 AM.

Details

Summary

This commit allows backpack signatures to enforce constraints like KnownNat
on data types. Thus it fixes Trac #15379. There were two important differences in the
way GHC used to handle classes like KnowNat

  1. Hand crafted instances of KnownNat were forbidden, and
  1. The dictionary for an instance KnownNat T was generated on the fly.

For supporting backpack both these points have to be revisited.

Disallowing instances of KnownNat

Users were disallowed to declare instances of certain builtin classes
like KnownNat for obvious safety reasons --- when we use the
constraint like KnownNat T, we want T to be associated to a natural
number. However, due to the reuse of this code while processing backpack
signatures, instance KnownNat T were being disallowed even in module
signature files.

There is an important difference when it comes to instance declarations
in a signature file. Consider the signature Abstract given below

signature Abstract where
  data T :: Nat
  instance KnownNat T

Inside a signature like Abstract, the instance Known T is not really
creating an instance but rather demanding any module that implements
this signature to enforce the constraint KnownNat on its type
T. While hand crafted KnownNat instances continued to be prohibited in modules,
this commit ensures that it is not forbidden while handling signatures.

Resolving Dictionaries

Normally GHC expects any instance T of class KnownNat to eventually resolve
to an integer and hence used to generate the evidence/dictionary for such instances
on the fly as in when it is required. However, when backpack module and signatures are involved
It is not always possible to resolve the type to a concrete integer utill the mixin stage. To illustrate
consider again the signature Abstract

signature Abstract where

data T :: Nat
instance KnownNat T

and a module Util that depends on it:

module Util where

import Abstract
printT :: IO ()
printT = do print $ natVal (Proxy :: Proxy T)

Clearly, we need to "use" the dictionary associated with KnownNat T
in the module Util, but it is too early for the compiler to produce
a real dictionary as we still have not fixed what T is. Only when we
mixin a concrete module

module Concrete where

type T = 42

do we really get hold of the underlying integer.

In this commit, we make the following changes in the resolution of instance dictionary
for constraints like KnownNat T

  1. If T is indeed available as a type alias for an integer constant, generate the dictionary on the fly as before, failing which
  1. Do not give up as before but look up the type class environment for the evidence.

This was enough to make the resolution of KnownNat dictionaries work in the setting of Backpack as
when actual code is generated, the signature Abstract (due to the import Abstract ) in Util gets
replaced by an actual module like Concrete, and resolution happens as before.

Everything that we said for KnownNat is applicable for KnownSymbol as well.

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 19 2018, 7:54 AM
ppk added a comment.Jul 19 2018, 8:02 AM

@ezang okey finally the patch for Trac #15379 is ready for review. I am told that there is a way to put a dependency on D4951. How does one do it ?

ppk added a subscriber: ezyang.Jul 19 2018, 8:03 AM

Sorry I meant @ezyang

ppk retitled this revision from supprot builtin classes like KnownNat in backpack fixes #15379. to support builtin classes like KnownNat in backpack fixes #15379..Jul 19 2018, 8:04 AM
ppk added a reviewer: ezyang.

Looks good to me -- *except* please add a Note that explains the thinking, supported by the example from comment:4 of the ticket. And, of course, point to the ticket.

Thanks for doing this

Simon

compiler/typecheck/ClsInst.hs
297–298

Please point to a Note that explains

compiler/typecheck/TcInstDcls.hs
542 ↗(On Diff #17399)

Please point to a Note (the same Note) that explains.

ppk updated this revision to Diff 17402.Jul 20 2018, 12:25 AM
  • added note on evidence generation in the setting of backpack.
ppk updated this revision to Diff 17403.Jul 20 2018, 12:52 AM
  • added note on evidence generation in the setting of backpack.
ppk updated this revision to Diff 17404.Jul 20 2018, 1:08 AM
  • added note for why not to reject builtin classes in sig files.
ppk added inline comments.Jul 20 2018, 1:11 AM
compiler/typecheck/ClsInst.hs
297–298

I have added the note.

compiler/typecheck/TcInstDcls.hs
542 ↗(On Diff #17399)

I have added a bit of explanation and also a pointer to the evidence generation note.

ppk updated this revision to Diff 17405.Jul 20 2018, 1:13 AM

fixed typo in commit message.

bgamari requested changes to this revision.Jul 22 2018, 9:50 AM
bgamari retitled this revision from support builtin classes like KnownNat in backpack fixes #15379. to Support builtin classes like KnownNat in backpack.

This should also have at least something of a commit message. It's fine to pull some language from the Note.

This revision now requires changes to proceed.Jul 22 2018, 9:51 AM
ppk added a comment.Jul 23 2018, 10:56 PM

This should also have at least something of a commit message. It's fine to pull some language from the Note.

@bgamari

May I do the following (in addition to the suggestions)

  1. Merge commits that add/modify the test cases (2d5278135c27,e989c29416f7) and
  1. Merge the commits allows user to use KnownNat in sig/boot file (3aa48dd58c53) and the one that restricts it to only sig files.

I will add the notes that you suggest in those commit message.

In D4988#137506, @ppk wrote:

This should also have at least something of a commit message. It's fine to pull some language from the Note.

@bgamari

May I do the following (in addition to the suggestions)

  1. Merge commits that add/modify the test cases (2d5278135c27,e989c29416f7) and
  2. Merge the commits allows user to use KnownNat in sig/boot file (3aa48dd58c53) and the one that restricts it to only sig files.

    I will add the notes that you suggest in those commit message.

I don't have the commits that you refer to but note that in Phabricator each differential corresponds to a single commit when merged, so I believe these are already merged. To add a commit message simply modify Differential summary at the top of this page.

ppk updated this revision to Diff 17446.Jul 24 2018, 11:44 PM
  • testsuite: Added test for Trac #15379.
  • allow instance of builtin classes in hsig files.
  • support builtin classes like KnownNat in backpack fixes Trac #15379.
ppk edited the summary of this revision. (Show Details)Jul 25 2018, 5:20 AM
ppk edited the summary of this revision. (Show Details)Jul 25 2018, 5:23 AM
ppk edited the summary of this revision. (Show Details)Jul 25 2018, 5:26 AM
ppk edited the summary of this revision. (Show Details)

I'm puzzled about one thing. In the test case, module Util will look up the KnownNat NatType instance, and generate code that refers to the dictionary function, say $df78 :: KnownNat NatType.

I expect that when compiling Concrete.hs we'll generate a binding for $df78. (for hs-boot files it'd be created in TcRnDriver.checkHiBootIface)
But I don't see where that happens.

Can you extend the Note to explain this, and how the binding is actually created.

compiler/typecheck/ClsInst.hs
244

Point to the Trac ticket.

ppk added a comment.Jul 25 2018, 6:27 AM

I'm puzzled about one thing. In the test case, module Util will look up the KnownNat NatType instance, and generate code that refers to the dictionary function, say $df78 :: KnownNat NatType.

I expect that when compiling Concrete.hs we'll generate a binding for $df78. (for hs-boot files it'd be created in TcRnDriver.checkHiBootIface)
But I don't see where that happens.

Actually this was something that I too find magical because we do indeed know that the resolution is happening as witnessed
by the test case. I will try hunting it down. Nothing has changed as far as Concrete.hs is concerned, as it is just a normal module
The magic is probably happening when the Concrete is getting mixed in which means that it would be happening in some of the
backpack specific code.

Can you extend the Note to explain this, and how the binding is actually created.

Actually this was something that I too find magical because we do indeed know that the resolution is happening as witnessed

by the test case. I will try hunting it down.

Using -ddump-ds or -ddump-simpl should help. Edward may help too.

In the end, it would be good if the Note explained the magic.

ppk updated this revision to Diff 17558.Aug 2 2018, 4:50 AM
ppk edited the summary of this revision. (Show Details)

Carry over from D4988.

  • better check for implementing literals.
    • fixup: docs
    • testsuite: Added test for Trac #15379.
    • allow instance of builtin classes in hsig files.
    • support builtin classes like KnownNat in backpack fixes Trac #15379.
ppk updated this revision to Diff 17559.Aug 2 2018, 9:13 AM
  • fixup: the just bug.
  • doc: fixup
  • testsuite: Added test for Trac #15379.
  • allow instance of builtin classes in hsig files.
  • support builtin classes like KnownNat in backpack fixes Trac #15379.
ppk updated this revision to Diff 17632.Aug 11 2018, 2:56 AM
  • testsuite: Added test for Trac #15379.
  • allow instance of builtin classes in hsig files.
  • support builtin classes like KnownNat in backpack fixes Trac #15379.
ppk added a comment.Aug 11 2018, 3:35 AM

The doClsInstErrorCheck which existed when I made this patch does not seem to exist any more. That is why it is now appearing in my patch although
I have not written them. I will not have to port the changes and see whether it works out or not.

ppk updated this revision to Diff 17633.Aug 11 2018, 5:23 AM

The instance checks that were happening in doClsInstErrorCheck now
needed to be ported into the check_valid_instance_head function
available in TcValidity.

ppk added inline comments.Aug 11 2018, 5:28 AM
compiler/typecheck/TcValidity.hs
1150

@simonpj You might want to review this section of the code as it is ported from what was before. I have only incorporated the changes so that KnownNat, KnownSymbol and Typeable works with backpack. The other clauses in the check_valid_inst_head might also be cases where we need to do different things based on whether we are in a signature file or not (their error messages are all the same).

ppk updated this revision to Diff 17700.Aug 20 2018, 12:44 AM
  • remove useless newline.
ppk added a comment.Aug 21 2018, 12:48 AM

Actually this was something that I too find magical because we do indeed know that the resolution is happening as witnessed
by the test case. I will try hunting it down.

Using -ddump-ds or -ddump-simpl should help. Edward may help too.

In the end, it would be good if the Note explained the magic.

I got a response from @ezyang on irc about how the dictionaries are finally resolved. I
am quoting him

Over IRC @ezyang wrote:
piyush-kurur: Ah, it's very simple. When we actual compile a Backpack
module (because everything is instantiated), a Backpack signature
turns into basically a module that reexports things from the
implementations; including typeclass instances. So KnownNat gets
resolved the normal way post-Backpack.

simonpj accepted this revision.Sep 5 2018, 4:56 AM

Sorry to be slow. Let's do it. I suggest a slight change to Note wording, above

compiler/typecheck/TcValidity.hs
1150

I've reworded the Note a bit

Note [Instances of built-in classes in signature files]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
User defined instances for KnownNat, KnownSymbol and Typeable are
disallowed -- they are generated when needed by GHC itself on-the-fly.

However, if they occur in a Backpack signature file, they have an
entirely different meaning. Suppose in M.hsig we see
  signature M where
    data T :: Nat
    instance KnownNat T

That says that any module satisfying M.hsig must provide a KnownNat
instance for T.  We absolultely need that instance when compiling a
module that imports M.hsig: see Trac #15379 and
Note [Fabricating Evidence for Literals in Backpack] in ClsInst.

Hence, checkValidInstHead accepts a user-written instance declaration
in hsig files, where `is_sig` is True.

(NB: we mostly write Notes in block comments, without -- on every line.)

ppk edited the summary of this revision. (Show Details)Sep 5 2018, 5:10 AM
ppk updated this revision to Diff 17919.Sep 5 2018, 11:10 PM

Update the notes as suggested by spj.

ppk updated this revision to Diff 17920.Sep 5 2018, 11:19 PM
  • added @ezyang's explanation on the "magic" that resolves KnownNat.
ppk edited the summary of this revision. (Show Details)Sep 5 2018, 11:33 PM
ppk added a comment.Sep 6 2018, 8:35 AM

@bgamari I think I have addressed all the outstanding issues here.

From the past what has changed is the following

  1. Updated the comment as suggested by @simonpj
  1. Added a note on how instances resolution happens in the case of KnownNat based on the feedback from @ezyang on irc
  1. Rebased to master.

Let me know if there is something left to do. Unfortunately Harbormaster builds are failing since but as far as I see it all the changes are in
the comments.

ppk updated this revision to Diff 17930.Sep 6 2018, 8:45 AM
  • tightened the language.
ppk edited the summary of this revision. (Show Details)Sep 6 2018, 8:46 AM
ppk updated this revision to Diff 18273.Oct 9 2018, 9:10 AM

rebased to recent master.

ppk updated this revision to Diff 18282.Oct 10 2018, 4:23 AM

another rebase to bring it to todays master

This revision was not accepted when it landed; it landed in state Needs Review.Oct 11 2018, 6:25 PM
Closed by commit rGHCce7a1c4ae4c9: Support builtin classes like KnownNat in backpack (authored by Piyush P Kurur <ppk@cse.iitk.ac.in>, committed by bgamari). · Explain Why
This revision was automatically updated to reflect the committed changes.