New kind-polymorphic core

This big patch implements a kind-polymorphic core for GHC. The current
implementation focuses on making sure that all kind-monomorphic programs still
work in the new core; it is not yet guaranteed that kind-polymorphic programs
(using the new -XPolyKinds flag) will work.

For more information, see http://haskell.org/haskellwiki/GHC/Kinds

68 files changed, 176 insertions, 187 deletions

diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index d1b12aa476..b7ae6fd406 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -38,7 +38,8 @@ expectedGhcOnlyExtensions = ["ParallelArrays",
                              "AlternativeLayoutRule",
                              "AlternativeLayoutRuleTransitional",
                              "MonadComprehensions",
-                             "TraditionalRecordSyntax"]
+                             "TraditionalRecordSyntax",
+                             "PolyKinds"]
 
 expectedCabalOnlyExtensions :: [String]
 expectedCabalOnlyExtensions = ["Generics",
diff --git a/testsuite/tests/gadt/gadt10.stderr b/testsuite/tests/gadt/gadt10.stderr
index 100c84bab7..7858f51e8b 100644
--- a/testsuite/tests/gadt/gadt10.stderr
+++ b/testsuite/tests/gadt/gadt10.stderr
@@ -1,7 +1,7 @@
 
 gadt10.hs:6:24:
     `RInt' is not applied to enough type arguments
-    Expected kind `?', but `RInt' has kind `k0 -> *'
+    Expected kind `??', but `RInt' has kind `k0 -> *'
     In the type `RInt'
     In the definition of data constructor `R'
     In the data type declaration for `RInt'
diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr
index dbac243ab6..612c809fb8 100644
--- a/testsuite/tests/gadt/rw.stderr
+++ b/testsuite/tests/gadt/rw.stderr
@@ -1,19 +1,20 @@
 
-rw.hs:14:47:
+rw.hs:14:42:
     Couldn't match type `a' with `Int'
       `a' is a rigid type variable bound by
           the type signature for writeInt :: T a -> IORef a -> IO ()
           at rw.hs:13:1
-    In the second argument of `writeIORef', namely `(1 :: Int)'
+    Expected type: IORef Int
+      Actual type: IORef a
+    In the first argument of `writeIORef', namely `ref'
     In the expression: writeIORef ref (1 :: Int)
-    In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)
 
-rw.hs:19:51:
+rw.hs:19:34:
     Couldn't match type `a' with `Bool'
       `a' is a rigid type variable bound by
           the type signature for readBool :: T a -> IORef a -> IO ()
           at rw.hs:17:1
-    Expected type: a -> Bool
-      Actual type: Bool -> Bool
-    In the second argument of `(.)', namely `not'
-    In the second argument of `(>>=)', namely `(print . not)'
+    Expected type: IORef Bool
+      Actual type: IORef a
+    In the first argument of `readIORef', namely `ref'
+    In the first argument of `(>>=)', namely `readIORef ref'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr
index 42bc53da2a..b001e553a6 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr
@@ -1,7 +1,7 @@
 
 SimpleFail14.hs:5:15:
     Predicate `a ~ a' used as a type
-    Expected kind `?', but `a ~ a' has kind `Constraint'
+    Expected kind `??', but `a ~ a' has kind `Constraint'
     In the type `a ~ a'
     In the definition of data constructor `T'
     In the data type declaration for `T'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
index 6bbbb32da9..24be6db7ed 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
@@ -1,4 +1,4 @@
 
 SimpleFail1a.hs:4:1:
-    Family instance has too few parameters; expected 2
+    Number of parameters must match family declaration; expected 2
     In the data type instance declaration for `T1'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
index 8ac486e003..3677317034 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
@@ -1,5 +1,4 @@
 
 SimpleFail1b.hs:4:1:
-    Kind mis-match
-    Expected kind `* -> * -> k0 -> k1', but `T1' has kind `* -> * -> *'
+    Number of parameters must match family declaration; expected 2
     In the data type instance declaration for `T1'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs
index de674a39fd..dad09a27fd 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
 
 module ShouldFail where
 
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index b3b8428a55..bba0274108 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -1,6 +1,6 @@
 
-T2664.hs:31:33:
-    Could not deduce (Dual a ~ Dual b)
+T2664.hs:31:17:
+    Could not deduce (b ~ a)
     from the context (Connect a, Connect b)
       bound by the instance declaration at T2664.hs:22:10-52
     or from ((a :*: b) ~ Dual c, c ~ Dual (a :*: b))
@@ -8,11 +8,13 @@ T2664.hs:31:33:
                  newPChan :: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
                              IO (PChan (a :*: b), PChan c)
       at T2664.hs:(23,5)-(31,87)
-    NB: `Dual' is a type function, and may not be injective
-    Expected type: c
-      Actual type: Dual b :+: Dual a
-    Expected type: PChan c
-      Actual type: PChan (Dual b :+: Dual a)
-    In the return type of a call of `E'
-    In the expression:
-      E (pchoose Right v newPChan) (pchoose Left v newPChan)
+      `b' is a rigid type variable bound by
+          the instance declaration at T2664.hs:22:30
+      `a' is a rigid type variable bound by
+          the instance declaration at T2664.hs:22:19
+    Expected type: PChan (a :*: b)
+      Actual type: PChan (b :*: a)
+    In the expression: O $ takeMVar v
+    In the first argument of `return', namely
+      `(O $ takeMVar v, 
+        E (pchoose Right v newPChan) (pchoose Left v newPChan))'
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 15eefb6c09..2bf23f0e62 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -58,7 +58,7 @@ test('T4093a', normal, compile_fail, [''])
 test('T4093b', normal, compile_fail, [''])
 test('T3330a', reqlib('mtl'), compile_fail, [''])
 test('T3330b', normal, compile_fail, [''])
