diff --git a/tests/arrows/should_fail/T5380.stderr b/tests/arrows/should_fail/T5380.stderr
index c9df47cf6f95849bb817111e0a2d7e7c49257207..7249be8f13d0df448c57a89cd19ebaec3dca6da1 100644
--- a/tests/arrows/should_fail/T5380.stderr
+++ b/tests/arrows/should_fail/T5380.stderr
@@ -4,7 +4,7 @@ T5380.hs:7:27:
       `not_bool' is a rigid type variable bound by
                  the type signature for
                    testB :: not_bool -> (() -> ()) -> () -> not_unit
-                 at T5380.hs:7:1
+                 at T5380.hs:6:10
     In the expression: b
     In the expression: proc () -> if b then f -< () else f -< ()
     In an equation for `testB':
@@ -15,7 +15,7 @@ T5380.hs:7:34:
       `not_unit' is a rigid type variable bound by
                  the type signature for
                    testB :: not_bool -> (() -> ()) -> () -> not_unit
-                 at T5380.hs:7:1
+                 at T5380.hs:6:42
     Expected type: () -> not_unit
       Actual type: () -> ()
     In the expression: f
diff --git a/tests/gadt/rw.stderr b/tests/gadt/rw.stderr
index 752d0fd8a3680e82a4fef85fe1ca870dfec3b5a4..c6e800b910b38d32e84d994476f53f6e228efb32 100644
--- a/tests/gadt/rw.stderr
+++ b/tests/gadt/rw.stderr
@@ -3,7 +3,7 @@ rw.hs:14:47:
     Couldn't match expected type `a' with actual type `Int'
       `a' is a rigid type variable bound by
           the type signature for writeInt :: T a -> IORef a -> IO ()
-          at rw.hs:13:1
+          at rw.hs:12:14
     In the second argument of `writeIORef', namely `(1 :: Int)'
     In the expression: writeIORef ref (1 :: Int)
     In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)
@@ -12,7 +12,7 @@ rw.hs:19:51:
     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
+          at rw.hs:16:14
     Expected type: a -> Bool
       Actual type: Bool -> Bool
     In the second argument of `(.)', namely `not'
diff --git a/tests/ghci/scripts/Defer02.stderr b/tests/ghci/scripts/Defer02.stderr
index 21cade847deced09a692639fc9caabcff9c30b47..cd146ddbffc67f1811ab3a5e5b462b150e21c490 100644
--- a/tests/ghci/scripts/Defer02.stderr
+++ b/tests/ghci/scripts/Defer02.stderr
@@ -37,7 +37,7 @@
     Couldn't match expected type `a' with actual type `Char'
       `a' is a rigid type variable bound by
           the type signature for h :: a -> (Char, Char)
-          at ../../typecheck/should_run/Defer01.hs:34:1
+          at ../../typecheck/should_run/Defer01.hs:33:6
     In the expression: x
     In the expression: (x, 'c')
     In an equation for `h': h x = (x, 'c')
diff --git a/tests/ghci/scripts/Defer02.stdout b/tests/ghci/scripts/Defer02.stdout
index 6dde3688337abd9613e516a8454ec0e701e363de..e845c09d4bc1b4fa43706cdd3b10ba4b4b73035f 100644
--- a/tests/ghci/scripts/Defer02.stdout
+++ b/tests/ghci/scripts/Defer02.stdout
@@ -36,7 +36,7 @@ Hello World*** Exception: ../../typecheck/should_run/Defer01.hs:11:40:
     Couldn't match expected type `a' with actual type `Char'
       `a' is a rigid type variable bound by
           the type signature for h :: a -> (Char, Char)
-          at ../../typecheck/should_run/Defer01.hs:34:1
+          at ../../typecheck/should_run/Defer01.hs:33:6
     In the expression: x
     In the expression: (x, 'c')
     In an equation for `h': h x = (x, 'c')
diff --git a/tests/indexed-types/should_compile/Simple14.stderr b/tests/indexed-types/should_compile/Simple14.stderr
index c86fffe2fe48e51231a4a45ce4661e27543a9d9e..18221db64e3ef28ee94caf9a99219289ac023def 100644
--- a/tests/indexed-types/should_compile/Simple14.stderr
+++ b/tests/indexed-types/should_compile/Simple14.stderr
@@ -7,7 +7,7 @@ Simple14.hs:17:12:
                       Maybe m ~ Maybe n => EQ_ z0 z0
       `n' is a rigid type variable bound by
           the type signature for foo :: EQ_ (Maybe m) (Maybe n)
-          at Simple14.hs:17:1
+          at Simple14.hs:16:17
     Expected type: EQ_ z0 z0
       Actual type: EQ_ m n
     In the second argument of `eqE', namely `(eqI :: EQ_ m n)'
diff --git a/tests/indexed-types/should_compile/T3208b.stderr b/tests/indexed-types/should_compile/T3208b.stderr
index f8c8db4bccb07f440ab5be23e4f7afe886385faa..292a91a674bdfa5fd78aebdd95cefc253a33b866 100644
--- a/tests/indexed-types/should_compile/T3208b.stderr
+++ b/tests/indexed-types/should_compile/T3208b.stderr
@@ -4,7 +4,7 @@ T3208b.hs:15:10:
     from the context (OTerm a ~ STerm a, OBJECT a, SUBST a)
       bound by the type signature for
                  fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
-      at T3208b.hs:15:1-22
+      at T3208b.hs:14:9-56
     NB: `STerm' is a type function, and may not be injective
     The type variable `a0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
@@ -18,7 +18,7 @@ T3208b.hs:15:15:
     from the context (OTerm a ~ STerm a, OBJECT a, SUBST a)
       bound by the type signature for
                  fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
-      at T3208b.hs:15:1-22
+      at T3208b.hs:14:9-56
     The type variable `a0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
     In the first argument of `fce', namely `(apply f)'
diff --git a/tests/indexed-types/should_compile/all.T b/tests/indexed-types/should_compile/all.T
index 9e37129f2c2d5109affb2bacd812e1edcd10871a..fd39b363dfabaaf76060f2bd46158d67ceff790d 100644
--- a/tests/indexed-types/should_compile/all.T
+++ b/tests/indexed-types/should_compile/all.T
@@ -21,7 +21,7 @@ test('Simple16', normal, compile, [''])
 test('Simple17', normal, compile, [''])
 test('Simple18', normal, compile, [''])
 test('Simple19', normal, compile, [''])
-test('Simple20', expect_broken(4296), compile, ['-fcontext-stack=50'])
+test('Simple20', expect_broken(4296), compile, ['-fcontext-stack=10'])
 test('Simple21', normal, compile, [''])
 test('Simple22', normal, compile, [''])
 test('Simple23', normal, compile, [''])
diff --git a/tests/indexed-types/should_fail/GADTwrong1.stderr b/tests/indexed-types/should_fail/GADTwrong1.stderr
index 6ec39c3daf01c4f7c9005f51928b6d1c515c96a8..a6010f671199797c642c4d273e8f2697b9c5b391 100644
--- a/tests/indexed-types/should_fail/GADTwrong1.stderr
+++ b/tests/indexed-types/should_fail/GADTwrong1.stderr
@@ -7,7 +7,7 @@ GADTwrong1.hs:12:19:
                in a case alternative
       at GADTwrong1.hs:12:12-14
       `b' is a rigid type variable bound by
-          the type signature for coerce :: a -> b at GADTwrong1.hs:11:1
+          the type signature for coerce :: a -> b at GADTwrong1.hs:10:20
       `a1' is a rigid type variable bound by
            a pattern with constructor
              T :: forall a. a -> T (Const a),
diff --git a/tests/indexed-types/should_fail/NoMatchErr.stderr b/tests/indexed-types/should_fail/NoMatchErr.stderr
index 77d93e87ff01b00ef3d783e98fe56f44027b743e..003c0144707b24b54c72262bd4a3acd0cd151b05 100644
--- a/tests/indexed-types/should_fail/NoMatchErr.stderr
+++ b/tests/indexed-types/should_fail/NoMatchErr.stderr
@@ -3,7 +3,7 @@ NoMatchErr.hs:20:5:
     Could not deduce (Memo d ~ Memo d0)
     from the context (Fun d)
       bound by the type signature for f :: Fun d => Memo d a -> Memo d a
-      at NoMatchErr.hs:20:1-15
+      at NoMatchErr.hs:19:7-37
     NB: `Memo' is a type function, and may not be injective
     The type variable `d0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
diff --git a/tests/indexed-types/should_fail/SimpleFail15.stderr b/tests/indexed-types/should_fail/SimpleFail15.stderr
index 8f97746510f5a636d34a1058d4c1c6a6f0e683c3..e2b7bba314505a2d91416ee2daf6df0a992ced21 100644
--- a/tests/indexed-types/should_fail/SimpleFail15.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail15.stderr
@@ -1,6 +1,6 @@
-
-SimpleFail15.hs:5:1:
-    Illegal polymorphic or qualified type: a ~ b => t
-    Perhaps you intended to use -XRankNTypes or -XRank2Types
-    In the type signature for `foo':
-      foo :: (a, b) -> (a ~ b => t) -> (a, b)
+
+SimpleFail15.hs:5:8:
+    Illegal polymorphic or qualified type: a ~ b => t
+    Perhaps you intended to use -XRankNTypes or -XRank2Types
+    In the type signature for `foo':
+      foo :: (a, b) -> (a ~ b => t) -> (a, b)
diff --git a/tests/indexed-types/should_fail/SimpleFail5a.stderr b/tests/indexed-types/should_fail/SimpleFail5a.stderr
index 861ef5c869013a967705b851bd61a1f0b561b047..b35b3712eee1713cc3dd565f5550599de9e925c7 100644
--- a/tests/indexed-types/should_fail/SimpleFail5a.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail5a.stderr
@@ -3,7 +3,7 @@ SimpleFail5a.hs:31:11:
     Couldn't match type `a' with `Int'
       `a' is a rigid type variable bound by
           the type signature for bar3wrong :: S3 a -> a
-          at SimpleFail5a.hs:31:1
+          at SimpleFail5a.hs:30:17
     Expected type: S3 a
       Actual type: S3 Int
     In the pattern: D3Int
diff --git a/tests/indexed-types/should_fail/SimpleFail6.stderr b/tests/indexed-types/should_fail/SimpleFail6.stderr
index c5c7e8a86a310dc5879e0d85820ee5421b000c52..679aaf872227ce70bc748df65fe47d658fd23f18 100644
--- a/tests/indexed-types/should_fail/SimpleFail6.stderr
+++ b/tests/indexed-types/should_fail/SimpleFail6.stderr
@@ -1,2 +1,5 @@
 
