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

5 files changed, 108 insertions, 12 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/T11503.hs b/testsuite/tests/pmcheck/should_compile/T11503.hs
new file mode 100644
index 0000000000..1309baf91f
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T11503.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T11503 where
+
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+import GHC.TypeNats
+  ( Nat, type (+), type (<=?) )
+import Data.Kind
+  ( Constraint, Type )
+
+-- Example 1: from #11503
+
+type NotInt :: Type -> Constraint
+type family NotInt a where
+  NotInt Int = TypeError (Text "That's Int, silly.")
+  NotInt _   = (() :: Constraint)
+
+data T a where
+  MkT1 :: a -> T a
+  MkT2 :: NotInt a => T a
+
+foo :: T Int -> Int
+foo (MkT1 x) = x
+-- Should not have any pattern match warnings for MkT2.
+
+-- Example 2: from #20180
+
+type Assert :: Bool -> Constraint -> Constraint
+type family Assert check errMsg where
+  Assert 'True  _errMsg = ()
+  Assert _check errMsg  = errMsg
+
+type List :: Nat -> Type -> Type
+data List n t where
+  Nil  :: List 0 t
+  (:-) :: t -> List n t -> List (n+1) t
+
+type (<=) :: Nat -> Nat -> Constraint
+type family x <= y where
+  x <= y = Assert (x <=? y) (TypeError (Text "Impossible!"))
+
+head' :: 1 <= n => List n t -> t
+head' (x :- _) = x
+-- Should not have any pattern match warnings for Nil.
diff --git a/testsuite/tests/pmcheck/should_compile/T14141.hs b/testsuite/tests/pmcheck/should_compile/T14141.hs
new file mode 100644
index 0000000000..e3df48545c
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14141.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14141 where
+
+import GHC.TypeLits
+  ( TypeError, ErrorMessage(..) )
+import Data.Kind
+  ( Constraint, Type )
+
+-- Example 1: from #14141
+
+data D where
+  MkD :: C => D
+
+type C :: Constraint
+type family C where
+    C = TypeError ('Text "error")
+
+f :: D -> ()
+f MkD = ()
+
+-- Example 2: from #16377
+
+type F :: Type -> Constraint
+type family F a :: Constraint
+type instance F Int  = ()
+type instance F Char = TypeError ('Text "Nope")
+
+data T where
+  A :: F Int  => T
+  B :: F Char => T
+
+exhaustive :: T -> ()
+exhaustive A = ()
+exhaustive B = ()
diff --git a/testsuite/tests/pmcheck/should_compile/T14141.stderr b/testsuite/tests/pmcheck/should_compile/T14141.stderr
new file mode 100644
index 0000000000..32eade4ce0
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/T14141.stderr
@@ -0,0 +1,8 @@
+
+T14141.hs:27:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f MkD = ...
+
+T14141.hs:42:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘exhaustive’: exhaustive B = ...
diff --git a/testsuite/tests/pmcheck/should_compile/T18478.hs b/testsuite/tests/pmcheck/should_compile/T18478.hs
index 6c0fbd9828..5ec331d092 100644
--- a/testsuite/tests/pmcheck/should_compile/T18478.hs
+++ b/testsuite/tests/pmcheck/should_compile/T18478.hs
@@ -505,11 +505,8 @@ type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where
     TypeError ('Text "Nested BigMaps are not allowed")
   FailOnNestedBigMapsFound 'False = ()
 
--- | This is like 'HasNoOp', it raises a more human-readable error
--- when @t@ type is concrete, but GHC cannot make any conclusions
--- from such constraint as it can for 'HasNoOp'.
--- Though, hopefully, it will someday:
--- <https://gitlab.haskell.org/ghc/ghc/issues/11503 #11503>.
+-- | This is like 'HasNoOp', but raises a more human-readable error
+-- when the @t@ type is concrete.
 --
 -- Use this constraint in our eDSL.
 type ForbidOp t = FailOnOperationFound (ContainsOp t)
@@ -523,12 +520,8 @@ type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
 -- | Evidence of that 'HasNoOp' is deducable from 'ForbidOp'.
 forbiddenOpEvi :: forall t. (SingI t, ForbidOp t) :- HasNoOp t
 forbiddenOpEvi = Sub $
-  -- It's not clear now to proof GHC that @HasNoOp t@ is implication of
-  -- @ForbidOp t@, so we use @error@ below and also disable
-  -- "-Wredundant-constraints" extension.
   case checkOpPresence (sing @t) of
     OpAbsent -> Dict
-    OpPresent -> error "impossible"
 
 -- | Reify 'HasNoOp' constraint from 'ForbidOp'.
 --
@@ -544,13 +537,11 @@ forbiddenBigMapEvi :: forall t. (SingI t, ForbidBigMap t) :- HasNoBigMap t
 forbiddenBigMapEvi = Sub $
   case checkBigMapPresence (sing @t) of
     BigMapAbsent -> Dict
-    BigMapPresent -> error "impossible"
 
 forbiddenNestedBigMapsEvi :: forall t. (SingI t, ForbidNestedBigMaps t) :- HasNoNestedBigMaps t
 forbiddenNestedBigMapsEvi = Sub $
   case checkNestedBigMapsPresence (sing @t) of
     NestedBigMapsAbsent -> Dict
-    NestedBigMapsPresent -> error "impossible"
 
 forbiddenBigMap
   :: forall t a.
@@ -572,7 +563,6 @@ forbiddenContractTypeEvi
 forbiddenContractTypeEvi = Sub $
   case checkContractTypePresence (sing @t) of
     ContractAbsent -> Dict
-    ContractPresent -> error "impossible"
 
 -- | Reify 'HasNoContract' constraint from 'ForbidContract'.
 forbiddenContractType
diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 3880ca0756..c732ef5691 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -50,12 +50,16 @@ test('T11822', collect_compiler_stats('bytes allocated',10), compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11195', collect_compiler_stats('bytes allocated',10), compile,
      ['-package ghc -fwarn-incomplete-patterns -fwarn-overlapping-patterns +RTS -M2G -RTS'])
+test('T11503', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T11984', normal, compile,
     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14086', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14098', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
+test('T14141', [], compile,
+     ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14813', normal, compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 test('T14899', normal, compile,