diff --git a/testsuite/tests/polykinds/Makefile b/testsuite/tests/polykinds/Makefile
index 0ea3b684d338e2d82da6d53c08b3b79ee4e85e13..9f3fb669b33a11ffb0395973ab2aa19ab1ea4199 100644
--- a/testsuite/tests/polykinds/Makefile
+++ b/testsuite/tests/polykinds/Makefile
@@ -9,3 +9,9 @@ T5881:
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T5881a.hs
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T5881.hs
 
+# T6025 is like T5881; needs separat compile
+T6025:
+	$(RM) -f T6025.hi T6025.o T6025a.hi T6025a.o
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T6025a.hs
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T6025.hs
+
diff --git a/testsuite/tests/polykinds/T6002.hs b/testsuite/tests/polykinds/T6002.hs
new file mode 100644
index 0000000000000000000000000000000000000000..b21914b0ffbd256ea99131bbf16ef7f13573fbd8
--- /dev/null
+++ b/testsuite/tests/polykinds/T6002.hs
@@ -0,0 +1,100 @@
+-- This module should compile with -XIncoherentInstances, but didn't in 7.4
+
+
+{- Here we define all the stuff that is needed for our singleton
+   types:
+ - phantom types (when GHC 7.4 arrives, the user-defined kinds)
+ - corresponding singleton types
+
+These are basically the constructs from Omega,
+reimplemented in Haskell for our purposes. -}
+
+{-# LANGUAGE GADTs, KindSignatures, StandaloneDeriving,
+             RankNTypes, TypeFamilies, FlexibleInstances, IncoherentInstances #-}
+module TypeMachinery where
+
+-- The natural numbers:
+--  o first the phantom types
+
+data Z; data S n
+
+-- o the using the above the singleton type Nat'
+
+data Nat' :: * -> * where
+  Z :: Nat' Z
+  S :: Nat' n -> Nat' (S n)
+
+deriving instance Show (Nat' a)
+
+-- Type-level addition
+
+type family Plus m n :: *
+type instance Plus Z n = n
+type instance Plus (S m) n = S (Plus m n)
+
+-- Nat' addition
+
+plus :: Nat' a -> Nat' b -> Nat' (Plus a b)
+plus Z n = n
+plus (S m) n = S (plus m n)
+
+-- Equality on Nat'
+
+sameNat' :: Nat' a -> Nat' b -> Bool
+sameNat' Z Z = True
+sameNat' (S m) (S n) = sameNat' m n
+sameNat' _ _ = False
+
+-- A data type for existentially hiding
+-- (e.g.) Nat' values
+
+data Hidden :: (* -> *) -> * where
+  Hide :: Show (a n) => a n -> Hidden a
+
+deriving instance Show (Hidden t)
+
+toNat' :: Integral i => i -> Hidden Nat'
+toNat' 0 = Hide Z
+toNat' n = case toNat' (n - 1) of
+           Hide n -> Hide (S n)
+
+-- Now we are ready to make Hidden Nat' an Integral type
+
+instance Eq (Hidden Nat') where
+Hide a == Hide b = sameNat' a b
+
+instance Ord (Hidden Nat') where
+  Hide Z `compare` Hide Z = EQ
+  Hide Z `compare` Hide _ = LT
+  Hide _ `compare` Hide Z = GT
+  Hide (S m) `compare` Hide (S n) = Hide m `compare` Hide n
+
+instance Enum (Hidden Nat') where
+  toEnum = toEnum . fromIntegral
+  fromEnum = fromIntegral
+
+instance Num (Hidden Nat') where
+  fromInteger = toNat'
+  signum (Hide Z) = 0
+  signum _ = 1
+  abs n = n
+  Hide a + Hide b = Hide $ plus a b
+  a * b = fromInteger $ toInteger a * toInteger b
+
+instance Real (Hidden Nat') where
+  toRational = toRational . toInteger
+
+instance Integral (Hidden Nat') where
+  toInteger (Hide Z) = 0
+  toInteger (Hide (S n)) = 1 + toInteger (Hide n)
+  quotRem a b = let (a', b') = toInteger a `quotRem` toInteger b in (fromInteger a', fromInteger b')
+
+-- McBride's Fin data type. By counting backwards from the
+-- result index, it only admits a fixed number of inhabitants.
+
+data Fin :: * -> * where
+    Stop :: Fin (S Z)
+    Retreat :: Fin s -> Fin (S s)
+
+deriving instance Show (Fin a)
+
diff --git a/testsuite/tests/polykinds/T6020.hs b/testsuite/tests/polykinds/T6020.hs
index fa7de49030c6c9bc834d94cd2aa1269a5147cd29..f9812392a04e3733910d1316be239695ff9730df 100644
--- a/testsuite/tests/polykinds/T6020.hs
+++ b/testsuite/tests/polykinds/T6020.hs
@@ -1,9 +1,8 @@
 {-# LANGUAGE DataKinds, FunctionalDependencies, FlexibleInstances,
              UndecidableInstances, PolyKinds, KindSignatures,
              ConstraintKinds, FlexibleContexts #-}
-module T6020 where
 
-import GHC.Prim (Constraint)
+module T6020 where
 
 class Id (a :: k) (b :: k) | a -> b
 instance Id a a
@@ -14,4 +13,3 @@ instance (Id x y, Id y z) => Test x z
 test :: Test True True => ()
 test = ()
 
-foo = test
diff --git a/testsuite/tests/polykinds/T6025.hs b/testsuite/tests/polykinds/T6025.hs
new file mode 100644
index 0000000000000000000000000000000000000000..8ed36fe56785cf0cb20f01844efffa4671b76278
--- /dev/null
+++ b/testsuite/tests/polykinds/T6025.hs
@@ -0,0 +1,5 @@
+module T6025 where
+
+import T6025a
+
+other = OTrue
diff --git a/testsuite/tests/polykinds/T6025a.hs b/testsuite/tests/polykinds/T6025a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..e1914b351427d90eba18c49b1c81c66fc2ce903c
--- /dev/null
+++ b/testsuite/tests/polykinds/T6025a.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE DataKinds, GADTs #-}
+module T6025a (Other (..)) where
+
+data Other a where
+  OTrue :: Other True
+  OFalse :: Other False
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 7f12a673f114f5eccd38cb9f44102491e8ff03b6..d99036740398c400bd8a87df3ba855073969ce2c 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -37,3 +37,5 @@ test('T5948', normal, compile, [''])
 test('T6020', normal, compile, [''])
 test('T6035', normal, compile, [''])
 test('T6036', normal, compile, [''])
+test('T6025', normal, run_command, ['$MAKE -s --no-print-directory T6025'])
+test('T6002', normal, compile, [''])
diff --git a/testsuite/tests/simplCore/should_run/T5997.hs b/testsuite/tests/simplCore/should_run/T5997.hs
new file mode 100644
index 0000000000000000000000000000000000000000..c4a708da9f6b461c96d1edcbb2fcf1d2cd0cd0de
--- /dev/null
+++ b/testsuite/tests/simplCore/should_run/T5997.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE BangPatterns #-}
+
+module Main where
+
+-- Stack overflow if the tail recursion does not work out properly
+
+incompleteBetaWorker :: Double -> Double
+incompleteBetaWorker _ = loop 1 1 1 1
+  where
+    -- Constants
+    eps = 1e-15
+    -- Loop
+    loop :: Double -> Int -> Double -> Double -> Double
+    loop !psq !ns !term !betain
+      | done           = betain'
+      | ns > 10000000  = betain'
+      | otherwise      = loop psq' (ns + 1) term' betain'
+      where
+        -- New values
+        term'   = term
+        betain' = betain
+        psq'    = if ns < 0 then psq + 1 else psq
+        -- This condition cause stack overflow
+        done = db <= eps && db <= eps*betain' where db = abs term'
+        -- With this it loops endlessly
+        -- done = db <= eps * betain' where db = abs term'
+
+main :: IO ()
+main = print $ incompleteBetaWorker 0
diff --git a/testsuite/tests/simplCore/should_run/T5997.stdout b/testsuite/tests/simplCore/should_run/T5997.stdout
new file mode 100644
index 0000000000000000000000000000000000000000..d3827e75a5cadb9fe4a27e1cb9b6d192e7323120
--- /dev/null
+++ b/testsuite/tests/simplCore/should_run/T5997.stdout
@@ -0,0 +1 @@
+1.0
diff --git a/testsuite/tests/simplCore/should_run/all.T b/testsuite/tests/simplCore/should_run/all.T
index 20b25787a05fe4967f54560d77bf5376e9a6f984..210618a90a8523579561008fc19d29856b8283e5 100644
--- a/testsuite/tests/simplCore/should_run/all.T
+++ b/testsuite/tests/simplCore/should_run/all.T
@@ -55,3 +55,5 @@ test('T5625', [ only_ways(['normal','optasm']), exit_code(1) ], compile_and_run,
 test('T5587', [ only_ways(['normal','optasm']), exit_code(1) ], compile_and_run, [''])
 test('T5915', only_ways(['normal','optasm']), compile_and_run, [''])
 test('T5920', only_ways(['normal','optasm']), compile_and_run, [''])
+test('T5997', normal, compile_and_run, [''])
+