Support builtin classes like KnownNat in backpack
authorPiyush P Kurur <ppk@cse.iitk.ac.in>
Tue, 9 Oct 2018 14:14:15 +0000 (10:14 -0400)
committerBen Gamari <ben@smart-cactus.org>
Thu, 11 Oct 2018 19:27:25 +0000 (15:27 -0400)
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

compiler/main/DriverPhases.hs
compiler/main/HscTypes.hs
compiler/typecheck/ClsInst.hs
compiler/typecheck/TcRnMonad.hs
compiler/typecheck/TcValidity.hs
testsuite/tests/backpack/should_run/T15379.bkp [new file with mode: 0644]
testsuite/tests/backpack/should_run/T15379.stdout [new file with mode: 0644]
testsuite/tests/backpack/should_run/all.T

index 57455a5..d923262 100644 (file)
@@ -10,7 +10,7 @@
 -----------------------------------------------------------------------------
 
 module DriverPhases (
-   HscSource(..), isHsBootOrSig, hscSourceString,
+   HscSource(..), isHsBootOrSig, isHsigFile, hscSourceString,
    Phase(..),
    happensBefore, eqPhase, anyHsc, isStopLn,
    startPhase,
@@ -124,6 +124,10 @@ isHsBootOrSig HsBootFile = True
 isHsBootOrSig HsigFile   = True
 isHsBootOrSig _          = False
 
+isHsigFile :: HscSource -> Bool
+isHsigFile HsigFile = True
+isHsigFile _        = False
+
 data Phase
         = Unlit HscSource
         | Cpp   HscSource
index 77067c2..0caafb0 100644 (file)
@@ -36,7 +36,7 @@ module HscTypes (
 
         -- * Information about the module being compiled
         -- (re-exported from DriverPhases)
-        HscSource(..), isHsBootOrSig, hscSourceString,
+        HscSource(..), isHsBootOrSig, isHsigFile, hscSourceString,
 
 
         -- * State relating to modules in this package
@@ -179,7 +179,8 @@ import TysWiredIn
 import Packages hiding  ( Version(..) )
 import CmdLineParser
 import DynFlags
-import DriverPhases     ( Phase, HscSource(..), isHsBootOrSig, hscSourceString )
+import DriverPhases     ( Phase, HscSource(..), hscSourceString
+                        , isHsBootOrSig, isHsigFile )
 import BasicTypes
 import IfaceSyn
 import Maybes
index 0af1965..b8ff6dd 100644 (file)
@@ -90,8 +90,10 @@ matchGlobalInst :: DynFlags
                              -- See Note [Shortcut solving: overlap]
                 -> Class -> [Type] -> TcM ClsInstResult
 matchGlobalInst dflags short_cut clas tys
-  | cls_name == knownNatClassName     = matchKnownNat        clas tys
-  | cls_name == knownSymbolClassName  = matchKnownSymbol     clas tys
+  | cls_name == knownNatClassName
+  = matchKnownNat    dflags short_cut clas tys
+  | cls_name == knownSymbolClassName
+  = matchKnownSymbol dflags short_cut clas tys
   | isCTupleClass clas                = matchCTuple          clas tys
   | cls_name == typeableClassName     = matchTypeable        clas tys
   | clas `hasKey` heqTyConKey         = matchHeteroEquality       tys
@@ -237,21 +239,77 @@ The story for kind `Symbol` is analogous:
   * class KnownSymbol
   * newtype SSymbol
   * Evidence: a Core literal (e.g. mkNaturalExpr)
+
+
+Note [Fabricating Evidence for Literals in Backpack]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Let `T` be a type of kind `Nat`. When solving for a purported instance
+of `KnownNat T`, ghc tries to resolve the type `T` to an integer `n`,
+in which case the evidence `EvLit (EvNum n)` is generated on the
+fly. It might appear that this is sufficient as users cannot define
+their own instances of `KnownNat`. However, for backpack module this
+would not work (see issue #15379). Consider 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. So the strategy that
+we follow is the following
+
+1. If T is indeed available as a type alias for an integer constant,
+   generate the dictionary on the fly, failing which
+
+2. Look up the type class environment for the evidence.
+
+Finally actual code gets generate for Util only when a module like
+Concrete gets "mixed-in" in place of the signature Abstract. As a
+result all things, including the typeclass instances, in Concrete gets
+reexported. So `KnownNat` gets resolved the normal way post-Backpack.
+
+A similar generation works for `KnownSymbol` as well
+
 -}
 
-matchKnownNat :: Class -> [Type] -> TcM ClsInstResult
-matchKnownNat clas [ty]     -- clas = KnownNat
+matchKnownNat :: DynFlags
+              -> Bool      -- True <=> caller is the short-cut solver
+                           -- See Note [Shortcut solving: overlap]
+              -> Class -> [Type] -> TcM ClsInstResult
+matchKnownNat _ _ clas [ty]     -- clas = KnownNat
   | Just n <- isNumLitTy ty = do
         et <- mkNaturalExpr n
         makeLitDict clas ty et
-matchKnownNat _ _           = return NoInstance
-
-matchKnownSymbol :: Class -> [Type] -> TcM ClsInstResult
-matchKnownSymbol clas [ty]  -- clas = KnownSymbol
+matchKnownNat df sc clas tys = matchInstEnv df sc clas tys
+ -- See Note [Fabricating Evidence for Literals in Backpack] for why
+ -- this lookup into the instance environment is required.
+
+matchKnownSymbol :: DynFlags
+                 -> Bool      -- True <=> caller is the short-cut solver
+                              -- See Note [Shortcut solving: overlap]
+                 -> Class -> [Type] -> TcM ClsInstResult
+matchKnownSymbol _ _ clas [ty]  -- clas = KnownSymbol
   | Just s <- isStrLitTy ty = do
         et <- mkStringExprFS s
         makeLitDict clas ty et
-matchKnownSymbol _ _       = return NoInstance
+matchKnownSymbol df sc clas tys = matchInstEnv df sc clas tys
+ -- See Note [Fabricating Evidence for Literals in Backpack] for why
+ -- this lookup into the instance environment is required.
 
 makeLitDict :: Class -> Type -> EvExpr -> TcM ClsInstResult
 -- makeLitDict adds a coercion that will convert the literal into a dictionary
index b93652f..bef1044 100644 (file)
@@ -48,7 +48,7 @@ module TcRnMonad(
 
   -- * Typechecker global environment
   getIsGHCi, getGHCiMonad, getInteractivePrintName,
-  tcIsHsBootOrSig, tcSelfBootInfo, getGlobalRdrEnv,
+  tcIsHsBootOrSig, tcIsHsig, tcSelfBootInfo, getGlobalRdrEnv,
   getRdrEnvs, getImports,
   getFixityEnv, extendFixityEnv, getRecFieldEnv,
   getDeclaredDefaultTys,
@@ -782,6 +782,9 @@ getInteractivePrintName = do { hsc <- getTopEnv; return (ic_int_print $ hsc_IC h
 tcIsHsBootOrSig :: TcRn Bool
 tcIsHsBootOrSig = do { env <- getGblEnv; return (isHsBootOrSig (tcg_src env)) }
 
+tcIsHsig :: TcRn Bool
+tcIsHsig = do { env <- getGblEnv; return (isHsigFile (tcg_src env)) }
+
 tcSelfBootInfo :: TcRn SelfBootInfo
 tcSelfBootInfo = do { env <- getGblEnv; return (tcg_self_boot env) }
 
index 12f1ac7..392c254 100644 (file)
@@ -1115,12 +1115,39 @@ checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
 checkValidInstHead ctxt clas cls_args
   = do { dflags   <- getDynFlags
        ; is_boot  <- tcIsHsBootOrSig
-       ; check_valid_inst_head dflags is_boot ctxt clas cls_args }
+       ; is_sig   <- tcIsHsig
+       ; check_valid_inst_head dflags is_boot is_sig ctxt clas cls_args
+       }
 
-check_valid_inst_head :: DynFlags -> Bool
+{-
+
+Note [Instances of built-in classes in signature files]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+User defined instances for KnownNat, KnownSymbol and Typeable are
+disallowed -- they are generated when needed by GHC itself on-the-fly.
+
+However, if they occur in a Backpack signature file, they have an
+entirely different meaning. Suppose in M.hsig we see
+
+  signature M where
+    data T :: Nat
+    instance KnownNat T
+
+That says that any module satisfying M.hsig must provide a KnownNat
+instance for T.  We absolultely need that instance when compiling a
+module that imports M.hsig: see Trac #15379 and
+Note [Fabricating Evidence for Literals in Backpack] in ClsInst.
+
+Hence, checkValidInstHead accepts a user-written instance declaration
+in hsig files, where `is_sig` is True.
+
+-}
+
+check_valid_inst_head :: DynFlags -> Bool -> Bool
                       -> UserTypeCtxt -> Class -> [Type] -> TcM ()
 -- Wow!  There are a surprising number of ad-hoc special cases here.
-check_valid_inst_head dflags is_boot ctxt clas cls_args
+check_valid_inst_head dflags is_boot is_sig ctxt clas cls_args
 
   -- If not in an hs-boot file, abstract classes cannot have instances
   | isAbstractClass clas
@@ -1129,14 +1156,18 @@ check_valid_inst_head dflags is_boot ctxt clas cls_args
 
   -- For Typeable, don't complain about instances for
   -- standalone deriving; they are no-ops, and we warn about
-  -- it in TcDeriv.deriveStandalone
+  -- it in TcDeriv.deriveStandalone.
   | clas_nm == typeableClassName
+  , not is_sig
+    -- Note [Instances of built-in classes in signature files]
   , hand_written_bindings
   = failWithTc rejected_class_msg
 
   -- Handwritten instances of KnownNat/KnownSymbol class
   -- are always forbidden (#12837)
   | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ]
+  , not is_sig
+    -- Note [Instances of built-in classes in signature files]
   , hand_written_bindings
   = failWithTc rejected_class_msg
 
diff --git a/testsuite/tests/backpack/should_run/T15379.bkp b/testsuite/tests/backpack/should_run/T15379.bkp
new file mode 100644 (file)
index 0000000..e0a9556
--- /dev/null
@@ -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 (file)
index 0000000..d9894ca
--- /dev/null
@@ -0,0 +1,2 @@
+The answer to life, universe and everything is: 42
+Int is its type
index 61277b8..c0cde0f 100644 (file)
@@ -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,[''])