diff options
| -rw-r--r-- | compiler/types/Unify.lhs | 41 | ||||
| -rw-r--r-- | libraries/base/Data/Typeable/Internal.hs | 38 | ||||
| -rw-r--r-- | 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 24aa7a755b..b6681867f0 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 1bee846a73..0e42bcdd87 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 53a6004b36..cc76bc9101 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. |