Add the Unsatisfiable class

This commit implements GHC proposal #433, adding the Unsatisfiable
class to the GHC.TypeError module. This provides an alternative to
TypeError for which error reporting is more predictable: we report it
when we are reporting unsolved Wanted constraints.

Fixes #14983 #16249 #16906 #18310 #20835

27 files changed, 470 insertions, 0 deletions

diff --git a/testsuite/tests/unsatisfiable/T11503_Unsat.hs b/testsuite/tests/unsatisfiable/T11503_Unsat.hs
new file mode 100644
index 0000000000..a685daf066
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T11503_Unsat.hs
@@ -0,0 +1,52 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T11503_Unsat where
+
+import GHC.TypeError
+  ( Unsatisfiable, 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 = Unsatisfiable (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) (Unsatisfiable (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/unsatisfiable/T14141_Unsat.hs b/testsuite/tests/unsatisfiable/T14141_Unsat.hs
new file mode 100644
index 0000000000..8be3b41960
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14141_Unsat.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE Haskell2010 #-}
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14141_Unsat where
+
+import GHC.TypeError
+import Data.Kind
+  ( Constraint, Type )
+
+-- Example 1: from #14141
+
+data D where
+  MkD :: C => D
+
+type C :: Constraint
+type family C where
+    C = Unsatisfiable ('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 = Unsatisfiable  ('Text "Nope")
+
+data T where
+  A :: F Int  => T
+  B :: F Char => T
+
+exhaustive :: T -> ()
+exhaustive A = ()
+exhaustive B = ()
diff --git a/testsuite/tests/unsatisfiable/T14141_Unsat.stderr b/testsuite/tests/unsatisfiable/T14141_Unsat.stderr
new file mode 100644
index 0000000000..d71928917f
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14141_Unsat.stderr
@@ -0,0 +1,8 @@
+
+T14141_Unsat.hs:26:1: warning: [GHC-94210] [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match has inaccessible right hand side
+    In an equation for ‘f’: f MkD = ...
+
+T14141_Unsat.hs:41:1: warning: [GHC-53633] [-Woverlapping-patterns (in -Wdefault)]
+    Pattern match is redundant
+    In an equation for ‘exhaustive’: exhaustive B = ...
diff --git a/testsuite/tests/unsatisfiable/T14339_Unsat.hs b/testsuite/tests/unsatisfiable/T14339_Unsat.hs
new file mode 100644
index 0000000000..ffa0c141ab
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14339_Unsat.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T14339_Unsat where
+
+import GHC.TypeError
+
+newtype Foo = Foo Int
+
+class Bar a where
+  bar :: a
+
+instance (Unsatisfiable (Text "Boo")) => Bar Foo where
+  bar = undefined
+
+newtype Baz1 = Baz1 Foo
+
+
+-- should be ok
+deriving instance Unsatisfiable (Text "Shouldn't see this") => Bar Baz1
+
+-- should emit the error "Boo"
+newtype Baz2 = Baz2 Foo
+  deriving Bar
diff --git a/testsuite/tests/unsatisfiable/T14339_Unsat.stderr b/testsuite/tests/unsatisfiable/T14339_Unsat.stderr
new file mode 100644
index 0000000000..c24a421eb8
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T14339_Unsat.stderr
@@ -0,0 +1,4 @@
+
+T14339_Unsat.hs:25:12: error: [GHC-22250]
+    • Boo
+    • When deriving the instance for (Bar Baz2)
diff --git a/testsuite/tests/unsatisfiable/T15232_Unsat.hs b/testsuite/tests/unsatisfiable/T15232_Unsat.hs
new file mode 100644
index 0000000000..c8a55e2be3
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T15232_Unsat.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module T15232_Unsat where
+
+import GHC.TypeError
+
+class C a where f :: a -> a
+instance {-# OVERLAPPING #-} C Int where f _ = 42
+instance {-# OVERLAPPABLE #-} Unsatisfiable ( 'Text "Only Int is supported" ) => C a where f = undefined
+
+main :: IO ()
+main = print $ f (42::Int)
diff --git a/testsuite/tests/unsatisfiable/T22696_Unsat.stderr b/testsuite/tests/unsatisfiable/T22696_Unsat.stderr
new file mode 100644
index 0000000000..26b5362362
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/T22696_Unsat.stderr
@@ -0,0 +1,4 @@
+
+T22696_Unsat.hs:25:12: error: [GHC-22250]
+    • Boo
+    • When deriving the instance for (Bar Baz2)
diff --git a/testsuite/tests/unsatisfiable/UnsatClassMethods.hs b/testsuite/tests/unsatisfiable/UnsatClassMethods.hs
new file mode 100644
index 0000000000..f0543df7ab
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatClassMethods.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatClassMethods where
+
+import GHC.TypeError
+
+-- Easy version
+
+class Cls a where
+  method :: a -> a -> a
+
+instance Unsatisfiable (Text "Not allowed for Bool") => (Cls Bool)
+
+
+-- Trickier version
+
+class C a where
+  {-# MINIMAL (method1, method3, method4) | (method2, method3, method4) | (method1, method2, method4) #-}
+  method1 :: a -> a
+  method1 = method2
+  method2 :: a -> a
+  method2 = method1
+  method3 :: a -> a
+  method3 = method2 . method1
+
+  method4 :: a -> a -> a
+
+instance Unsatisfiable (Text "Not allowed for Int") => (C Int) where
+  method3 = error "not implemented"
diff --git a/testsuite/tests/unsatisfiable/UnsatDefault.hs b/testsuite/tests/unsatisfiable/UnsatDefault.hs
new file mode 100644
index 0000000000..5593fa092e
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefault.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+
+module UnsatDefault where
+
+import GHC.TypeError
+
+class C a where
+  method :: a
+  default method :: Unsatisfiable (Text "Please define the method manually. You can try...") => a
+  method = unsatisfiable
+
+
+instance C Int
diff --git a/testsuite/tests/unsatisfiable/UnsatDefault.stderr b/testsuite/tests/unsatisfiable/UnsatDefault.stderr
new file mode 100644
index 0000000000..b4db515840
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefault.stderr
@@ -0,0 +1,6 @@
+
+UnsatDefault.hs:14:10: error: [GHC-22250]
+    • Please define the method manually. You can try...
+    • In the expression: UnsatDefault.$dmmethod @(Int)
+      In an equation for ‘method’: method = UnsatDefault.$dmmethod @(Int)
+      In the instance declaration for ‘C Int’
diff --git a/testsuite/tests/unsatisfiable/UnsatDefer.hs b/testsuite/tests/unsatisfiable/UnsatDefer.hs
new file mode 100644
index 0000000000..8169fc2483
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefer.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE DataKinds #-}
+
+{-# OPTIONS_GHC -Wno-deferred-type-errors #-}
+
+module Main where
+
+import GHC.TypeError
+
+-- This test makes sure we don't end up with duplication of error messages
+-- when adding Unsatisfiable contexts to classes with superclasses.
+
+-- Test 1: we add an Unsatisfiable context to both the class and its superclass.
+
+class ReflexiveEq a where
+    reflexiveEq :: a -> a -> Bool
+
+type DoubleMsg = Text "Equality is not reflexive on Double"
+instance Unsatisfiable DoubleMsg => ReflexiveEq Double
+
+foo = reflexiveEq 0 (0 :: Double)
+
+main :: IO ()
+main = print foo
diff --git a/testsuite/tests/unsatisfiable/UnsatDefer.stderr b/testsuite/tests/unsatisfiable/UnsatDefer.stderr
new file mode 100644
index 0000000000..fa802c3b3d
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatDefer.stderr
@@ -0,0 +1,5 @@
+UnsatDefer.exe: UnsatDefer.hs:20:7: error: [GHC-22250]
+    • Equality is not reflexive on Double
+    • In the expression: reflexiveEq 0 (0 :: Double)
+      In an equation for ‘foo’: foo = reflexiveEq 0 (0 :: Double)
+(deferred type error)
diff --git a/testsuite/tests/unsatisfiable/UnsatFunDeps.hs b/testsuite/tests/unsatisfiable/UnsatFunDeps.hs
new file mode 100644
index 0000000000..1abf8910af
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatFunDeps.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module UnsatFunDeps where
+
+import GHC.TypeError
+
+class C a b | a -> b
+instance Unsatisfiable (Text "No") => C a b
diff --git a/testsuite/tests/unsatisfiable/UnsatInstance.hs b/testsuite/tests/unsatisfiable/UnsatInstance.hs
new file mode 100644
index 0000000000..c95089cb17
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatInstance.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatInstance where
+
+import GHC.TypeError
+
+instance Unsatisfiable (Text "hello")
diff --git a/testsuite/tests/unsatisfiable/UnsatInstance.stderr b/testsuite/tests/unsatisfiable/UnsatInstance.stderr
new file mode 100644
index 0000000000..d79574e73b
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatInstance.stderr
@@ -0,0 +1,4 @@
+
+UnsatInstance.hs:7:10: error: [GHC-97044]
+    • Class ‘Unsatisfiable’ does not support user-specified instances.
+    • In the instance declaration for ‘Unsatisfiable (Text "hello")’
diff --git a/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs b/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs
new file mode 100644
index 0000000000..13a6ee3e6e
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatPMWarnings.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module UnsatPMWarnings where
+
+import Data.Kind
+import Data.Void
+import GHC.TypeError
+
+data MyGADT a where
+  MyInt :: MyGADT Int
+
+type IsBool :: Type -> Constraint
+type family IsBool a where
+  IsBool Bool = ()
+  IsBool a    = Unsatisfiable (Text "Must be Bool")
+
+foo :: IsBool a => MyGADT a -> Void
+foo x = case x of {}
diff --git a/testsuite/tests/unsatisfiable/Unsatisfiable1.hs b/testsuite/tests/unsatisfiable/Unsatisfiable1.hs
new file mode 100644
index 0000000000..357cd296a1
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/Unsatisfiable1.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+
+module Unsatisfiable1 where
+
+import GHC.TypeError ( Unsatisfiable, unsatisfiable, ErrorMessage(Text) )
+
+type Msg = Text "Cannot call 'uncallable'."
+
+uncallable :: Unsatisfiable Msg => ()
+uncallable = unsatisfiable @Msg
+
+uncallable' :: Unsatisfiable Msg => ()
+uncallable' = uncallable
+
+-------------------------------------
+
+unusual :: Unsatisfiable Msg => Char
+unusual = 42  -- no error
+
+k :: Unsatisfiable (Text "No") => ()
+k = uncallable  -- no error
diff --git a/testsuite/tests/unsatisfiable/Unsatisfiable2.hs b/testsuite/tests/unsatisfiable/Unsatisfiable2.hs
new file mode 100644
index 0000000000..88241a7e46
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/Unsatisfiable2.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds #-}
+
+module Unsatisfiable2 where
+
+import GHC.TypeError
+import Data.Type.Bool ( If )
+import Data.Kind
+import Data.Proxy
+
+
+type ExpectTrue x = If x (() :: Constraint) (Unsatisfiable (Text "Input was False!"))
+
+h1 :: ExpectTrue x => proxy x -> ()
+h1 _ = ()
+
+h2 :: If x (() :: Constraint) (Unsatisfiable (Text "Input was False!")) => proxy x -> ()
+h2 _ = ()
+
+eg11 _ = h1 (Proxy @True)
+eg12 p = h1 p
+eg21 _ = h2 (Proxy @True)
+eg22 p = h2 p
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs
new file mode 100644
index 0000000000..70e2b78ac5
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatisfiableFail1 where
+
+import GHC.TypeError
+
+type Msg = Text "Cannot call 'uncallable'."
+
+uncallable :: Unsatisfiable Msg => ()
+uncallable = unsatisfiable @Msg
+
+rejected = uncallable
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr
new file mode 100644
index 0000000000..9babaf7aea
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail1.stderr
@@ -0,0 +1,5 @@
+
+UnsatisfiableFail1.hs:12:12: error: [GHC-22250]
+    • Cannot call 'uncallable'.
+    • In the expression: uncallable
+      In an equation for ‘rejected’: rejected = uncallable
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs
new file mode 100644
index 0000000000..07309c25a4
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatisfiableFail2 where
+
+import GHC.TypeError
+import Data.Type.Bool ( If )
+import Data.Kind
+import Data.Proxy
+
+type ExpectTrue x = If x (() :: Constraint) (Unsatisfiable (Text "Input was False!"))
+
+h :: ExpectTrue x => proxy x -> ()
+h _ = ()
+
+eg3 _ = h (Proxy @False)  -- error
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr
new file mode 100644
index 0000000000..04c9574f49
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail2.stderr
@@ -0,0 +1,5 @@
+
+UnsatisfiableFail2.hs:15:9: error: [GHC-22250]
+    • Input was False!
+    • In the expression: h (Proxy @False)
+      In an equation for ‘eg3’: eg3 _ = h (Proxy @False)
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs
new file mode 100644
index 0000000000..90befcd5a9
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE DataKinds #-}
+
+module UnsatisfiableFail3 where
+
+import GHC.TypeError
+
+
+-- This test makes sure we don't end up with duplication of error messages
+-- when adding Unsatisfiable contexts to classes with superclasses.
+
+-- Test 1: we add an Unsatisfiable context to both the class and its superclass.
+
+class Eq a => ReflexiveEq a where
+    reflexiveEq :: a -> a -> Bool
+    reflexiveEq = (==)
+
+instance Unsatisfiable (Text "Can't compare functions with (==)") => Eq (a -> b) where
+  (==) = unsatisfiable
+
+instance Unsatisfiable (Text "Can't compare functions with reflexiveEq") => ReflexiveEq (a -> b)
+
+type DoubleMsg = Text "Equality is not reflexive on Double"
+instance Unsatisfiable DoubleMsg => ReflexiveEq Double where
+    reflexiveEq = unsatisfiable @DoubleMsg
+
+foo = reflexiveEq 0 (0 :: Double)
+
+bar = reflexiveEq (\ (x :: Int) -> x + 1)
+
+
+-- Test 2: we add an Unsatisfiable context to the class, but not the superclass.
+
+class Eq a => ReflexiveEq' a where
+    reflexiveEq' :: a -> a -> Bool
+    reflexiveEq' = (==)
+
+instance Unsatisfiable (Text "Can't compare functions with reflexiveEq'") => ReflexiveEq' (a -> b)
+instance Unsatisfiable DoubleMsg => ReflexiveEq' Double where
+    reflexiveEq' = unsatisfiable @DoubleMsg
+
+foo' = reflexiveEq' 0 (0 :: Double)
+
+bar' = reflexiveEq' (\ (x :: Int) -> x + 1)
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr
new file mode 100644
index 0000000000..5db0db1c04
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail3.stderr
@@ -0,0 +1,21 @@
+
+UnsatisfiableFail3.hs:26:7: error: [GHC-22250]
+    • Equality is not reflexive on Double
+    • In the expression: reflexiveEq 0 (0 :: Double)
+      In an equation for ‘foo’: foo = reflexiveEq 0 (0 :: Double)
+
+UnsatisfiableFail3.hs:28:7: error: [GHC-22250]
+    • Can't compare functions with reflexiveEq
+    • In the expression: reflexiveEq (\ (x :: Int) -> x + 1)
+      In an equation for ‘bar’: bar = reflexiveEq (\ (x :: Int) -> x + 1)
+
+UnsatisfiableFail3.hs:41:8: error: [GHC-22250]
+    • Equality is not reflexive on Double
+    • In the expression: reflexiveEq' 0 (0 :: Double)
+      In an equation for ‘foo'’: foo' = reflexiveEq' 0 (0 :: Double)
+
+UnsatisfiableFail3.hs:43:8: error: [GHC-22250]
+    • Can't compare functions with reflexiveEq'
+    • In the expression: reflexiveEq' (\ (x :: Int) -> x + 1)
+      In an equation for ‘bar'’:
+          bar' = reflexiveEq' (\ (x :: Int) -> x + 1)
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs
new file mode 100644
index 0000000000..070c621d4e
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds, PartialTypeSignatures #-}
+
+module UnsatisfiableFail4 where
+
+import GHC.TypeError
+
+data D = MkD
+
+-- Check that we don't try to solve errors in kinds using Unsatisfiable.
+
+instance Unsatisfiable (Text "msg") => Eq D where
+  _ == _ = let y :: Maybe Maybe
+               y = unsatisfiable
+           in unsatisfiable
+
+instance Unsatisfiable (Text "msg") => Ord D where
+  compare _ _
+    = let y :: _ => Maybe Maybe
+          y = unsatisfiable
+      in unsatisfiable
diff --git a/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr
new file mode 100644
index 0000000000..5ce4735a42
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/UnsatisfiableFail4.stderr
@@ -0,0 +1,22 @@
+
+UnsatisfiableFail4.hs:12:27: error: [GHC-83865]
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the first argument of ‘Maybe’, namely ‘Maybe’
+      In the type signature: y :: Maybe Maybe
+      In the expression:
+        let
+          y :: Maybe Maybe
+          y = unsatisfiable
+        in unsatisfiable
+
+UnsatisfiableFail4.hs:18:27: error: [GHC-83865]
+    • Expecting one more argument to ‘Maybe’
+      Expected a type, but ‘Maybe’ has kind ‘* -> *’
+    • In the first argument of ‘Maybe’, namely ‘Maybe’
+      In the type signature: y :: _ => Maybe Maybe
+      In the expression:
+        let
+          y :: _ => Maybe Maybe
+          y = unsatisfiable
+        in unsatisfiable
diff --git a/testsuite/tests/unsatisfiable/all.T b/testsuite/tests/unsatisfiable/all.T
new file mode 100644
index 0000000000..2358c7eabc
--- /dev/null
+++ b/testsuite/tests/unsatisfiable/all.T
@@ -0,0 +1,19 @@
+
+test('Unsatisfiable1', normal, compile, [''])
+test('Unsatisfiable2', normal, compile, [''])
+test('UnsatisfiableFail1', normal, compile_fail, [''])
+test('UnsatisfiableFail2', normal, compile_fail, [''])
+test('UnsatisfiableFail3', normal, compile_fail, [''])
+test('UnsatisfiableFail4', normal, compile_fail, [''])
+
+test('UnsatClassMethods', normal, compile, ['-Werror=missing-methods'])
+test('UnsatDefault', normal, compile_fail, [''])
+test('UnsatDefer', exit_code(1), compile_and_run, ['-fdefer-type-errors'])
+test('UnsatFunDeps', normal, compile, [''])
+test('UnsatInstance', normal, compile_fail, [''])
+test('UnsatPMWarnings', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns'])
+
+test('T11503_Unsat', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns'])
+test('T14141_Unsat', normal, compile, ['-Woverlapping-patterns -Wincomplete-patterns'])
+test('T14339_Unsat', normal, compile_fail, [''])
+test('T15232_Unsat', normal, compile, ['-Wredundant-constraints'])