-SimpleFail6.hs:7:11: Illegal repeated type variable `a'
+SimpleFail6.hs:7:11:
+    Conflicting definitions for `a'
+    Bound at: SimpleFail6.hs:7:11
+              SimpleFail6.hs:7:13
diff --git a/tests/indexed-types/should_fail/SkolemOccursLoop.hs b/tests/indexed-types/should_fail/SkolemOccursLoop.hs
index 2d51ea42fc1d3d1cd7e1092c64f5caea5ebc2315..1696a454ddd247f911ba89d6caeb72b2b042a868 100644
--- a/tests/indexed-types/should_fail/SkolemOccursLoop.hs
+++ b/tests/indexed-types/should_fail/SkolemOccursLoop.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -fcontext-stack=10 #-}
+{-# OPTIONS_GHC -fcontext-stack=3 #-}
 {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls #-}
 
 module SkolemOccursLoop where
diff --git a/tests/indexed-types/should_fail/SkolemOccursLoop.stderr b/tests/indexed-types/should_fail/SkolemOccursLoop.stderr
index 0900da8e331624768d53b6200769862313e5cd2a..d1eb0efcb5fb607c61e6deef049db106c037d286 100644
--- a/tests/indexed-types/should_fail/SkolemOccursLoop.stderr
+++ b/tests/indexed-types/should_fail/SkolemOccursLoop.stderr
@@ -1,10 +1 @@
-
-SkolemOccursLoop.hs:18:0:
-    Couldn't match expected type `F a'
-           against inferred type `[T (F (T (F a)))]'
-    When generalising the type(s) for `test1'
-
-SkolemOccursLoop.hs:31:0:
-    Couldn't match expected type `S (G (a, a))'
-           against inferred type `G [S (G (a, a))]'
-    When generalising the type(s) for `test2'
+Skolem occurs loop 
diff --git a/tests/indexed-types/should_fail/T1900.stderr b/tests/indexed-types/should_fail/T1900.stderr
index 2044c6cab86575cf56c2aec75341bb2787a9c3a0..8ea8471d713789793c7bbd738db5b0839caeee82 100644
--- a/tests/indexed-types/should_fail/T1900.stderr
+++ b/tests/indexed-types/should_fail/T1900.stderr
@@ -11,7 +11,7 @@ T1900.hs:14:22:
     Could not deduce (Depend s0 ~ Depend s)
     from the context (Bug s)
       bound by the type signature for check :: Bug s => Depend s -> Bool
-      at T1900.hs:14:1-22
+      at T1900.hs:13:10-36
     NB: `Depend' is a type function, and may not be injective
     The type variable `s0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
diff --git a/tests/indexed-types/should_fail/T3330a.stderr b/tests/indexed-types/should_fail/T3330a.stderr
index d8b5d2606d2fc0843f5ae740ab5add52dedb49fd..9cd0995a058aeb8f4aee0655590092bfd5797e15 100644
--- a/tests/indexed-types/should_fail/T3330a.stderr
+++ b/tests/indexed-types/should_fail/T3330a.stderr
@@ -1,22 +1,22 @@
-
-T3330a.hs:19:34:
-    Couldn't match type `s' with `(->) (s0 ix1 -> ix1)'
-      `s' is a rigid type variable bound by
-          the type signature for children :: s ix -> PF s r ix -> [AnyF s]
-          at T3330a.hs:19:1
-    Expected type: (s0 ix0 -> ix1) -> r ix1 -> Writer [AnyF s] (r ix1)
-      Actual type: s ix
-    In the first argument of `hmapM', namely `p'
-    In the first argument of `execWriter', namely `(hmapM p collect x)'
-    In the expression: execWriter (hmapM p collect x)
-
-T3330a.hs:19:36:
-    Couldn't match type `ix' with `r ix0 -> Writer [AnyF s0] (r ix0)'
-      `ix' is a rigid type variable bound by
-           the type signature for children :: s ix -> PF s r ix -> [AnyF s]
-           at T3330a.hs:19:1
-    Expected type: s0 ix0 -> ix
-      Actual type: s0 ix0 -> r ix0 -> Writer [AnyF s0] (r ix0)
-    In the second argument of `hmapM', namely `collect'
-    In the first argument of `execWriter', namely `(hmapM p collect x)'
-    In the expression: execWriter (hmapM p collect x)
+
+T3330a.hs:19:34:
+    Couldn't match type `s' with `(->) (s0 ix1 -> ix1)'
+      `s' is a rigid type variable bound by
+          the type signature for children :: s ix -> PF s r ix -> [AnyF s]
+          at T3330a.hs:18:13
+    Expected type: (s0 ix0 -> ix1) -> r ix1 -> Writer [AnyF s] (r ix1)
+      Actual type: s ix
+    In the first argument of `hmapM', namely `p'
+    In the first argument of `execWriter', namely `(hmapM p collect x)'
+    In the expression: execWriter (hmapM p collect x)
+
+T3330a.hs:19:36:
+    Couldn't match type `ix' with `r ix0 -> Writer [AnyF s0] (r ix0)'
+      `ix' is a rigid type variable bound by
+           the type signature for children :: s ix -> PF s r ix -> [AnyF s]
+           at T3330a.hs:18:15
+    Expected type: s0 ix0 -> ix
+      Actual type: s0 ix0 -> r ix0 -> Writer [AnyF s0] (r ix0)
+    In the second argument of `hmapM', namely `collect'
+    In the first argument of `execWriter', namely `(hmapM p collect x)'
+    In the expression: execWriter (hmapM p collect x)
diff --git a/tests/indexed-types/should_fail/T3440.stderr b/tests/indexed-types/should_fail/T3440.stderr
index 4e77eef70e138de9e1639b048bcfc860c33c29f6..772d26c1be2ad6743eb7a2aa9ebb218449929007 100644
--- a/tests/indexed-types/should_fail/T3440.stderr
+++ b/tests/indexed-types/should_fail/T3440.stderr
@@ -8,7 +8,7 @@ T3440.hs:11:22:
       at T3440.hs:11:9-16
       `a' is a rigid type variable bound by
           the type signature for unwrap :: GADT (Fam a) -> (a, Fam a)
-          at T3440.hs:11:1
+          at T3440.hs:10:21
       `a1' is a rigid type variable bound by
            a pattern with constructor
              GADT :: forall a. a -> Fam a -> GADT (Fam a),
diff --git a/tests/indexed-types/should_fail/T4093a.stderr b/tests/indexed-types/should_fail/T4093a.stderr
index 0b36936be9f8e7604821d0ecfca11d1d8132c232..bb6d5b915f770105da3e5e4157f94b1dc46bd893 100644
--- a/tests/indexed-types/should_fail/T4093a.stderr
+++ b/tests/indexed-types/should_fail/T4093a.stderr
@@ -3,10 +3,10 @@ T4093a.hs:8:8:
     Could not deduce (e ~ ())
     from the context (Foo e ~ Maybe e)
       bound by the type signature for hang :: Foo e ~ Maybe e => Foo e
-      at T4093a.hs:8:1-14
+      at T4093a.hs:7:9-34
       `e' is a rigid type variable bound by
           the type signature for hang :: Foo e ~ Maybe e => Foo e
-          at T4093a.hs:8:1
+          at T4093a.hs:7:14
     Expected type: Foo e
       Actual type: Maybe ()
     In the return type of a call of `Just'
diff --git a/tests/indexed-types/should_fail/T4093b.stderr b/tests/indexed-types/should_fail/T4093b.stderr
index 6818e006ef8f01d150a7d5ff0d2ed96e712cadce..948ba565df92a6858d9f4cc2bd688e576421f27d 100644
--- a/tests/indexed-types/should_fail/T4093b.stderr
+++ b/tests/indexed-types/should_fail/T4093b.stderr
@@ -7,13 +7,13 @@ T4093b.hs:31:13:
                  blockToNodeList :: (EitherCO e (A C O n) (A O O n) ~ A e O n,
                                      EitherCO x (A C C n) (A C O n) ~ A C x n) =>
                                     Block n e x -> A e x n
-      at T4093b.hs:(25,1)-(34,19)
+      at T4093b.hs:(20,3)-(22,26)
       `e' is a rigid type variable bound by
           the type signature for
             blockToNodeList :: (EitherCO e (A C O n) (A O O n) ~ A e O n,
                                 EitherCO x (A C C n) (A C O n) ~ A C x n) =>
                                Block n e x -> A e x n
-          at T4093b.hs:25:1
+          at T4093b.hs:20:12
     Expected type: EitherCO e (A C O n) (A O O n)
       Actual type: (MaybeC C (n C O), MaybeC O (n O C))
     In the expression: (JustC n, NothingC)
diff --git a/tests/indexed-types/should_fail/T4179.stderr b/tests/indexed-types/should_fail/T4179.stderr
index 021e73e413c1c9590890c9d1a468103a12291020..35209c591f1068cb80770e31c146902f88fc86fe 100644
--- a/tests/indexed-types/should_fail/T4179.stderr
+++ b/tests/indexed-types/should_fail/T4179.stderr
@@ -6,7 +6,7 @@ T4179.hs:26:16:
       bound by the type signature for
                  fCon :: (Functor x, DoC (FCon x)) =>
                          Con x -> A2 (FCon x) -> A3 (FCon x)
-      at T4179.hs:26:1-17
+      at T4179.hs:25:9-72
     NB: `A3' is a type function, and may not be injective
     Expected type: x (A2 (x (Con x)) -> A3 (x (Con x)))
                    -> A2 (x (Con x)) -> A3 (x (Con x))
diff --git a/tests/indexed-types/should_fail/T4272.stderr b/tests/indexed-types/should_fail/T4272.stderr
index 0a6b3be8ffd290b24e70e4486f3ced9f69d66424..24f0cbdff47b9035869cce0fc6a5acab0885419e 100644
--- a/tests/indexed-types/should_fail/T4272.stderr
+++ b/tests/indexed-types/should_fail/T4272.stderr
@@ -27,10 +27,10 @@ T4272.hs:11:19:
     from the context (TermLike a)
       bound by the type signature for
                  laws :: TermLike a => TermFamily a a -> b
-      at T4272.hs:11:1-54
+      at T4272.hs:10:9-53
       `a' is a rigid type variable bound by
           the type signature for laws :: TermLike a => TermFamily a a -> b
-          at T4272.hs:11:1
+          at T4272.hs:10:16
     In the return type of a call of `terms'
     In the second argument of `prune', namely
       `(terms (undefined :: TermFamily a a))'
diff --git a/tests/module/mod45.stderr b/tests/module/mod45.stderr
index 8ead3b58b89c13495cb62b3a8bc018e31fe00241..8aadf22b1011d155b473a80b8589bb89b7b05413 100644
--- a/tests/module/mod45.stderr
+++ b/tests/module/mod45.stderr
@@ -1,6 +1,6 @@
-
-mod45.hs:5:3:
-    Illegal type signature in instance declaration:
-      (==) :: T -> T -> Bool
-    (Use -XInstanceSigs to allow this)
-    In the instance declaration for `Eq T'
+
+mod45.hs:5:11:
+    Illegal type signature in instance declaration:
+      (==) :: T -> T -> Bool
+    (Use -XInstanceSigs to allow this)
+    In the instance declaration for `Eq T'
diff --git a/tests/parser/should_fail/readFail036.stderr b/tests/parser/should_fail/readFail036.stderr
index 8c89f29e3488e20bd2016c77a9eb3e519c772e2c..088f0a9975729d65c72afc7adcfdf854ad1e6097 100644
--- a/tests/parser/should_fail/readFail036.stderr
+++ b/tests/parser/should_fail/readFail036.stderr
@@ -1,4 +1,5 @@
 
-readFail036.hs:4:1:
-    Illegal kind signature for `a'
+readFail036.hs:4:16:
+    Illegal kind signature: `*'
       Perhaps you intended to use -XKindSignatures
+    In the data type declaration for `Foo'
diff --git a/tests/perf/compiler/all.T b/tests/perf/compiler/all.T
index f130f0adfaa15ad0f5fb868002d40216869cad82..ed729ad26d4992c5fb8aa6ff549882b0b59153f2 100644
--- a/tests/perf/compiler/all.T
+++ b/tests/perf/compiler/all.T
@@ -24,7 +24,7 @@ test('T1969',
                              #                 5717704 (x86/Windows 17/05/10)
                              #                 6149572 (x86/Linux, 31/12/09)
       if_wordsize(64,
-          compiler_stats_range_field('max_bytes_used', 11178376, 10)),
+          compiler_stats_range_field('max_bytes_used', 12000000, 10)),
                                    # expected value: 11178376 (amd64/Linux)
       if_wordsize(32,
           compiler_stats_num_field('bytes allocated', 210000000,
diff --git a/tests/polykinds/Freeman.hs b/tests/polykinds/Freeman.hs
new file mode 100644
index 0000000000000000000000000000000000000000..ea8aff0f8a97e2933d4e04d1d858dbf7c5391b77
--- /dev/null
+++ b/tests/polykinds/Freeman.hs
@@ -0,0 +1,259 @@
+-- From the blog post Fun With XPolyKinds : Polykinded Folds
+--   http://www.typesandotherdistractions.com/2012/02/fun-with-xpolykinds-polykinded-folds.html
+
+{-
+In the following, I will write a polykinded version of the combinators
+fold and unfold, along with three examples: folds for regular
+datatypes (specialized to kind *), folds for nested datatypes
+(specialized to kind * -> *), and folds for mutually recursive data
+types (specialized to the product kind (*,*)). The approach should
+generalise easily enough to things such as types indexed by another
+kind (e.g. by specializing to kind Nat -> *, using the XDataKinds
+extension), or higher order nested datatypes (e.g. by specializing to
+kind (* -> *) -> (* -> *)).
+
+The following will compile in the new GHC 7.4.1 release. We require
+the following GHC extensions:
+-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module Main where
+
+{- The basic fold and unfold combinators can be written as follows:
+
+fold phi = phi . fmap (fold phi) . out
+unfold psi = in . fmap (unfold psi) . psi
+
+The idea now is to generalize these combinators by working over
+different categories. We can capture the basic operations in a
+category with a typeclass: -}
+
+class Category hom where
+  ident :: hom a a
+  compose :: hom a b -> hom b c -> hom a c
+
+{- A category has two operations: an identity morphism for every
+object, and for every two compatible morphisms, the composition of
+those morphisms.
+
+In earlier versions of GHC, the type hom would have been specialized
+to kind * -> * -> *, but with the new PolyKinds extension, hom is
+polykinded, and the Category typeclass can be instantiated to k -> k
+-> * for any kind k. This means that in addition to all of the
+Category instances that we could have written before, we can now write
+instances of Category for type constructors, type constructor
+constructors, etc.
+
+Here is the instance for the category Hask of Haskell types. Objects
+are Haskell types and morphisms are functions between types. The
+identity is the regular polymorphic identity function id, and
+composition is given by the (flipped) composition operator (.) -}
+
+instance Category (->) where
+  ident = id
+  compose = flip (.)
+
+{- Another example is the category of type constructors and natural
+transformations. A natural transformation is defined as follows: -}
+
+newtype Nat f g = Nat { nu :: (forall a. f a -> g a) } 
+
+{- Here is the Category instance for natural transformations. This
+time the type hom is inferred to have kind (* -> *) -> (* -> *) ->
+*. Identity and composition are both defined pointwise. -}
+
+instance Category (Nat :: (* -> *) -> (* -> *) -> *) where
+  ident = Nat id
+  compose f g = Nat (nu g . nu f)
+
+{- Let's define a type class which will capture the idea of a fixed point
+in a category. This generalizes the idea of recursive types in Hask: -}
+
+class Rec hom f t where
+  _in :: hom (f t) t
+  out :: hom t (f t)
+
+{- The class Rec defines two morphisms: _in, which is the constructor of
+the fixed point type t, and out, its destructor.
+
+The final piece is the definition of a higher order functor, which
+generalizes the typeclass Functor: -}
+
+class HFunctor hom f where
+  hmap :: hom a b -> hom (f a) (f b)
+
+{- Note the similarity with the type signature of the function fmap ::
+(Functor f) => (a -> b) -> f a -> f b. Indeed, specializing hom to
+(->) in the definition of HFunctor gives back the type signature of
+fmap. 
+
+Finally, we can define folds and unfolds in a category. The
+definitions are as before, but with explicit composition, constructors
+and destructors replaced with the equivalent type class methods, and
+hmap in place of fmap: -}
+
+fold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom (f t) t -> hom rec t
+fold phi = compose out (compose (hmap (fold phi)) phi)
+
+unfold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom t (f t) -> hom t rec
+unfold phi = compose phi (compose (hmap (unfold phi)) _in)
+
+-- Now for some examples.
+
+-- The first example is a regular recursive datatype of binary leaf
+-- trees. The functor FTree is the base functor of this recursive type:
+
+data FTree a b = FLeaf a | FBranch b b
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+-- An instance of Rec shows the relationship between the defining functor
+-- and the recursive type itself:
+
+instance Rec (->) (FTree a) (Tree a) where
+  _in (FLeaf a) = Leaf a
+  _in (FBranch a b) = Branch a b
+  out (Leaf a) = FLeaf a
+  out (Branch a b) = FBranch a b
+
+-- FTree is indeed a functor, so it is also a HFunctor:
+
+instance HFunctor (->) (FTree a) where
+  hmap f (FLeaf a) = FLeaf a
+  hmap f (FBranch a b) = FBranch (f a) (f b)
+
+-- These instances are enough to define folds and unfolds for this
+-- type. The following fold calculates the depth of a tree:
+
+depth :: Tree a -> Int
+depth = (fold :: (FTree a Int -> Int) -> Tree a -> Int) phi where
+  phi :: FTree a Int -> Int
+  phi (FLeaf a) = 1
+  phi (FBranch a b) = 1 + max a b
+
+-- The second example is a fold for the nested (or non-regular)
+-- datatype of complete binary leaf trees. The higher order functor
+-- FCTree defines the type constructor CTree as its fixed point:
+
+data FCTree f a = FCLeaf a | FCBranch (f (a, a))
+  -- FCTree :: (* -> *) -> * -> *
+
+data CTree a = CLeaf a | CBranch (CTree (a, a))
+
+-- Again, we define type class instances for HFunctor and Rec:
+
+instance HFunctor Nat FCTree where
+  hmap (f :: Nat (f :: * -> *) (g :: * -> *)) = Nat ff where
+    ff :: forall a. FCTree f a -> FCTree g a
+    ff (FCLeaf a) = FCLeaf a
+    ff (FCBranch a) = FCBranch (nu f a)
+
+instance Rec Nat FCTree CTree where
+  _in = Nat inComplete where
+    inComplete (FCLeaf a) = CLeaf a
+    inComplete (FCBranch a) = CBranch a
+  out = Nat outComplete where
+    outComplete(CLeaf a) = FCLeaf a
+    outComplete(CBranch a) = FCBranch a
+
+-- Morphisms between type constructors are natural transformations, so we
+-- need a type constructor to act as the target of the fold. For our
+-- purposes, a constant functor will do:
+
+data K a b = K a  -- K :: forall k. * -> k -> *
+
+
+-- And finally, the following fold calculates the depth of a complete binary leaf tree:
+
+cdepth :: CTree a -> Int
+cdepth c = let (K d) = nu (fold (Nat phi)) c in d where
+  phi :: FCTree (K Int) a -> K Int a
+  phi (FCLeaf a) = K 1
+  phi (FCBranch (K n)) = K (n + 1)
+
+{- The final example is a fold for the pair of mutually recursive
+datatype of lists of even and odd lengths. The fold will take a list
+of even length and produce a list of pairs.
+
+We cannot express type constructors in Haskell whose return kind is
+anything other than *, so we cheat a little and emulate the product
+kind using an arrow kind Choice -> *, where Choice is a two point
+kind, lifted using the XDataKinds extension: -}
+
+data Choice = Fst | Snd
+
+-- A morphism of pairs of types is just a pair of morphisms. For
+-- technical reasons, we represent this using a Church-style encoding,
+-- along with helper methods, as follows:
+
+newtype PHom h1 h2 p1 p2 = PHom { runPHom :: forall r. (h1 (p1 Fst) (p2 Fst) -> h2 (p1 Snd) (p2 Snd) -> r) -> r }
+
+mkPHom f g = PHom (\h -> h f g)
+fstPHom p = runPHom p (\f -> \g -> f)
+sndPHom p = runPHom p (\f -> \g -> g)
+
+-- Now, PHom allows us to take two categories and form the product category:
+
+instance (Category h1, Category h2) => Category (PHom h1 h2) where
+  ident = mkPHom ident ident
+  compose p1 p2 = mkPHom (compose (fstPHom p1) (fstPHom p2)) (compose (sndPHom p1) (sndPHom p2))
+
+-- We can define the types of lists of even and odd length as
+-- follows. Note that the kind annotation indicates the appearance of the
+-- kind Choice -> *:
+
+data FAlt :: * -> (Choice -> *) -> Choice -> * where
+  FZero :: FAlt a p Fst
+  FSucc1 :: a -> (p Snd) -> FAlt a p Fst
+  FSucc2 :: a -> (p Fst) -> FAlt a p Snd
+
+data Alt :: * -> Choice -> * where
+  Zero :: Alt a Fst
+  Succ1 :: a -> Alt a Snd -> Alt a Fst
+  Succ2 :: a -> Alt a Fst -> Alt a Snd
+
+deriving instance Show a => Show (Alt a b)
+
+-- Again, we need to define instances of Rec and HFunctor:
+
+instance Rec (PHom (->) (->)) (FAlt a) (Alt a) where
+  _in = mkPHom f g where
+    f FZero = Zero
+    f (FSucc1 a b) = Succ1 a b
+    g (FSucc2 a b) = Succ2 a b
+  out = mkPHom f g where
+    f Zero = FZero
+    f (Succ1 a b) = FSucc1 a b
+    g (Succ2 a b) = FSucc2 a b
+
+instance HFunctor (PHom (->) (->)) (FAlt a) where
+  hmap p = mkPHom hf hg where
+    hf FZero = FZero
+    hf (FSucc1 a x) = FSucc1 a (sndPHom p x)
+    hg (FSucc2 a x) = FSucc2 a (fstPHom p x)
+
+-- As before, we create a target type for our fold, and this time a type synonym as well:
+
+data K2 :: * -> * -> Choice -> * where
+  K21 :: a -> K2 a b Fst
+  K22 :: b -> K2 a b Snd
+
+type PairUpResult a = K2 [(a, a)] (a, [(a, a)])
+
+-- At last, here is the fold pairUp, taking even length lists to lists of pairs:
+
+pairUp :: Alt a Fst -> [(a, a)]
+pairUp xs = let (K21 xss) = (fstPHom (fold (mkPHom phi psi))) xs in xss 
+ where
+   phi FZero = K21 []
+   phi (FSucc1 x1 (K22 (x2, xss))) = K21 ((x1, x2):xss) 
+   psi (FSucc2 x (K21 xss)) = K22 (x, xss) 
+
+main = print (Succ1 (0::Int) $ Succ2 1 $ Succ1 2 $ Succ2 3 $ Succ1 4 $ Succ2 5 Zero)
diff --git a/tests/polykinds/Freeman.stdout b/tests/polykinds/Freeman.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..691a9d3e9b8b7f0a4fe6f16acbc082934d42270a
--- /dev/null
+++ b/tests/polykinds/Freeman.stdout
@@ -0,0 +1 @@
+Succ1 0 (Succ2 1 (Succ1 2 (Succ2 3 (Succ1 4 (Succ2 5 Zero)))))
diff --git a/tests/polykinds/MonoidsFD.hs b/tests/polykinds/MonoidsFD.hs
new file mode 100644
index 0000000000000000000000000000000000000000..8bfb1637c19ed6a19ed9bd667c160970ac49f1b8
--- /dev/null
+++ b/tests/polykinds/MonoidsFD.hs
@@ -0,0 +1,106 @@
+-- From a blog post: http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-with-polymorphic-kinds.html
+
+-------------------- FUNCTIONAL DEPENDENCY VERSION ----------------
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE UnicodeSyntax #-}
+
+module Main where
+import Control.Monad (Monad(..), join)
+import Data.Monoid (Monoid(..))
+
+-- First we define the type class Monoidy:
+
+class Monoidy (~>) comp id m | m (~>) → comp id where
+  munit :: id ~> m
+  mjoin :: m `comp` m ~> m
+
+-- We use functional dependencies to help the typechecker understand that
+-- m and ~> uniquely determine comp (times) and id.
+-- 
+-- This kind of type class would not have been possible in previous
+-- versions of GHC; with the new kind system, however, we can abstract
+-- over kinds!2 Now, let’s create types for the additive and
+-- multiplicative monoids over the natural numbers:
+
+newtype Sum a = Sum a deriving Show
+newtype Product a = Product a deriving Show
+instance Num a ⇒ Monoidy (→) (,) () (Sum a) where
+  munit _ = Sum 0
+  mjoin (Sum x, Sum y) = Sum $ x + y
+instance Num a ⇒ Monoidy (→) (,) () (Product a) where
+  munit _ = Product 1
+  mjoin (Product x, Product y) = Product $ x * y
+
+-- It will be slightly more complicated to make a monadic instance with
+-- Monoidy. First, we need to define the identity functor, a type for
+-- natural transformations, and a type for functor composition:
+
+data Id α = Id { runId :: α } deriving Functor
+
+-- A natural transformation (Λ f g α. (f α) → (g α)) may be encoded in Haskell as follows:
+
+data NT f g = NT { runNT :: ∀ α. f α → g α }
+
+-- Functor composition (Λ f g α. f (g α)) is encoded as follows:
+
+data FC f g α = FC { runFC :: f (g α) }
+
+-- Now, let us define some type T which should be a monad:
+
+data Wrapper a = Wrapper { runWrapper :: a } deriving (Show, Functor)
+instance Monoidy NT FC Id Wrapper where
+  munit = NT $ Wrapper . runId
+  mjoin = NT $ runWrapper . runFC
+
+-- With these defined, we can use them as follows:
+
+test1 = do { print (mjoin (munit (), Sum 2))
+                 -- Sum 2
+           ; print (mjoin (Product 2, Product 3))
+                 -- Product 6
+           ; print (runNT mjoin $ FC $ Wrapper (Wrapper "hello, world"))
+                 -- Wrapper {runWrapper = "hello, world" }
+           }
+
+-- We can even provide a special binary operator for the appropriate monoids as follows:
+
+(<+>) :: Monoidy (→) (,) () m ⇒ m → m → m
+(<+>) = curry mjoin
+
+test2 = print (Sum 1 <+> Sum 2 <+> Sum 4)  -- Sum 7
+
+-- Now, all the extra wrapping that Haskell requires for encoding this is
+-- rather cumbersome in actual use. So, we can give traditional Monad and
+-- Monoid instances for instances of Monoidy:
+
+instance Monoidy (→) (,) () m ⇒ Monoid m where
+  mempty = munit ()
+  mappend = curry mjoin
+
+-- instance (Functor m, Monoidy NT FC Id m) ⇒ Monad m where
+instance Monad Wrapper where
+   return x = runNT munit $ Id x
+   x >>= f = runNT mjoin $ FC (f `fmap` x)
+
+-- And so the following works:
+
+test3
+ = do { print (mappend mempty (Sum 2))  
+             -- Sum 2
+      ; print (mappend (Product 2) (Product 3))
+             -- Product 6
+      ; print (join $ Wrapper $ Wrapper "hello")
+             -- Wrapper {runWrapper = "hello" }
+      ; print (Wrapper "hello, world" >>= return)
+             -- Wrapper {runWrapper = "hello, world" }
+      }
+
+main = test1 >> test2 >> test3
diff --git a/tests/polykinds/MonoidsFD.stdout b/tests/polykinds/MonoidsFD.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..8d96f6d428384af62d13673b1c9a62465fcf4371
--- /dev/null
+++ b/tests/polykinds/MonoidsFD.stdout
@@ -0,0 +1,8 @@
+Sum 2
+Product 6
+Wrapper {runWrapper = "hello, world"}
+Sum 7
+Sum 2
+Product 6
+Wrapper {runWrapper = "hello"}
+Wrapper {runWrapper = "hello, world"}
diff --git a/tests/polykinds/MonoidsTF.hs b/tests/polykinds/MonoidsTF.hs
new file mode 100644
index 0000000000000000000000000000000000000000..f0dc2be5368871d8b31506d92d210d2c5744b1b9
--- /dev/null
+++ b/tests/polykinds/MonoidsTF.hs
@@ -0,0 +1,116 @@
+-- From a blog post: http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-with-polymorphic-kinds.html
+
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Main where
+import Control.Monad (Monad(..), join)
+import Data.Monoid (Monoid(..))
+
+-- First we define the type class Monoidy:
+
+class Monoidy ((~>) :: k0 -> k1 -> *) (m :: k1)  where
+  type MComp (~>) m :: k1 -> k1 -> k0
+  type MId   (~>) m :: k0
+  munit :: MId (~>) m ~> m
+  mjoin :: MComp (~>) m m m ~> m
+
+-- We use functional dependencies to help the typechecker understand that
+-- m and ~> uniquely determine comp (times) and id.
+
+-- This kind of type class would not have been possible in previous
+-- versions of GHC; with the new kind system, however, we can abstract
+-- over kinds!2 Now, let’s create types for the additive and
+-- multiplicative monoids over the natural numbers:
+
+newtype Sum a = Sum a deriving Show
+newtype Product a = Product a deriving Show
+instance Num a ⇒ Monoidy (→) (Sum a) where
+  type MComp (→) (Sum a) = (,)
+  type MId   (→) (Sum a) = ()
+  munit _ = Sum 0
+  mjoin (Sum x, Sum y) = Sum $ x + y
+
+instance Num a ⇒ Monoidy (→) (Product a) where
+  type MComp (→) (Product a) = (,)
+  type MId   (→) (Product a) = ()
+  munit _ = Product 1
+  mjoin (Product x, Product y) = Product $ x * y
+
+-- It will be slightly more complicated to make a monadic instance with
+-- Monoidy. First, we need to define the identity functor, a type for
+-- natural transformations, and a type for functor composition:
+
+data Id α = Id { runId :: α } deriving Functor
+
+-- A natural transformation (Λ f g α. (f α) → (g α)) may be encoded in Haskell as follows:
+
+data NT f g = NT { runNT :: ∀ α. f α → g α }
+
+-- Functor composition (Λ f g α. f (g α)) is encoded as follows:
+
+data FC f g α = FC { runFC :: f (g α) }
+
+-- Now, let us define some type T which should be a monad:
+
+data Wrapper a = Wrapper { runWrapper :: a } deriving (Show, Functor)
+instance Monoidy NT Wrapper where
+  type MComp NT Wrapper = FC
+  type MId   NT Wrapper = Id
+  munit = NT $ Wrapper . runId
+  mjoin = NT $ runWrapper . runFC
+
+
+-- With these defined, we can use them as follows:
+
+test1 = do { print (mjoin (munit (), Sum 2))
+                 -- Sum 2
+           ; print (mjoin (Product 2, Product 3))
+                 -- Product 6
+           ; print (runNT mjoin $ FC $ Wrapper (Wrapper "hello, world"))
+                 -- Wrapper {runWrapper = "hello, world" }
+           }
+
+-- We can even provide a special binary operator for the appropriate monoids as follows:
+
+(<+>) :: (Monoidy (→) m, MId (→) m ~ (), MComp (→) m ~ (,)) 
+       ⇒ m → m → m
+(<+>) = curry mjoin
+
+test2 = print (Sum 1 <+> Sum 2 <+> Sum 4)  -- Sum 7
+
+-- Now, all the extra wrapping that Haskell requires for encoding this is
+-- rather cumbersome in actual use. So, we can give traditional Monad and
+-- Monoid instances for instances of Monoidy:
+
+instance (MId (→) m ~ (), MComp (→) m ~ (,), Monoidy (→) m) 
+       ⇒ Monoid m where
+  mempty = munit ()
+  mappend = curry mjoin
+
+instance Monad Wrapper where
+  return x = runNT munit $ Id x
+  x >>= f = runNT mjoin $ FC (f `fmap` x)
+
+-- And so the following works:
+
+test3
+ = do { print (mappend mempty (Sum 2))  
+             -- Sum 2
+      ; print (mappend (Product 2) (Product 3))
+             -- Product 6
+      ; print (join $ Wrapper $ Wrapper "hello")
+             -- Wrapper {runWrapper = "hello" }
+      ; print (Wrapper "hello, world" >>= return)
+             -- Wrapper {runWrapper = "hello, world" }
+      }
+
+main = test1 >> test2 >> test3
diff --git a/tests/polykinds/MonoidsTF.stdout b/tests/polykinds/MonoidsTF.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..8d96f6d428384af62d13673b1c9a62465fcf4371
--- /dev/null
+++ b/tests/polykinds/MonoidsTF.stdout
@@ -0,0 +1,8 @@
+Sum 2
+Product 6
+Wrapper {runWrapper = "hello, world"}
+Sum 7
+Sum 2
+Product 6
+Wrapper {runWrapper = "hello"}
+Wrapper {runWrapper = "hello, world"}
diff --git a/tests/polykinds/PolyKinds06.stderr b/tests/polykinds/PolyKinds06.stderr
index 151e636cb17a48be0da5669431327bed4dc02902..b2de4bc5968f78c99450aa11cd60b5646950a828 100644
--- a/tests/polykinds/PolyKinds06.stderr
+++ b/tests/polykinds/PolyKinds06.stderr
@@ -1,4 +1,6 @@
 
-PolyKinds06.hs:9:11:
-    Promoted kind `A' used in a mutually recursive group
-    In the kind `A -> *'
+PolyKinds06.hs:10:11:
+    Promoted kind `A1' used in a mutually recursive group
+    In the type `B A1'
+    In the definition of data constructor `B1'
+    In the data type declaration for `B'
diff --git a/tests/polykinds/PolyKinds07.stderr b/tests/polykinds/PolyKinds07.stderr
index 77fd295fa316c0813fc01c0eae4233961d1145ba..2063af06454beeaa0709dbd983b47dab52dd00bb 100644
--- a/tests/polykinds/PolyKinds07.stderr
+++ b/tests/polykinds/PolyKinds07.stderr
@@ -1,6 +1,6 @@
 
 PolyKinds07.hs:10:11:
-    Opaque thing `A1' used as a type
+    Promoted kind `A1' used in a mutually recursive group
     In the type `B A1'
     In the definition of data constructor `B1'
     In the data type declaration for `B'
diff --git a/tests/polykinds/PolyKinds12.hs b/tests/polykinds/PolyKinds12.hs
index 4d18551cb95255d7d871dacaf3e9d6a855568f4a..4c1cc4df5ce87af64160e7e0987d3cbfe1f37ac4 100644
--- a/tests/polykinds/PolyKinds12.hs
+++ b/tests/polykinds/PolyKinds12.hs
@@ -2,14 +2,10 @@
 
 module PolyKinds12 where
 
-type family If1 b t f
+type family If1 (b::Bool) (t::k) (f::k) :: k
 type instance If1 True t f = t
 type instance If1 False t f = f
 
-type family If2 (b :: Bool) t f
-type instance If2 True t f = t
-type instance If2 False t f = f
-
 data SBool b where
   STrue :: SBool True
   SFalse :: SBool False
@@ -18,15 +14,13 @@ test1 :: SBool b -> If1 b Int Char
 test1 STrue = 42
 test1 SFalse = 'H'
 
-test2 :: SBool b -> If2 b Int Char
+test2 :: SBool b -> If1 b Int Char
 test2 STrue = 42
 test2 SFalse = 'H'
 
 type family Apply f x
 type instance Apply f x = f x
 
--- Does not work because we do not abstract the return kind of type families
--- Currently If1 returns kind *, which is too restrictive
 higher1v1 :: SBool b -> (If1 b Maybe []) Char
 higher1v1 STrue = Just 'H'
 higher1v1 SFalse = "Hello"
@@ -35,6 +29,6 @@ higher1v2 :: SBool b -> Apply (If1 b Maybe []) Char
 higher1v2 STrue = Just 'H'
 higher1v2 SFalse = "Hello"
 
--- higher2 :: SBool b -> (If2 b Maybe []) Int
--- higher2 STrue = Just 42
--- higher2 SFalse = "Hello"
+higher2 :: SBool b -> If1 b Maybe [] Int
+higher2 STrue  = Just 42
+higher2 SFalse = [45]
diff --git a/tests/polykinds/PolyKinds13.hs b/tests/polykinds/PolyKinds13.hs
index 315c62a998fdb598b1a7a1931d9176c7887cb0ba..a7546833241fc9e8c3e5bf3b75a620c50fe39a23 100644
--- a/tests/polykinds/PolyKinds13.hs
+++ b/tests/polykinds/PolyKinds13.hs
@@ -16,11 +16,14 @@ instance Functor Proxy where
 data TypeRep = TypeRep
 
 class MyTypeable t where
+-- MyTypeable :: forall k. k -> Constraint
   myTypeOf :: Proxy t -> TypeRep
   myTypeOf _ = TypeRep
 
 data Apply f t = Apply (f t)
+-- Apply :: forall k.  (k -> *) -> k -> * 
 
 instance MyTypeable Apply
+-- df :: forall k. MyTypeable ((k -> *) -> k -> *) (Apply k)
 instance MyTypeable Int
 instance MyTypeable Maybe
diff --git a/tests/polykinds/T5770.hs b/tests/polykinds/T5770.hs
new file mode 100644
index 0000000000000000000000000000000000000000..d6cf604886db67983710fb60c1d5b84f318fbb55
--- /dev/null
+++ b/tests/polykinds/T5770.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE TypeFamilies,
+             PolyKinds,
+             ScopedTypeVariables
+ #-}
+
+module T5770 where
+import GHC.Base
+
+convert :: a -> b
+convert = convert
+
+type family Foo a 
+type instance Foo Int = Bool
+
+barT5770 :: forall a b c dummya. (b -> c) -> ((Foo a) -> c)
+barT5770 f = (convert f :: (Foo a) -> c)
+
+barT5769 :: forall b a. b -> (Foo a)
+barT5769 f = (convert f :: (Foo a))
+
+barT5768 :: forall b a. b -> (Foo a)
+barT5768 f = (convert f :: (Foo a))
diff --git a/tests/polykinds/T5771.hs b/tests/polykinds/T5771.hs
new file mode 100644
index 0000000000000000000000000000000000000000..00d760439a1c02b4ed429009577384f1cf240d34
--- /dev/null
+++ b/tests/polykinds/T5771.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module T5771 where
+
+class IndexedMonad m where
+  unit :: a -> m i i a
+  bind :: m i j a -> (a -> m j k b) -> m i k b
+
+newtype IndexedIO i j a = IndexedIO {runIndexedIO :: IO a}
+
+-- i and j are both *; instance is accepted
+instance IndexedMonad IndexedIO where
+  unit = IndexedIO . return
+  bind m k = IndexedIO $ runIndexedIO m >>= runIndexedIO . k
+infixl 1 `bind`
+
+data HList xs where
+  N    :: HList '[]
+  (:>) :: a -> HList as -> HList (a ': as)
+infixr 5 :>
+
+newtype HLState xs ys a = HLState {runHLState :: HList xs -> (a, HList ys)}
+
+-- i and j are now [*]; rejected with the MPTCs message
+instance IndexedMonad HLState where
+  unit x = HLState $ \s -> (x, s)
+  bind (HLState f) k = HLState $ \xs ->
+    case f xs of (a, ys) -> runHLState (k a) ys
diff --git a/tests/polykinds/all.T b/tests/polykinds/all.T
index 7cb6d89add374110c8b7738f8d31ad3001476307..a5bdebe5f5ae8555e1b5a10d1a6d8e3e622f0a2c 100644
--- a/tests/polykinds/all.T
+++ b/tests/polykinds/all.T
@@ -15,6 +15,13 @@ test('PolyKinds04', normal, compile_fail, [''])
 test('PolyKinds06', normal, compile_fail, [''])
 test('PolyKinds07', normal, compile_fail, [''])
 
-test('PolyKinds12', expect_fail, compile, [''])
+test('PolyKinds12', normal, compile, [''])
 
 test('T5798', normal, compile, [''])
+test('T5770', normal, compile, [''])
+test('T5771', normal, compile, [''])
+
+test('Freeman', normal, compile_and_run, [''])
+test('MonoidsTF', normal, compile_and_run, [''])
+test('MonoidsFD', normal, compile_and_run, [''])
+
diff --git a/tests/simplCore/should_compile/rule2.stderr b/tests/simplCore/should_compile/rule2.stderr
index f41296a15fcd6702bdc0fda6d857f29aba7559b6..8279fce14f6a406f001d938acd8e8e5e6f372029 100644
--- a/tests/simplCore/should_compile/rule2.stderr
+++ b/tests/simplCore/should_compile/rule2.stderr
@@ -21,10 +21,10 @@ Total ticks:     11
   1 f
   1 m
   1 a
-  1 m
-  1 a
   1 b
   1 m
+  1 m
+  1 a
 8 SimplifierDone 8
 
 
diff --git a/tests/th/T3177a.stderr b/tests/th/T3177a.stderr
index 00b0c0d92cc5d4ae3250d4ff03a739f7894292fa..806a1f92a7dff6c349dee018d66e4e96970850aa 100644
--- a/tests/th/T3177a.stderr
+++ b/tests/th/T3177a.stderr
@@ -7,5 +7,4 @@ T3177a.hs:8:15:
 
 T3177a.hs:11:6:
     `Int' is applied to too many type arguments
-    In the type signature for `g':
-      g :: Int Int
+    In the type signature for `g': g :: Int Int
diff --git a/tests/typecheck/prog001/typecheck.prog001.stderr-ghc b/tests/typecheck/prog001/typecheck.prog001.stderr-ghc
index 04d55b4447533c8f242e29f84a0a21c26cc1b5fc..17d8e2cf849ff98a587198848f45ca27714c52b0 100644
--- a/tests/typecheck/prog001/typecheck.prog001.stderr-ghc
+++ b/tests/typecheck/prog001/typecheck.prog001.stderr-ghc
@@ -1,4 +1,5 @@
-
-B.hs:7:10:
-    Warning: No explicit method or default declaration for `row'
-    In the instance declaration for `Matrix Bool Val'
+
+B.hs:7:10:
+    Warning: No explicit method or default declaration for `row'
+    In the instance declaration for `Matrix Bool Val'
+
diff --git a/tests/typecheck/should_compile/FD1.stderr b/tests/typecheck/should_compile/FD1.stderr
index 6f98877b84a90b94d5a1dfc666a7dd3018ffb12a..0bec66931ad9eef411fb513e5193628c400c0aee 100644
--- a/tests/typecheck/should_compile/FD1.stderr
+++ b/tests/typecheck/should_compile/FD1.stderr
@@ -4,9 +4,9 @@ FD1.hs:16:1:
     from the context (E a (Int -> Int))
       bound by the type signature for
                  plus :: E a (Int -> Int) => Int -> a
-      at FD1.hs:16:1-16
+      at FD1.hs:15:9-38
       `a' is a rigid type variable bound by
           the type signature for plus :: E a (Int -> Int) => Int -> a
-          at FD1.hs:16:1
+          at FD1.hs:15:12
     The equation(s) for `plus' have two arguments,
     but its type `Int -> a' has only one
diff --git a/tests/typecheck/should_compile/FD2.stderr b/tests/typecheck/should_compile/FD2.stderr
index 2b2fee3eb9c679aad03d753f6fedc7cd2eb6f1df..392f92723dd19161fe73838e216616534bd34ab9 100644
--- a/tests/typecheck/should_compile/FD2.stderr
+++ b/tests/typecheck/should_compile/FD2.stderr
@@ -7,19 +7,19 @@ FD2.hs:26:36:
     or from (Elem a e)
       bound by the type signature for
                  foldr1 :: Elem a e => (e -> e -> e) -> a -> e
-      at FD2.hs:(22,3)-(26,39)
+      at FD2.hs:21:13-47
     or from (Elem a e1)
       bound by the type signature for
                  mf :: Elem a e1 => e1 -> Maybe e1 -> Maybe e1
-      at FD2.hs:(25,12)-(26,39)
+      at FD2.hs:24:18-54
       `e' is a rigid type variable bound by
           the type signature for
             foldr1 :: Elem a e => (e -> e -> e) -> a -> e
-          at FD2.hs:22:3
+          at FD2.hs:21:20
       `e1' is a rigid type variable bound by
            the type signature for
              mf :: Elem a e1 => e1 -> Maybe e1 -> Maybe e1
-           at FD2.hs:25:12
+           at FD2.hs:24:25
     In the first argument of `f', namely `x'
     In the first argument of `Just', namely `(f x y)'
     In the expression: Just (f x y)
diff --git a/tests/typecheck/should_compile/FD3.stderr b/tests/typecheck/should_compile/FD3.stderr
index 6f6aa8a1a2a9236760583cd9feb6ad3ec1bf89bf..9144b5fdb368d6e3ec15cb926733c7e6663e6865 100644
--- a/tests/typecheck/should_compile/FD3.stderr
+++ b/tests/typecheck/should_compile/FD3.stderr
@@ -3,7 +3,7 @@ FD3.hs:15:15:
     Couldn't match type `a' with `([Char], a)'
       `a' is a rigid type variable bound by
           the type signature for translate :: (String, a) -> A a
-          at FD3.hs:15:1
+          at FD3.hs:14:23
     When using functional dependencies to combine
       MkA a a,
         arising from the dependency `a -> b'
diff --git a/tests/typecheck/should_compile/tc141.stderr b/tests/typecheck/should_compile/tc141.stderr
index 2fdf1fa99c336ce21fce2edcadca9c5b7f6a3086..0d083033458b24d8fe5e022995bab35520e0a252 100644
--- a/tests/typecheck/should_compile/tc141.stderr
+++ b/tests/typecheck/should_compile/tc141.stderr
@@ -1,6 +1,43 @@
 
-tc141.hs:11:15: Not in scope: type variable `a'
+tc141.hs:11:12:
+    You cannot bind scoped type variable `a'
+      in a pattern binding signature
+    In the pattern: p :: a
+    In the pattern: (p :: a, q :: a)
+    In a pattern binding: (p :: a, q :: a) = x
 
-tc141.hs:11:20: Not in scope: type variable `a'
+tc141.hs:11:31:
+    Couldn't match expected type `a1' with actual type `a'
+      `a1' is a rigid type variable bound by
+           an expression type signature: a1 at tc141.hs:11:31
+      `a' is a rigid type variable bound by
+          the inferred type of f :: (a, a) -> (t, a) at tc141.hs:11:1
+    In the expression: q :: a
+    In the expression: (q :: a, p)
+    In the expression: let (p :: a, q :: a) = x in (q :: a, p)
 
-tc141.hs:13:16: Not in scope: type variable `a'
+tc141.hs:13:13:
+    You cannot bind scoped type variable `a'
+      in a pattern binding signature
+    In the pattern: y :: a
+    In a pattern binding: y :: a = a
+    In the expression:
+      let y :: a = a in
+      let
+        v :: a
+        v = b
+      in v
+
+tc141.hs:15:18:
+    Couldn't match expected type `a1' with actual type `t1'
+      `a1' is a rigid type variable bound by
+           the type signature for v :: a1 at tc141.hs:14:19
+      `t1' is a rigid type variable bound by
+           the inferred type of g :: t -> t1 -> a at tc141.hs:13:1
+    In the expression: b
+    In an equation for `v': v = b
+    In the expression:
+      let
+        v :: a
+        v = b
+      in v
diff --git a/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr b/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr
index 229b14a15b2aba3394c944a1255024d4012b6557..24b2149bf5bb68b6ee4596d76ee695aae9f5eb24 100644
--- a/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr
+++ b/tests/typecheck/should_fail/FailDueToGivenOverlapping.stderr
@@ -7,7 +7,7 @@ FailDueToGivenOverlapping.hs:27:9:
     Matching givens (or their superclasses):
       (E [Int])
         bound by the type signature for bar :: E [Int] => () -> ()
-        at FailDueToGivenOverlapping.hs:27:1-23
+        at FailDueToGivenOverlapping.hs:26:8-26
     (The choice depends on the instantiation of `t0')
     In the expression: eop [undefined]
     In an equation for `bar': bar _ = eop [undefined]
diff --git a/tests/typecheck/should_fail/FrozenErrorTests.stderr b/tests/typecheck/should_fail/FrozenErrorTests.stderr
index f5a49c89d0da265a3105faf982468228b9871871..f6df41763fb16081d13acd1601fd1f7bc52fb848 100644
--- a/tests/typecheck/should_fail/FrozenErrorTests.stderr
+++ b/tests/typecheck/should_fail/FrozenErrorTests.stderr
@@ -1,9 +1,9 @@
 
-FrozenErrorTests.hs:11:1:
+FrozenErrorTests.hs:10:8:
     Couldn't match type `a' with `T a'
       `a' is a rigid type variable bound by
           the type signature for foo :: a ~ T a => a -> a
-          at FrozenErrorTests.hs:11:1
+          at FrozenErrorTests.hs:10:15
     Inaccessible code in
       the type signature for foo :: a ~ T a => a -> a
 
diff --git a/tests/typecheck/should_fail/IPFail.stderr b/tests/typecheck/should_fail/IPFail.stderr
index 7d0d8980af044794a90ef97926cce839e1be331d..dbb25d553ff4b0f9ffbb328e63e65ad4ea4d8c92 100644
--- a/tests/typecheck/should_fail/IPFail.stderr
+++ b/tests/typecheck/should_fail/IPFail.stderr
@@ -3,7 +3,7 @@ IPFail.hs:6:18:
     Could not deduce (Num Bool) arising from the literal `5'
     from the context (?x::Int)
       bound by the type signature for f0 :: (?x::Int) => () -> Bool
-      at IPFail.hs:6:1-24
+      at IPFail.hs:5:7-31
     Possible fix:
       add (Num Bool) to the context of
         the type signature for f0 :: (?x::Int) => () -> Bool
diff --git a/tests/typecheck/should_fail/T1899.stderr b/tests/typecheck/should_fail/T1899.stderr
index 5779301745cba8939157a130db4ff50878985ab0..5a37c8949a5e2d96e4c7882f3b2569c6f17879de 100644
--- a/tests/typecheck/should_fail/T1899.stderr
+++ b/tests/typecheck/should_fail/T1899.stderr
@@ -3,7 +3,7 @@ T1899.hs:14:36:
     Couldn't match type `a' with `Proposition a0'
       `a' is a rigid type variable bound by
           the type signature for transRHS :: [a] -> Int -> Constraint a
-          at T1899.hs:10:2
+          at T1899.hs:9:15
     Expected type: [Proposition a0]
       Actual type: [a]
     In the first argument of `Auxiliary', namely `varSet'
diff --git a/tests/typecheck/should_fail/T2538.stderr b/tests/typecheck/should_fail/T2538.stderr
index e4e9a7551af002af4378578ed8f4de643d114466..b2d1d3aeb6fc04f99c7e09eb555f47856187bc62 100644
--- a/tests/typecheck/should_fail/T2538.stderr
+++ b/tests/typecheck/should_fail/T2538.stderr
@@ -1,14 +1,14 @@
-
-T2538.hs:6:1:
-    Illegal polymorphic or qualified type: Eq a => a -> a
-    Perhaps you intended to use -XRankNTypes or -XRank2Types
-    In the type signature for `f': f :: (Eq a => a -> a) -> Int
-
-T2538.hs:9:1:
-    Illegal polymorphic or qualified type: Eq a => a -> a
-    Perhaps you intended to use -XImpredicativeTypes
-    In the type signature for `g': g :: [Eq a => a -> a] -> Int
-
-T2538.hs:12:1:
-    Illegal polymorphic or qualified type: Eq a => a -> a
-    In the type signature for `h': h :: Ix (Eq a => a -> a) => Int
+
+T2538.hs:6:6:
+    Illegal polymorphic or qualified type: Eq a => a -> a
+    Perhaps you intended to use -XRankNTypes or -XRank2Types
+    In the type signature for `f': f :: (Eq a => a -> a) -> Int
+
+T2538.hs:9:6:
+    Illegal polymorphic or qualified type: Eq a => a -> a
+    Perhaps you intended to use -XImpredicativeTypes
+    In the type signature for `g': g :: [Eq a => a -> a] -> Int
+
+T2538.hs:12:6:
+    Illegal polymorphic or qualified type: Eq a => a -> a
+    In the type signature for `h': h :: Ix (Eq a => a -> a) => Int
diff --git a/tests/typecheck/should_fail/T2714.stderr b/tests/typecheck/should_fail/T2714.stderr
index 18e36fa80009ead6aacfb962e5b864957d7113a0..e7f3b4aa92bc120e4a31ebb741d3e1d47f745ca2 100644
--- a/tests/typecheck/should_fail/T2714.stderr
+++ b/tests/typecheck/should_fail/T2714.stderr
@@ -3,7 +3,7 @@ T2714.hs:8:5:
     Couldn't match type `a' with `f0 b'
       `a' is a rigid type variable bound by
           the type signature for f :: ((a -> b) -> b) -> forall c. c -> a
-          at T2714.hs:8:1
+          at T2714.hs:7:8
     Expected type: ((a -> b) -> b) -> c -> a
       Actual type: ((a -> b) -> b) -> f0 (a -> b) -> f0 b
     In the expression: ffmap
diff --git a/tests/typecheck/should_fail/T5300.stderr b/tests/typecheck/should_fail/T5300.stderr
index a051692bc528489f84d36050c34dde6d74939dc1..272f8b5762dfc80332598bfdedb81ab53ad8ed12 100644
--- a/tests/typecheck/should_fail/T5300.stderr
+++ b/tests/typecheck/should_fail/T5300.stderr
@@ -5,7 +5,7 @@ T5300.hs:15:9:
       bound by the type signature for
                  f2 :: (Monad m, C1 a1 b1 c1, C2 a2 b2 c2) =>
                        a1 -> StateT (T b2) m a2
-      at T5300.hs:15:1-36
+      at T5300.hs:14:7-69
     The type variable `c0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
     In the first argument of `(>>=)', namely `f1 fm'
diff --git a/tests/typecheck/should_fail/tcfail034.stderr b/tests/typecheck/should_fail/tcfail034.stderr
index db8e148eb94c2b4f3a1e3737fd2f3f9449bc34af..38b04c10c6c035ceec84a0f70931b382c8ca5236 100644
--- a/tests/typecheck/should_fail/tcfail034.stderr
+++ b/tests/typecheck/should_fail/tcfail034.stderr
@@ -3,7 +3,7 @@ tcfail034.hs:17:13:
     Could not deduce (Integral a) arising from a use of `mod'
     from the context (Num a, Eq a)
       bound by the type signature for test :: (Num a, Eq a) => a -> Bool
-      at tcfail034.hs:17:1-25
+      at tcfail034.hs:16:7-32
     Possible fix:
       add (Integral a) to the context of
         the type signature for test :: (Num a, Eq a) => a -> Bool
diff --git a/tests/typecheck/should_fail/tcfail067.stderr b/tests/typecheck/should_fail/tcfail067.stderr
index 513f5e997727c7a3d4383cdc2042601be8f97171..6be6ef494b7674804ee82e9614c0696ccbf6a6ca 100644
--- a/tests/typecheck/should_fail/tcfail067.stderr
+++ b/tests/typecheck/should_fail/tcfail067.stderr
@@ -1,6 +1,6 @@
 
-tcfail067.hs:1:14:
-    Warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
+tcfail067.hs:1:14: Warning:
+    -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
 
 tcfail067.hs:12:16:
     No instance for (Ord a)
@@ -20,7 +20,7 @@ tcfail067.hs:46:12:
     from the context (Show a)
       bound by the type signature for
                  showRange :: Show a => SubRange a -> String
-      at tcfail067.hs:(46,1)-(47,58)
+      at tcfail067.hs:45:14-43
     Possible fix:
       add (Ord a) to the context of
         the type signature for showRange :: Show a => SubRange a -> String
@@ -59,7 +59,7 @@ tcfail067.hs:74:5:
       bound by the type signature for
                  numSubRangeBinOp :: Num a =>
                                      (a -> a -> a) -> SubRange a -> SubRange a -> SubRange a
-      at tcfail067.hs:(73,1)-(76,53)
+      at tcfail067.hs:(71,21)-(72,58)
     Possible fix:
       add (Ord a) to the context of
         the type signature for
diff --git a/tests/typecheck/should_fail/tcfail068.stderr b/tests/typecheck/should_fail/tcfail068.stderr
index 11d39617dbd0bc9cc2c5941f2b867307bff3efc9..4b9c8064a7cc0a8e340d3751eacd64e280c6a3dd 100644
--- a/tests/typecheck/should_fail/tcfail068.stderr
+++ b/tests/typecheck/should_fail/tcfail068.stderr
@@ -4,14 +4,14 @@ tcfail068.hs:14:9:
     from the context (Constructed a)
       bound by the type signature for
                  itgen :: Constructed a => (Int, Int) -> a -> IndTree s a
-      at tcfail068.hs:(12,1)-(14,31)
+      at tcfail068.hs:11:10-55
       `s1' is a rigid type variable bound by
            a type expected by the context: GHC.ST.ST s1 (IndTree s a)
            at tcfail068.hs:13:9
       `s' is a rigid type variable bound by
           the type signature for
             itgen :: Constructed a => (Int, Int) -> a -> IndTree s a
-          at tcfail068.hs:12:1
+          at tcfail068.hs:11:53
     Expected type: GHC.ST.ST s1 (IndTree s a)
       Actual type: GHC.ST.ST s1 (STArray s1 (Int, Int) a)
     In the return type of a call of `newSTArray'
@@ -25,12 +25,12 @@ tcfail068.hs:19:21:
       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)
+      at tcfail068.hs:16:10-75
       `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
+          at tcfail068.hs:16:58
       `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
@@ -48,12 +48,12 @@ tcfail068.hs:24:35:
       bound by the type signature for
                  itrap :: Constructed a =>
                           ((Int, Int), (Int, Int)) -> (a -> a) -> IndTree s a -> IndTree s a
-      at tcfail068.hs:(24,1)-(32,41)
+      at tcfail068.hs:23:10-87
       `s' is a rigid type variable bound by
           the type signature for
             itrap :: Constructed a =>
                      ((Int, Int), (Int, Int)) -> (a -> a) -> IndTree s a -> IndTree s a
-          at tcfail068.hs:24:1
+          at tcfail068.hs:23:70
       `s1' is a rigid type variable bound by
            a type expected by the context: GHC.ST.ST s1 (IndTree s a)
            at tcfail068.hs:24:29
@@ -75,7 +75,7 @@ tcfail068.hs:36:46:
                                -> c
                                -> IndTree s b
                                -> (c, IndTree s b)
-      at tcfail068.hs:(36,1)-(45,66)
+      at tcfail068.hs:(34,15)-(35,62)
       `s' is a rigid type variable bound by
           the type signature for
             itrapstate :: Constructed b =>
@@ -86,7 +86,7 @@ tcfail068.hs:36:46:
                           -> c
                           -> IndTree s b
                           -> (c, IndTree s b)
-          at tcfail068.hs:36:1
+          at tcfail068.hs:35:40
       `s1' is a rigid type variable bound by
            a type expected by the context: GHC.ST.ST s1 (c, IndTree s b)
            at tcfail068.hs:36:40
diff --git a/tests/typecheck/should_fail/tcfail072.stderr b/tests/typecheck/should_fail/tcfail072.stderr
index 4d6bd867b20cdbfe415de6613af99fa5d429275a..052083f237ed191c946201adb1b6cda136fa5ffb 100644
--- a/tests/typecheck/should_fail/tcfail072.stderr
+++ b/tests/typecheck/should_fail/tcfail072.stderr
@@ -4,7 +4,7 @@ tcfail072.hs:23:13:
     from the context (Ord p, Ord q)
       bound by the type signature for
                  g :: (Ord p, Ord q) => AB p q -> Bool
-      at tcfail072.hs:23:1-15
+      at tcfail072.hs:22:6-38
     The type variables `p0', `q0' are ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
     In the expression: g A
diff --git a/tests/typecheck/should_fail/tcfail097.stderr b/tests/typecheck/should_fail/tcfail097.stderr
index 967b172bb9b7c065ebbf556bd73fd1e22d12f50c..2fabae4b4080be22cc4f96a8f206543ecdb8c028 100644
--- a/tests/typecheck/should_fail/tcfail097.stderr
+++ b/tests/typecheck/should_fail/tcfail097.stderr
@@ -1,6 +1,6 @@
-
-tcfail097.hs:5:1:
-    Ambiguous constraint `Eq a'
-        At least one of the forall'd type variables mentioned by the constraint
-        must be reachable from the type after the '=>'
-    In the type signature for `f': f :: Eq a => Int -> Int
+
+tcfail097.hs:5:6:
+    Ambiguous constraint `Eq a'
+      At least one of the forall'd type variables mentioned by the constraint
+      must be reachable from the type after the '=>'
+    In the type signature for `f': f :: Eq a => Int -> Int
diff --git a/tests/typecheck/should_fail/tcfail101.stderr b/tests/typecheck/should_fail/tcfail101.stderr
index 0d82b50750db63ca05ad6f78e2cb4f37a298594f..5cca6de0a3fcc19c64bee369926260a8afde3c4c 100644
--- a/tests/typecheck/should_fail/tcfail101.stderr
+++ b/tests/typecheck/should_fail/tcfail101.stderr
@@ -1,4 +1,4 @@
 
-tcfail101.hs:9:1:
+tcfail101.hs:9:6:
     Type synonym `A' should have 1 argument, but has been given none
     In the type signature for `f': f :: T A
diff --git a/tests/typecheck/should_fail/tcfail102.stderr b/tests/typecheck/should_fail/tcfail102.stderr
index 792c941081865bbeaf4c6c1c759490afb6290b7a..541bb432fa6de6ab38c57239433eadc147077e75 100644
--- a/tests/typecheck/should_fail/tcfail102.stderr
+++ b/tests/typecheck/should_fail/tcfail102.stderr
@@ -1,18 +1,18 @@
-
-tcfail102.hs:1:14:
-    Warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
-
-tcfail102.hs:9:15:
-    Could not deduce (Integral (Ratio a)) arising from a use of `p'
-    from the context (Integral a)
-      bound by the type signature for
-                 f :: Integral a => P (Ratio a) -> P (Ratio a)
-      at tcfail102.hs:9:1-19
-    Possible fix:
-      add (Integral (Ratio a)) to the context of
-        the type signature for
-          f :: Integral a => P (Ratio a) -> P (Ratio a)
-      or add an instance declaration for (Integral (Ratio a))
-    In the `p' field of a record
-    In the expression: x {p = p x}
-    In an equation for `f': f x = x {p = p x}
+
+tcfail102.hs:1:14: Warning:
+    -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
+
+tcfail102.hs:9:15:
+    Could not deduce (Integral (Ratio a)) arising from a use of `p'
+    from the context (Integral a)
+      bound by the type signature for
+                 f :: Integral a => P (Ratio a) -> P (Ratio a)
+      at tcfail102.hs:8:6-45
+    Possible fix:
+      add (Integral (Ratio a)) to the context of
+        the type signature for
+          f :: Integral a => P (Ratio a) -> P (Ratio a)
+      or add an instance declaration for (Integral (Ratio a))
+    In the `p' field of a record
+    In the expression: x {p = p x}
+    In an equation for `f': f x = x {p = p x}
diff --git a/tests/typecheck/should_fail/tcfail103.stderr b/tests/typecheck/should_fail/tcfail103.stderr
index 7d6e4dfd6cd4eb61faf7cf5d9f60eacb8cf5aff7..5a9b1839f6faba0ee544291b5f7ba9367984c193 100644
--- a/tests/typecheck/should_fail/tcfail103.stderr
+++ b/tests/typecheck/should_fail/tcfail103.stderr
@@ -2,9 +2,9 @@
 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
+          the type signature for f :: ST t Int at tcfail103.hs:10:8
       `s' is a rigid type variable bound by
-          the type signature for g :: ST s Int at tcfail103.hs:15:9
+          the type signature for g :: ST s Int at tcfail103.hs:13:17
     Expected type: STRef s Int
       Actual type: STRef t Int
     In the first argument of `readSTRef', namely `v'
diff --git a/tests/typecheck/should_fail/tcfail107.stderr b/tests/typecheck/should_fail/tcfail107.stderr
index eae3610c1d566cd2053111241c23392fe503502f..92a89b75449447cbc8bb5486ccf4e45dab4337e6 100644
--- a/tests/typecheck/should_fail/tcfail107.stderr
+++ b/tests/typecheck/should_fail/tcfail107.stderr
@@ -1,5 +1,5 @@
 
-tcfail107.hs:13:1:
+tcfail107.hs:13:9:
     Type synonym `Const' should have 2 arguments, but has been given 1
     In the type signature for `test':
       test :: Thing (Const Int) -> Thing (Const Int)
diff --git a/tests/typecheck/should_fail/tcfail127.stderr b/tests/typecheck/should_fail/tcfail127.stderr
index 8fa64fb204217262775b5b8e5a81ac46fff24577..021120314ffc25f7e493c5ceab620d6fd6079d44 100644
--- a/tests/typecheck/should_fail/tcfail127.stderr
+++ b/tests/typecheck/should_fail/tcfail127.stderr
@@ -1,5 +1,5 @@
-
-tcfail127.hs:3:1:
-    Illegal polymorphic or qualified type: Num a => a -> a
-    Perhaps you intended to use -XImpredicativeTypes
-    In the type signature for `foo': foo :: IO (Num a => a -> a)
+
+tcfail127.hs:3:8:
+    Illegal polymorphic or qualified type: Num a => a -> a
+    Perhaps you intended to use -XImpredicativeTypes
+    In the type signature for `foo': foo :: IO (Num a => a -> a)
diff --git a/tests/typecheck/should_fail/tcfail129.stderr b/tests/typecheck/should_fail/tcfail129.stderr
index f9ee8a567de111aab585beb1777d9068825ae7a6..f6ee765ce411f7aeab742d608195a99bd3b0e74d 100644
--- a/tests/typecheck/should_fail/tcfail129.stderr
+++ b/tests/typecheck/should_fail/tcfail129.stderr
@@ -1,11 +1,11 @@
 
-tcfail129.hs:12:8:
+tcfail129.hs:12:21:
     Type synonym `Foo' should have 1 argument, but has been given none
     In an expression type signature: Bar Foo
     In the expression: undefined :: Bar Foo
     In an equation for `blah': blah = undefined :: Bar Foo
 
-tcfail129.hs:17:9:
+tcfail129.hs:17:22:
     Type synonym `Foo1' should have 1 argument, but has been given none
     In an expression type signature: Bar1 Foo1
     In the expression: undefined :: Bar1 Foo1
diff --git a/tests/typecheck/should_fail/tcfail131.stderr b/tests/typecheck/should_fail/tcfail131.stderr
index 548e063929fbf1f4b729fa0ca9a5ea15a87bbe76..9c93a0f9169e1197241f69a9c3a6f4a907ca9c23 100644
--- a/tests/typecheck/should_fail/tcfail131.stderr
+++ b/tests/typecheck/should_fail/tcfail131.stderr
@@ -1,11 +1,11 @@
-
-tcfail131.hs:7:9:
-    Could not deduce (b ~ Integer)
-    from the context (Num b)
-      bound by the type signature for g :: Num b => b -> b
-      at tcfail131.hs:7:3-13
-      `b' is a rigid type variable bound by
-          the type signature for g :: Num b => b -> b at tcfail131.hs:7:3
-    In the return type of a call of `f'
-    In the expression: f x x
-    In an equation for `g': g x = f x x
+
+tcfail131.hs:7:9:
+    Could not deduce (b ~ Integer)
+    from the context (Num b)
+      bound by the type signature for g :: Num b => b -> b
+      at tcfail131.hs:6:8-22
+      `b' is a rigid type variable bound by
+          the type signature for g :: Num b => b -> b at tcfail131.hs:6:12
+    In the return type of a call of `f'
+    In the expression: f x x
+    In an equation for `g': g x = f x x
diff --git a/tests/typecheck/should_fail/tcfail153.stderr b/tests/typecheck/should_fail/tcfail153.stderr
index ca0b42b054aaa73afb6b61f4a9fdbba8f44a36fe..e648dc556da7fcf0d9058d18b6072608dec8a207 100644
--- a/tests/typecheck/should_fail/tcfail153.stderr
+++ b/tests/typecheck/should_fail/tcfail153.stderr
@@ -2,7 +2,7 @@
 tcfail153.hs:6:9:
     Couldn't match expected type `a' with actual type `Bool'
       `a' is a rigid type variable bound by
-          the type signature for f :: a -> [a] at tcfail153.hs:6:1
+          the type signature for f :: a -> [a] at tcfail153.hs:5:6
     In the first argument of `g', namely `x'
     In the expression: g x
     In an equation for `f':
diff --git a/tests/typecheck/should_fail/tcfail162.stderr b/tests/typecheck/should_fail/tcfail162.stderr
index 53f0129f48e403bad66d303ef9942ad85fd8c576..d1bb892ab03903cee7455e9e41c0dc33c59cec6f 100644
--- a/tests/typecheck/should_fail/tcfail162.stderr
+++ b/tests/typecheck/should_fail/tcfail162.stderr
@@ -1,6 +1,6 @@
 
 tcfail162.hs:10:33:
     Expecting one more argument to `ForeignPtr'
-    In the type `{-# UNPACK #-} !ForeignPtr'
+    In the type `ForeignPtr'
     In the definition of data constructor `Foo'
     In the data type declaration for `Foo'
diff --git a/tests/typecheck/should_fail/tcfail174.stderr b/tests/typecheck/should_fail/tcfail174.stderr
index 89135d656eb17e19b3255571ea3e929c4f1703e1..52a627ad9f00ac1bfd7ba2960e7e11e0ba02601a 100644
--- a/tests/typecheck/should_fail/tcfail174.stderr
+++ b/tests/typecheck/should_fail/tcfail174.stderr
@@ -23,7 +23,7 @@ tcfail174.hs:16:14:
       `a' is a rigid type variable bound by
           the type forall a. a -> a at tcfail174.hs:16:14
       `b' is a rigid type variable bound by
-          the type signature for h2 :: Capture b at tcfail174.hs:16:1
+          the type signature for h2 :: Capture b at tcfail174.hs:15:15
     Expected type: Capture (forall x. x -> b)
       Actual type: Capture (forall a. a -> a)
     In the first argument of `Capture', namely `g'
diff --git a/tests/typecheck/should_fail/tcfail175.stderr b/tests/typecheck/should_fail/tcfail175.stderr
index 4fe5bfbe4177de5bf8cc4fdb31189d1f6b5e1050..ded6ea65eb84361738c4b9f0ec3842be68254f56 100644
--- a/tests/typecheck/should_fail/tcfail175.stderr
+++ b/tests/typecheck/should_fail/tcfail175.stderr
@@ -3,6 +3,6 @@ tcfail175.hs:11:1:
     Couldn't match expected type `a'
                 with actual type `String -> String -> String'
       `a' is a rigid type variable bound by
-          the type signature for evalRHS :: Int -> a at tcfail175.hs:11:1
+          the type signature for evalRHS :: Int -> a at tcfail175.hs:10:19
     The equation(s) for `evalRHS' have three arguments,
     but its type `Int -> a' has only one
diff --git a/tests/typecheck/should_fail/tcfail179.stderr b/tests/typecheck/should_fail/tcfail179.stderr
index a24d404e15a725ed2dd78badb38652c5b06e5cc4..7a2970572351812444c1f02353c4649b6615be15 100644
--- a/tests/typecheck/should_fail/tcfail179.stderr
+++ b/tests/typecheck/should_fail/tcfail179.stderr
@@ -2,7 +2,7 @@
 tcfail179.hs:14:39:
     Couldn't match expected type `s' with actual type `x'
       `s' is a rigid type variable bound by
-          the type signature for run :: T s -> Int at tcfail179.hs:13:1
+          the type signature for run :: T s -> Int at tcfail179.hs:12:10
       `x' is a rigid type variable bound by
           a pattern with constructor
             T :: forall s x. (s -> (x -> s) -> (x, s, Int)) -> T s,
diff --git a/tests/typecheck/should_fail/tcfail196.stderr b/tests/typecheck/should_fail/tcfail196.stderr
index 79cc7266eb6965b415ce87c460448a1a10373391..ea6f16fd989248ac16efb67149c31e4e8f570f49 100644
--- a/tests/typecheck/should_fail/tcfail196.stderr
+++ b/tests/typecheck/should_fail/tcfail196.stderr
@@ -1,5 +1,5 @@
-
-tcfail196.hs:5:1:
-    Illegal polymorphic or qualified type: forall a. a
-    In the type signature for `bar':
-      bar :: Num (forall a. a) => Int -> Int
+
+tcfail196.hs:5:8:
+    Illegal polymorphic or qualified type: forall a. a
+    In the type signature for `bar':
+      bar :: Num (forall a. a) => Int -> Int
diff --git a/tests/typecheck/should_fail/tcfail197.stderr b/tests/typecheck/should_fail/tcfail197.stderr
index 3abe57be7ba4822291b282474b7db48cdd980892..464dacb078ab6417a82db4dbeccda319b55631ad 100644
--- a/tests/typecheck/should_fail/tcfail197.stderr
+++ b/tests/typecheck/should_fail/tcfail197.stderr
@@ -1,6 +1,5 @@
 
-tcfail197.hs:5:1:
+tcfail197.hs:5:8:
     Illegal polymorphic or qualified type: forall a. a
     Perhaps you intended to use -XImpredicativeTypes
-    In the type signature for `foo':
-      foo :: [forall a. a] -> Int
+    In the type signature for `foo': foo :: [forall a. a] -> Int
diff --git a/tests/typecheck/should_fail/tcfail201.stderr b/tests/typecheck/should_fail/tcfail201.stderr
index f45b899b901ea5c99b2de04e7eaea22f977a20e3..0cb16557f8b30d2bb210eab9e967f08c1fd55c1f 100644
--- a/tests/typecheck/should_fail/tcfail201.stderr
+++ b/tests/typecheck/should_fail/tcfail201.stderr
@@ -5,7 +5,7 @@ tcfail201.hs:18:28:
           the type signature for
             gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
                        -> (forall g. g -> c g) -> a -> c a
-          at tcfail201.hs:16:1
+          at tcfail201.hs:15:78
     In the pattern: DocParagraph hsDoc
     In a case alternative:
         (DocParagraph hsDoc) -> z DocParagraph `k` hsDoc
diff --git a/tests/typecheck/should_fail/tcfail206.stderr b/tests/typecheck/should_fail/tcfail206.stderr
index 76b5c7ebd2aaa116d578bd0111cb34e576592456..3283089afc135875e5f6fef1117ff25ea0ef208a 100644
--- a/tests/typecheck/should_fail/tcfail206.stderr
+++ b/tests/typecheck/should_fail/tcfail206.stderr
@@ -16,7 +16,7 @@ tcfail206.hs:8:5:
 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
+          the type signature for c :: a -> (a, Bool) at tcfail206.hs:10:6
     Expected type: a -> (a, Bool)
       Actual type: a -> (a, a)
     In the expression: (True || False,)
@@ -40,7 +40,7 @@ tcfail206.hs:17:5:
 tcfail206.hs:20:5:
     Couldn't match type `a' with `Bool'
       `a' is a rigid type variable bound by
-          the type signature for f :: a -> (# a, Bool #) at tcfail206.hs:20:1
+          the type signature for f :: a -> (# a, Bool #) at tcfail206.hs:19:6
     Expected type: a -> (# a, Bool #)
       Actual type: a -> (# a, a #)
     In the expression: (# True || False, #)
diff --git a/tests/typecheck/should_fail/tcfail208.stderr b/tests/typecheck/should_fail/tcfail208.stderr
index 64200a696d178d10158774d6460b30600a5ba87a..0a4ce1cd4dd4337517274415f803f3d86c8ebc59 100644
--- a/tests/typecheck/should_fail/tcfail208.stderr
+++ b/tests/typecheck/should_fail/tcfail208.stderr
@@ -4,7 +4,7 @@ tcfail208.hs:4:19:
     from the context (Monad m, Eq a)
       bound by the type signature for
                  f :: (Monad m, Eq a) => a -> m a -> Bool
-      at tcfail208.hs:4:1-23
+      at tcfail208.hs:3:6-40
     Possible fix:
       add (Eq (m a)) to the context of
         the type signature for f :: (Monad m, Eq a) => a -> m a -> Bool
diff --git a/tests/typecheck/should_fail/tcfail209.stderr b/tests/typecheck/should_fail/tcfail209.stderr
index ba90b2d1633fad5a3791112e0f054f40a4ba7dce..b5329ff6dcd88c5cc7d9fa0ce2b6046402d02128 100644
--- a/tests/typecheck/should_fail/tcfail209.stderr
+++ b/tests/typecheck/should_fail/tcfail209.stderr
@@ -1,10 +1,10 @@
 
-tcfail209.hs:5:1:
+tcfail209.hs:5:6:
     Illegal irreducible constraint Showish a
     (Use -XConstraintKinds to permit this)
     In the type signature for `f': f :: Showish a => a -> a
 
-tcfail209.hs:8:1:
+tcfail209.hs:8:6:
     Illegal tuple constraint (Show a, Num a)
     (Use -XConstraintKinds to permit this)
     In the type signature for `g':
diff --git a/tests/typecheck/should_run/tcrun041.hs b/tests/typecheck/should_run/tcrun041.hs
index dbdebf7687c6514ac171cb3515fed4d8b3db7ae1..6342fcd0e29bd216c6420e200097f4c3c59f95a2 100644
--- a/tests/typecheck/should_run/tcrun041.hs
+++ b/tests/typecheck/should_run/tcrun041.hs
@@ -25,7 +25,6 @@ h = (# ,1, #)
 unchanged :: a -> (# Int #)
 unchanged _binding = (# 1 #)
 
-
 main = do
     print (a 1, b False, c "Hello", c 1337, d "Yeah" "Baby")
     case e 1 of { (# x1, x2 #) ->