-test('T3330c', normal, compile_fail, [''])
+test('T3330c', expect_fail, compile_fail, [''])
 test('T4179', normal, compile_fail, [''])
 test('T4254', normal, compile_fail, [''])
 test('T2239', normal, compile_fail, [''])
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 7edc63653d..1ff54b048e 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -133,7 +133,7 @@ test('T3064',
       # expected value: 108937496 (amd64/Linux) (28/6/2011):
       if_wordsize(64,
           compiler_stats_num_field('bytes allocated', 110000000,
-                                                      140000000)),
+                                                      150000000)),
       # expected value: 2247016 (x86/Linux) (28/6/2011):
       if_wordsize(32,
           compiler_stats_num_field('max_bytes_used', 2000000,
@@ -160,7 +160,7 @@ test('T5030',
       # expected value: 1255998208 (amd64/Linux):
       if_wordsize(64,
           compiler_stats_num_field('bytes allocated', 1200000000,
-                                                      1300000000)),
+                                                      1330000000)),
        only_ways(['normal'])
       ],
      compile,
diff --git a/testsuite/tests/rename/should_fail/rnfail057.hs b/testsuite/tests/rename/should_fail/rnfail057.hs
index df068812fe..88b556584f 100644
--- a/testsuite/tests/rename/should_fail/rnfail057.hs
+++ b/testsuite/tests/rename/should_fail/rnfail057.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE KindSignatures #-}
+
 module BindKindName where
 
 type Foo (a :: DontExistKind) = a
diff --git a/testsuite/tests/rename/should_fail/rnfail057.stderr b/testsuite/tests/rename/should_fail/rnfail057.stderr
index 556fab629f..79a5ac7edc 100644
--- a/testsuite/tests/rename/should_fail/rnfail057.stderr
+++ b/testsuite/tests/rename/should_fail/rnfail057.stderr
@@ -1,4 +1,3 @@
 
-rnfail057.hs:3:16:
-    Unexpected named kind:
-        DontExistKind
+rnfail057.hs:5:16:
+    Not in scope: type constructor or class `DontExistKind'
diff --git a/testsuite/tests/safeHaskell/safeLanguage/SafeLang12.stderr b/testsuite/tests/safeHaskell/safeLanguage/SafeLang12.stderr
index 03c4d1abe8..117316192f 100644
--- a/testsuite/tests/safeHaskell/safeLanguage/SafeLang12.stderr
+++ b/testsuite/tests/safeHaskell/safeLanguage/SafeLang12.stderr
@@ -6,5 +6,6 @@ SafeLang12_B.hs:2:14:
     Warning: -XTemplateHaskell is not allowed in Safe Haskell; ignoring -XTemplateHaskell
 [1 of 3] Compiling SafeLang12_B     ( SafeLang12_B.hs, SafeLang12_B.o )
 
-SafeLang12_B.hs:14:68:
-    lexical error in string/character literal at character '\''
+SafeLang12_B.hs:14:67:
+    Syntax error on ''Class
+    Perhaps you intended to use -XTemplateHaskell
diff --git a/testsuite/tests/simplCore/should_compile/T4201.stdout b/testsuite/tests/simplCore/should_compile/T4201.stdout
index 0009de14cc..46073c488c 100644
--- a/testsuite/tests/simplCore/should_compile/T4201.stdout
+++ b/testsuite/tests/simplCore/should_compile/T4201.stdout
@@ -1 +1 @@
-                   ((->) (Sym (Eta.NTCo:Foo)) (Refl Eta.T))) -}
+                  Eta.bof `cast` ((->) (Sym (Eta.NTCo:Foo)) (Refl Eta.T)) -}
diff --git a/testsuite/tests/simplCore/should_compile/rule2.stderr b/testsuite/tests/simplCore/should_compile/rule2.stderr
index 2bdb17fa4a..f41296a15f 100644
--- a/testsuite/tests/simplCore/should_compile/rule2.stderr
+++ b/testsuite/tests/simplCore/should_compile/rule2.stderr
@@ -13,21 +13,18 @@
 Total ticks:     11
 
 2 PreInlineUnconditionally
-    1 f
-    1 lvl
-1 UnfoldingDone
-    1 Roman.bar
-1 RuleFired
-    1 foo/bar
+  1 f
+  1 lvl
+1 UnfoldingDone 1 Roman.bar
+1 RuleFired 1 foo/bar
 7 BetaReduction
-    1 f
-    1 m
-    1 a
-    1 m
-    1 a
-    1 m
-    1 b
-8 SimplifierDone
-    8
+  1 f
+  1 m
+  1 a
+  1 m
+  1 a
+  1 b
+  1 m
+8 SimplifierDone 8
 
 
diff --git a/testsuite/tests/simplCore/should_compile/simpl017.stderr b/testsuite/tests/simplCore/should_compile/simpl017.stderr
index ab82e56c36..d82014bdb9 100644
--- a/testsuite/tests/simplCore/should_compile/simpl017.stderr
+++ b/testsuite/tests/simplCore/should_compile/simpl017.stderr
@@ -1,7 +1,7 @@
 
 simpl017.hs:44:12:
     Couldn't match expected type `forall v. [E m i] -> E' v m a'
