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

0 files changed, 0 insertions, 0 deletions