diff options
author | Piyush P Kurur <ppk@cse.iitk.ac.in> | 2018-10-09 10:14:15 -0400 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2018-10-11 15:27:25 -0400 |
commit | ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2 (patch) | |
tree | 18a2c6aa01069af8522e8c9adfef3ef53eb444fb /testsuite/tests/backpack | |
parent | 2f693b3e496bd90df037e7928b13d24449cee6e5 (diff) | |
download | haskell-ce7a1c4ae4c93f2d0d3d7a0b573ddd876fc855c2.tar.gz |
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
Diffstat (limited to 'testsuite/tests/backpack')
-rw-r--r-- | testsuite/tests/backpack/should_run/T15379.bkp | 54 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_run/T15379.stdout | 2 | ||||
-rw-r--r-- | testsuite/tests/backpack/should_run/all.T | 1 |
3 files changed, 57 insertions, 0 deletions
diff --git a/testsuite/tests/backpack/should_run/T15379.bkp b/testsuite/tests/backpack/should_run/T15379.bkp new file mode 100644 index 0000000000..e0a9556669 --- /dev/null +++ b/testsuite/tests/backpack/should_run/T15379.bkp @@ -0,0 +1,54 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} + +unit indef where + + signature Abstract where + import GHC.TypeLits + import Data.Typeable + data NatType :: Nat + instance KnownNat NatType + + data SymbolType :: Symbol + instance KnownSymbol SymbolType + + data TypeableType + instance Typeable TypeableType + + module Util where + import Abstract + import Data.Proxy + import Data.Typeable + import GHC.TypeLits + + name :: String + name = showsTypeRep (typeRep (Proxy :: Proxy TypeableType)) "" + + printSomething :: IO () + printSomething = do putStr $ symbolVal (Proxy :: Proxy SymbolType) + print $ natVal (Proxy :: Proxy NatType) + putStrLn $ name ++ " is its type" + +unit concrete where + + module Concrete where + + type TypeableType = Int + type NatType = 42 + type SymbolType = "The answer to life, universe and everything is: " + + +unit main where + dependency indef[Abstract=concrete:Concrete] (Util as MyUtil) + + module Main where + import Data.Proxy + import MyUtil + + main :: IO () + main = printSomething diff --git a/testsuite/tests/backpack/should_run/T15379.stdout b/testsuite/tests/backpack/should_run/T15379.stdout new file mode 100644 index 0000000000..d9894cac4a --- /dev/null +++ b/testsuite/tests/backpack/should_run/T15379.stdout @@ -0,0 +1,2 @@ +The answer to life, universe and everything is: 42 +Int is its type diff --git a/testsuite/tests/backpack/should_run/all.T b/testsuite/tests/backpack/should_run/all.T index 61277b8f31..c0cde0fdc1 100644 --- a/testsuite/tests/backpack/should_run/all.T +++ b/testsuite/tests/backpack/should_run/all.T @@ -9,3 +9,4 @@ test('bkprun08', normal, backpack_run, ['']) test('bkprun09', normal, backpack_run, ['-O']) test('T13955', normal, backpack_run, ['']) test('T15138', normal, backpack_run, ['']) +test('T15379', normal, backpack_run,['']) |