-                with actual type `[E m i] -> E' v0 m a'
+                with actual type `[E m i] -> E' v0 m0 e0'
     In the first argument of `return', namely `f'
     In a stmt of a 'do' block: return f
     In the first argument of `E', namely
diff --git a/testsuite/tests/th/T3319.stderr b/testsuite/tests/th/T3319.stderr
index 00b123d289..214b1eff9f 100644
--- a/testsuite/tests/th/T3319.stderr
+++ b/testsuite/tests/th/T3319.stderr
@@ -2,7 +2,7 @@ T3319.hs:1:1: Splicing declarations
     return
       [ForeignD
          (ImportF
-            CCall Unsafe "&" (mkName "foo") (AppT (ConT 'Ptr) (ConT '())))]
+            CCall Unsafe "&" (mkName "foo") (AppT (ConT ''Ptr) (ConT ''())))]
   ======>
     T3319.hs:8:3-93
     foreign import ccall unsafe "static &foo" foo :: Ptr GHC.Tuple.()
diff --git a/testsuite/tests/th/T5290.stderr b/testsuite/tests/th/T5290.stderr
index d8afd836b1..9f7067be06 100644
--- a/testsuite/tests/th/T5290.stderr
+++ b/testsuite/tests/th/T5290.stderr
@@ -1,6 +1,6 @@
 T5290.hs:1:1: Splicing declarations
     let n = mkName "T"
-    in return [DataD [] n [] [NormalC n [(Unpacked, ConT 'Int)]] []]
+    in return [DataD [] n [] [NormalC n [(Unpacked, ConT ''Int)]] []]
   ======>
     T5290.hs:(7,4)-(8,67)
     data T = T {-# UNPACK #-} !Int
diff --git a/testsuite/tests/th/TH_foreignInterruptible.stderr b/testsuite/tests/th/TH_foreignInterruptible.stderr
index 39112c150b..6893d0a773 100644
--- a/testsuite/tests/th/TH_foreignInterruptible.stderr
+++ b/testsuite/tests/th/TH_foreignInterruptible.stderr
@@ -6,7 +6,7 @@ TH_foreignInterruptible.hs:1:1: Splicing declarations
             Interruptible
             "&"
             (mkName "foo")
-            (AppT (ConT 'Ptr) (ConT '())))]
+            (AppT (ConT ''Ptr) (ConT ''())))]
   ======>
     TH_foreignInterruptible.hs:8:3-100
     foreign import ccall interruptible "static &foo" foo
diff --git a/testsuite/tests/th/TH_genEx.stderr b/testsuite/tests/th/TH_genEx.stderr
index 88eeca7d5c..843959f693 100644
--- a/testsuite/tests/th/TH_genEx.stderr
+++ b/testsuite/tests/th/TH_genEx.stderr
@@ -1,5 +1,5 @@
 TH_genEx.hs:1:1: Splicing declarations
-    genAny (reify 'MyInterface)
+    genAny (reify ''MyInterface)
   ======>
     TH_genEx.hs:13:3-30
     data AnyMyInterface1111
diff --git a/testsuite/tests/typecheck/should_compile/T5581.hs b/testsuite/tests/typecheck/should_compile/T5581.hs
index 3f5eafdbf0..0e957285f8 100644
--- a/testsuite/tests/typecheck/should_compile/T5581.hs
+++ b/testsuite/tests/typecheck/should_compile/T5581.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE ConstraintKinds, FlexibleContexts, FlexibleInstances, KindSignatures #-}
 module TcShouldTerminate where
 
+import GHC.Prim (Constraint)
+
 class C (p :: Constraint)
 class D (p :: Constraint)
 
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 60b7d09603..a411c6d085 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -167,7 +167,7 @@ test('tc163', only_compiler_types(['ghc']), compile, [''])
 test('tc164', normal, compile, [''])
 test('tc165', normal, compile, [''])
 test('tc166', only_compiler_types(['ghc']), compile, [''])
-test('tc167', only_compiler_types(['ghc']), compile, [''])
+test('tc167', only_compiler_types(['ghc']), compile_fail, [''])
 test('tc168', only_compiler_types(['ghc']), compile_fail, [''])
 test('tc169', normal, compile, [''])
 
diff --git a/testsuite/tests/typecheck/should_compile/tc056.stderr b/testsuite/tests/typecheck/should_compile/tc056.stderr
index c49396721c..786c88e804 100644
--- a/testsuite/tests/typecheck/should_compile/tc056.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc056.stderr
@@ -2,5 +2,5 @@
 tc056.hs:16:10:
     Warning: Duplicate constraint(s): Eq' a
     In the context: (Eq' a, Eq' a)
-    While checking the context of an instance declaration
+    While checking an instance declaration
     In the instance declaration for `Eq' [a]'
diff --git a/testsuite/tests/typecheck/should_compile/tc255.hs b/testsuite/tests/typecheck/should_compile/tc255.hs
index a9b0440db9..d77a7b688b 100644
--- a/testsuite/tests/typecheck/should_compile/tc255.hs
+++ b/testsuite/tests/typecheck/should_compile/tc255.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-}
 module Ctx where
 
+import GHC.Prim( Constraint )
+
 type family Indirect :: * -> Constraint
 type instance Indirect = Show
 
diff --git a/testsuite/tests/typecheck/should_compile/tc256.hs b/testsuite/tests/typecheck/should_compile/tc256.hs
index dcfbf1a1a7..f06eabf1c3 100644
--- a/testsuite/tests/typecheck/should_compile/tc256.hs
+++ b/testsuite/tests/typecheck/should_compile/tc256.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE TypeFamilies, ConstraintKinds, UndecidableInstances #-}
 module Ctx where
 
+import GHC.Prim( Constraint )
+
 type family Indirect :: * -> Constraint
 type instance Indirect = Show
 
diff --git a/testsuite/tests/typecheck/should_compile/tc257.hs b/testsuite/tests/typecheck/should_compile/tc257.hs
index b1db39f77e..efab2df224 100644
--- a/testsuite/tests/typecheck/should_compile/tc257.hs
+++ b/testsuite/tests/typecheck/should_compile/tc257.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE KindSignatures, ConstraintKinds, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
 module Ctx where
 
+import GHC.Prim( Constraint )
+
 data Proxy (ctxt :: * -> Constraint) = Proxy
 
 -- At one time, this one worked:
