[commit: ghc] master: Support builtin classes like KnownNat in backpack (ce7a1c4)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2/ghc

>---------------------------------------------------------------

commit ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2
Author: Piyush P Kurur <ppk at cse.iitk.ac.in>
Date:   Tue Oct 9 10:14:15 2018 -0400

    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


>---------------------------------------------------------------

ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2
 compiler/main/DriverPhases.hs                      |  6 +-
 compiler/main/HscTypes.hs                          |  5 +-
 compiler/typecheck/ClsInst.hs                      | 76 +++++++++++++++++++---
 compiler/typecheck/TcRnMonad.hs                    |  5 +-
 compiler/typecheck/TcValidity.hs                   | 39 +++++++++--
 .../backpack/should_run/{T15138.bkp => T15379.bkp} | 28 ++++++--
 testsuite/tests/backpack/should_run/T15379.stdout  |  2 +
 testsuite/tests/backpack/should_run/all.T          |  1 +
 8 files changed, 140 insertions(+), 22 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2