[commit: ghc] master: Implement `Typeable` support for type-level literals (#8778). (0354fb3)
git at git.haskell.org
git at git.haskell.org
Sat Jun 14 21:51:45 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/0354fb3676e5b0044601c8e0a5f8039f0cac0c8d/ghc
>---------------------------------------------------------------
commit 0354fb3676e5b0044601c8e0a5f8039f0cac0c8d
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date: Sat Jun 14 14:08:23 2014 -0700
Implement `Typeable` support for type-level literals (#8778).
>---------------------------------------------------------------
0354fb3676e5b0044601c8e0a5f8039f0cac0c8d
compiler/types/Unify.lhs | 41 +++++++++++++++++++++++++++++++-
libraries/base/Data/Typeable/Internal.hs | 38 +++++++++++++++++++++++++++++
libraries/base/GHC/TypeLits.hs | 19 +++++++++++----
3 files changed, 93 insertions(+), 5 deletions(-)
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs
index 24aa7a7..b668186 100644
--- a/compiler/types/Unify.lhs
+++ b/compiler/types/Unify.lhs
@@ -39,8 +39,10 @@ import Type
import TyCon
import TypeRep
import Util
+import PrelNames(typeNatKindConNameKey, typeSymbolKindConNameKey)
+import Unique(hasKey)
-import Control.Monad (liftM, ap)
+import Control.Monad (liftM, ap, unless, guard)
import Control.Applicative (Applicative(..))
\end{code}
@@ -173,6 +175,8 @@ match menv subst (TyVarTy tv1) ty2
then Nothing -- Occurs check
else do { subst1 <- match_kind menv subst (tyVarKind tv1) (typeKind ty2)
-- Note [Matching kinds]
+ ; guard (validKindShape (tyVarKind tv1) ty2)
+ -- Note [Kinds Containing Only Literals]
; return (extendVarEnv subst1 tv1' ty2) }
| otherwise -- tv1 is not a template tyvar
@@ -205,6 +209,37 @@ match _ subst (LitTy x) (LitTy y) | x == y = return subst
match _ _ _ _
= Nothing
+
+{- Note [Kinds Containing Only Literals]
+
+The kinds `Nat` and `Symbol` contain only literal types (e.g., 17, "Hi", etc.).
+As such, they can only ever match and unify with a type variable or a literal
+type. We check for this during matching and unification, and reject
+binding variables to types that have an unacceptable shape.
+
+This helps us avoid "overlapping instance" errors in the presence of
+very general instances. The main motivating example for this is the
+implementation of `Typeable`, which conatins the instances:
+
+... => Typeable (f a) where ...
+... => Typeable (a :: Nat) where ...
+
+Without the explicit check these look like they overlap, and are rejected.
+The two do not overlap, however, because nothing of kind `Nat` can be
+of the form `f a`.
+-}
+
+validKindShape :: Kind -> Type -> Bool
+validKindShape k ty
+ | Just (tc,[]) <- splitTyConApp_maybe k
+ , tc `hasKey` typeNatKindConNameKey ||
+ tc `hasKey` typeSymbolKindConNameKey = case ty of
+ TyVarTy _ -> True
+ LitTy _ -> True
+ _ -> False
+validKindShape _ _ = True
+
+
--------------
match_kind :: MatchEnv -> TvSubstEnv -> Kind -> Kind -> Maybe TvSubstEnv
-- Match the kind of the template tyvar with the kind of Type
@@ -653,6 +688,10 @@ uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable
-- See Note [Fine-grained unification]
| otherwise
= do { subst' <- unify subst k1 k2
+ -- Note [Kinds Containing Only Literals]
+ ; let ki = substTy (mkOpenTvSubst subst') k1
+ ; unless (validKindShape ki ty2')
+ surelyApart
; bindTv subst' tv1 ty2 } -- Bind tyvar to the synonym if poss
where
k1 = tyVarKind tv1
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 1bee846..0e42bcd 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -22,6 +22,8 @@
, PolyKinds
, ConstraintKinds
, DeriveDataTypeable
+ , DataKinds
+ , UndecidableInstances
, StandaloneDeriving #-}
module Data.Typeable.Internal (
@@ -63,6 +65,7 @@ import GHC.STRef ( STRef )
import GHC.Ptr ( Ptr, FunPtr )
-- import GHC.Stable
import GHC.Arr ( Array, STArray, Ix )
+import GHC.TypeLits ( Nat, Symbol, KnownNat, KnownSymbol, natVal', symbolVal' )
import Data.Type.Coercion
import Data.Type.Equality
import Text.ParserCombinators.ReadP ( ReadP )
@@ -411,3 +414,38 @@ deriving instance Typeable Monad
deriving instance Typeable MonadPlus
deriving instance Typeable Typeable
+
+
+
+--------------------------------------------------------------------------------
+-- Instances for type literals
+
+instance KnownNat n => Typeable (n :: Nat) where
+ typeRep# p = mkTyConApp tc []
+ where
+ tc = TyCon
+ { tyConHash = fingerprintString (mk pack modu nm)
+ , tyConPackage = pack
+ , tyConModule = modu
+ , tyConName = nm
+ }
+ pack = "base"
+ modu = "GHC.TypeLits"
+ nm = show (natVal' p)
+ mk a b c = a ++ " " ++ b ++ " " ++ c
+
+
+instance KnownSymbol s => Typeable (s :: Symbol) where
+ typeRep# p = mkTyConApp tc []
+ where
+ tc = TyCon
+ { tyConHash = fingerprintString (mk pack modu nm)
+ , tyConPackage = pack
+ , tyConModule = modu
+ , tyConName = nm
+ }
+ pack = "base"
+ modu = "GHC.TypeLits"
+ nm = show (symbolVal' p)
+ mk a b c = a ++ " " ++ b ++ " " ++ c
+
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index 53a6004..cc76bc9 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -10,6 +10,7 @@
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-} -- for compiling instances of (==)
{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE MagicHash #-}
{-| This module is an internal GHC module. It declares the constants used
in the implementation of type-level natural numbers. The programmer interface
@@ -23,8 +24,8 @@ module GHC.TypeLits
Nat, Symbol
-- * Linking type and value level
- , KnownNat, natVal
- , KnownSymbol, symbolVal
+ , KnownNat, natVal, natVal'
+ , KnownSymbol, symbolVal, symbolVal'
, SomeNat(..), SomeSymbol(..)
, someNatVal, someSymbolVal
, sameNat, sameSymbol
@@ -41,9 +42,9 @@ import GHC.Num(Integer)
import GHC.Base(String)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
-import GHC.Prim(magicDict)
+import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
-import Data.Proxy(Proxy(..))
+import Data.Proxy (Proxy(..))
import Data.Type.Equality(type (==), (:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)
@@ -80,6 +81,16 @@ symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal _ = case symbolSing :: SSymbol n of
SSymbol x -> x
+-- | /Since: 4.7.0.0/
+natVal' :: forall n. KnownNat n => Proxy# n -> Integer
+natVal' _ = case natSing :: SNat n of
+ SNat x -> x
+
+-- | /Since: 4.7.0.0/
+symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
+symbolVal' _ = case symbolSing :: SSymbol n of
+ SSymbol x -> x
+
-- | This type represents unknown type-level natural numbers.
More information about the ghc-commits
mailing list