diff --git a/testsuite/tests/typecheck/should_compile/tc258.hs b/testsuite/tests/typecheck/should_compile/tc258.hs
index 00f030d7a8..54a3e637be 100644
--- a/testsuite/tests/typecheck/should_compile/tc258.hs
+++ b/testsuite/tests/typecheck/should_compile/tc258.hs
@@ -2,6 +2,8 @@
 
 module AltPrelude where
 
+import GHC.Prim (Constraint)
+
 class MyFunctor f where
        type FunctorCtxt f a :: Constraint
        type FunctorCtxt f a = ()
diff --git a/testsuite/tests/typecheck/should_fail/AssocTyDef06.stderr b/testsuite/tests/typecheck/should_fail/AssocTyDef06.stderr
index d71a83b587..417e0f8419 100644
--- a/testsuite/tests/typecheck/should_fail/AssocTyDef06.stderr
+++ b/testsuite/tests/typecheck/should_fail/AssocTyDef06.stderr
@@ -1,6 +1,5 @@
 
 AssocTyDef06.hs:6:5:
-    Kind mis-match
-    Expected kind `k0 -> k1 -> k2', but `Typ' has kind `k0 -> *'
+    Number of parameters must match family declaration; expected 1
     In the type synonym instance default declaration for `Typ'
     In the class declaration for `Cls'
diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr
index de91620078..f7215b7abd 100644
--- a/testsuite/tests/typecheck/should_fail/T2688.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2688.stderr
@@ -1,13 +1,12 @@
 
-T2688.hs:8:22:
-    Could not deduce (s ~ v)
+T2688.hs:8:14:
+    Could not deduce (v ~ s)
     from the context (VectorSpace v s)
       bound by the class declaration for `VectorSpace'
       at T2688.hs:(5,1)-(8,23)
-      `s' is a rigid type variable bound by
-          the class declaration for `VectorSpace' at T2688.hs:5:21
       `v' is a rigid type variable bound by
           the class declaration for `VectorSpace' at T2688.hs:5:19
-    In the second argument of `(/)', namely `s'
-    In the second argument of `(*^)', namely `(1 / s)'
+      `s' is a rigid type variable bound by
+          the class declaration for `VectorSpace' at T2688.hs:5:21
     In the expression: v *^ (1 / s)
