#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ppk): I have started working on this bug at <https://github.com/piyush- kurur/ghc/tree/literal-instac>. Not yet on phab because I am waiting for the fix of #15138 to get merged. Will rebase and send the patches then. But here is a status report of what I have done 1. Added a testcase 2. Made the minimal modification that we discussed over IRC Unfortunately just 2 does not help as there is a overlapping instance error that is being thrown. I will investigate this and let you known. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ppk): Resolving the overlapping instance problem is more tricky than I thought. I am adding additional notes here so that some one can better guide the process. This is my current understanding on the issues The `KnownNat` and `KnownSymbol` instance witness and dictionary generating is done by ghc itself in the file `compiler/typecheck/ClsInst.hs`. However this is problematic in the backpack setting because of the following Let us consider the following signature fragment {{{#!haskell signature Abstract where data Foo :: Nat instance KnownNat Foo }}} Suppose this abstract signature is included in a module `Util` {{{#!haskell module Util where import Abstract printFoo :: IO () printFoo = do print $ natVal (Proxy :: Proxy Foo) }}} Notice that the `natVal` function will need a dictionary of `KnownNat Foo` at this point and will need to get it from a concrete implementation of the kind {{{#!haskell module Concrete where type Foo = 42 }}} It is not clear to me how this can be generated "inside the compiler" like what happens in `ClsInst.hs`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ppk): I think I have fixed it. It turned out that the patch is simpler than I though. Essentially I just made the matchGlobalInstance function to first actually search for an instance and failing which try out the KnownNat and KnownSymbol cases. The commit is https://github.com/piyush- kurur/ghc/commit/364de810f315faba50a4fbe4a68fba3876eb0555 I have also written up an explanation. See if it makes sense. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ppk): Replying to [comment:7 simonpj]:

The current implementation only ever has instances for `KnownNat 1`, `KnownNat 2` etc. This is described in `Note [KnownNat & KnownSymbol and EvLit]` in `TcInteract`.

Yes that note was quite useful in fact.

But now you want to allow `instance KnownNat T` for some abstract type `T`; you explain this well in comment:4.

Very well; but I really dislike messing with `matchInstEnv`. Better: make `mathKnownNat` have an `otherwise` case that, instead of returning `NoInstance` uses `matchInstEnv`. With a careful `Note` to explain.

[snip]

But `Typeable` can fail; I wonder if you might end up wanting a `Typeable` instance in a `hsig` file. I think that's all... but the big

Okey I will think about it and try it out. The only thing puzzling for me is that the old code is returning Overlapping instances, which to me appears to be finding too many instances rather than finding too few. So there is some problem with my comment:4 which I cannot really pin-point. point is that GHC's treatment of built-in classes may need attention because of Backpack; KnownNat is just an example. Again the `Typeable` instances in backpack works fine //even with the old version// of the code (unlike `KnownNat` or `KnownSymbol`). In fact, I realised and has tweaked the test case to have all the three problematic classes (KnownNat, KnownSymbol and Typeable) but only the first two was giving the overlapping instance error. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ppk): * differential: => Phab:D4988 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ezyang): Piyush, I don't think the behavior of your example is consistent with the hypothesis. Consider the following program: {{{ {-# LANGUAGE DataKinds, KindSignatures #-} unit p where signature Abstract where import GHC.TypeLits data Foo :: Nat instance KnownNat Foo module Util where import Data.Proxy import Abstract import GHC.TypeLits foo = natVal (Proxy :: Proxy Foo) }}} I get: {{{ ezyang@autobox:~/Dev/ghc-known-nat$ inplace/bin/ghc-stage2 --backpack test.bkp -fforce-recomp [1 of 1] Processing p [1 of 2] Compiling Abstract[sig] ( p/Abstract.hsig, nothing ) [2 of 2] Compiling Util ( p/Util.hs, nothing ) test.bkp:12:11: error: • Overlapping instances for KnownNat Foo arising from a use of ‘natVal’ Matching instances: instance [safe] KnownNat Foo -- Defined at test.bkp:6:14 There exists a (perhaps superclass) match: (The choice depends on the instantiation of ‘’ To pick the first instance above, use IncoherentInstances when compiling the other instance declarations) • In the expression: natVal (Proxy :: Proxy Foo) In an equation for ‘foo’: foo = natVal (Proxy :: Proxy Foo) | 12 | foo = natVal (Proxy :: Proxy Foo) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} The overlap occurs before Concrete is considered at all. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ppk): Some of the test cases in `backpack/should_fail/` are failing. Of which I think the bkpfail46.bkp is actually //not giving// a compilation failure (and hence the test is failing). Can you have a look at this test case ? Was this a previous limitation of backpack that was now fixed or is it the case that some thing that should not have been acceptable is now being accepted (thereby seriously questioning the type safety). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ppk): * Attachment "test.bkp" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ppk): * Attachment "out-desugar" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ppk): As mentioned by @simonpj, it would be desirable to actually pinpoint how the dictionaries of `KnownNat` and friends get resolved in the context of backpack. This comment is more to document what I have learned by simply dumping the desugared version. I have attached a test backpack program (attachment:test.bkp) with the output after compiling with `-ddump-ds` and `-ddump-simpl`. The desugared version is avaliable in attachment:out-desugar One can clearly see that an the KnownNat instance is substituted for and the appropriate versions of Util is created [https://ghc.haskell.org/trac/ghc/attachment/ticket/15379/out-desugar#L58 Line 56] and [https://ghc.haskell.org/trac/ghc/attachment/ticket/15379/out- desugar#L92 Line 92]. Although there is no trace of the Util module without the substitution, if we had no mixing-in there will also be a variant of Util with the abstract dictionary for `KnownNat NatType`. So my understanding would be that backpack is going ahead and "inlining" the dictionary when mixing a module that uses a abstract signature with a concrete implementation of that signature. I hope that makes sense. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2/ghc" ce7a1c4/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2" Support builtin classes like KnownNat in backpack This commit allows backpack signatures to enforce constraints like KnownNat on data types. Thus it fixes #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 2. 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 2. 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. Reviewers: bgamari, ezyang, goldfire, simonpj Reviewed By: simonpj Subscribers: simonpj, ezyang, rwbarton, thomie, carter GHC Trac Issues: #15379 Differential Revision: https://phabricator.haskell.org/D4988 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#15379: Don't reject user-written instances of KnownNat and friends in hsig files -------------------------------------+------------------------------------- Reporter: ezyang | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D4988 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * milestone: 8.10.1 => 8.8.1 Comment: This is in the 8.8 branch -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15379#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler