Detect TypeError when checking for insolubility

We detect insoluble Givens by making getInertInsols
take into account TypeError constraints, on top of insoluble equalities
such as Int ~ Bool (which it already took into account).

This allows pattern matches with insoluble contexts to be reported
as redundant (tyOracle calls tcCheckGivens which calls getInertInsols).

As a bonus, we get to remove a workaround in Data.Typeable.Internal:
we can directly use a NotApplication type family, as opposed to
needing to cook up an insoluble equality constraint.

Fixes #11503 #14141 #16377 #20180

1 files changed, 3 insertions, 20 deletions

diff --git a/compiler/GHC/Utils/Binary/Typeable.hs b/compiler/GHC/Utils/Binary/Typeable.hs
index b0f4833cbf..7bef358e73 100644
--- a/compiler/GHC/Utils/Binary/Typeable.hs
+++ b/compiler/GHC/Utils/Binary/Typeable.hs
@@ -1,10 +1,9 @@
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GADTs #-}
 
 {-# OPTIONS_GHC -O2 -funbox-strict-fields #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-orphans -Wincomplete-patterns #-}
 #if MIN_VERSION_base(4,16,0)
 #define HAS_TYPELITCHAR
 #endif
@@ -19,7 +18,7 @@ import GHC.Prelude
 
 import GHC.Utils.Binary
 
-import GHC.Exts (TYPE, RuntimeRep(..), VecCount(..), VecElem(..))
+import GHC.Exts (RuntimeRep(..), VecCount(..), VecElem(..))
 #if __GLASGOW_HASKELL__ >= 901
 import GHC.Exts (Levity(Lifted, Unlifted))
 #endif
@@ -49,7 +48,6 @@ getSomeTypeRep bh = do
         1 -> do con <- get bh :: IO TyCon
                 ks <- get bh :: IO [SomeTypeRep]
                 return $ SomeTypeRep $ mkTrCon con ks
-
         2 -> do SomeTypeRep f <- getSomeTypeRep bh
                 SomeTypeRep x <- getSomeTypeRep bh
                 case typeRepKind f of
@@ -68,20 +66,8 @@ getSomeTypeRep bh = do
                        [ "    Applied type: " ++ show f
                        , "    To argument:  " ++ show x
                        ]
-        3 -> do SomeTypeRep arg <- getSomeTypeRep bh
-                SomeTypeRep res <- getSomeTypeRep bh
-                if
-                  | App argkcon _ <- typeRepKind arg
-                  , App reskcon _ <- typeRepKind res
-                  , Just HRefl <- argkcon `eqTypeRep` tYPErep
-                  , Just HRefl <- reskcon `eqTypeRep` tYPErep
-                  -> return $ SomeTypeRep $ Fun arg res
-                  | otherwise -> failure "Kind mismatch" []
         _ -> failure "Invalid SomeTypeRep" []
   where
-    tYPErep :: TypeRep TYPE
-    tYPErep = typeRep
-
     failure description info =
         fail $ unlines $ [ "Binary.getSomeTypeRep: "++description ]
                       ++ map ("    "++) info
@@ -201,10 +187,7 @@ instance Binary TypeLitSort where
           _ -> fail "Binary.putTypeLitSort: invalid tag"
 
 putTypeRep :: BinHandle -> TypeRep a -> IO ()
--- Special handling for TYPE, (->), and RuntimeRep due to recursive kind
--- relations.
--- See Note [Mutually recursive representations of primitive types]
-putTypeRep bh rep
+putTypeRep bh rep -- Handle Type specially since it's so common
   | Just HRefl <- rep `eqTypeRep` (typeRep :: TypeRep Type)
   = put_ bh (0 :: Word8)
 putTypeRep bh (Con' con ks) = do