[commit: ghc] master: Eliminate `Unify.validKindShape` (#9242) (b7f9b6a)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/b7f9b6a7c800da98d5ba17c45df2a589cc999975/ghc

>---------------------------------------------------------------

commit b7f9b6a7c800da98d5ba17c45df2a589cc999975
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sun Jun 29 17:37:34 2014 -0700

    Eliminate `Unify.validKindShape` (#9242)


>---------------------------------------------------------------

b7f9b6a7c800da98d5ba17c45df2a589cc999975
 compiler/types/Unify.lhs                 | 38 +-------------------------------
 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 94fdb9c..f44e260 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 e962752..93b64ef 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