diff options
| -rw-r--r-- | compiler/types/Unify.lhs | 38 | ||||
| -rw-r--r-- | libraries/base/Data/Typeable/Internal.hs | 6 |
2 files changed, 2 insertions, 42 deletions
diff --git a/compiler/types/Unify.lhs b/compiler/types/Unify.lhs index 94fdb9c3f2..f44e260c57 100644 --- a/compiler/types/Unify.lhs +++ b/compiler/types/Unify.lhs @@ -39,10 +39,8 @@ import Type import TyCon import TypeRep import Util -import PrelNames(typeNatKindConNameKey, typeSymbolKindConNameKey) -import Unique(hasKey) -import Control.Monad (liftM, ap, unless, guard) +import Control.Monad (liftM, ap) import Control.Applicative (Applicative(..)) \end{code} @@ -175,8 +173,6 @@ 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 @@ -210,35 +206,6 @@ 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 contains 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 @@ -689,9 +656,6 @@ uUnrefined subst tv1 ty2 ty2' -- ty2 is not a type variable | 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 e962752ad7..93b64ef9e9 100644 --- a/libraries/base/Data/Typeable/Internal.hs +++ b/libraries/base/Data/Typeable/Internal.hs @@ -263,7 +263,7 @@ type Typeable7 (a :: * -> * -> * -> * -> * -> * -> * -> *) = Typeable a {-# DEPRECATED Typeable7 "renamed to 'Typeable'" #-} -- deprecated in 7.8 -- | Kind-polymorphic Typeable instance for type application -instance (Typeable s, Typeable a) => Typeable (s a) where +instance {-# INCOHERENT #-} (Typeable s, Typeable a) => Typeable (s a) where typeRep# = \_ -> rep -- Note [Memoising typeOf] where !ty1 = typeRep# (proxy# :: Proxy# s) !ty2 = typeRep# (proxy# :: Proxy# a) @@ -446,8 +446,6 @@ lifted types with infinitely many inhabitants. Indeed, `Nat` is isomorphic to (lifted) `[()]` and `Symbol` is isomorphic to `[Char]`. -} --- See `Note [Kinds Containing Only Literals]` in `types/Unify.hs` for --- an explanation of how we avoid overlap with `Typeable (f a)`. instance KnownNat n => Typeable (n :: Nat) where -- See #9203 for an explanation of why this is written as `\_ -> rep`. typeRep# = \_ -> rep @@ -465,8 +463,6 @@ instance KnownNat n => Typeable (n :: Nat) where mk a b c = a ++ " " ++ b ++ " " ++ c --- See `Note [Kinds Containing Only Literals]` in `types/Unify.hs` for --- an explanation of how we avoid overlap with `Typeable (f a)`. instance KnownSymbol s => Typeable (s :: Symbol) where -- See #9203 for an explanation of why this is written as `\_ -> rep`. typeRep# = \_ -> rep |