Re: [GHC] #15379: Don't reject user-written instances of KnownNat and friends in hsig files

11 Oct 2018

      #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