+    In an equation for `^/': v ^/ s = v *^ (1 / s)
diff --git a/testsuite/tests/typecheck/should_fail/T2994.stderr b/testsuite/tests/typecheck/should_fail/T2994.stderr
index da472a3316..1e3bd0a434 100644
--- a/testsuite/tests/typecheck/should_fail/T2994.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2994.stderr
@@ -5,10 +5,10 @@ T2994.hs:11:10:
     but `MonadReader Int' has kind `* -> Constraint'
     In the instance declaration for `MonadReader Int'
 
-T2994.hs:13:10:
-    `MonadReader (Reader' r)' is not applied to enough type arguments
-    Expected kind `Constraint',
-    but `MonadReader (Reader' r)' has kind `* -> Constraint'
+T2994.hs:13:23:
+    `Reader' r' is not applied to enough type arguments
+    The first argument of `MonadReader' should have kind `*',
+    but `Reader' r' has kind `* -> *'
     In the instance declaration for `MonadReader (Reader' r)'
 
 T2994.hs:15:10:
diff --git a/testsuite/tests/typecheck/should_fail/T3540.stderr b/testsuite/tests/typecheck/should_fail/T3540.stderr
index d29dc2e145..348c14c905 100644
--- a/testsuite/tests/typecheck/should_fail/T3540.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3540.stderr
@@ -1,7 +1,6 @@
 
-T3540.hs:4:12:
-    Predicate `a ~ Int' used as a type
-    Expected kind `*', but `a ~ Int' has kind `Constraint'
+T3540.hs:4:1:
+    Expecting an ordinary type, but found a type of kind Constraint
     In the type signature for `thing': thing :: a ~ Int
 
 T3540.hs:7:20:
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index bdecc12835..8eb1ab9a4d 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,7 +1,7 @@
 
 T3950.hs:15:13:
-    Couldn't match expected type `Id p' with actual type `Id p x0'
+    Couldn't match expected type `Id p' with actual type `Id p0 x0'
     Expected type: w (Id p)
-      Actual type: Sealed (Id p x0)
+      Actual type: Sealed (Id p0 x0)
     In the first argument of `Just', namely rp'
     In the expression: Just rp'
diff --git a/testsuite/tests/typecheck/should_fail/T5573a.stderr b/testsuite/tests/typecheck/should_fail/T5573a.stderr
index 192ef4cacc..f11c123951 100644
--- a/testsuite/tests/typecheck/should_fail/T5573a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5573a.stderr
@@ -1,15 +1,16 @@
-

-T5573a.hs:11:16:

-    Kind incompatibility when matching types:

-      t0 :: ??

-      (# Bool, Bool #) :: (#)

-    In the expression: (# True, False #)

-    In the expression: (# x, (# True, False #) #)

-    In an equation for `foo2': foo2 x = (# x, (# True, False #) #)

-

-T5573a.hs:14:6:

-    Kind incompatibility when matching types:

-      t0 :: ??

-      (# t1, t2 #) :: (#)

-    In the pattern: (# x, y #)

-    In an equation for `foo3': foo3 (# x, y #) = x

+
+T5573a.hs:11:16:
+    Couldn't match kind `??' against `(#)'
+    Kind incompatibility when matching types:
+      t0 :: ??
+      (# t1, t2 #) :: (#)
+    In the expression: (# True, False #)
+    In the expression: (# x, (# True, False #) #)
+
+T5573a.hs:14:6:
+    Couldn't match kind `??' against `(#)'
+    Kind incompatibility when matching types:
+      t0 :: ??
+      (# t1, t2 #) :: (#)
+    In the pattern: (# x, y #)
+    In an equation for `foo3': foo3 (# x, y #) = x
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index d8435d2d43..03f0f7b60c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -145,7 +145,7 @@ test('tcfail154', normal, compile_fail, [''])
 test('tcfail155', normal, compile_fail, [''])
 test('tcfail156', normal, compile_fail, [''])
 test('tcfail157', normal, compile_fail, [''])
-test('tcfail158', normal, compile_fail, [''])
+test('tcfail158', expect_fail, compile_fail, [''])
 test('tcfail159', normal, compile_fail, [''])
 test('tcfail160', normal, compile_fail, [''])
 test('tcfail161', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/mc19.stderr b/testsuite/tests/typecheck/should_fail/mc19.stderr
index c7bca0afd4..f77da6fe4b 100644
--- a/testsuite/tests/typecheck/should_fail/mc19.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc19.stderr
@@ -1,9 +1,7 @@
 
 mc19.hs:10:31:
-    Couldn't match type `a' with `[a]'
-      `a' is a rigid type variable bound by
-          a type expected by the context: [a] -> [a] at mc19.hs:10:26
+    Occurs check: cannot construct the infinite type: a0 = [a0]
     Expected type: [a] -> [a]
-      Actual type: [a] -> [[a]]
+      Actual type: [a0] -> [[a0]]
     In the expression: inits
     In a stmt of a monad comprehension: then inits
diff --git a/testsuite/tests/typecheck/should_fail/mc21.stderr b/testsuite/tests/typecheck/should_fail/mc21.stderr
index 95c077cb25..c712b4b4be 100644
--- a/testsuite/tests/typecheck/should_fail/mc21.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc21.stderr
@@ -4,6 +4,6 @@ mc21.hs:12:26:
       `a' is a rigid type variable bound by
           a type expected by the context: [a] -> [[a]] at mc21.hs:12:9
     Expected type: [a] -> [[a]]
-      Actual type: [a] -> [a]
+      Actual type: [[a]] -> [[a]]
     In the return type of a call of `take'
     In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/mc22.stderr b/testsuite/tests/typecheck/should_fail/mc22.stderr
index 96294ae693..943b7624f0 100644
--- a/testsuite/tests/typecheck/should_fail/mc22.stderr
+++ b/testsuite/tests/typecheck/should_fail/mc22.stderr
@@ -4,6 +4,6 @@ mc22.hs:10:26:
       `a' is a rigid type variable bound by
           a type expected by the context: [a] -> [t0 a] at mc22.hs:10:9
     Expected type: [a] -> [t0 a]
-      Actual type: [a] -> [a]
+      Actual type: [t0 a] -> [t0 a]
     In the return type of a call of `take'
     In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/tcfail028.stderr b/testsuite/tests/typecheck/should_fail/tcfail028.stderr
index 7ad9ecbb23..e6d06db31d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail028.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail028.stderr
@@ -1,7 +1,7 @@
 
 tcfail028.hs:4:17:
     `A a' is not applied to enough type arguments
-    Expected kind `?', but `A a' has kind `k0 -> *'
+    Expected kind `??', but `A a' has kind `k0 -> *'
     In the type `A a'
     In the definition of data constructor `B'
     In the data type declaration for `A'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail065.stderr b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
index 9d94b920ff..637ebcaabc 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail065.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
@@ -1,11 +1,12 @@
 
-tcfail065.hs:29:20:
-    Couldn't match type `x1' with `x'
+tcfail065.hs:29:18:
+    Couldn't match type `x' with `x1'
+      `x' is a rigid type variable bound by
+          the instance declaration at tcfail065.hs:28:18
       `x1' is a rigid type variable bound by
            the type signature for setX :: x1 -> X x -> X x
            at tcfail065.hs:29:3
-      `x' is a rigid type variable bound by
-          the instance declaration at tcfail065.hs:28:18
-    In the first argument of `X', namely `x'
+    Expected type: X x1
+      Actual type: X x
+    In the return type of a call of `X'
     In the expression: X x
-    In an equation for `setX': setX x (X _) = X x
diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
index 1a7c840e0b..afc8a3cc7b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
@@ -12,30 +12,30 @@ tcfail068.hs:14:9:
           the type signature for
             itgen :: Constructed a => (Int, Int) -> a -> IndTree s a
           at tcfail068.hs:12:1
-    Expected type: GHC.ST.ST s (IndTree s1 a)
+    Expected type: GHC.ST.ST s1 (IndTree s a)
       Actual type: GHC.ST.ST s (STArray s (Int, Int) a)
     In the return type of a call of `newSTArray'
     In the first argument of `runST', namely
       `(newSTArray ((1, 1), n) x)'
 
-tcfail068.hs:20:22:
-    Could not deduce (s ~ s1)
+tcfail068.hs:20:9:
+    Could not deduce (s1 ~ s)
     from the context (Constructed a)
       bound by the type signature for
                  itiap :: Constructed a =>
                           (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
       at tcfail068.hs:(17,1)-(21,19)
+      `s1' is a rigid type variable bound by
+           a type expected by the context: GHC.ST.ST s1 (IndTree s a)
+           at tcfail068.hs:18:9
       `s' is a rigid type variable bound by
           the type signature for
             itiap :: Constructed a =>
                      (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
           at tcfail068.hs:17:1
-      `s1' is a rigid type variable bound by
-           a type expected by the context: GHC.ST.ST s1 (IndTree s a)
-           at tcfail068.hs:18:9
-    Expected type: STArray s1 (Int, Int) a
-      Actual type: IndTree s a
-    In the first argument of `writeSTArray', namely `arr'
+    Expected type: GHC.ST.ST s1 ()
+      Actual type: GHC.ST.ST s ()
+    In the return type of a call of `writeSTArray'
     In the first argument of `(>>)', namely
       `writeSTArray arr i (f val)'
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail087.stderr b/testsuite/tests/typecheck/should_fail/tcfail087.stderr
index 17d9f48537..b9e9d2fa6a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail087.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail087.stderr
@@ -1,5 +1,7 @@
 
-tcfail087.hs:6:11:
-    Illegal unboxed tuple type as function argument: (# Int, Int #)
+tcfail087.hs:6:14:
+    Kind mis-match
+    Expected kind `??', but `(# Int, Int #)' has kind `(#)'
+    In the type `(# Int, Int #)'
     In the definition of data constructor `Ex'
     In the data type declaration for `Ex'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail090.stderr b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
index c63ced52c3..f63d96ee9e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail090.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail090.stderr
@@ -1,5 +1,6 @@
 
 tcfail090.hs:8:9:
+    Couldn't match kind `*' against `#'
     Kind incompatibility when matching types:
       a0 :: *
       ByteArray# :: #
diff --git a/testsuite/tests/typecheck/should_fail/tcfail103.stderr b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
index 636ab29ae7..a892b23c43 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail103.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
@@ -1,11 +1,11 @@
 
-tcfail103.hs:15:23:
-    Couldn't match type `t' with `s'
-      `t' is a rigid type variable bound by
-          the type signature for f :: ST t Int at tcfail103.hs:11:1
+tcfail103.hs:15:13:
+    Couldn't match type `s' with `t'
       `s' is a rigid type variable bound by
           the type signature for g :: ST s Int at tcfail103.hs:15:9
-    Expected type: STRef s Int
-      Actual type: STRef t Int
-    In the first argument of `readSTRef', namely `v'
+      `t' is a rigid type variable bound by
+          the type signature for f :: ST t Int at tcfail103.hs:11:1
+    Expected type: ST s Int
+      Actual type: ST t Int
+    In the return type of a call of `readSTRef'
     In the expression: readSTRef v
diff --git a/testsuite/tests/typecheck/should_fail/tcfail108.stderr b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
index 5d406cd5a6..56c97c20dd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail108.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail108.stderr
@@ -3,5 +3,5 @@ tcfail108.hs:7:10:
     Non type-variable argument in the constraint: Eq (f (Rec f))
     (Use -XFlexibleContexts to permit this)
     In the context: (Eq (f (Rec f)))
-    While checking the context of an instance declaration
+    While checking an instance declaration
     In the instance declaration for `Eq (Rec f)'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail110.stderr b/testsuite/tests/typecheck/should_fail/tcfail110.stderr
index e663999edb..2bc79183ac 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail110.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail110.stderr
@@ -1,6 +1,6 @@
 
-tcfail110.hs:8:30:
+tcfail110.hs:8:19:
     `Foo a' is not applied to enough type arguments
-    Expected kind `*', but `Foo a' has kind `* -> *'
+    Expected kind `??', but `Foo a' has kind `* -> *'
     In the type signature for `bar':
       bar :: String -> (forall a. Foo a) -> IO ()
diff --git a/testsuite/tests/typecheck/should_fail/tcfail115.stderr b/testsuite/tests/typecheck/should_fail/tcfail115.stderr
index fd1a02c02d..00352afd9e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail115.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail115.stderr
@@ -1,11 +1,11 @@
 
 tcfail115.hs:9:24:
+    Couldn't match kind `??' against `(#)'
     Kind incompatibility when matching types:
       t0 :: ??
       (# Int, Int #) :: (#)
     In the expression: (r :: (# Int, Int #))
     In a case alternative: r -> (r :: (# Int, Int #))
-    In the expression: case t of { r -> (r :: (# Int, Int #)) }
 
 tcfail115.hs:12:25:
     The variable `r' cannot have an unboxed tuple type: (# Int, Int #)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
index 3f6c035a55..7002ee0960 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr
@@ -1,26 +1,11 @@
 
 tcfail122.hs:8:9:
-    Kind incompatibility when matching types:
-      d0 :: * -> *
-      b0 :: *
-    Expected type: a0 b0
-      Actual type: c0 d0
-    In the expression:
-        undefined :: forall c :: ((* -> *) -> *) d :: (* -> *). c d
-    In the expression:
-      [undefined :: forall a b. a b,
-       undefined :: forall c :: ((* -> *) -> *) d :: (* -> *). c d]
-
-tcfail122.hs:8:9:
+    Couldn't match kind `* -> *' against `*'
     Kind incompatibility when matching types:
       c0 :: (* -> *) -> *
       a0 :: * -> *
     In the expression:
-        undefined :: forall c :: ((* -> *) -> *) d :: (* -> *). c d
+        undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d
     In the expression:
       [undefined :: forall a b. a b,
-       undefined :: forall c :: ((* -> *) -> *) d :: (* -> *). c d]
-    In an equation for `foo':
-        foo
-          = [undefined :: forall a b. a b,
-             undefined :: forall c :: ((* -> *) -> *) d :: (* -> *). c d]
+       undefined :: forall (c :: (* -> *) -> *) (d :: * -> *). c d]
diff --git a/testsuite/tests/typecheck/should_fail/tcfail123.stderr b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
index 560c8d9048..b7ec97fd3b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail123.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail123.stderr
@@ -1,16 +1,8 @@
 
 tcfail123.hs:11:10:
+    Couldn't match kind `*' against `#'
     Kind incompatibility when matching types:
       t0 :: *
       GHC.Prim.Int# :: #
     In the first argument of `f', namely `3#'
     In the expression: f 3#
-    In the expression: (f 3#, f 4.3#, f True)
-
-tcfail123.hs:11:16:
-    Kind incompatibility when matching types:
-      t1 :: *
-      GHC.Prim.Float# :: #
-    In the first argument of `f', namely `4.3#'
-    In the expression: f 4.3#
-    In the expression: (f 3#, f 4.3#, f True)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail136.stderr b/testsuite/tests/typecheck/should_fail/tcfail136.stderr
index cdeff3c8a5..229cd1ff41 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail136.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail136.stderr
@@ -1,7 +1,7 @@
 
 tcfail136.hs:9:35:
     `SymDict' is not applied to enough type arguments
-    Expected kind `?', but `SymDict' has kind `* -> *'
+    Expected kind `??', but `SymDict' has kind `* -> *'
     In the type `SymDict'
     In the definition of data constructor `SymTable'
     In the data type declaration for `SymTable'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail146.stderr b/testsuite/tests/typecheck/should_fail/tcfail146.stderr
index 9e1c99a766..e66dc94a76 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail146.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail146.stderr
@@ -1,7 +1,7 @@
 
 tcfail146.hs:7:22:
     Predicate `SClass a' used as a type
-    Expected kind `?', but `SClass a' has kind `Constraint'
+    Expected kind `??', but `SClass a' has kind `Constraint'
     In the type `SClass a'
     In the definition of data constructor `SCon'
     In the data type declaration for `SData'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail147.stderr b/testsuite/tests/typecheck/should_fail/tcfail147.stderr
index 360fb0996b..51c32ad8a2 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail147.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail147.stderr
@@ -1,7 +1,7 @@
 
 tcfail147.hs:7:19:
     `XClass' is not applied to enough type arguments
-    Expected kind `?', but `XClass' has kind `k0 -> Constraint'
+    Expected kind `??', but `XClass' has kind `k0 -> Constraint'
     In the type `XClass'
     In the definition of data constructor `XCon'
     In the data type declaration for `XData'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail148.stderr b/testsuite/tests/typecheck/should_fail/tcfail148.stderr
index 13d4293807..670f440314 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail148.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail148.stderr
@@ -1,7 +1,7 @@
 
 tcfail148.hs:5:28:
     `List' is not applied to enough type arguments
-    Expected kind `?', but `List' has kind `* -> *'
+    Expected kind `??', but `List' has kind `* -> *'
     In the type `List'
     In the definition of data constructor `Cons'
     In the data type declaration for `List'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail151.hs b/testsuite/tests/typecheck/should_fail/tcfail151.hs
index 112973b71e..00578a1eb2 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail151.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail151.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DatatypeContexts #-}
+{-# LANGUAGE DatatypeContexts, MultiParamTypeClasses #-}
 module ShouldFail where
 
 class (Show a, Eq a, Monad m) => Name m a where 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
index b389ef1e96..0556582417 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr
@@ -1,8 +1,8 @@
 
 tcfail159.hs:9:11:
+    Couldn't match kind `*' against `(#)'
     Kind incompatibility when matching types:
       t0 :: *
       (# Int, Int #) :: (#)
     In the pattern: ~(# p, q #)
     In a case alternative: ~(# p, q #) -> p
-    In the expression: case h x of { ~(# p, q #) -> p }
diff --git a/testsuite/tests/typecheck/should_fail/tcfail162.stderr b/testsuite/tests/typecheck/should_fail/tcfail162.stderr
index ae7b1c5d27..d4c3903b18 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail162.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail162.stderr
@@ -1,7 +1,7 @@
 
 tcfail162.hs:10:16:
     `ForeignPtr' is not applied to enough type arguments
-    Expected kind `?', but `ForeignPtr' has kind `* -> *'
+    Expected kind `??', but `ForeignPtr' has kind `* -> *'
     In the type `{-# UNPACK #-} !ForeignPtr'
     In the definition of data constructor `Foo'
     In the data type declaration for `Foo'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail174.stderr b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
index 84c0868db4..de8bb6004d 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail174.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail174.stderr
@@ -15,9 +15,9 @@ tcfail174.hs:13:14:
     In the expression: Capture g
 
 tcfail174.hs:16:14:
-    Couldn't match expected type `forall x. x -> b'
+    Couldn't match expected type `forall x. x -> a0'
                 with actual type `forall a. a -> a'
-    Expected type: Capture (forall x. x -> b)
+    Expected type: Capture (forall x. x -> a0)
       Actual type: Capture (forall a. a -> a)
     In the first argument of `Capture', namely `g'
     In the expression: Capture g
diff --git a/testsuite/tests/typecheck/should_fail/tcfail179.stderr b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
index ba995b65ea..d9b4538a17 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail179.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
@@ -1,5 +1,5 @@
 
-tcfail179.hs:14:41:
+tcfail179.hs:14:37:
     Couldn't match type `x' with `s'
       `x' is a rigid type variable bound by
           a pattern with constructor
@@ -8,7 +8,7 @@ tcfail179.hs:14:41:
           at tcfail179.hs:14:14
       `s' is a rigid type variable bound by
           the type signature for run :: T s -> Int at tcfail179.hs:13:1
-    Expected type: x -> s
-      Actual type: x -> x
-    In the second argument of `g', namely `id'
+    Expected type: (s, s, Int)
+      Actual type: (x, s, Int)
+    In the return type of a call of `g'
     In the expression: g x id
diff --git a/testsuite/tests/typecheck/should_fail/tcfail191.stderr b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
index 6fd626afd4..178eebf7ff 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail191.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail191.stderr
@@ -4,6 +4,6 @@ tcfail191.hs:11:26:
       `a' is a rigid type variable bound by
           a type expected by the context: [a] -> [[a]] at tcfail191.hs:11:9
     Expected type: [a] -> [[a]]
-      Actual type: [a] -> [a]
+      Actual type: [[a]] -> [[a]]
     In the return type of a call of `take'
     In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/tcfail192.stderr b/testsuite/tests/typecheck/should_fail/tcfail192.stderr
index d72c821fd6..400671b684 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail192.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail192.stderr
@@ -13,6 +13,6 @@ tcfail192.hs:10:26:
       `a' is a rigid type variable bound by
           a type expected by the context: [a] -> [[a]] at tcfail192.hs:10:9
     Expected type: [a] -> [[a]]
-      Actual type: [a] -> [a]
+      Actual type: [[a]] -> [[a]]
     In the return type of a call of `take'
     In the expression: take 5
diff --git a/testsuite/tests/typecheck/should_fail/tcfail193.stderr b/testsuite/tests/typecheck/should_fail/tcfail193.stderr
index 6fd99ae61b..f19720f796 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail193.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail193.stderr
@@ -1,9 +1,7 @@
 
 tcfail193.hs:10:31:
-    Couldn't match type `a' with `[a]'
-      `a' is a rigid type variable bound by
-          a type expected by the context: [a] -> [a] at tcfail193.hs:10:26
+    Occurs check: cannot construct the infinite type: a0 = [a0]
     Expected type: [a] -> [a]
-      Actual type: [a] -> [[a]]
+      Actual type: [a0] -> [[a0]]
     In the expression: inits
     In a stmt of a list comprehension: then inits
diff --git a/testsuite/tests/typecheck/should_fail/tcfail200.stderr b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
index 90f590d8e2..c75dc8f885 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail200.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail200.stderr
@@ -1,8 +1,8 @@
 
 tcfail200.hs:5:15:
+    Couldn't match kind `*' against `#'
     Kind incompatibility when matching types:
       t0 :: *
       GHC.Prim.Int# :: #
     In the expression: 1#
     In the expression: (1#, 'c')
-    In an equation for `x': x = (1#, 'c')
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index 653e503edc..5efb129a45 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,14 +1,13 @@
 
-tcfail201.hs:18:58:
+tcfail201.hs:18:56:
     Couldn't match type `a' with `HsDoc t0'
       `a' is a rigid type variable bound by
           the type signature for
             gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
-                       -> (forall g. g -> c g)
-                       -> a
-                       -> c a
+                       -> (forall g. g -> c g) -> a -> c a
           at tcfail201.hs:16:1
-    Expected type: HsDoc t0 -> a
-      Actual type: HsDoc t0 -> HsDoc t0
-    In the first argument of `z', namely `DocParagraph'
-    In the first argument of `k', namely `z DocParagraph'
+    Expected type: c a
+      Actual type: c (HsDoc t0)
+    In the expression: z DocParagraph `k` hsDoc
+    In a case alternative:
+        (DocParagraph hsDoc) -> z DocParagraph `k` hsDoc
diff --git a/testsuite/tests/typecheck/should_fail/tcfail206.stderr b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
index 46419c4522..4cb3172926 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail206.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail206.stderr
@@ -14,11 +14,12 @@ tcfail206.hs:8:5:
     In the expression: (1,)
     In an equation for `b': b = (1,)
 
-tcfail206.hs:11:6:
+tcfail206.hs:11:5:
     Couldn't match type `a' with `Bool'
       `a' is a rigid type variable bound by
           the type signature for c :: a -> (a, Bool) at tcfail206.hs:11:1
-    In the expression: True || False
+    Expected type: a -> (a, Bool)
+      Actual type: Bool -> (Bool, Bool)
     In the expression: (True || False,)
     In an equation for `c': c = (True || False,)
 
diff --git a/testsuite/tests/typecheck/should_fail/tcfail210.stderr b/testsuite/tests/typecheck/should_fail/tcfail210.stderr
index d5b106a86d..95aba8e61b 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail210.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail210.stderr
@@ -1,5 +1,3 @@
 
 tcfail210.hs:4:31:
-    Unexpected named kind:
-        Constraint
-    Perhaps you meant to use -XConstraintKinds?
+    Not in scope: type constructor or class `Constraint'
diff --git a/testsuite/tests/typecheck/should_fail/tcfail213.hs b/testsuite/tests/typecheck/should_fail/tcfail213.hs
index 9451533a15..c93c4ad999 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail213.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail213.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE TypeFamilies, ConstraintKinds #-}
 module ShouldFail where
 
+import GHC.Prim( Constraint )
+
 type family F a :: Constraint
 
 class (F a) => C a where
diff --git a/testsuite/tests/typecheck/should_fail/tcfail213.stderr b/testsuite/tests/typecheck/should_fail/tcfail213.stderr
index e67034fcc8..a999e21666 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail213.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail213.stderr
@@ -1,5 +1,5 @@
 
-tcfail213.hs:6:1:
+tcfail213.hs:8:1:
     Illegal irreducible constraint F a
     in superclass/instance head context (Use -XUndecidableInstances to permit this)
     In the context: (F a)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail214.hs b/testsuite/tests/typecheck/should_fail/tcfail214.hs
index 553dfcfcc6..81162e678e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail214.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail214.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE TypeFamilies, ConstraintKinds #-}
 module ShouldFail where
 
+import GHC.Prim( Constraint )
+
 type family F a :: Constraint
 
 class C a where
diff --git a/testsuite/tests/typecheck/should_fail/tcfail214.stderr b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
index 2832df99b4..c924e50a19 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail214.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail214.stderr
@@ -1,7 +1,7 @@
 
-tcfail214.hs:7:10:
+tcfail214.hs:9:10:
     Illegal irreducible constraint F a
     in superclass/instance head context (Use -XUndecidableInstances to permit this)
     In the context: (F a)
-    While checking the context of an instance declaration
+    While checking an instance declaration
     In the instance declaration for `C [a]'