Move tests from tests/ghc-regress/* to just tests/*

281 files changed, 5368 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/Makefile b/testsuite/tests/indexed-types/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/indexed-types/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/indexed-types/should_compile/ATLoop.hs b/testsuite/tests/indexed-types/should_compile/ATLoop.hs
new file mode 100644
index 0000000000..19f9e5b8a2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ATLoop.hs
@@ -0,0 +1,22 @@
+{-# OPTIONS_GHC -O2 #-}

+

+-- Reading the interface file caused a black hole

+-- in earlier versions of GHC

+

+-- Also, foo should compile to very tight code with -O2

+-- (The O2 was nothing to do with the black hole though.)

+

+module ShouldCompile where

+

+import ATLoop_help

+

+foo :: FooT Int -> Int -> Int

+foo t n = t `seq` bar n

+   where

+     bar 0 = 0

+     bar n | even n = bar (n `div` 2)

+     bar n          = bar (n - int t)

+

+

+

+

diff --git a/testsuite/tests/indexed-types/should_compile/ATLoop_help.hs b/testsuite/tests/indexed-types/should_compile/ATLoop_help.hs
new file mode 100644
index 0000000000..8814f480eb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ATLoop_help.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}

+module ATLoop_help where

+

+class Foo a where

+   data FooT a :: *

+   int :: FooT a -> Int

+

+instance Foo Int where

+    data FooT Int = FooInt !Int

+    int (FooInt n) = n

diff --git a/testsuite/tests/indexed-types/should_compile/Class1.hs b/testsuite/tests/indexed-types/should_compile/Class1.hs
new file mode 100644
index 0000000000..4e58e13d58
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Class1.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
+
+-- Results in context reduction stack overflow
+
+module Class1 where
+
+class C a where
+  foo :: a x -> a y
+
+class C (T a) => D a where
+  type T a :: * -> *
+
+  bar :: a -> T a x -> T a y
+
+instance C Maybe where
+  foo Nothing = Nothing
+
+instance D () where
+  type T () = Maybe
+
+  bar x t = foo t
diff --git a/testsuite/tests/indexed-types/should_compile/Class2.hs b/testsuite/tests/indexed-types/should_compile/Class2.hs
new file mode 100644
index 0000000000..f0d90f35f5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Class2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Class2 where
+
+data family T a
+data instance T Int = TInt Int
+
+data U = U (T Int)
+
+instance Show a => Show (T a) where
+  showsPrec k t = showString "T"
+
+instance Show U where
+  showsPrec k (U x) = showsPrec k x
+
diff --git a/testsuite/tests/indexed-types/should_compile/Class3.hs b/testsuite/tests/indexed-types/should_compile/Class3.hs
new file mode 100644
index 0000000000..6bea22e1a4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Class3.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Class3 where
+
+class C a where
+  foo :: a -> a
+instance C ()
+
+bar :: (a ~ ()) => a -> a
+bar = foo
+
diff --git a/testsuite/tests/indexed-types/should_compile/Class3.stderr b/testsuite/tests/indexed-types/should_compile/Class3.stderr
new file mode 100644
index 0000000000..58367939d0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Class3.stderr
@@ -0,0 +1,4 @@
+
+Class3.hs:7:10:
+    Warning: No explicit method nor default method for `foo'
+    In the instance declaration for `C ()'
diff --git a/testsuite/tests/indexed-types/should_compile/ClassEqContext.hs b/testsuite/tests/indexed-types/should_compile/ClassEqContext.hs
new file mode 100644
index 0000000000..7de87362b4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ClassEqContext.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+
+module ClassEqContext  where 
+
+class a ~ b => C a b
diff --git a/testsuite/tests/indexed-types/should_compile/ClassEqContext2.hs b/testsuite/tests/indexed-types/should_compile/ClassEqContext2.hs
new file mode 100644
index 0000000000..a491577723
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ClassEqContext2.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module ClassEqContext  where 
+
+class (Show a,a ~ b) => C a b
diff --git a/testsuite/tests/indexed-types/should_compile/ClassEqContext3.hs b/testsuite/tests/indexed-types/should_compile/ClassEqContext3.hs
new file mode 100644
index 0000000000..e2fd14515f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ClassEqContext3.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module ClassEqContext  where 
+
+class a ~ b => C a b
+
+instance C Char Char
diff --git a/testsuite/tests/indexed-types/should_compile/CoTest3.hs b/testsuite/tests/indexed-types/should_compile/CoTest3.hs
new file mode 100644
index 0000000000..971a464a89
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/CoTest3.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TypeFamilies #-}

+{-# LANGUAGE RankNTypes #-}

+{-# LANGUAGE FlexibleContexts #-}

+{-# LANGUAGE GADTs #-}

+

+-- This test uses the PushC rule of the System FC operational semantics

+-- Writen by Tom Schrijvers

+

+module CoTest3 where 

+

+data T a = K (a ~ Int => a -> Int) 

+

+

+{-# INLINE[2] f #-}

+f :: T s1 ~ T s2 => T s1 -> T s2

+f x = x

+

+{-# INLINE[3] test #-}

+test :: T s1 ~ T s2 => (s1 ~ Int => s1 -> Int) -> (s2 ~ Int => s2 -> Int) 

+test g = case f (K g) of

+           K r -> r

+e :: s ~ Int => s -> s -> Int

+e _ s = s

+

+final :: s1 ~ s2 => s1 -> (s2 ~ Int => s2 -> Int)

+final x = test (e x)

diff --git a/testsuite/tests/indexed-types/should_compile/Col.hs b/testsuite/tests/indexed-types/should_compile/Col.hs
new file mode 100644
index 0000000000..62c309bd91
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Col.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Col  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ singleton :: Elem c -> c
+ add :: c -> Elem c -> c
+
+instance Col [e] where
+ singleton = \x -> [x]
+ add = flip (:)
+
diff --git a/testsuite/tests/indexed-types/should_compile/Col2.hs b/testsuite/tests/indexed-types/should_compile/Col2.hs
new file mode 100644
index 0000000000..97a10aef84
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Col2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module Col  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class (Eq (Elem c)) => Col c where
+  count     :: Elem c -> c -> Int
+
+instance Eq e => Col [e] where
+  count	    x = length . filter (==x)
diff --git a/testsuite/tests/indexed-types/should_compile/ColGivenCheck.hs b/testsuite/tests/indexed-types/should_compile/ColGivenCheck.hs
new file mode 100644
index 0000000000..288c6e0608
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColGivenCheck.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+addAll :: (Col c1, Col c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
+addAll c1 c2 
+	| isEmpty c1
+	= c2
+	| otherwise
+	= let (x,c1') = headTail c1
+	  in addAll c1' (add c2 x)
diff --git a/testsuite/tests/indexed-types/should_compile/ColGivenCheck2.hs b/testsuite/tests/indexed-types/should_compile/ColGivenCheck2.hs
new file mode 100644
index 0000000000..2da7cb4117
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColGivenCheck2.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+-- addAll :: (Col c1, Col c2, Elem c1 ~ Elem c2) => c1 -> c2 -> c2
+-- addAll c1 c2 
+-- 	| isEmpty c1
+-- 	= c2
+-- 	| otherwise
+-- 	= let (x,c1') = headTail c1
+-- 	  in addAll c1' (add c2 x)
+
+sumCol :: (Col c, Elem c ~ Int) => c -> Int
+sumCol c | isEmpty c
+	 = 0
+	 | otherwise
+ 	 = let (x,xs) = headTail c
+	   in x + (sumCol xs)
+
+-- data CP :: * -> * where
+--  CP :: (Col c1, Col c2, Elem c1 ~ Elem c2, Elem c2 ~ Int) => (c1,c2) -> CP Char
+
diff --git a/testsuite/tests/indexed-types/should_compile/ColInference.hs b/testsuite/tests/indexed-types/should_compile/ColInference.hs
new file mode 100644
index 0000000000..a70b7dd444
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColInference.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+addAll c1 c2 
+	| isEmpty c1
+	= c2
+	| otherwise
+	= let (x,c1') = headTail c1
+	  in addAll c1' (add c2 x)
diff --git a/testsuite/tests/indexed-types/should_compile/ColInference2.hs b/testsuite/tests/indexed-types/should_compile/ColInference2.hs
new file mode 100644
index 0000000000..9785d717a7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColInference2.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+sawpOne c1 c2 
+	= let (x,c1') = headTail c1
+              (y,c2') = headTail c2
+	  in (add c1' y,add c2' x)
diff --git a/testsuite/tests/indexed-types/should_compile/ColInference3.hs b/testsuite/tests/indexed-types/should_compile/ColInference3.hs
new file mode 100644
index 0000000000..f946e89120
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColInference3.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Main where 
+
+type family Elem c
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+-- LIST
+instance Col [a] where
+  isEmpty   	  = null
+  add	   	  = flip (:)
+  headTail (x:xs) =  (x,xs)
+
+type instance Elem [a] = a
+
+-- SEQUENCE
+data Sequence a = Nil | Snoc (Sequence a) a deriving Show
+
+instance Col (Sequence a) where
+  isEmpty Nil = True
+  isEmpty _   = False
+
+  add     s x = Snoc s x
+
+  headTail (Snoc s x) = (x,s)
+
+type instance Elem (Sequence a) = a
+
+-- 
+addAll c1 c2 
+	| isEmpty c1
+	= c2
+	| otherwise
+	= let (x,c1') = headTail c1
+	  in addAll c1' (add c2 x)
+
+--
+main = print $ addAll c1 c2
+       where c1 = ['a','b','c']
+             c2 = (Snoc (Snoc (Snoc Nil 'd') 'e') 'f')
diff --git a/testsuite/tests/indexed-types/should_compile/ColInference4.hs b/testsuite/tests/indexed-types/should_compile/ColInference4.hs
new file mode 100644
index 0000000000..27675b1051
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColInference4.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+sawpOne c1 c2 
+	= let (x,c1') = headTail c1
+              (y,c2') = headTail c2
+	  in (add c1' y,add c1' x)
diff --git a/testsuite/tests/indexed-types/should_compile/ColInference5.hs b/testsuite/tests/indexed-types/should_compile/ColInference5.hs
new file mode 100644
index 0000000000..b65a90092e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColInference5.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+ isEmpty   :: c -> Bool
+ add       :: c -> Elem c -> c
+ headTail  :: c -> (Elem c,c)
+
+sawpOne c1 c2 
+	= let (x,c1') = headTail c1
+              (y,c2') = headTail c2
+	  in (add c1' y,add c1' y)
diff --git a/testsuite/tests/indexed-types/should_compile/ColInference6.hs b/testsuite/tests/indexed-types/should_compile/ColInference6.hs
new file mode 100644
index 0000000000..9273632e2b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ColInference6.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ColInference6  where 
+
+type family Elem c
+
+type instance Elem [e] = e
+
+class Col c where
+  toList :: c -> [Elem c]
+
+
+sumCol c = sum . toList $ c
diff --git a/testsuite/tests/indexed-types/should_compile/DataFamDeriv.hs b/testsuite/tests/indexed-types/should_compile/DataFamDeriv.hs
new file mode 100644
index 0000000000..3800b51a3f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/DataFamDeriv.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+module DataFamDeriv where
+
+data family Foo a
+data Bar = Bar
+data instance Foo Bar
+    = Bar1 | Bar2 | Bar3 | Bar4 | Bar5 | Bar6 | Bar7 | Bar8 | Bar9
+    deriving Eq
+
+
+
diff --git a/testsuite/tests/indexed-types/should_compile/Deriving.hs b/testsuite/tests/indexed-types/should_compile/Deriving.hs
new file mode 100644
index 0000000000..fd0eff2016
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Deriving.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving, FlexibleInstances #-}
+
+module ShouldCompile where
+
+data family T a
+
+data instance T Int = A | B
+		    deriving Eq
+
+foo :: T Int -> Bool
+foo x = x == x
+
+data instance T Char = C
+
+instance Eq (T Char) where
+  C == C = False
+
+data family R a
+data instance R [a] = R
+
+deriving instance Eq (R [a])
+
+class C a where
+  data S a
+
+instance C Int where
+  data S Int = SInt deriving Eq
+
+bar :: S Int -> Bool
+bar x = x == x
diff --git a/testsuite/tests/indexed-types/should_compile/DerivingNewType.hs b/testsuite/tests/indexed-types/should_compile/DerivingNewType.hs
new file mode 100644
index 0000000000..65f3b8520d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/DerivingNewType.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies, GeneralizedNewtypeDeriving #-}
+
+module ShouldCompile where
+
+data family S a
+
+newtype instance S Int = S Int
+		       deriving Eq
+
+data family S2 a b
+
+newtype instance S2 Int b = S2 (IO b)
+		          deriving Monad
+
diff --git a/testsuite/tests/indexed-types/should_compile/Exp.hs b/testsuite/tests/indexed-types/should_compile/Exp.hs
new file mode 100644
index 0000000000..60cb12f098
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Exp.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Exp (C, C(type T), T, foo, S)
+where
+
+class C a where
+  data T a :: *
+  foo :: a -> a
+
+data family S a b :: *
diff --git a/testsuite/tests/indexed-types/should_compile/GADT1.hs b/testsuite/tests/indexed-types/should_compile/GADT1.hs
new file mode 100644
index 0000000000..7761eafe97
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT1.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
+
+-- This wrongly fails with
+-- 
+--   Can't construct the infinite type n = PLUS n ZERO
+
+module GADT1 where
+
+data ZERO
+data SUCC n
+
+data Nat n where
+  Zero :: Nat ZERO
+  Succ :: Nat n -> Nat (SUCC n)
+
+type family PLUS m n
+type instance PLUS ZERO n = n
+type instance PLUS (SUCC m) n = SUCC (PLUS m n)
+
+data EQUIV x y where
+  EQUIV :: EQUIV x x
+
+plus_zero :: Nat n -> EQUIV (PLUS n ZERO) n
+plus_zero Zero = EQUIV
+plus_zero (Succ n) = case plus_zero n of
+                       EQUIV -> EQUIV 
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT10.hs b/testsuite/tests/indexed-types/should_compile/GADT10.hs
new file mode 100644
index 0000000000..76efaf1fcc
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT10.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes #-}
+
+module GADT10 where
+
+-- [Sept 2010] Now works in GHC 7.0!
+
+-- This fails with
+--
+-- GADT10.hs:37:0:
+--     All of the type variables in the constraint `x ~
+--                                                  y' are already in scope
+--         (at least one must be universally quantified here)
+--     In the type signature for `foo':
+--       foo :: EQUAL x y -> ((x ~ y) => t) -> t
+-- 
+-- GADT10.hs:38:4:
+--     Couldn't match expected type `y' against inferred type `x'
+--       `y' is a rigid type variable bound by
+--           the type signature for `foo' at GADT10.hs:8:15
+--       `x' is a rigid type variable bound by
+--           the type signature for `foo' at GADT10.hs:8:13
+--     In the pattern: EQUAL
+--     In the definition of `foo': foo EQUAL t = t
+--
+-- The first error can be fixed by using FlexibleContexts but I don't think that
+-- should be required here. In fact, if we remove RankNTypes, we get
+--
+--     Illegal polymorphic or qualified type: forall (co_wild_B1 :: x ~
+--                                                                  y).
+--                                            t
+--     In the type signature for `foo':
+--       foo :: EQUAL x y -> ((x ~ y) => t) -> t
+--
+-- which seems to contradict (at least sort of) the first error message.
+
+data EQUAL x y where
+  EQUAL :: EQUAL x x
+
+foo :: EQUAL x y -> (x~y => t) -> t
+foo EQUAL t = t
+
+bar :: EQUAL x y -> x -> y
+bar equ x = foo equ x
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT11.hs b/testsuite/tests/indexed-types/should_compile/GADT11.hs
new file mode 100644
index 0000000000..70c5d75d84
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT11.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, EmptyDataDecls #-}
+
+module ShouldCompile where
+
+data Z
+data S a
+
+type family Sum n m
+type instance Sum n Z = n
+type instance Sum n (S m) = S (Sum n m)
+
+data Nat n where
+  NZ :: Nat Z
+  NS :: (S n ~ sn) => Nat n -> Nat sn
+
+data EQ a b = forall q . (a ~ b) => Refl
+
+zerol :: Nat n -> EQ n (Sum Z n)
+zerol NZ = Refl
+-- zerol (NS n) = case zerol n of Refl -> Refl
diff --git a/testsuite/tests/indexed-types/should_compile/GADT12.hs b/testsuite/tests/indexed-types/should_compile/GADT12.hs
new file mode 100644
index 0000000000..4eb5124c1d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT12.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TypeFamilies, GADTs, ScopedTypeVariables, KindSignatures #-}
+{-# LANGUAGE EmptyDataDecls #-}
+
+-- Tests whether a type signature can refine a type
+-- See the definition of bug2a
+
+module ShouldCompile where
+
+data Typed
+data Untyped
+
+type family TU a b :: *
+type instance TU Typed b = b
+type instance TU Untyped b = ()
+
+-- A type witness type, use eg. for pattern-matching on types
+data Type a where
+    TypeInt     :: Type Int
+    TypeBool    :: Type Bool
+    TypeString  :: Type String
+    TypeList    :: Type t -> Type [t]
+
+data Expr :: * -> * -> * {- tu a -} where
+    Const :: Type a -> a -> Expr tu (TU tu a)
+    Var2  :: String -> TU tu (Type a) -> Expr tu (TU tu a)
+
+bug1 :: Expr Typed Bool -> ()
+bug1 (Const TypeBool False) = ()
+
+bug2a :: Expr Typed Bool -> ()
+bug2a (Var2 "x" (TypeBool :: Type Bool)) = ()
+
+bug2c :: Expr Typed Bool -> ()
+bug2c (Var2 "x" TypeBool) = ()
+
+bug2b :: Expr Typed (TU Typed Bool) -> ()
+bug2b (Var2 "x" TypeBool) = ()
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT12.stderr b/testsuite/tests/indexed-types/should_compile/GADT12.stderr
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT12.stderr
diff --git a/testsuite/tests/indexed-types/should_compile/GADT13.hs b/testsuite/tests/indexed-types/should_compile/GADT13.hs
new file mode 100644
index 0000000000..b5724b2500
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT13.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module GADT13 where
+
+data family HiThere a :: *
+
+data instance HiThere () where
+    HiThere :: HiThere ()
diff --git a/testsuite/tests/indexed-types/should_compile/GADT14.hs b/testsuite/tests/indexed-types/should_compile/GADT14.hs
new file mode 100644
index 0000000000..ace1de45da
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT14.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, GADTs,  RankNTypes, FlexibleContexts #-}
+module Equality( (:=:), eq_elim, eq_refl ) where
+
+data a:=: b where
+  EQUAL :: a :=: a
+
+eq_refl :: a :=: a
+eq_refl = EQUAL
+
+eq_elim :: (a~b) => a :=: b -> (a~b => p) -> p
+eq_elim EQUAL p = p 
diff --git a/testsuite/tests/indexed-types/should_compile/GADT2.hs b/testsuite/tests/indexed-types/should_compile/GADT2.hs
new file mode 100644
index 0000000000..eb8354ba28
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+-- Fails with
+--
+--   Couldn't match expected type `y' against inferred type `x'
+
+module GADT2 where
+
+data EQUAL x y where
+  EQUAL :: x~y => EQUAL x y
+
+foo :: EQUAL x y -> x -> y
+foo EQUAL x = x
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT3.hs b/testsuite/tests/indexed-types/should_compile/GADT3.hs
new file mode 100644
index 0000000000..f630ad5d22
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT3.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
+
+-- Panics in bind_args
+
+module GADT3 where
+
+data EQUAL x y where
+  EQUAL :: x~y => EQUAL x y
+
+data ZERO
+data SUCC n
+
+data Nat n where
+  Zero :: Nat ZERO
+  Succ :: Nat n -> Nat (SUCC n)
+
+type family PLUS m n
+type instance PLUS ZERO n = n
+
+plus_zero :: Nat n -> EQUAL (PLUS ZERO n) n
+plus_zero Zero = EQUAL
+plus_zero (Succ n) = EQUAL
+
+data FOO n where
+  FOO_Zero :: FOO ZERO
+
+foo :: Nat m -> Nat n -> FOO n -> FOO (PLUS m n)
+foo Zero n s = case plus_zero n of EQUAL -> s
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT4.hs b/testsuite/tests/indexed-types/should_compile/GADT4.hs
new file mode 100644
index 0000000000..07cf492843
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT4.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module GADT4 where
+
+type family F a
+type instance F () = ()
+
+data T a where
+  T :: T ()
+
+foo :: T () -> T (F ()) -> ()
+foo T T = ()
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT5.hs b/testsuite/tests/indexed-types/should_compile/GADT5.hs
new file mode 100644
index 0000000000..69a6481fd0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT5.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module GADT5 where
+
+data T a where
+  T :: T (a,b)
+  -- this works:
+  -- T :: p ~ (a,b) => T p
+
+type family F a
+
+bar :: T (F a) -> ()
+bar T = ()
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT6.hs b/testsuite/tests/indexed-types/should_compile/GADT6.hs
new file mode 100644
index 0000000000..0e976b441e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT6.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module GADT6 where
+
+data Pair p  where
+  Pair :: p~(a,b) => a -> b -> Pair p
+  -- this works:
+  -- Pair :: a -> b -> Pair (a,b)
+
+foo :: Pair ((), ()) -> a
+foo (Pair () ()) = undefined
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT7.hs b/testsuite/tests/indexed-types/should_compile/GADT7.hs
new file mode 100644
index 0000000000..00912605b4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT7.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module GADT7 where
+
+data Pair p  where
+  Pair :: p~(a,b) => a -> b -> Pair p
+  -- this works:
+--  Pair :: a -> b -> Pair (a,b)
+
+foo :: a
+foo = case Pair () () of
+   -- this works:
+--   case Pair () () :: Pair ((), ()) of
+        Pair x y -> undefined
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT8.hs b/testsuite/tests/indexed-types/should_compile/GADT8.hs
new file mode 100644
index 0000000000..6d9381296e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT8.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module GADT8 where
+
+data Pair p  where
+  Pair :: p~(a,b) => a -> b -> Pair p
+  -- this works:
+  -- Pair :: a -> b -> Pair (a,b)
+
+foo :: Pair ((), ()) -> Pair ((), ())
+foo (Pair x y) = Pair x y
+
diff --git a/testsuite/tests/indexed-types/should_compile/GADT9.hs b/testsuite/tests/indexed-types/should_compile/GADT9.hs
new file mode 100644
index 0000000000..7ced0f76d1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GADT9.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+-- Fails with
+--
+--   Couldn't match expected type `z' against inferred type `y'
+--
+-- See also GADT2
+
+module GADT2 where
+
+data EQUAL x y where
+  EQUAL :: x~y => EQUAL x y
+
+foo :: EQUAL x y -> EQUAL y z -> x -> z
+foo EQUAL EQUAL x = x
+
diff --git a/testsuite/tests/indexed-types/should_compile/Gentle.hs b/testsuite/tests/indexed-types/should_compile/Gentle.hs
new file mode 100644
index 0000000000..a32ac798a0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Gentle.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
+             FlexibleInstances,
+             OverlappingInstances, UndecidableInstances #-}
+
+-- Rather exotic example posted to Haskell mailing list 17 Oct 07
+-- It concerns context reduction and functional dependencies
+
+module FooModule where
+
+class Concrete a b | a -> b where
+	bar :: a -> String
+
+instance (Show a) => Concrete a b where
+	bar = error "urk"
+
+wib :: Concrete a b => a -> String
+wib x = bar x
+
+-- Uncommenting this solves the problem:
+-- instance Concrete Bool Bool
+
+{- This is a nice example of the trickiness of functional dependencies.
+Here's what is happening.
+
+Consider type inference for 'wib'.  GHC 6.6 figures out that the call
+of 'bar' gives rise to the constraint (Concrete p q), where x has type
+'p'.  Ah, but x must have type 'a', so the constraint is (Concrete a
+q).
+
+Now GHC tries to satisfy (Concrete a q) from (Concrete a b). If it
+applied improvement right away it'd succeed, but sadly it first looks
+at instances declarations.  Success: we can get (Concrete a q) from
+(Show a).  So it uses the instance decl and now we can't get (Show a)
+from (Concrete a b).
+
+
+OK,  found that in GHC 6.6, adding
+	instance Concrete Bool Bool
+fixed the problem. That's weird isn't it?  The reason is this. When GHC looks
+at the instance decls, it now sees *two* instance decls matching
+(Concrete a q), and so it declines for now to use either of them
+(since it's not clear which would be the right one).  Once it has
+finished with instance decls it tries improvement.  And, yes, it now
+sees that q=b, so all is well.
+
+You might say that GHC should use improvement more vigorously, and
+perhaps you'd be right.  And indeed the upcoming GHC 6.8 does exactly
+that.
+-}
+
diff --git a/testsuite/tests/indexed-types/should_compile/Gentle.stderr b/testsuite/tests/indexed-types/should_compile/Gentle.stderr
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Gentle.stderr
diff --git a/testsuite/tests/indexed-types/should_compile/GivenCheck.hs b/testsuite/tests/indexed-types/should_compile/GivenCheck.hs
new file mode 100644
index 0000000000..20320ae1c9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenCheck.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module GivenCheck where 
+
+type family S x
+
+f :: a -> S a
+f = undefined
+
+g :: S a ~ Char => a -> Char
+g y   | False  		= f y
+      |	otherwise	= 'a'
diff --git a/testsuite/tests/indexed-types/should_compile/GivenCheckDecomp.hs b/testsuite/tests/indexed-types/should_compile/GivenCheckDecomp.hs
new file mode 100644
index 0000000000..3d2492770d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenCheckDecomp.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module GivenCheckDecomp where 
+
+type family S x
+
+f :: a -> S a
+f = undefined
+
+g :: [S a] ~ [Char] => a -> Char
+g y   | 'a' == 'b'	= f y
diff --git a/testsuite/tests/indexed-types/should_compile/GivenCheckSwap.hs b/testsuite/tests/indexed-types/should_compile/GivenCheckSwap.hs
new file mode 100644
index 0000000000..8d053f312a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenCheckSwap.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module GivenCheckSwapMain where 
+
+type family S x
+
+f :: a -> S a
+f = undefined
+
+g :: Char ~ S a => a -> Char
+g y   | False  		= f y
+      |	otherwise	= 'a'
diff --git a/testsuite/tests/indexed-types/should_compile/GivenCheckTop.hs b/testsuite/tests/indexed-types/should_compile/GivenCheckTop.hs
new file mode 100644
index 0000000000..bc81d1acc7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/GivenCheckTop.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module GivenCheckTop where 
+
+type family S x
+
+type instance S [e] = e 
+
+f :: a -> S a
+f = undefined
+
+g :: S [a] ~ Char => a -> Char
+g y = y
diff --git a/testsuite/tests/indexed-types/should_compile/HO.hs b/testsuite/tests/indexed-types/should_compile/HO.hs
new file mode 100644
index 0000000000..40d597a76f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/HO.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, RankNTypes #-}
+
+module HO where 
+
+import Data.IORef
+
+type family SMRef    (m::(* -> *)) :: * -> *
+type family SMMonad  (r::(* -> *)) :: * -> *
+
+type instance SMRef   IO 	= IORef
+type instance SMMonad IORef	= IO
+
+
+class SMMonad (SMRef m) ~ m => SM m where
+	new   :: forall a. a -> m (SMRef m a)
+	read  :: forall a. (SMRef m a) -> m a
+	write :: forall a. (SMRef m a) -> a -> m ()
+
diff --git a/testsuite/tests/indexed-types/should_compile/Imp.hs b/testsuite/tests/indexed-types/should_compile/Imp.hs
new file mode 100644
index 0000000000..6ae1812083
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Imp.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Imp
+where
+
+import Exp (C, T, S)
+
+instance C Int where
+  data T Int = TInt
+
+data instance S Int Bool = SIntBool
diff --git a/testsuite/tests/indexed-types/should_compile/Ind2_help.hs b/testsuite/tests/indexed-types/should_compile/Ind2_help.hs
new file mode 100644
index 0000000000..b088302fec
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Ind2_help.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Ind2_help where
+
+class C a where
+  data T a :: *
+  unT :: T a -> a
+  mkT :: a -> T a
+
+instance (C a, C b) => C (a,b) where
+  data T (a,b) = TProd (T a) (T b)
+  unT (TProd x y) = (unT x, unT y)
+  mkT (x,y)       = TProd (mkT x) (mkT y)
+
diff --git a/testsuite/tests/indexed-types/should_compile/IndTypesPerf.hs b/testsuite/tests/indexed-types/should_compile/IndTypesPerf.hs
new file mode 100644
index 0000000000..4edcd03988
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/IndTypesPerf.hs
@@ -0,0 +1,11 @@
+
+-- This used lots of memory, and took a long time to compile, with GHC 6.12:
+-- http://www.haskell.org/pipermail/glasgow-haskell-users/2010-May/018835.html
+
+module IndTypesPerf where
+
+import IndTypesPerfMerge
+
+data Rec1 = Rec1 !Int
+
+mkRec1 v = mk $ merge v () where mk (Tagged i :* ()) = Rec1 i
diff --git a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
new file mode 100644
index 0000000000..18ed35bdc1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE EmptyDataDecls, TypeFamilies, UndecidableInstances,
+             ScopedTypeVariables, OverlappingInstances, TypeOperators,
+             FlexibleInstances, NoMonomorphismRestriction,
+             MultiParamTypeClasses #-}
+module IndTypesPerfMerge where
+
+data a :* b = a :* b
+infixr 6 :*
+
+data TRUE
+data FALSE
+data Zero
+data Succ a
+
+type family Equals m n
+type instance Equals Zero Zero = TRUE
+type instance Equals (Succ a) Zero = FALSE
+type instance Equals Zero (Succ a) = FALSE
+type instance Equals (Succ a) (Succ b) = Equals a b
+
+type family LessThan m n
+type instance LessThan Zero Zero = FALSE
+type instance LessThan (Succ n) Zero = FALSE
+type instance LessThan Zero (Succ n) = TRUE
+type instance LessThan (Succ m) (Succ n) = LessThan m n
+
+newtype Tagged n a = Tagged a deriving (Show,Eq)
+
+type family Cond p a b
+
+type instance Cond TRUE a b = a
+type instance Cond FALSE a b = b
+
+class Merger a where
+    type Merged a
+    type UnmergedLeft a
+    type UnmergedRight a
+    mkMerge :: a -> UnmergedLeft a -> UnmergedRight a -> Merged a
+
+class Mergeable a b where
+    type MergerType a b
+    merger :: a -> b -> MergerType a b
+
+merge x y = mkMerge (merger x y) x y
+
+data TakeRight a
+data TakeLeft a
+data DiscardRightHead a b c d
+data LeftHeadFirst a b c d
+data RightHeadFirst a b c d
+data EndMerge
+
+instance Mergeable () () where
+    type MergerType () () = EndMerge
+    merger = undefined
+
+instance Mergeable () (a :* b) where
+    type MergerType () (a :* b) = TakeRight (a :* b)
+    merger = undefined
+instance Mergeable (a :* b) () where
+    type MergerType (a :* b) () = TakeLeft (a :* b)
+    merger = undefined
+
+instance Mergeable (Tagged m a :* t1) (Tagged n b :* t2) where
+    type MergerType (Tagged m a :* t1) (Tagged n b :* t2) =
+        Cond (Equals m n) (DiscardRightHead (Tagged m a) t1 (Tagged n b) t2)
+           (Cond (LessThan m n) (LeftHeadFirst (Tagged m a) t1 (Tagged n b) t2)
+               (RightHeadFirst (Tagged m a ) t1 (Tagged n b) t2))
+    merger = undefined
+
+instance Merger EndMerge where
+    type Merged EndMerge = ()
+    type UnmergedLeft EndMerge = ()
+    type UnmergedRight EndMerge = ()
+    mkMerge _ () () = ()
+
+instance Merger (TakeRight a) where
+    type Merged (TakeRight a) = a
+    type UnmergedLeft (TakeRight a) = ()
+    type UnmergedRight (TakeRight a) = a
+    mkMerge _ () a = a
+
+instance Merger (TakeLeft a) where
+    type Merged (TakeLeft a) = a
+    type UnmergedLeft (TakeLeft a) = a
+    type UnmergedRight (TakeLeft a) = ()
+    mkMerge _ a () = a
+
+instance
+    (Mergeable t1 t2,
+     Merger (MergerType t1 t2),
+     t1 ~ UnmergedLeft (MergerType t1 t2),
+     t2 ~ UnmergedRight (MergerType t1 t2)) =>
+    Merger (DiscardRightHead h1 t1 h2 t2) where
+    type Merged (DiscardRightHead h1 t1 h2 t2) = h1 :* Merged (MergerType t1 t2)
+    type UnmergedLeft (DiscardRightHead h1 t1 h2 t2) = h1 :* t1
+    type UnmergedRight (DiscardRightHead h1 t1 h2 t2) = h2 :* t2
+    mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 t2) t1 t2
+
+instance
+    (Mergeable t1 (h2 :* t2),
+     Merger (MergerType t1 (h2 :* t2)),
+     t1 ~ UnmergedLeft (MergerType t1 (h2 :* t2)),
+     (h2 :* t2) ~ UnmergedRight (MergerType t1 (h2 :* t2))) =>
+    Merger (LeftHeadFirst h1 t1 h2 t2) where
+    type Merged (LeftHeadFirst h1 t1 h2 t2) = h1 :* Merged (MergerType t1 (h2 :* t2))
+    type UnmergedLeft (LeftHeadFirst h1 t1 h2 t2) = h1 :* t1
+    type UnmergedRight (LeftHeadFirst h1 t1 h2 t2) = h2 :* t2
+    mkMerge _ (h1 :* t1) (h2 :* t2) = h1 :* mkMerge (merger t1 (h2 :* t2)) t1 (h2 :* t2)
+
+instance
+    (Mergeable (h1 :* t1) t2,
+     Merger (MergerType (h1 :* t1) t2),
+     (h1 :* t1) ~ UnmergedLeft (MergerType (h1 :* t1) t2),
+     t2 ~ UnmergedRight (MergerType (h1 :* t1) t2)) =>
+    Merger (RightHeadFirst h1 t1 h2 t2) where
+    type Merged (RightHeadFirst h1 t1 h2 t2) = h2 :* Merged (MergerType (h1 :* t1) t2)
+    type UnmergedLeft (RightHeadFirst h1 t1 h2 t2) = h1 :* t1
+    type UnmergedRight (RightHeadFirst h1 t1 h2 t2) = h2 :* t2
+    mkMerge _ (h1 :* t1) (h2 :* t2) = h2 :* mkMerge (merger (h1 :* t1) t2) (h1 :* t1) t2
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Infix.hs b/testsuite/tests/indexed-types/should_compile/Infix.hs
new file mode 100644
index 0000000000..dee389331b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Infix.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, TypeOperators #-}
+
+-- Test infix type constructors in type families
+
+module Infix where
+
+type family x :+: y
+type instance Int :+: Int = Int
+
diff --git a/testsuite/tests/indexed-types/should_compile/InstContextNorm.hs b/testsuite/tests/indexed-types/should_compile/InstContextNorm.hs
new file mode 100644
index 0000000000..329756aa9c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/InstContextNorm.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
+{-# LANGUAGE EmptyDataDecls, FlexibleInstances #-}
+
+module InstContextNorm
+where
+
+data EX _x _y (p :: * -> *)
+data ANY
+
+class Base p
+
+class Base (Def p) => Prop p where
+ type Def p
+
+instance Base ()
+instance Prop () where
+ type Def () = ()
+
+instance (Base (Def (p ANY))) => Base (EX _x _y p)
+instance (Prop (p ANY)) => Prop (EX _x _y p) where
+ type Def (EX _x _y p) = EX _x _y p
+
+
+data FOO x
+
+instance Prop (FOO x) where
+ type Def (FOO x) = ()
+
+data BAR
+
+instance Prop BAR where
+ type Def BAR = EX () () FOO
+  
+  -- Needs Base (Def BAR)
+  -- And (Def Bar = Ex () () FOO)
+  -- so we need Base (Def (Foo ANY))
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/InstEqContext.hs b/testsuite/tests/indexed-types/should_compile/InstEqContext.hs
new file mode 100644
index 0000000000..e178e110a5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/InstEqContext.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module InstEqContext  where 
+
+
+{- encoding of 
+ -	class C a | -> a
+ -}
+class a ~ Int => C a 
+
+instance C Int
+
+unC :: (C a) => a -> Int
+unC i = undefined
+
+test :: Int
+test = unC undefined
diff --git a/testsuite/tests/indexed-types/should_compile/InstEqContext2.hs b/testsuite/tests/indexed-types/should_compile/InstEqContext2.hs
new file mode 100644
index 0000000000..c5d017a644
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/InstEqContext2.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
+
+module InstEqContext2  where 
+
+data E v a = E a
+data RValue
+
+instance (Eq a, v ~ RValue) => Eq (E v a) where
+    E x == E y  =  x == y
+
+a :: E v Int
+a = undefined
+
+foo = a == a
+
diff --git a/testsuite/tests/indexed-types/should_compile/InstEqContext3.hs b/testsuite/tests/indexed-types/should_compile/InstEqContext3.hs
new file mode 100644
index 0000000000..3f307f8941
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/InstEqContext3.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module InstEqContext  where 
+
+
+{- encoding of 
+ -	class C a | -> a
+ - with extra indirection
+ -}
+class a ~ Int => D a 
+instance D Int
+
+class D a => C a 
+instance C Int
+
+unC :: (C a) => a -> Int
+unC i = undefined
+
+test :: Int
+test = unC undefined
diff --git a/testsuite/tests/indexed-types/should_compile/Kind.hs b/testsuite/tests/indexed-types/should_compile/Kind.hs
new file mode 100644
index 0000000000..73c528df11
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Kind.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Kind where
+
+class C (a :: * -> *) where
+  type T a
+
+foo :: a x -> T a
+foo = undefined
+
diff --git a/testsuite/tests/indexed-types/should_compile/Makefile b/testsuite/tests/indexed-types/should_compile/Makefile
new file mode 100644
index 0000000000..a5dfe03de8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Makefile
@@ -0,0 +1,15 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
+
+NewTyCo:
+	$(RM) NewTyCo1.o NewTyCo1.hi NewTyCo2.o NewTyCo2.hi
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c NewTyCo1.hs
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c NewTyCo2.hs
+
+.PHONY: IndTypesPerf
+IndTypesPerf:
+	$(RM) IndTypesPerf.o IndTypesPerf.hi
+	$(RM) IndTypesPerfMerge.o IndTypesPerfMerge.hi
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c IndTypesPerfMerge.hs +RTS -M20M
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c IndTypesPerf.hs      +RTS -M20M
diff --git a/testsuite/tests/indexed-types/should_compile/NewTyCo1.hs b/testsuite/tests/indexed-types/should_compile/NewTyCo1.hs
new file mode 100644
index 0000000000..9af6d9ee92
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/NewTyCo1.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module NewTyCo1 where
+
+data family T a
+newtype instance T Int = TInt Int
+
+foo :: T Int -> Int
+foo (TInt n) = n
diff --git a/testsuite/tests/indexed-types/should_compile/NewTyCo2.hs b/testsuite/tests/indexed-types/should_compile/NewTyCo2.hs
new file mode 100644
index 0000000000..6ff2bc1ecd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/NewTyCo2.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module NewTyCo2 where
+
+import NewTyCo1
+
+bar x = foo x + 1
diff --git a/testsuite/tests/indexed-types/should_compile/NonLinearLHS.hs b/testsuite/tests/indexed-types/should_compile/NonLinearLHS.hs
new file mode 100644
index 0000000000..dc0ae5392a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/NonLinearLHS.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls, FlexibleContexts #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-}
+
+module NonLinearLHS where
+
+type family E a b
+type instance E a a = [a]
+
+foo :: E [Int] (E Int Int) -> Int
+foo = sum . concat
+
+data family F a b
+data instance F a a = MkF [a] 
+
+goo :: F Int Int -> F Bool Bool
+goo (MkF xs) = MkF $ map odd xs
+
+
+-- HList-like type equality
+
+data True; data False;
+
+type family EqTy a b
+type instance EqTy a a = True
+
+class EqTyP a b result
+instance (EqTy a b ~ isEq, Proxy isEq result) => EqTyP a b result
+
+class Proxy inp out
+instance (result ~ True) => Proxy True result
+instance (result ~ False) => Proxy notTrue result
+
+testTrue :: EqTyP Int Int r => r
+testTrue = undefined
+
+testFalse :: EqTyP Int Bool r => r
+testFalse = undefined
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Numerals.hs b/testsuite/tests/indexed-types/should_compile/Numerals.hs
new file mode 100644
index 0000000000..17fb30c3ca
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Numerals.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Numerals
+where
+
+data Z          -- empty data type
+data S a        -- empty data type
+
+data SNat n where  -- natural numbers as singleton type
+  Zero :: SNat Z
+  Succ :: SNat n -> SNat (S n)
+
+zero  = Zero
+one   = Succ zero
+two   = Succ one
+three = Succ two
+-- etc...we really would like some nicer syntax here
+
+type family (:+:) n m :: *
+type instance Z     :+: m = m
+type instance (S n) :+: m = S (n :+: m)
+
+add :: SNat n -> SNat m -> SNat (n :+: m)
+add Zero     m = m
+add (Succ n) m = Succ (add n m)
+
diff --git a/testsuite/tests/indexed-types/should_compile/OversatDecomp.hs b/testsuite/tests/indexed-types/should_compile/OversatDecomp.hs
new file mode 100644
index 0000000000..a93256c92c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/OversatDecomp.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+
+module OversatDecomp where
+
+class Blah f a where
+  blah :: a -> T f f a
+
+class A f where
+  type T f :: (* -> *) -> * -> *
+
+wrapper :: Blah f a => a -> T f f a
+wrapper x = blah x
diff --git a/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.hs b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.hs
new file mode 100644
index 0000000000..0117b81d47
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/PushedInAsGivens.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies #-}

+module PushedInAsGivens where 

+

+

+type family F a

+

+

+

+bar y = let foo :: (F Int ~ [a]) => a -> Int 

+            foo x = length [x,y]  

+      in (y,foo y)

+

+

+-- This example demonstrates why we need to push in 

+-- an unsolved wanted as a given and not a given/solved.

+-- [Wanted] F Int ~ [beta]

+--- forall a. F Int ~ [a] => a ~ beta 

+-- We we push in the [Wanted] as given, it will interact and solve the implication

+-- constraint, and finally we quantify over F Int ~ [beta]. If we push it in as

+-- Given/Solved, it will be discarded when we meet the given (F Int ~ [a]) and 

+-- we will not be able to solve the implication constraint.

+

+

+

diff --git a/testsuite/tests/indexed-types/should_compile/Records.hs b/testsuite/tests/indexed-types/should_compile/Records.hs
new file mode 100644
index 0000000000..4a08125e30
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Records.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- See Trac #1204
+
+module ShouldCompile where
+
+data FooC = FooC
+
+data family T c
+data instance T FooC = MkT { moo :: Int }
+
+t1 :: Int -> T FooC
+t1 i = MkT { moo = i }
+
+t2 :: T FooC -> Int
+t2 (MkT { moo = i }) = i
+
+t3 :: T FooC -> Int
+t3 m = moo m
+
+f :: T FooC -> T FooC
+f r = r { moo = 3 }
+
+
+------------------------------------------------------------------------------
+class D c where
+  data D1 c
+  works :: Int -> D1 c -> D1 c
+  buggy :: Int -> D1 c -> D1 c 
+  buggy2 :: Int -> D1 c -> D1 c
+
+instance D FooC where
+  data D1 FooC = D1F { noo :: Int }
+
+  works x d = d  -- d unchanged, so OK
+
+  buggy x d@(D1F { noo = k }) = 
+    d { noo = k + x }
+
+  buggy2 x d@(D1F { noo = k }) =
+    (d :: D1 FooC) { noo = k + x }
diff --git a/testsuite/tests/indexed-types/should_compile/Refl.hs b/testsuite/tests/indexed-types/should_compile/Refl.hs
new file mode 100644
index 0000000000..0b1b1f7a36
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Refl.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Refl where
+
+type family T a :: * -> *
+
+foo :: a x -> a y
+foo = undefined
+
+bar :: a -> T a x -> T a y
+bar x t = foo t
+
+{- GHC complains that it could not deduce (T a x ~ T a x) where problem is
+that with -dppr-debug, we get "x{tv a7z} [sk]" on the lhs and "x{tv a7C}
+[box]" on the rhs
+ -}
+
diff --git a/testsuite/tests/indexed-types/should_compile/Refl2.hs b/testsuite/tests/indexed-types/should_compile/Refl2.hs
new file mode 100644
index 0000000000..b6f5d056b5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Refl2.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Refl2 where
+
+type family T (a :: * -> *) :: * -> *
+
+data U a x = U (T a x)
+
+mkU :: a x -> U a x
+mkU x = U undefined
+
+-- The first definition says "Could not deduce (T a x ~ T a x)", the other two
+-- work fine
+
+foo :: a x -> U a x
+foo x = case mkU x of U t -> id (U t)
+-- foo x = case mkU x of U t -> id ((U :: T a x -> U a x) t)
+-- foo x = case mkU x of U t -> U t
+
diff --git a/testsuite/tests/indexed-types/should_compile/RelaxedExamples.hs b/testsuite/tests/indexed-types/should_compile/RelaxedExamples.hs
new file mode 100644
index 0000000000..a58fb3da67
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/RelaxedExamples.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module RelaxedExamples where
+
+type family F1 a
+type family F2 a
+type family F3 a
+type family F4 a
+
+type instance F1 x      = x
+type instance F2 [Bool] = F2 Char
+type instance F3 (a, b) = (F3 a, F3 b)
+type instance F4 x      = (x, x)
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Roman1.hs b/testsuite/tests/indexed-types/should_compile/Roman1.hs
new file mode 100644
index 0000000000..491fee04c5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Roman1.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE TypeFamilies, Rank2Types #-}
+
+-- This test made the type checker produce an
+-- ill-kinded coercion term.
+
+module Roman where
+
+import Control.Monad.ST
+
+type family Mut (v :: * -> *) :: * -> * -> *
+type family State (m :: * -> *)
+type instance State (ST s) = s
+
+unsafeFreeze :: Mut v (State (ST s)) a -> ST s (v a)
+unsafeFreeze = undefined
+
+new :: (forall v s. ST s (v s a)) -> v a
+new p = runST (do
+                 mv <- p
+                 unsafeFreeze mv)
+
+---------------------------------------------
+-- Here's a simpler version that also failed
+
+type family FMut :: * -> *	-- No args	
+     	    	     		-- Same thing happens with one arg
+
+type family   FState (m :: *)
+type instance FState Char = Int
+
+funsafeFreeze :: FMut (FState Char) -> ()
+funsafeFreeze = undefined
+
+flop :: forall mv. mv Int
+flop = undefined
+
+noo =  flop `rapp` funsafeFreeze
+
+rapp :: a -> (a->()) -> ()
+rapp arg fun = fun arg
+
diff --git a/testsuite/tests/indexed-types/should_compile/Rules1.hs b/testsuite/tests/indexed-types/should_compile/Rules1.hs
new file mode 100644
index 0000000000..497c5bbeb9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Rules1.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Rules1 where
+
+class C a where
+  data T a
+
+instance (C a, C b) => C (a,b) where
+  data T (a,b) = TPair (T a) (T b)
+
+mapT :: (C a, C b) => (a -> b) -> T a -> T b
+mapT = undefined
+
+zipT :: (C a, C b) => T a -> T b -> T (a,b)
+zipT = undefined
+
+{-# RULES
+
+"zipT/mapT" forall f x y.
+  zipT (mapT f x) y = mapT (\(x,y) -> (f x, y)) (zipT x y)
+
+ #-}
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple1.hs b/testsuite/tests/indexed-types/should_compile/Simple1.hs
new file mode 100644
index 0000000000..e442042bb1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple1.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+class C a where
+  data Sd a :: *
+  data Sn a :: *
+  type St a :: *
+
+instance C Int where
+  data    Sd Int = SdC Char
+  newtype Sn Int = SnC Char
+  type    St Int = Char
diff --git a/testsuite/tests/indexed-types/should_compile/Simple10.hs b/testsuite/tests/indexed-types/should_compile/Simple10.hs
new file mode 100644
index 0000000000..2e6aacf510
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple10.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple10 where
+
+type family T a
+
+foo, bar :: T a -> a
+foo = undefined
+bar x = foo x
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple11.hs b/testsuite/tests/indexed-types/should_compile/Simple11.hs
new file mode 100644
index 0000000000..2d507a728e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple11.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple11 where
+
+type family F a
+
+same :: a -> a -> a
+same = undefined
+
+mkf :: a -> F a
+mkf p = undefined
+
+-- Works with explicit signature
+-- foo :: a -> a -> (F a, a)
+foo p q = same (mkf p, p) (mkf q, q)
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple12.hs b/testsuite/tests/indexed-types/should_compile/Simple12.hs
new file mode 100644
index 0000000000..c425d78db5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple12.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple12 where
+
+type family F a
+
+same :: a -> a -> a
+same = undefined
+
+mkf :: a -> F a
+mkf p = undefined
+
+-- works with either of these signatures
+-- foo :: a ~ F a => a -> a
+-- foo :: a ~ F a => a -> F a
+foo p = same p (mkf p)
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple13.hs b/testsuite/tests/indexed-types/should_compile/Simple13.hs
new file mode 100644
index 0000000000..7633f01f98
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple13.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- This should fail, I think, because of the loopy equality,
+-- but the error message is hopeless
+
+module Simple13 where
+
+type family F a
+
+same :: a -> a -> a
+same = undefined
+
+mkf :: a -> [F a]
+mkf p = undefined
+
+foo :: a ~ [F a] => a -> a
+foo p = same p (mkf p)
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.hs b/testsuite/tests/indexed-types/should_compile/Simple14.hs
new file mode 100644
index 0000000000..16158d9714
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}
+
+module Simple14 where
+
+data EQ_ x y = EQ_
+
+eqE :: EQ_ x y -> (x~y => EQ_ z z) -> p
+eqE = undefined
+
+eqI :: EQ_ x x
+eqI = undefined
+
+ntI :: (forall p. EQ_ x y -> p) -> EQ_ x y
+ntI = undefined
+
+foo :: forall m n. EQ_ (Maybe m) (Maybe n)
+foo = ntI (`eqE` (eqI :: EQ_ m n))
+-- Alternative
+-- foo = ntI (\eq -> eq `eqE` (eqI :: EQ_ m n))
+
+-- eq :: EQ_ (Maybe m) (Maybe n)
+-- Need (Maybe m ~ Maybe n) =>  EQ_ m n ~ EQ_ zeta zeta
+-- which redues to (m~n) => m ~ zeta
+-- but then we are stuck
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Simple14.stderr b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
new file mode 100644
index 0000000000..a5250d556f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple14.stderr
@@ -0,0 +1,13 @@
+
+Simple14.hs:17:12:
+    Couldn't match type `z0' with `n'
+      `z0' is untouchable
+           inside the constraints (Maybe m ~ Maybe n)
+           bound at a type expected by the context:
+                      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
+    In the second argument of `eqE', namely `(eqI :: EQ_ m n)'
+    In the first argument of `ntI', namely `(`eqE` (eqI :: EQ_ m n))'
+    In the expression: ntI (`eqE` (eqI :: EQ_ m n))
diff --git a/testsuite/tests/indexed-types/should_compile/Simple15.hs b/testsuite/tests/indexed-types/should_compile/Simple15.hs
new file mode 100644
index 0000000000..8a28d27b6f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple15.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple15 where
+
+(<$) :: p -> (p -> q) -> q
+x <$ f = f x
+
+type family Def p
+
+def :: Def p -> p
+def = undefined
+
+data EQU a b = EQU
+
+equ_refl :: EQU a a
+equ_refl = EQU
+
+data FOO = FOO
+type instance Def FOO = EQU () ()
+
+foo :: FOO
+foo = equ_refl <$ def
+-- This works:
+-- foo = def $ equ_refl
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple16.hs b/testsuite/tests/indexed-types/should_compile/Simple16.hs
new file mode 100644
index 0000000000..f1958c3ffd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple16.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+-- submitted by g9ks157k@acme.softbase.org as #1713
+module TypeFamilyBug where
+
+type family TestFamily a :: *
+
+type instance TestFamily () = [()]
+
+testFunction :: value -> TestFamily value -> ()
+testFunction = const (const ())
+
+testApplication :: ()
+testApplication = testFunction () (return ())
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Simple17.hs b/testsuite/tests/indexed-types/should_compile/Simple17.hs
new file mode 100644
index 0000000000..4e812be0fe
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple17.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+module Simple17 where
+
+foo :: Int -> Int
+foo n = bar n
+  where
+    bar :: t ~ Int => Int -> t
+    bar n = n
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple18.hs b/testsuite/tests/indexed-types/should_compile/Simple18.hs
new file mode 100644
index 0000000000..c7d94c4984
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple18.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple18 where
+
+type family F a
+
+type instance F Int = [Int]
+
+foo :: F Int
+foo = [1]
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Simple19.hs b/testsuite/tests/indexed-types/should_compile/Simple19.hs
new file mode 100644
index 0000000000..d738b0bd85
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple19.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies, LiberalTypeSynonyms #-}
+                           -- ^ crucial for exercising the code paths to be
+                           --   tested here
+
+module ShouldCompile where
+
+type family Element c :: *
+
+f :: Element x
+f = undefined
diff --git a/testsuite/tests/indexed-types/should_compile/Simple2.hs b/testsuite/tests/indexed-types/should_compile/Simple2.hs
new file mode 100644
index 0000000000..2dc673f58b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple2.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+class C3 a where
+  data S3  a		-- kind is optional
+  data S3n a		-- kind is optional
+  foo3  :: a -> S3 a
+  foo3n :: a -> S3n a
+  bar3  :: S3 a -> a
+  bar3n :: S3n a -> a
+
+instance C3 Int where
+  data    S3  Int  = D3Int
+  newtype S3n Int  = D3Intn ()
+  foo3  _          = D3Int
+  foo3n _          = D3Intn ()
+  bar3  D3Int      = 1
+  bar3n (D3Intn _) = 1
+
+instance C3 Char where
+  data S3 Char = D3Char
+  foo3 _       = D3Char
+  bar3 D3Char  = 'c'
+
+bar3' :: S3 Char -> Char
+bar3' D3Char = 'a'
+
+instance C3 Bool where
+  data S3 Bool = S3_1 | S3_2
+  foo3 False = S3_1
+  foo3 True  = S3_2
+  bar3 S3_1 = False
+  bar3 S3_2 = True
+
+-- It's ok to omit ATs in instances, as it is ok to omit method definitions,
+-- but similar to methods, "undefined" is the only inhabitant of these types,
+-- then.
+instance C3 Float where
+  foo3 1.0 = undefined
+  bar3 _   = 1.0
diff --git a/testsuite/tests/indexed-types/should_compile/Simple2.stderr b/testsuite/tests/indexed-types/should_compile/Simple2.stderr
new file mode 100644
index 0000000000..e2d5ce6973
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple2.stderr
@@ -0,0 +1,40 @@
+
+Simple2.hs:21:1:
+    Warning: No explicit AT declaration for `S3n'
+    In the instance declaration for `C3 Char'
+
+Simple2.hs:21:10:
+    Warning: No explicit method nor default method for `foo3n'
+    In the instance declaration for `C3 Char'
+
+Simple2.hs:21:10:
+    Warning: No explicit method nor default method for `bar3n'
+    In the instance declaration for `C3 Char'
+
+Simple2.hs:29:1:
+    Warning: No explicit AT declaration for `S3n'
+    In the instance declaration for `C3 Bool'
+
+Simple2.hs:29:10:
+    Warning: No explicit method nor default method for `foo3n'
+    In the instance declaration for `C3 Bool'
+
+Simple2.hs:29:10:
+    Warning: No explicit method nor default method for `bar3n'
+    In the instance declaration for `C3 Bool'
+
+Simple2.hs:39:1:
+    Warning: No explicit AT declaration for `S3'
+    In the instance declaration for `C3 Float'
+
+Simple2.hs:39:1:
+    Warning: No explicit AT declaration for `S3n'
+    In the instance declaration for `C3 Float'
+
+Simple2.hs:39:10:
+    Warning: No explicit method nor default method for `foo3n'
+    In the instance declaration for `C3 Float'
+
+Simple2.hs:39:10:
+    Warning: No explicit method nor default method for `bar3n'
+    In the instance declaration for `C3 Float'
diff --git a/testsuite/tests/indexed-types/should_compile/Simple20.hs b/testsuite/tests/indexed-types/should_compile/Simple20.hs
new file mode 100644
index 0000000000..81a8522804
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple20.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+type family F a 
+type instance F [a] = [F a]
+
+foo :: (F [a] ~ a) => a
+foo = undefined
diff --git a/testsuite/tests/indexed-types/should_compile/Simple20.stderr b/testsuite/tests/indexed-types/should_compile/Simple20.stderr
new file mode 100644
index 0000000000..6c8feeb75b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple20.stderr
@@ -0,0 +1,4 @@
+
+Simple20.hs:9:1:
+    Warning: Dropping loopy given equality `[F a] ~ a'
+    When generalising the type(s) for `foo'
diff --git a/testsuite/tests/indexed-types/should_compile/Simple21.hs b/testsuite/tests/indexed-types/should_compile/Simple21.hs
new file mode 100644
index 0000000000..e858ae3ba9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple21.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+import Prelude hiding (foldr, foldr1)
+
+import Data.Maybe
+
+type family Elem x
+
+class Foldable a where
+  foldr :: (Elem a -> b -> b) -> b -> a -> b
+
+  foldr1 :: (Elem a -> Elem a -> Elem a) -> a -> Elem a
+  foldr1 f xs = fromMaybe (error "foldr1: empty structure")
+                  (foldr mf Nothing xs)
+     where mf x Nothing  = Just x
+           mf x (Just y) = Just (f x y)
diff --git a/testsuite/tests/indexed-types/should_compile/Simple22.hs b/testsuite/tests/indexed-types/should_compile/Simple22.hs
new file mode 100644
index 0000000000..dd0a558c4f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple22.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+data X1 = X1
+
+class C t where
+    type D t
+    f :: t -> D t -> ()
+
+instance C X1 where
+    type D X1 = Bool -> Bool
+    f _ h = ()
+
+foo = f X1 (\x -> x)
diff --git a/testsuite/tests/indexed-types/should_compile/Simple23.hs b/testsuite/tests/indexed-types/should_compile/Simple23.hs
new file mode 100644
index 0000000000..b7d5ee4ccb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple23.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+plus :: (a ~ (Int -> Int)) => Int -> a
+plus x y = x + y
diff --git a/testsuite/tests/indexed-types/should_compile/Simple24.hs b/testsuite/tests/indexed-types/should_compile/Simple24.hs
new file mode 100644
index 0000000000..de33458bc7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple24.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleContexts #-}
+
+module Simple24 where
+
+linear :: HasTrie (Basis v) => (Basis v, v)
+linear =  basisValue
+ 
+class HasTrie a where
+ 
+type family Basis u :: *
+ 
+basisValue :: (Basis v,v)
+basisValue = error "urk"
diff --git a/testsuite/tests/indexed-types/should_compile/Simple3.hs b/testsuite/tests/indexed-types/should_compile/Simple3.hs
new file mode 100644
index 0000000000..aa37ac215d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple3.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
+
+module ShouldCompile where
+
+class C7 a b where
+  data S7 b :: *
+
+instance C7 Char (a, Bool) where
+  data S7 (a, Bool) = S7_1
diff --git a/testsuite/tests/indexed-types/should_compile/Simple4.hs b/testsuite/tests/indexed-types/should_compile/Simple4.hs
new file mode 100644
index 0000000000..bd8ae3d66a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple4.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+class C8 a where
+  data S8 a :: * -> *
+
+instance C8 Int where
+  data S8 Int a = S8Int a
diff --git a/testsuite/tests/indexed-types/should_compile/Simple5.hs b/testsuite/tests/indexed-types/should_compile/Simple5.hs
new file mode 100644
index 0000000000..ecae60d53d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple5.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+data family C9 a b :: *
+data instance C9 Int Int = C9IntInt
+data instance C9 [a] Int = C9ListInt
+data instance C9 [Int] [a]   = C9ListList2
+
+type family D a
+type instance D (Int, a) = (Int, a)
+type instance D (a, Int) = (Int, Int)
+
+type family E a
+type instance E (Char, b) = ([Char], b)
+type instance E (a, Int)  = (String, Int)
diff --git a/testsuite/tests/indexed-types/should_compile/Simple6.hs b/testsuite/tests/indexed-types/should_compile/Simple6.hs
new file mode 100644
index 0000000000..ead121ab2d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple6.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+import Data.IORef
+
+data family T a
+data instance T a = T
+
+foo :: T Int -> T Char
+foo T = T
+
+type family S a
+type instance S a = a
+
+type family SMRef (m:: * -> *) :: * -> *
+type instance SMRef IO = IORef 
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/Simple7.hs b/testsuite/tests/indexed-types/should_compile/Simple7.hs
new file mode 100644
index 0000000000..61ba22117f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple7.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+class C1 a where
+  data S1 a :: *
+
+-- instance of data families can be data or newtypes
+instance C1 Char where
+  newtype S1 Char = S1Char ()
diff --git a/testsuite/tests/indexed-types/should_compile/Simple8.hs b/testsuite/tests/indexed-types/should_compile/Simple8.hs
new file mode 100644
index 0000000000..f819763579
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple8.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple8 where
+
+type family F a
+
+-- Manuel says that duplicate instances are ok. This gives a strange error but
+-- works if one of the duplicates is removed.
+
+type instance F () = ()
+type instance F () = ()
+
+foo :: F () -> ()
+foo x = x
+
diff --git a/testsuite/tests/indexed-types/should_compile/Simple9.hs b/testsuite/tests/indexed-types/should_compile/Simple9.hs
new file mode 100644
index 0000000000..4075d4845f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/Simple9.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple9 where
+
+-- The test succeeds with
+--
+-- type family F a b
+-- type instance F () b = Maybe b
+
+type family F a :: * -> *
+type instance F () = Maybe
+
+type family G a
+type instance G (Maybe a) = Int
+
+foo :: G (F () a) -> Int
+foo x = x
+
diff --git a/testsuite/tests/indexed-types/should_compile/T1769.hs b/testsuite/tests/indexed-types/should_compile/T1769.hs
new file mode 100644
index 0000000000..57b966051b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T1769.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving, DeriveDataTypeable, FlexibleInstances #-}

+

+module T1769 where

+

+import Data.Typeable

+

+data family T a

+deriving instance Typeable1 T

+-- deriving instance Functor T

+

+data instance T [b] = T1 | T2 b 

+deriving instance Eq b => Eq (T [b])

diff --git a/testsuite/tests/indexed-types/should_compile/T1981.hs b/testsuite/tests/indexed-types/should_compile/T1981.hs
new file mode 100644
index 0000000000..658821ea73
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T1981.hs
@@ -0,0 +1,8 @@
+{-# OPTIONS_GHC -XTypeFamilies #-}
+
+module ShouldCompile where
+
+type family T a
+
+f :: T a -> Int
+f x = x `seq` 3
diff --git a/testsuite/tests/indexed-types/should_compile/T2102.hs b/testsuite/tests/indexed-types/should_compile/T2102.hs
new file mode 100644
index 0000000000..6283b18071
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2102.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
+
+module T2102 where
+
+type family Cat ts0 ts
+type instance Cat ()      ts' = ts'
+type instance Cat (s, ts) ts' = (s, Cat ts ts')
+
+class (Cat ts () ~ ts) => Valid ts
+instance Valid () -- compiles OK
+instance Valid ts => Valid (s, ts) -- fails to compile
+
+-- need to prove Cat (s, ts) () ~ (s, Cat ts ())
+-- for the superclass of class Valid.
+-- (1) From Valid ts: Cat ts () ~ ts
+-- (2) Therefore:     (s, Cat ts ()) ~ (s, ts)
+
+coerce :: forall f ts. Valid ts => f (Cat ts ()) -> f ts
+coerce x = x
diff --git a/testsuite/tests/indexed-types/should_compile/T2203b.hs b/testsuite/tests/indexed-types/should_compile/T2203b.hs
new file mode 100644
index 0000000000..74517aeadd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2203b.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}
+
+module T2203b where
+
+class Foo a where
+   type TheFoo a
+   foo :: TheFoo a -> a
+   foo' :: a -> Int
+
+class Bar b where
+   bar :: b -> Int
+
+instance (b ~ TheFoo a, Foo a) => Bar (Either a b) where
+   bar (Left a) = foo' a
+   bar (Right b) = foo' (foo b :: a)
+
+instance Foo Int where
+   type TheFoo Int = Int
+   foo = id
+   foo' = id
+
+val :: Either Int Int
+val = Left 5
+
+res :: Int
+res = bar val
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/T2219.hs b/testsuite/tests/indexed-types/should_compile/T2219.hs
new file mode 100644
index 0000000000..ea7d442f74
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2219.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators #-}
+
+module Test where
+
+data Zero
+data Succ a
+
+data FZ
+data FS fn
+
+data Fin n fn where
+  FZ :: Fin (Succ n) FZ
+  FS :: Fin n fn -> Fin (Succ n) (FS fn)
+
+data Nil
+data a ::: b
+
+type family Lookup ts fn :: *
+type instance Lookup (t ::: ts) FZ = t
+type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn
+
+data Tuple n ts where
+  Nil   :: Tuple Zero Nil
+  (:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)
+
+proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
+proj FZ      (v ::: _)  = v
+proj (FS fn) (_ ::: vs) = proj fn vs
diff --git a/testsuite/tests/indexed-types/should_compile/T2238.hs b/testsuite/tests/indexed-types/should_compile/T2238.hs
new file mode 100644
index 0000000000..8e77283d77
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2238.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+-- Trac #2238
+-- Notice that class CTF has just one value field, but
+-- it also has an equality predicate. 
+-- See Note [Class newtypes and equality predicates] in BuildTyCl
+
+module Foo where
+
+data A
+data B
+
+-- via functional dependencies
+
+class HowFD a how | a -> how
+
+class HowFD a how => CFD a how where
+  cfd :: a -> String
+  cfd _ = "cfd"
+instance HowFD a how => CFD a how
+
+instance HowFD Bool A
+
+-- via type families
+
+type family HowTF a
+
+class how ~ HowTF a => CTF a how where
+  ctf :: a -> String
+  ctf _ = "ctf"
+
+instance how ~ HowTF a => CTF a how
+
+type instance HowTF Bool = A
diff --git a/testsuite/tests/indexed-types/should_compile/T2291.hs b/testsuite/tests/indexed-types/should_compile/T2291.hs
new file mode 100644
index 0000000000..a6832b60ad
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2291.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+module Small where
+
+class CoCCC k where
+        type Coexp k :: * -> * -> *
+        type Sum k :: * -> * -> *
+        coapply :: k b (Sum k (Coexp k a b) a)
+        cocurry :: k c (Sum k a b) -> k (Coexp k b c) a
+        uncocurry :: k (Coexp k b c) a -> k c (Sum k a b)
+
+{-# RULES
+"cocurry coapply"               cocurry coapply = id
+"cocurry . uncocurry"           cocurry . uncocurry = id
+"uncocurry . cocurry"           uncocurry . cocurry = id
+ #-}
diff --git a/testsuite/tests/indexed-types/should_compile/T2448.hs b/testsuite/tests/indexed-types/should_compile/T2448.hs
new file mode 100644
index 0000000000..806df3ff4c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2448.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+
+module T2448 where
+
+-- Demonstrates a bug in propagating type equality constraints
+
+class VectorSpace v where
+  type Scalar v :: *
+
+class VectorSpace v => InnerSpace v
+
+instance (VectorSpace u,VectorSpace v, Scalar u ~ Scalar v) => 
+  VectorSpace (u,v) 
+  where
+  type Scalar (u,v) = Scalar u
+
+instance (InnerSpace u,InnerSpace v, Scalar u ~ Scalar v) => InnerSpace (u,v)
diff --git a/testsuite/tests/indexed-types/should_compile/T2627.hs b/testsuite/tests/indexed-types/should_compile/T2627.hs
new file mode 100644
index 0000000000..6a29d611e5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2627.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}
+
+module T2627 where
+
+data R a b
+data W a b
+data Z
+
+type family Dual a
+type instance Dual Z = Z
+type instance Dual (R a b) = W a (Dual b)
+type instance Dual (W a b) = R a (Dual b)
+
+data Comm a where
+    Rd :: (a -> Comm b) -> Comm (R a b)
+    Wr :: a  -> Comm b  -> Comm (W a b)
+    Fin :: Int -> Comm Z
+
+conn :: (Dual a ~ b, Dual b ~ a) => Comm a -> Comm b -> (Int, Int)
+conn (Fin x) (Fin y) = (x,y)
+conn (Rd k) (Wr a r) = conn (k a) r
+conn (Wr a r) (Rd k) = conn r (k a)
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/T2639.hs b/testsuite/tests/indexed-types/should_compile/T2639.hs
new file mode 100644
index 0000000000..43e6c98a1d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2639.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
+
+module T2639 where
+
+data Eps
+
+data family Work a v
+data instance Work Eps v = Eps v
+
+type family Dual a
+type instance Dual Eps = Eps
+
+class Connect s where
+    connect :: (Dual s ~ c, Dual c ~ s) => Work s a -> Work c b -> (a,b)
+
+instance Connect Eps where
+    connect (Eps a) (Eps b) = (a,b)
diff --git a/testsuite/tests/indexed-types/should_compile/T2715.hs b/testsuite/tests/indexed-types/should_compile/T2715.hs
new file mode 100644
index 0000000000..0fae15eaf8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2715.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
+
+module T2715 where
+
+data Interval v where
+   Intv :: (Ord v, Enum v) => (v,v) -> Interval v
+
+type family Domain (d :: * -> *) :: * -> *
+type instance Domain Interval = Interval 
+
+type family Value (d :: * -> *) :: *
+
+
+class IDomain d where
+   empty   :: (Ord (Value d), Enum (Value d)) => (Domain d) (Value d)
+
+class (IDomain d1) -- (IDomain d1, IDomain d2, Value d1 ~ Value d2) 
+   => IIDomain (d1 :: * -> *) (d2 :: * -> * ) where
+   equals  :: Domain d1 (Value d1) -> Domain d2 (Value d2) -> Bool
+
+
+instance Ord (Value Interval) 
+      => IDomain Interval where
+   empty                   = Intv (toEnum 1, toEnum 0)
+
+instance Ord (Value Interval) 
+      => IIDomain Interval Interval where
+   equals  (Intv ix) (Intv iy) = ix == iy
diff --git a/testsuite/tests/indexed-types/should_compile/T2767.hs b/testsuite/tests/indexed-types/should_compile/T2767.hs
new file mode 100644
index 0000000000..7104db2fa3
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2767.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeFamilies, NoMonomorphismRestriction #-}
+
+module T2767a where
+
+main = return ()
+
+-- eval' :: Solver solver => Tree solver a -> [(Label solver,Tree solver a)] -> solver [a]
+eval' (NewVar f) wl = do v <- newvarSM
+                         eval' (f v) wl
+eval' Fail       wl = continue wl
+
+-- continue :: Solver solver => [(Label solver,Tree solver a)] -> solver [a] 
+continue ((past,t):wl) = do gotoSM past
+                            eval' t wl
+data Tree s a
+                = Fail
+                | NewVar (Term s -> Tree s a)
+
+class Monad solver => Solver solver where
+        type Term solver        :: *
+        type Label solver       :: *
+        newvarSM        :: solver (Term solver)
+        gotoSM          :: Label solver -> solver ()
diff --git a/testsuite/tests/indexed-types/should_compile/T2850.hs b/testsuite/tests/indexed-types/should_compile/T2850.hs
new file mode 100644
index 0000000000..bdb423b6eb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2850.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, TypeFamilies, FlexibleContexts, FlexibleInstances #-}

+

+module T2850 where

+

+class K a where

+  bar :: a -> a

+

+class K (B a) => M a where

+  data B a :: *

+  foo :: B a -> B a

+

+instance M Bool where

+  data B Bool = B1Bool Bool | B2Bool Bool

+  foo = id

+

+instance K (B Bool) where

+  bar = id

+

+instance M Int where

+  newtype B Int = BInt (B Bool) deriving K

+  foo = id

diff --git a/testsuite/tests/indexed-types/should_compile/T2944.hs b/testsuite/tests/indexed-types/should_compile/T2944.hs
new file mode 100644
index 0000000000..19c009b0f9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T2944.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+-- Test Trac #2944
+
+module T2944 where
+
+type family T a :: *
+
+f1 :: T a ~ () => a
+f1 = f2
+
+f2 :: T a ~ () => a
+f2 = f1
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.hs b/testsuite/tests/indexed-types/should_compile/T3017.hs
new file mode 100644
index 0000000000..8e4e5bd999
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3017.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- Trac #3017
+
+module Foo where
+ class Coll c where
+   type Elem c
+   empty :: c
+   insert :: Elem c -> c -> c
+
+ data ListColl a = L [a]
+ instance Coll (ListColl a) where
+   type Elem (ListColl a) = a
+   empty = L []
+   insert x (L xs) = L (x:xs)
+
+ emptyL :: ListColl a
+ emptyL = empty
+
+ test2 c = insert (0, 0) c
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
new file mode 100644
index 0000000000..5afb822c32
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -0,0 +1,19 @@
+TYPE SIGNATURES
+    emptyL :: forall a. ListColl a
+    test2 :: forall c t t1.
+             (Num t, Num t1, Coll c, Elem c ~ (t, t1)) =>
+             c -> c
+TYPE CONSTRUCTORS
+  data ListColl a
+      RecFlag NonRecursive
+      = L :: forall a. [a] -> ListColl a Stricts: _
+      FamilyInstance: none
+COERCION AXIOMS
+  axiom Foo.TFCo:R:ElemListColl [a]
+    :: Elem (ListColl a) ~ Foo.R:ElemListColl a
+INSTANCES
+  instance Coll (ListColl a) -- Defined at T3017.hs:12:11-27
+FAMILY INSTANCES
+  type Elem (ListColl a) -- Defined at T3017.hs:13:9-12
+Dependent modules: []
+Dependent packages: [base, ghc-prim, integer-gmp]
diff --git a/testsuite/tests/indexed-types/should_compile/T3023.hs b/testsuite/tests/indexed-types/should_compile/T3023.hs
new file mode 100644
index 0000000000..26966daed7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3023.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
+{-# OPTIONS_GHC -fwarn-missing-signatures #-}
+
+module Bug where
+
+class C a b | a -> b, b -> a where
+    f :: a -> b
+
+instance C Int Bool where
+    f = undefined
+instance (C a c, C b d) => C (a -> b) (c -> d) where
+    f = undefined
+
+foo :: Int -> Int
+foo = undefined
+
+bar = f foo
diff --git a/testsuite/tests/indexed-types/should_compile/T3023.stderr b/testsuite/tests/indexed-types/should_compile/T3023.stderr
new file mode 100644
index 0000000000..68066bac91
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3023.stderr
@@ -0,0 +1,4 @@
+
+T3023.hs:17:1:
+    Warning: Top-level binding with no type signature:
+               bar :: Bool -> Bool
diff --git a/testsuite/tests/indexed-types/should_compile/T3208a.hs b/testsuite/tests/indexed-types/should_compile/T3208a.hs
new file mode 100644
index 0000000000..fded5bf55d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3208a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T3208a where
+  
+class SUBST s where
+    type STerm s
+
+class OBJECT o where
+    type OTerm o
+    apply :: (SUBST s, OTerm o ~ STerm s) => s -> o
+
+fce' f = fce . apply $ f
+
+fce f = fce' f
diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.hs b/testsuite/tests/indexed-types/should_compile/T3208b.hs
new file mode 100644
index 0000000000..012756abd1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3208b.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- This should fail
+
+module T3208b where
+  
+class SUBST s where
+    type STerm s
+
+class OBJECT o where
+    type OTerm o
+    apply :: (SUBST s, OTerm o ~ STerm s) => s -> o
+
+fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
+fce' f = fce (apply f)
+-- f :: a
+-- apply f :: (OBJECT a, SUBST a, OTerm o ~ STerm a) => o
+-- fce called with a=o, gives wanted (OTerm o ~ STerm o, OBJECT o, SUBST o)
+
+
+fce :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
+fce f = fce' f
diff --git a/testsuite/tests/indexed-types/should_compile/T3208b.stderr b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
new file mode 100644
index 0000000000..712f732b06
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3208b.stderr
@@ -0,0 +1,22 @@
+
+T3208b.hs:15:10:
+    Could not deduce (STerm a0 ~ STerm a)
+    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
+    NB: `STerm' is a type function, and may not be injective
+    Expected type: STerm a0
+      Actual type: OTerm a0
+    In the expression: fce (apply f)
+    In an equation for `fce'': fce' f = fce (apply f)
+
+T3208b.hs:15:15:
+    Could not deduce (OTerm a0 ~ STerm a)
+    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
+    In the first argument of `fce', namely `(apply f)'
+    In the expression: fce (apply f)
+    In an equation for `fce'': fce' f = fce (apply f)
diff --git a/testsuite/tests/indexed-types/should_compile/T3220.hs b/testsuite/tests/indexed-types/should_compile/T3220.hs
new file mode 100644
index 0000000000..7d6190a7fa
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3220.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE TypeFamilies, ScopedTypeVariables#-}
+
+module T3220 where
+
+class Foo m where
+    type Bar m :: *
+    action :: m -> Bar m -> m
+
+right x m = action m (Right x)
+
+right' :: (Either a b ~ Bar m, Foo m) => b -> m -> m
+right' x m = action m (Right x)
+
+instance Foo Int where
+    type Bar Int = Either Int Int
+    action m a = either (*) (+) a m
+
+instance Foo Float where
+    type Bar Float = Either Float Float
+    action m a = either (*) (+) a m
+
+foo = print $ right (1::Int) (3 :: Int)
+bar = print $ right (1::Float) (3 :: Float)
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/T3418.hs b/testsuite/tests/indexed-types/should_compile/T3418.hs
new file mode 100644
index 0000000000..a0ffaf0aed
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3418.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeFamilies, DatatypeContexts #-}
+module T3418 where
+
+newtype (a ~ b) => S a b = S { unS :: a }
diff --git a/testsuite/tests/indexed-types/should_compile/T3418.stderr b/testsuite/tests/indexed-types/should_compile/T3418.stderr
new file mode 100644
index 0000000000..657e2a07b7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3418.stderr
@@ -0,0 +1,3 @@
+
+T3418.hs:1:28:
+    Warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language.
diff --git a/testsuite/tests/indexed-types/should_compile/T3423.hs b/testsuite/tests/indexed-types/should_compile/T3423.hs
new file mode 100644
index 0000000000..bbca944374
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3423.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, UndecidableInstances, StandaloneDeriving #-}

+{-# LANGUAGE FlexibleInstances #-}

+

+module T3423 where

+

+newtype Trie m k a = Trie (Maybe a, m (SubKey k) (Trie m k a))

+

+type family SubKey k

+type instance SubKey [k] = k

+

+deriving instance (Eq (m k (Trie m [k] a)), Eq a) 

+               => Eq (Trie m [k] a)

diff --git a/testsuite/tests/indexed-types/should_compile/T3460.hs b/testsuite/tests/indexed-types/should_compile/T3460.hs
new file mode 100644
index 0000000000..ea4f59cd6b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3460.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
+module T3460 where
+
+class Nat n where
+    toInt :: n -> Int
+
+class (Nat (Arity f)) => Model f where
+    type Arity f
+
+ok :: Model f => f -> Arity f -> Int
+ok _ n = toInt n
+
+bug :: (Model f, Arity f ~ n) => f -> n -> Int
+bug _ n = toInt n
diff --git a/testsuite/tests/indexed-types/should_compile/T3484.hs b/testsuite/tests/indexed-types/should_compile/T3484.hs
new file mode 100644
index 0000000000..4d1570915e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3484.hs
@@ -0,0 +1,42 @@
+{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, FlexibleContexts, ScopedTypeVariables #-}
+{-# OPTIONS_GHC -Wall #-}
+module Absurd where
+
+data Z = Z
+newtype S n = S n
+class Nat n where
+   caseNat :: (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> n -> r
+instance Nat Z where
+   caseNat = error "urk1"
+instance Nat n => Nat (S n) where
+   caseNat = error "urk2"
+
+-- empty type
+newtype Naught = Naught (forall a. a)
+-- types are equal!
+data TEq a b where
+   TEq :: (a ~ b) => TEq a b
+
+type family NatEqProves m n
+type instance NatEqProves (S m) (S n) = TEq m n
+
+noConf :: (Nat m, Nat n) => m -> TEq m n -> NatEqProves m n
+noConf = undefined
+predEq :: TEq (S a) (S b) -> TEq a b
+predEq = undefined
+
+data IsEq a b = Yes (TEq a b) | No (TEq a b -> Naught)
+
+natEqDec :: forall m n. (Nat m, Nat n) => m -> n -> IsEq m n
+natEqDec m n = caseNat undefined mIsS m where
+    mIsS :: forall pm. (m ~ S pm, Nat pm) => pm -> IsEq m n
+    mIsS pm = caseNat undefined nIsS n where
+        nIsS :: forall pn. (n ~ S pn, Nat pn) => pn -> IsEq m n
+        nIsS pn = case natEqDec pm pn of
+            Yes TEq -> Yes TEq
+            No contr -> No (contr . noConf m)
+--            No contr -> No (contr . predEq)
+
+-- strange things:
+-- (1) commenting out the "Yes" case or changing it to "undefined" makes compilation succeed
+-- (2) replacing the "No" line with with the commented out "No" line makes compilation succeed
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_compile/T3590.hs b/testsuite/tests/indexed-types/should_compile/T3590.hs
new file mode 100644
index 0000000000..1b4ba426aa
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3590.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
+
+-- Trac #3590: a bug in typechecking of sections
+
+module T3590 where
+
+newtype ListT m a =
+  ListT { runListT :: m (Maybe (a, ListT m a)) }
+
+class Monad (ItemM l) => List l where
+  type ItemM l :: * -> *
+  joinL :: [ItemM l (l a) -> l a]
+
+instance Monad m => List (ListT m) where
+  type ItemM (ListT m) = m
+  joinL = [ ListT . (>>= runListT)	-- Right section
+          , ListT . (runListT <<=)      -- Left section
+          ]
+
+(<<=) :: Monad m => (a -> m b) -> m a -> m b
+(<<=) k m = m >>= k
+
diff --git a/testsuite/tests/indexed-types/should_compile/T3787.hs b/testsuite/tests/indexed-types/should_compile/T3787.hs
new file mode 100644
index 0000000000..955b6a1cdd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3787.hs
@@ -0,0 +1,475 @@
+{- 
+    Copyright 2009 Mario Blazevic
+
+    This file is part of the Streaming Component Combinators (SCC) project.
+
+    The SCC project is free software: you can redistribute it and/or modify it under the terms of the GNU General Public
+    License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later
+    version.
+
+    SCC is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty
+    of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along with SCC.  If not, see
+    <http://www.gnu.org/licenses/>.
+-}
+
+-- | Module "Trampoline" defines the trampoline computations and their basic building blocks.
+
+{-# LANGUAGE ScopedTypeVariables, Rank2Types, MultiParamTypeClasses, TypeFamilies, KindSignatures,
+             FlexibleContexts, FlexibleInstances, OverlappingInstances, UndecidableInstances
+ #-}
+
+module T3787 where
+
+import Control.Concurrent (forkIO)
+import Control.Concurrent.MVar (newEmptyMVar, putMVar, takeMVar)
+import Control.Monad (liftM, liftM2, when)
+import Control.Monad.Identity
+import Control.Monad.Trans (MonadTrans(..))
+
+import Data.Foldable (toList)
+import Data.Maybe (maybe)
+import Data.Sequence (Seq, viewl)
+
+par, pseq :: a -> b -> b
+par = error "urk"
+pseq = error "urk"
+
+-- | Class of monads that can perform two computations in parallel.
+class Monad m => ParallelizableMonad m where
+   -- | Combine two computations into a single parallel computation. Default implementation of `parallelize` is
+   -- @liftM2 (,)@
+   parallelize :: m a -> m b -> m (a, b)
+   parallelize = liftM2 (,)
+
+-- | Any monad that allows the result value to be extracted, such as `Identity` or `Maybe` monad, can implement
+-- `parallelize` by using `par`.
+instance ParallelizableMonad Identity where
+   parallelize ma mb = let a = runIdentity ma
+                           b = runIdentity mb
+                       in  a `par` (b `pseq` a `pseq` Identity (a, b))
+
+instance ParallelizableMonad Maybe where
+   parallelize ma mb = case ma `par` (mb `pseq` (ma, mb))
+                       of (Just a, Just b) -> Just (a, b)
+                          _ -> Nothing
+
+-- | IO is parallelizable by `forkIO`.
+instance ParallelizableMonad IO where
+   parallelize ma mb = do va <- newEmptyMVar
+                          vb <- newEmptyMVar
+                          forkIO (ma >>= putMVar va)
+                          forkIO (mb >>= putMVar vb)
+                          a <- takeMVar va
+                          b <- takeMVar vb
+                          return (a, b)
+
+-- | Suspending monadic computations.
+newtype Trampoline s m r = Trampoline {
+   -- | Run the next step of a `Trampoline` computation.
+   bounce :: m (TrampolineState s m r)
+   }
+
+data TrampolineState s m r =
+   -- | Trampoline computation is finished with final value /r/.
+   Done r
+   -- | Computation is suspended, its remainder is embedded in the functor /s/.
+ | Suspend! (s (Trampoline s m r))
+
+instance (Functor s, Monad m) => Monad (Trampoline s m) where
+   return x = Trampoline (return (Done x))
+   t >>= f = Trampoline (bounce t >>= apply f)
+      where apply f (Done x) = bounce (f x)
+            apply f (Suspend s) = return (Suspend (fmap (>>= f) s))
+
+instance (Functor s, ParallelizableMonad m) => ParallelizableMonad (Trampoline s m) where
+   parallelize t1 t2 = Trampoline $ liftM combine $ parallelize (bounce t1) (bounce t2) where
+      combine (Done x, Done y) = Done (x, y)
+      combine (Suspend s, Done y) = Suspend (fmap (liftM $ \x-> (x, y)) s)
+      combine (Done x, Suspend s) = Suspend (fmap (liftM $ (,) x) s)
+      combine (Suspend s1, Suspend s2) = Suspend (fmap (parallelize $ suspend s1) s2)
+
+instance Functor s => MonadTrans (Trampoline s) where
+   lift = Trampoline . liftM Done
+
+data Yield x y = Yield! x y
+instance Functor (Yield x) where
+   fmap f (Yield x y) = Yield x (f y)
+
+data Await x y = Await! (x -> y)
+instance Functor (Await x) where
+   fmap f (Await g) = Await (f . g)
+
+data EitherFunctor l r x = LeftF (l x) | RightF (r x)
+instance (Functor l, Functor r) => Functor (EitherFunctor l r) where
+   fmap f (LeftF l) = LeftF (fmap f l)
+   fmap f (RightF r) = RightF (fmap f r)
+
+newtype NestedFunctor l r x = NestedFunctor (l (r x))
+instance (Functor l, Functor r) => Functor (NestedFunctor l r) where
+   fmap f (NestedFunctor lr) = NestedFunctor ((fmap . fmap) f lr)
+
+data SomeFunctor l r x = LeftSome (l x) | RightSome (r x) | Both (NestedFunctor l r x)
+instance (Functor l, Functor r) => Functor (SomeFunctor l r) where
+   fmap f (LeftSome l) = LeftSome (fmap f l)
+   fmap f (RightSome r) = RightSome (fmap f r)
+   fmap f (Both lr) = Both (fmap f lr)
+
+type TryYield x = EitherFunctor (Yield x) (Await Bool)
+
+suspend :: (Monad m, Functor s) => s (Trampoline s m x) -> Trampoline s m x
+suspend s = Trampoline (return (Suspend s))
+
+yield :: forall m x. Monad m => x -> Trampoline (Yield x) m ()
+yield x = suspend (Yield x (return ()))
+
+await :: forall m x. Monad m => Trampoline (Await x) m x
+await = suspend (Await return)
+
+tryYield :: forall m x. Monad m => x -> Trampoline (TryYield x) m Bool
+tryYield x = suspend (LeftF (Yield x (suspend (RightF (Await return)))))
+
+canYield :: forall m x. Monad m => Trampoline (TryYield x) m Bool
+canYield = suspend (RightF (Await return))
+
+fromTrampoline :: Monad m => Trampoline s m x -> m x
+fromTrampoline t = bounce t >>= \(Done x)-> return x
+
+runTrampoline :: Monad m => Trampoline Identity m x -> m x
+runTrampoline = fromTrampoline
+
+pogoStick :: (Functor s, Monad m) => (s (Trampoline s m x) -> Trampoline s m x) -> Trampoline s m x -> m x
+pogoStick reveal t = bounce t
+                     >>= \s-> case s 
+                              of Done result -> return result
+                                 Suspend c -> pogoStick reveal (reveal c)
+
+pogoStickNested :: (Functor s1, Functor s2, Monad m) => 
+                   (s2 (Trampoline (EitherFunctor s1 s2) m x) -> Trampoline (EitherFunctor s1 s2) m x)
+                   -> Trampoline (EitherFunctor s1 s2) m x -> Trampoline s1 m x
+pogoStickNested reveal t = 
+   Trampoline{bounce= bounce t
+                      >>= \s-> case s
+                               of Done result -> return (Done result)
+                                  Suspend (LeftF s) -> return (Suspend (fmap (pogoStickNested reveal) s))
+                                  Suspend (RightF c) -> bounce (pogoStickNested reveal (reveal c))
+             }
+
+nest :: (Functor a, Functor b) => a x -> b y -> NestedFunctor a b (x, y)
+nest a b = NestedFunctor $ fmap (\x-> fmap ((,) x) b) a
+
+-- couple :: (Monad m, Functor s1, Functor s2) => 
+--           Trampoline s1 m x -> Trampoline s2 m y -> Trampoline (NestedFunctor s1 s2) m (x, y)
+-- couple t1 t2 = Trampoline{bounce= do ts1 <- bounce t1
+--                                      ts2 <- bounce t2
+--                                      case (ts1, ts2) of (Done x, Done y) -> return $ Done (x, y)
+--                                                         (Suspend s1, Suspend s2) -> return $ Suspend $ 
+--                                                                                     fmap (uncurry couple) (nest s1 s2)
+--                          }
+
+coupleAlternating :: (Monad m, Functor s1, Functor s2) => 
+                     Trampoline s1 m x -> Trampoline s2 m y -> Trampoline (SomeFunctor s1 s2) m (x, y)
+coupleAlternating t1 t2 = 
+   Trampoline{bounce= do ts1 <- bounce t1
+                         ts2 <- bounce t2
+                         case (ts1, ts2) of (Done x, Done y) -> return $ Done (x, y)
+                                            (Suspend s1, Suspend s2) ->
+                                               return $ Suspend $ fmap (uncurry coupleAlternating) (Both $ nest s1 s2)
+                                            (Done x, Suspend s2) ->
+                                               return $ Suspend $ fmap (coupleAlternating (return x)) (RightSome s2)
+                                            (Suspend s1, Done y) ->
+                                               return $ Suspend $ fmap (flip coupleAlternating (return y)) (LeftSome s1)
+             }
+
+coupleParallel :: (ParallelizableMonad m, Functor s1, Functor s2) => 
+                  Trampoline s1 m x -> Trampoline s2 m y -> Trampoline (SomeFunctor s1 s2) m (x, y)
+coupleParallel t1 t2 = 
+   Trampoline{bounce= parallelize (bounce t1) (bounce t2)
+                      >>= \pair-> case pair
+                                  of (Done x, Done y) -> return $ Done (x, y)
+                                     (Suspend s1, Suspend s2) ->
+                                        return $ Suspend $ fmap (uncurry coupleParallel) (Both $ nest s1 s2)
+                                     (Done x, Suspend s2) ->
+                                        return $ Suspend $ fmap (coupleParallel (return x)) (RightSome s2)
+                                     (Suspend s1, Done y) ->
+                                        return $ Suspend $ fmap (flip coupleParallel (return y)) (LeftSome s1)
+             }
+
+coupleNested :: (Monad m, Functor s0, Functor s1, Functor s2) => 
+                Trampoline (EitherFunctor s0 s1) m x -> Trampoline (EitherFunctor s0 s2) m y -> 
+                Trampoline (EitherFunctor s0 (SomeFunctor s1 s2)) m (x, y)
+coupleNested t1 t2 = 
+   Trampoline{bounce= do ts1 <- bounce t1
+                         ts2 <- bounce t2
+                         case (ts1, ts2) of (Done x, Done y) -> return $ Done (x, y)
+                                            (Suspend (RightF s), Done y) -> 
+                                               return $ Suspend $ RightF $ fmap (flip coupleNested (return y)) (LeftSome s)
+                                            (Done x, Suspend (RightF s)) -> 
+                                               return $ Suspend $ RightF $ fmap (coupleNested (return x)) (RightSome s)
+                                            (Suspend (RightF s1), Suspend (RightF s2)) ->
+                                               return $ Suspend $ RightF $ fmap (uncurry coupleNested) (Both $ nest s1 s2)
+                                            (Suspend (LeftF s), Done y) ->
+                                               return $ Suspend $ LeftF $ fmap (flip coupleNested (return y)) s
+                                            (Done x, Suspend (LeftF s)) ->
+                                               return $ Suspend $ LeftF $ fmap (coupleNested (return x)) s
+                                            (Suspend (LeftF s1), Suspend (LeftF s2)) -> 
+                                               return $ Suspend $ LeftF $ fmap (coupleNested $ suspend $ LeftF s1) s2
+             }
+
+seesaw :: (Monad m, Functor s1, Functor s2) => 
+           (forall x y s t. (s ~ SomeFunctor s1 s2, t ~ Trampoline s m (x, y)) => s t -> t)
+           -> Trampoline s1 m x -> Trampoline s2 m y -> m (x, y)
+seesaw resolve t1 t2 = pogoStick resolve (coupleAlternating t1 t2)
+
+seesawParallel :: (ParallelizableMonad m, Functor s1, Functor s2) => 
+                  (forall x y s t. (s ~ SomeFunctor s1 s2, t ~ Trampoline s m (x, y)) => s t -> t)
+                  -> Trampoline s1 m x -> Trampoline s2 m y -> m (x, y)
+seesawParallel resolve t1 t2 = pogoStick resolve (coupleParallel t1 t2)
+
+resolveProducerConsumer :: forall a s s0 t t' m x. 
+                           (Functor s0, Monad m, s ~ SomeFunctor (TryYield a) (Await (Maybe a)), 
+                            t ~ Trampoline (EitherFunctor s0 s) m x) => 
+                           s t -> t
+-- Arg :: s t
+-- (LeftSome (LeftF ...)) : SomeFunctor (EitherFunctor .. ..) (...) t
+resolveProducerConsumer (LeftSome (LeftF (Yield _ c))) = c
+resolveProducerConsumer (LeftSome (RightF (Await c))) = c False
+resolveProducerConsumer (RightSome (Await c)) = c Nothing
+resolveProducerConsumer (Both (NestedFunctor (LeftF (Yield x (Await c))))) = c (Just x)
+resolveProducerConsumer (Both (NestedFunctor (RightF (Await c)))) = suspend (RightF $ RightSome $ c True)
+
+couplePC :: ParallelizableMonad m => Trampoline (Yield a) m x -> Trampoline (Await (Maybe a)) m y -> m (x, y)
+couplePC t1 t2 = parallelize (bounce t1) (bounce t2)
+                 >>= \(s1, s2)-> case (s1, s2)
+                                 of (Done x, Done y) -> return (x, y)
+                                    (Suspend (Yield x c1), Suspend (Await c2)) -> couplePC c1 (c2 $ Just x)
+                                    (Suspend (Yield _ c1), Done y) -> couplePC c1 (return y)
+                                    (Done x, Suspend (Await c2)) -> couplePC (return x) (c2 Nothing)
+
+coupleFinite :: ParallelizableMonad m => Trampoline (TryYield a) m x -> Trampoline (Await (Maybe a)) m y -> m (x, y)
+coupleFinite t1 t2 =
+   parallelize (bounce t1) (bounce t2)
+   >>= \(s1, s2)-> case (s1, s2)
+                   of (Done x, Done y) -> return (x, y)
+                      (Done x, Suspend (Await c2)) -> coupleFinite (return x) (c2 Nothing)
+                      (Suspend (LeftF (Yield x c1)), Suspend (Await c2)) -> coupleFinite c1 (c2 $ Just x)
+                      (Suspend (LeftF (Yield _ c1)), Done y) -> coupleFinite c1 (return y)
+                      (Suspend (RightF (Await c1)), Suspend s2@Await{}) -> coupleFinite (c1 True) (suspend s2)
+                      (Suspend (RightF (Await c1)), Done y) -> coupleFinite (c1 False) (return y)
+
+coupleFiniteSequential :: Monad m => Trampoline (TryYield a) m x -> Trampoline (Await (Maybe a)) m y -> m (x, y)
+coupleFiniteSequential t1 t2 =
+   bounce t1
+   >>= \s1-> bounce t2
+             >>= \s2-> case (s1, s2)
+                       of (Done x, Done y) -> return (x, y)
+                          (Done x, Suspend (Await c2)) -> coupleFiniteSequential (return x) (c2 Nothing)
+                          (Suspend (LeftF (Yield x c1)), Suspend (Await c2)) -> coupleFiniteSequential c1 (c2 $ Just x)
+                          (Suspend (LeftF (Yield _ c1)), Done y) -> coupleFiniteSequential c1 (return y)
+                          (Suspend (RightF (Await c1)), Suspend s2@Await{}) -> coupleFiniteSequential (c1 True) (suspend s2)
+                          (Suspend (RightF (Await c1)), Done y) -> coupleFiniteSequential (c1 False) (return y)
+
+-- coupleNested :: (Functor s, Monad m) =>
+--                 Trampoline (EitherFunctor s (Yield a)) m x
+--              -> Trampoline (EitherFunctor s (Await (Maybe a))) m y -> Trampoline s m (x, y)
+             
+-- coupleNested t1 t2 =
+--    lift (liftM2 (,) (bounce t1) (bounce t2))
+--    >>= \(s1, s2)-> case (s1, s2)
+--                    of (Done x, Done y) -> return (x, y)
+--                       (Suspend (RightF (Yield _ c1)), Done y) -> coupleNested c1 (return y)
+--                       (Done x, Suspend (RightF (Await c2))) -> coupleNested (return x) (c2 Nothing)
+--                       (Suspend (RightF (Yield x c1)), Suspend (RightF (Await c2))) -> coupleNested c1 (c2 $ Just x)
+--                       (Suspend (LeftF s), Done y) -> suspend (fmap (flip coupleNested (return y)) s)
+--                       (Done x, Suspend (LeftF s)) -> suspend (fmap (coupleNested (return x)) s)
+--                       (Suspend (LeftF s1), Suspend (LeftF s2)) -> suspend (fmap (coupleNested $ suspend $ LeftF s1) s2)
+
+coupleNestedFinite :: (Functor s, ParallelizableMonad m) =>
+                      Trampoline (SinkFunctor s a) m x -> Trampoline (SourceFunctor s a) m y -> Trampoline s m (x, y)
+coupleNestedFinite t1 t2 = lift (parallelize (bounce t1) (bounce t2))
+                           >>= stepCouple coupleNestedFinite
+
+coupleNestedFiniteSequential :: (Functor s, Monad m) =>
+                                Trampoline (SinkFunctor s a) m x
+                             -> Trampoline (SourceFunctor s a) m y
+                             -> Trampoline s m (x, y)
+coupleNestedFiniteSequential producer consumer = 
+   pogoStickNested resolveProducerConsumer (coupleNested producer consumer)
+-- coupleNestedFiniteSequential t1 t2 = lift (liftM2 (,) (bounce t1) (bounce t2))
+--                                      >>= stepCouple coupleNestedFiniteSequential
+
+stepCouple :: (Functor s, Monad m) =>
+              (Trampoline (EitherFunctor s (TryYield a)) m x
+                  -> Trampoline (EitherFunctor s (Await (Maybe a))) m y
+                  -> Trampoline s m (x, y))
+              -> (TrampolineState (EitherFunctor s (TryYield a)) m x,
+                  TrampolineState (EitherFunctor s (Await (Maybe a))) m y)
+              -> Trampoline s m (x, y)
+stepCouple f couple = case couple
+                      of (Done x, Done y) -> return (x, y)
+                         (Done x, Suspend (RightF (Await c2))) -> f (return x) (c2 Nothing)
+                         (Suspend (RightF (LeftF (Yield _ c1))), Done y) -> f c1 (return y)
+                         (Suspend (RightF (LeftF (Yield x c1))), Suspend (RightF (Await c2))) -> f c1 (c2 $ Just x)
+                         (Suspend (RightF (RightF (Await c1))), Suspend s2@(RightF Await{})) -> f (c1 True) (suspend s2)
+                         (Suspend (RightF (RightF (Await c1))), Done y) -> f (c1 False) (return y)
+                         (Suspend (LeftF s), Done y) -> suspend (fmap (flip f (return y)) s)
+                         (Done x, Suspend (LeftF s)) -> suspend (fmap (f (return x)) s)
+                         (Suspend (LeftF s1), Suspend (LeftF s2)) -> suspend (fmap (f $ suspend $ LeftF s1) s2)
+                         (Suspend (LeftF s1), Suspend (RightF s2)) -> suspend (fmap (flip f (suspend $ RightF s2)) s1)
+                         (Suspend (RightF s1), Suspend (LeftF s2)) -> suspend (fmap (f (suspend $ RightF s1)) s2)
+
+local :: forall m l r x. (Functor r, Monad m) => Trampoline r m x -> Trampoline (EitherFunctor l r) m x
+local (Trampoline mr) = Trampoline (liftM inject mr)
+   where inject :: TrampolineState r m x -> TrampolineState (EitherFunctor l r) m x
+         inject (Done x) = Done x
+         inject (Suspend r) = Suspend (RightF $ fmap local r)
+
+out :: forall m l r x. (Functor l, Monad m) => Trampoline l m x -> Trampoline (EitherFunctor l r) m x
+out (Trampoline ml) = Trampoline (liftM inject ml)
+   where inject :: TrampolineState l m x -> TrampolineState (EitherFunctor l r) m x
+         inject (Done x) = Done x
+         inject (Suspend l) = Suspend (LeftF $ fmap out l)
+
+-- | Class of functors that can be lifted.
+class (Functor a, Functor d) => AncestorFunctor a d where
+   -- | Convert the ancestor functor into its descendant. The descendant functor typically contains the ancestor.
+   liftFunctor :: a x -> d x
+
+instance Functor a => AncestorFunctor a a where
+   liftFunctor = id
+instance (Functor a, Functor d', Functor d, d ~ EitherFunctor d' s, AncestorFunctor a d') => AncestorFunctor a d where
+   liftFunctor = LeftF . (liftFunctor :: a x -> d' x)
+
+liftOut :: forall m a d x. (Monad m, Functor a, AncestorFunctor a d) => Trampoline a m x -> Trampoline d m x
+liftOut (Trampoline ma) = Trampoline (liftM inject ma)
+   where inject :: TrampolineState a m x -> TrampolineState d m x
+         inject (Done x) = Done x
+         inject (Suspend a) = Suspend (liftFunctor $ fmap liftOut a)
+
+type SourceFunctor a x = EitherFunctor a (Await (Maybe x))
+type SinkFunctor a x = EitherFunctor a (TryYield x)
+
+-- | A 'Sink' can be used to yield values from any nested `Trampoline` computation whose functor provably descends from
+-- the functor /a/. It's the write-only end of a 'Pipe' communication channel.
+data Sink (m :: * -> *) a x =
+   Sink
+   {
+   -- | Function 'put' tries to put a value into the given `Sink`. The intervening 'Trampoline' computations suspend up
+   -- to the 'pipe' invocation that has created the argument sink. The result of 'put' indicates whether the operation
+   -- succeded.
+   put :: forall d. (AncestorFunctor a d) => x -> Trampoline d m Bool,
+   -- | Function 'canPut' checks if the argument `Sink` accepts values, i.e., whether a 'put' operation would succeed on
+   -- the sink.
+   canPut :: forall d. (AncestorFunctor a d) => Trampoline d m Bool
+   }
+
+-- | A 'Source' can be used to read values into any nested `Trampoline` computation whose functor provably descends from
+-- the functor /a/. It's the read-only end of a 'Pipe' communication channel.
+newtype Source (m :: * -> *) a x =
+   Source
+   {
+   -- | Function 'get' tries to get a value from the given 'Source' argument. The intervening 'Trampoline' computations
+   -- suspend all the way to the 'pipe' function invocation that created the source. The function returns 'Nothing' if
+   -- the argument source is empty.
+   get :: forall d. (AncestorFunctor a d) => Trampoline d m (Maybe x)
+   }
+
+-- | Converts a 'Sink' on the ancestor functor /a/ into a sink on the descendant functor /d/.
+liftSink :: forall m a d x. (Monad m, AncestorFunctor a d) => Sink m a x -> Sink m d x
+liftSink s = Sink {put= liftOut . (put s :: x -> Trampoline d m Bool),
+                   canPut= liftOut (canPut s :: Trampoline d m Bool)}
+
+-- | Converts a 'Source' on the ancestor functor /a/ into a source on the descendant functor /d/.
+liftSource :: forall m a d x. (Monad m, AncestorFunctor a d) => Source m a x -> Source m d x
+liftSource s = Source {get= liftOut (get s :: Trampoline d m (Maybe x))}
+
+-- | The 'pipe' function splits the computation into two concurrent parts, /producer/ and /consumer/. The /producer/ is
+-- given a 'Sink' to put values into, and /consumer/ a 'Source' to get those values from. Once producer and consumer
+-- both complete, 'pipe' returns their paired results.
+pipe :: forall m a a1 a2 x r1 r2. (Monad m, Functor a, a1 ~ SinkFunctor a x, a2 ~ SourceFunctor a x) =>
+        (Sink m a1 x -> Trampoline a1 m r1) -> (Source m a2 x -> Trampoline a2 m r2) -> Trampoline a m (r1, r2)
+pipe producer consumer = coupleNestedFiniteSequential (producer sink) (consumer source) where
+   sink = Sink {put= liftOut . (local . tryYield :: x -> Trampoline a1 m Bool),
+                canPut= liftOut (local canYield :: Trampoline a1 m Bool)} :: Sink m a1 x
+   source = Source (liftOut (local await :: Trampoline a2 m (Maybe x))) :: Source m a2 x
+
+-- | The 'pipeP' function is equivalent to 'pipe', except the /producer/ and /consumer/ are run in parallel.
+pipeP :: forall m a a1 a2 x r1 r2. (ParallelizableMonad m, Functor a, a1 ~ SinkFunctor a x, a2 ~ SourceFunctor a x) =>
+         (Sink m a1 x -> Trampoline a1 m r1) -> (Source m a2 x -> Trampoline a2 m r2) -> Trampoline a m (r1, r2)
+pipeP producer consumer = coupleNestedFinite (producer sink) (consumer source) where
+   sink = Sink {put= liftOut . (local . tryYield :: x -> Trampoline a1 m Bool),
+                canPut= liftOut (local canYield :: Trampoline a1 m Bool)} :: Sink m a1 x
+   source = Source (liftOut (local await :: Trampoline a2 m (Maybe x))) :: Source m a2 x
+
+-- | The 'pipePS' function acts either as 'pipeP' or as 'pipe', depending on the argument /parallel/.
+pipePS :: forall m a a1 a2 x r1 r2. (ParallelizableMonad m, Functor a, a1 ~ SinkFunctor a x, a2 ~ SourceFunctor a x) =>
+          Bool -> (Sink m a1 x -> Trampoline a1 m r1) -> (Source m a2 x -> Trampoline a2 m r2) ->
+          Trampoline a m (r1, r2)
+pipePS parallel = if parallel then pipeP else pipe
+
+getSuccess :: forall m a d x . (Monad m, AncestorFunctor a d)
+              => Source m a x -> (x -> Trampoline d m ()) {- ^ Success continuation -} -> Trampoline d m ()
+getSuccess source succeed = get source >>= maybe (return ()) succeed
+
+-- | Function 'get'' assumes that the argument source is not empty and returns the value the source yields. If the
+-- source is empty, the function throws an error.
+get' :: forall m a d x . (Monad m, AncestorFunctor a d) => Source m a x -> Trampoline d m x
+get' source = get source >>= maybe (error "get' failed") return
+
+-- | 'pour' copies all data from the /source/ argument into the /sink/ argument, as long as there is anything to copy
+-- and the sink accepts it.
+pour :: forall m a1 a2 d x . (Monad m, AncestorFunctor a1 d, AncestorFunctor a2 d)
+        => Source m a1 x -> Sink m a2 x -> Trampoline d m ()
+pour source sink = fill'
+   where fill' = canPut sink >>= flip when (getSuccess source (\x-> put sink x >> fill'))
+
+-- | 'pourMap' is like 'pour' that applies the function /f/ to each argument before passing it into the /sink/.
+pourMap :: forall m a1 a2 d x y . (Monad m, AncestorFunctor a1 d, AncestorFunctor a2 d)
+           => (x -> y) -> Source m a1 x -> Sink m a2 y -> Trampoline d m ()
+pourMap f source sink = loop
+   where loop = canPut sink >>= flip when (get source >>= maybe (return ()) (\x-> put sink (f x) >> loop))
+
+-- | 'pourMapMaybe' is to 'pourMap' like 'Data.Maybe.mapMaybe' is to 'Data.List.Map'.
+pourMapMaybe :: forall m a1 a2 d x y . (Monad m, AncestorFunctor a1 d, AncestorFunctor a2 d)
+                => (x -> Maybe y) -> Source m a1 x -> Sink m a2 y -> Trampoline d m ()
+pourMapMaybe f source sink = loop
+   where loop = canPut sink >>= flip when (get source >>= maybe (return ()) (\x-> maybe (return False) (put sink) (f x) >> loop))
+
+-- | 'tee' is similar to 'pour' except it distributes every input value from the /source/ arguments into both /sink1/
+-- and /sink2/.
+tee :: forall m a1 a2 a3 d x . (Monad m, AncestorFunctor a1 d, AncestorFunctor a2 d, AncestorFunctor a3 d)
+       => Source m a1 x -> Sink m a2 x -> Sink m a3 x -> Trampoline d m ()
+tee source sink1 sink2 = distribute
+   where distribute = do c1 <- canPut sink1
+                         c2 <- canPut sink2
+                         when (c1 && c2)
+                            (get source >>= maybe (return ()) (\x-> put sink1 x >> put sink2 x >> distribute))
+
+-- | 'putList' puts entire list into its /sink/ argument, as long as the sink accepts it. The remainder that wasn't
+-- accepted by the sink is the result value.
+putList :: forall m a d x. (Monad m, AncestorFunctor a d) => [x] -> Sink m a x -> Trampoline d m [x]
+putList [] sink = return []
+putList l@(x:rest) sink = put sink x >>= cond (putList rest sink) (return l)
+
+-- | 'getList' returns the list of all values generated by the source.
+getList :: forall m a d x. (Monad m, AncestorFunctor a d) => Source m a x -> Trampoline d m [x]
+getList source = getList' return
+   where getList' f = get source >>= maybe (f []) (\x-> getList' (f . (x:)))
+
+-- | 'consumeAndSuppress' consumes the entire source ignoring the values it generates.
+consumeAndSuppress :: forall m a d x. (Monad m, AncestorFunctor a d) => Source m a x -> Trampoline d m ()
+consumeAndSuppress source = get source
+                            >>= maybe (return ()) (const (consumeAndSuppress source))
+
+-- | A utility function wrapping if-then-else, useful for handling monadic truth values
+cond :: a -> a -> Bool -> a
+cond x y test = if test then x else y
+
+-- | A utility function, useful for handling monadic list values where empty list means success
+whenNull :: forall a m. Monad m => m [a] -> [a] -> m [a]
+whenNull action list = if null list then action else return list
+
+-- | Like 'putList', except it puts the contents of the given 'Data.Sequence.Seq' into the sink.
+putQueue :: forall m a d x. (Monad m, AncestorFunctor a d) => Seq x -> Sink m a x -> Trampoline d m [x]
+putQueue q sink = putList (toList (viewl q)) sink
diff --git a/testsuite/tests/indexed-types/should_compile/T3826.hs b/testsuite/tests/indexed-types/should_compile/T3826.hs
new file mode 100644
index 0000000000..39c597f69c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3826.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}

+

+module T3826 where

+

+class C a where

+  type E a

+  c :: E a -> a -> a

+

+data T a = T a

+

+instance C (T a) where

+  type E (T a) = a

+  c x (T _) = T x

+

+f t@(T x) = c x t

diff --git a/testsuite/tests/indexed-types/should_compile/T3851.hs b/testsuite/tests/indexed-types/should_compile/T3851.hs
new file mode 100644
index 0000000000..3b40db1bce
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T3851.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE GADTs, TypeFamilies #-}

+

+module T3851 where

+

+type family TF a :: * -> *

+type instance TF () = App (Equ ())

+

+data Equ ix ix' where Refl :: Equ ix ix

+data App f x = App (f x)

+

+-- does not typecheck in 6.12.1 (but works in 6.10.4)

+bar :: TF () () -> ()

+bar (App Refl) = ()

+

+-- does typecheck in 6.12.1 and 6.10.4

+ar :: App (Equ ()) () -> ()

+ar (App Refl) = ()

+

+------------------

+data family DF a :: * -> *

+data instance DF () a = D (App (Equ ()) a)

+

+bar_df :: DF () () -> ()

+bar_df (D (App Refl)) = ()

diff --git a/testsuite/tests/indexed-types/should_compile/T4120.hs b/testsuite/tests/indexed-types/should_compile/T4120.hs
new file mode 100644
index 0000000000..57dd21a39b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4120.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE Rank2Types, TypeFamilies #-}
+
+-- Unification yielding a coercion under a forall
+
+module Data.Vector.Unboxed where
+
+import Control.Monad.ST ( ST )
+
+
+data MVector s a = MV
+data Vector a    = V
+
+type family Mutable (v :: * -> *) :: * -> * -> *
+type instance Mutable Vector = MVector
+
+create :: (forall s. MVector s a) -> Int
+create = create1
+-- Here we get  Couldn't match expected type `forall s. MVector s a'
+--                          with actual type `forall s. Mutable Vector s a1'
+-- Reason: when unifying under a for-all we don't solve type 
+--         equalities.  Think more about this.
+
+create1 :: (forall s. Mutable Vector s a) -> Int
+create1 = error "urk"
+
+
diff --git a/testsuite/tests/indexed-types/should_compile/T4120.stderr b/testsuite/tests/indexed-types/should_compile/T4120.stderr
new file mode 100644
index 0000000000..d957620b78
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4120.stderr
@@ -0,0 +1,8 @@
+
+T4120.hs:17:10:
+    Couldn't match expected type `forall s. MVector s a'
+                with actual type `forall s. Mutable Vector s a0'
+    Expected type: (forall s. MVector s a) -> Int
+      Actual type: (forall s. Mutable Vector s a0) -> Int
+    In the expression: create1
+    In an equation for `create': create = create1
diff --git a/testsuite/tests/indexed-types/should_compile/T4160.hs b/testsuite/tests/indexed-types/should_compile/T4160.hs
new file mode 100644
index 0000000000..f13aafa103
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4160.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, TypeFamilies #-}
+module Foo where
+
+data P f g r = f r :*: g r
+type family TrieMapT (f :: * -> *) :: * -> (* -> *) -> * -> *
+newtype PMap m1 (m2 :: * -> (* -> *) -> * -> *) k (a :: * -> *) ix = PMap (m1 k (m2 k a) ix)
+type instance TrieMapT (P f g) = PMap (TrieMapT f) (TrieMapT g)
+
+class TrieKeyT f m where
+	unionT :: (TrieMapT f ~ m) => (f k -> a ix -> a ix -> a ix) ->
+		m k a ix -> m k a ix -> m k a ix
+	sizeT :: (TrieMapT f ~ m) => m k a ix -> Int
+
+instance (TrieKeyT f m1, TrieKeyT g m2) => TrieKeyT (P f g) (PMap m1 m2) where
+	unionT f (PMap m1) (PMap m2) = PMap (uT  (\ a -> unionT (\ b -> f (a :*: b))) m1 m2)
+		where uT = unionT
+        sizeT = error "urk"
+
diff --git a/testsuite/tests/indexed-types/should_compile/T4178.hs b/testsuite/tests/indexed-types/should_compile/T4178.hs
new file mode 100644
index 0000000000..b0a34b28e1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4178.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE
+	FlexibleContexts,
+	Rank2Types,
+	TypeFamilies,
+	MultiParamTypeClasses,
+	FlexibleInstances #-}
+
+-- See Trac #4178
+
+module T4178 where
+
+data True = T
+data False = F
+
+class Decide tf a b where
+  type If tf a b
+  nonFunctionalIf :: tf -> a -> b -> If tf a b
+
+instance Decide True a b where
+  type If True a b = a
+  nonFunctionalIf T a b = a
+
+instance Decide False a b where
+  type If False a b = b
+  nonFunctionalIf F a b = b
+
+useRank2 :: (forall a . a -> b) -> b
+useRank2 f = f "foo"
+
+hasTrouble a = nonFunctionalIf F a (2 :: Int)
+blurg = useRank2 hasTrouble
+
+hasNoTrouble :: a -> Int
+hasNoTrouble = hasTrouble
+blurg2 = useRank2 hasNoTrouble
diff --git a/testsuite/tests/indexed-types/should_compile/T4200.hs b/testsuite/tests/indexed-types/should_compile/T4200.hs
new file mode 100644
index 0000000000..0d0e23a419
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4200.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}

+

+module T4200 where

+

+class C a where

+  type In a :: *

+  op :: In a -> Int

+

+-- Should be ok; no -XUndecidableInstances required

+instance (In c ~ Int) => C [c] where 

+  type In [c] = In c

+  op x = 3

diff --git a/testsuite/tests/indexed-types/should_compile/T4338.hs b/testsuite/tests/indexed-types/should_compile/T4338.hs
new file mode 100644
index 0000000000..6fa2ae85ac
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4338.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, FlexibleContexts #-}
+
+module Main where
+
+class (There a ~ b, BackAgain b ~ a) => Foo a b where
+     type There a
+     type BackAgain b
+     there :: a -> b
+     back :: b -> a
+     tickle :: b -> b
+
+instance Foo Char Int where
+     type There Char = Int
+     type BackAgain Int = Char
+     there = fromEnum
+     back = toEnum
+     tickle = (+1)
+
+test :: (Foo a b) => a -> a
+test = back . tickle . there
+
+main :: IO ()
+main = print $ test 'F'
diff --git a/testsuite/tests/indexed-types/should_compile/T4356.hs b/testsuite/tests/indexed-types/should_compile/T4356.hs
new file mode 100644
index 0000000000..400314eeb2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4356.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+module T4356 where
+
+type family T t :: * -> * -> *
+type instance T Bool = (->)
+
+f :: T Bool Bool Bool
+f = not
diff --git a/testsuite/tests/indexed-types/should_compile/T4358.hs b/testsuite/tests/indexed-types/should_compile/T4358.hs
new file mode 100644
index 0000000000..92ac3a743b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4358.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies, Rank2Types, FlexibleContexts #-}
+
+module T4358 where
+
+type family T a
+
+t2 :: forall a. ((T a ~ a) => a) -> a
+t2 = t
+  
+t :: forall a. ((T a ~ a) => a) -> a
+t = undefined
diff --git a/testsuite/tests/indexed-types/should_compile/T4484.hs b/testsuite/tests/indexed-types/should_compile/T4484.hs
new file mode 100644
index 0000000000..94a76ee7d4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4484.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls, GADTs #-}
+
+module T4484 where
+
+type family F f :: *
+
+data Id c = Id
+type instance F (Id c) = c
+
+data C :: * -> * where
+  C :: f -> C (W (F f))
+
+data W :: * -> *
+
+fails :: C a -> C a
+fails (C _)
+  = -- We know (W (F f) ~ a)
+    C Id  -- We need (a ~ W (F (Id beta)))
+          --    ie   (a ~ W beta)
+          -- Use the equality; we need
+          --         (W (F f) ~ W beta)
+          --    ie   (F f ~ beta)
+          -- Solve with beta := f
+
+works :: C (W a) -> C (W a)
+works (C _)
+  = -- We know (W (F f) ~ W a)
+    C Id -- We need (W a ~ W (F (Id beta)))
+         --      ie (W a ~ W beta)
+         -- Solve with beta := a
diff --git a/testsuite/tests/indexed-types/should_compile/T4492.hs b/testsuite/tests/indexed-types/should_compile/T4492.hs
new file mode 100644
index 0000000000..0c01cbc973
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4492.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, RankNTypes #-}
+
+module T4492 where
+
+type family F a b
+type instance F (Maybe a) b = b -> F a b
+
+class C a where
+   go :: (forall a. Maybe a -> b -> a) -> a -> F a b
+
+instance C a => C (Maybe a) where
+   go f a b = go f (f a b)
diff --git a/testsuite/tests/indexed-types/should_compile/T4494.hs b/testsuite/tests/indexed-types/should_compile/T4494.hs
new file mode 100644
index 0000000000..52e1435272
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4494.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts,  ScopedTypeVariables #-}
+
+module T4494 where
+
+type family H s
+type family F v
+
+bar :: (forall t. Maybe t -> a) -> H a -> Int
+bar = error "urk"
+
+call :: F Bool -> Int
+call x = bar (\_ -> x) (undefined :: H (F Bool))
diff --git a/testsuite/tests/indexed-types/should_compile/T4497.hs b/testsuite/tests/indexed-types/should_compile/T4497.hs
new file mode 100644
index 0000000000..57d3d48ca4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4497.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, TypeFamilies #-}  

+

+module T4497 where

+

+norm2PropR a = twiddle (norm2 a) a

+

+twiddle :: Normed a => a -> a -> Double  

+twiddle a b = undefined

+

+norm2 :: e -> RealOf e

+norm2 = undefined

+

+class (Num (RealOf t)) => Normed t

+

+type family RealOf x

diff --git a/testsuite/tests/indexed-types/should_compile/T4935.hs b/testsuite/tests/indexed-types/should_compile/T4935.hs
new file mode 100644
index 0000000000..2c9d16a9b8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4935.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeFamilies, Rank2Types, ScopedTypeVariables #-}
+module T4935 where
+
+import Control.Applicative
+
+data TFalse
+data TTrue
+
+data Tagged b a = Tagged {at :: a}
+type At b = forall a. Tagged b a -> a
+
+class TBool b where onTBool :: (b ~ TFalse => c) -> (b ~ TTrue => c) -> Tagged b c
+instance TBool TFalse where onTBool f _ = Tagged $ f
+instance TBool TTrue where onTBool _ t = Tagged $ t
+
+type family CondV c f t
+type instance CondV TFalse f t = f
+type instance CondV TTrue f t = t
+
+newtype Cond c f a = Cond {getCond :: CondV c a (f a)}
+cond :: forall c f a g. (TBool c, Functor g) => (c ~ TFalse => g a) -> (c ~ TTrue => g (f a)) -> g (Cond c f a)
+cond f t = (at :: At c) $ onTBool (fmap Cond f) (fmap Cond t)
+condMap :: (TBool c, Functor f) => (a -> b) -> Cond c f a -> Cond c f b
+condMap g (Cond n) = cond g (fmap g) n
diff --git a/testsuite/tests/indexed-types/should_compile/T4981-V1.hs b/testsuite/tests/indexed-types/should_compile/T4981-V1.hs
new file mode 100644
index 0000000000..14f675ca59
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4981-V1.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE CPP, TypeFamilies, FlexibleContexts #-}

+module Class ( cleverNamedResolve ) where

+

+data FL p = FL p

+

+class PatchInspect p where

+instance PatchInspect p => PatchInspect (FL p) where

+

+type family PrimOf p

+type instance PrimOf (FL p) = PrimOf p

+

+data WithName prim = WithName prim

+

+instance PatchInspect prim => PatchInspect (WithName prim) where

+

+class (PatchInspect (PrimOf p)) => Conflict p where

+    resolveConflicts :: p -> PrimOf p

+

+instance Conflict p => Conflict (FL p) where

+    resolveConflicts = undefined

+

+type family OnPrim p

+

+class FromPrims p where

+

+instance FromPrims (FL p) where

+

+joinPatches :: FromPrims p => p -> p

+joinPatches = id 

+

+cleverNamedResolve :: (Conflict (OnPrim p)

+                      ,PrimOf (OnPrim p) ~ WithName (PrimOf p))

+                   => FL (OnPrim p) -> WithName (PrimOf p)

+cleverNamedResolve = resolveConflicts . joinPatches

diff --git a/testsuite/tests/indexed-types/should_compile/T4981-V2.hs b/testsuite/tests/indexed-types/should_compile/T4981-V2.hs
new file mode 100644
index 0000000000..d18d67e91c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4981-V2.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE CPP, TypeFamilies, FlexibleContexts #-}

+module Class ( cleverNamedResolve ) where

+

+data FL p = FL p

+

+class PatchInspect p where

+instance PatchInspect p => PatchInspect (FL p) where

+

+type family PrimOf p

+type instance PrimOf (FL p) = PrimOf p

+

+data WithName prim = WithName prim

+

+instance PatchInspect prim => PatchInspect (WithName prim) where

+

+class (PatchInspect (PrimOf p)) => Conflict p where

+    resolveConflicts :: p -> PrimOf p

+

+instance Conflict p => Conflict (FL p) where

+    resolveConflicts = undefined

+

+type family OnPrim p

+

+joinPatches :: FL p -> FL p

+

+joinPatches = id

+

+cleverNamedResolve :: (Conflict (OnPrim p)

+                      ,PrimOf (OnPrim p) ~ WithName (PrimOf p))

+                   => FL (OnPrim p) -> WithName (PrimOf p)

+cleverNamedResolve = resolveConflicts . joinPatches

diff --git a/testsuite/tests/indexed-types/should_compile/T4981-V3.hs b/testsuite/tests/indexed-types/should_compile/T4981-V3.hs
new file mode 100644
index 0000000000..9e0eda54eb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T4981-V3.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE CPP, TypeFamilies, FlexibleContexts #-}

+module Class ( cleverNamedResolve ) where

+

+data FL p = FL p

+

+class PatchInspect p where

+instance PatchInspect p => PatchInspect (FL p) where

+

+type family PrimOf p

+type instance PrimOf (FL p) = PrimOf p

+

+data WithName prim = WithName prim

+

+instance PatchInspect prim => PatchInspect (WithName prim) where

+

+class (PatchInspect (PrimOf p)) => Conflict p where

+    resolveConflicts :: p -> PrimOf p

+

+instance Conflict p => Conflict (FL p) where

+    resolveConflicts = undefined

+

+type family OnPrim p

+

+joinPatches :: p -> p

+

+joinPatches = id

+

+cleverNamedResolve :: (Conflict (OnPrim p)

+                      ,PrimOf (OnPrim p) ~ WithName (PrimOf p))

+                   => FL (OnPrim p) -> WithName (PrimOf p)

+cleverNamedResolve = resolveConflicts . joinPatches

diff --git a/testsuite/tests/indexed-types/should_compile/T5002.hs b/testsuite/tests/indexed-types/should_compile/T5002.hs
new file mode 100644
index 0000000000..cfc82d559e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T5002.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, FlexibleContexts #-}

+

+class A a

+class B a where b :: a -> ()

+instance A a => B a where b = undefined

+

+newtype Y a = Y (a -> ())

+

+okIn701 :: B a => Y a

+okIn701 = wrap $ const () . b

+

+okIn702 :: B a => Y a

+okIn702 = wrap $ b

+

+okInBoth :: B a => Y a

+okInBoth = Y $ const () . b

+

+class Wrapper a where

+    type Wrapped a

+    wrap :: Wrapped a -> a

+instance Wrapper (Y a) where

+  type Wrapped (Y a) = a -> ()

+  wrap = Y

+

+fromTicket3018 :: Eq [a] => a -> ()

+fromTicket3018 x = let {g :: Int -> Int; g = [x]==[x] `seq` id} in ()

+

+main = undefined

+

diff --git a/testsuite/tests/indexed-types/should_compile/TF_GADT.hs b/testsuite/tests/indexed-types/should_compile/TF_GADT.hs
new file mode 100644
index 0000000000..345b5748e0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/TF_GADT.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE GADTs, TypeFamilies #-}

+

+module TF_GADT where

+

+-- Check that type families can be declared in GADT syntax

+-- and indeed *be* GADTs

+

+data family T a

+

+data instance T [a] where

+  T1 :: a -> T [a]

+

+

+data instance T (Maybe a) where

+  T3 :: Int -> T (Maybe Int)

+  T4 :: a -> b -> T (Maybe (a,b))

+

+

+f :: a -> T (Maybe a) -> T (Maybe a)

+f x (T3 i) = T3 x

+f x (T4 p q) = T4 p (snd x)

diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
new file mode 100644
index 0000000000..241bbe49c6
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -0,0 +1,184 @@
+setTestOpts(only_compiler_types(['ghc']))
+# Keep optimised tests, so we test coercion optimisation
+setTestOpts(omit_ways(['optasm', 'optllvm', 'hpc']))
+
+test('Simple1', normal, compile, [''])
+test('Simple2', normal, compile, [''])
+test('Simple3', normal, compile, [''])
+test('Simple4', normal, compile, [''])
+test('Simple5', normal, compile, [''])
+test('Simple6', normal, compile, [''])
+test('Simple7', normal, compile, [''])
+test('Simple8', normal, compile, [''])
+test('Simple9', normal, compile, [''])
+test('Simple10', normal, compile, [''])
+test('Simple11', normal, compile, [''])
+test('Simple12', normal, compile, [''])
+test('Simple13', normal, compile, [''])
+test('Simple14', normal, compile_fail, [''])
+test('Simple15', normal, compile, [''])
+test('Simple16', normal, compile, [''])
+test('Simple17', normal, compile, [''])
+test('Simple18', normal, compile, [''])
+test('Simple19', normal, compile, [''])
+test('Simple20', expect_broken(4296), compile, [''])
+test('Simple21', normal, compile, [''])
+test('Simple22', normal, compile, [''])
+test('Simple23', normal, compile, [''])
+test('Simple24', normal, compile, [''])
+
+test('RelaxedExamples', normal, compile, [''])
+test('NonLinearLHS', normal, compile, [''])
+
+test('ind1', normal, compile, [''])
+test('ind2',
+     extra_clean(['Ind2_help.hi', 'Ind2_help.o']),
+     multimod_compile,
+     ['ind2', '-v0'])
+test('impexp',
+     extra_clean(['Exp.hi', 'Exp.o', 'Imp.hi', 'Imp.o']),
+     multimod_compile, 
+     ['Imp', '-w -no-hs-main -c'])
+
+test('ATLoop',
+     extra_clean(['ATLoop_help.o','ATLoop_help.hi']),
+     multimod_compile,
+     ['ATLoop.hs','-v0'])
+
+test('Deriving', normal, compile, [''])
+test('DerivingNewType', expect_fail, compile, [''])
+test('Records', normal, compile, [''])
+
+# The point about this test is that it compiles NewTyCo1 and NewTyCo2
+# *separately*
+#
+test('NewTyCo',
+     extra_clean(['NewTyCo1.o', 'NewTyCo1.hi', 'NewTyCo2.o', 'NewTyCo2.hi']),
+     run_command,
+     ['$MAKE -s --no-print-directory NewTyCo'])
+
+test('Infix', normal, compile, [''])
+test('Kind', normal, compile, [''])
+
+test('GADT1', normal, compile, [''])
+test('GADT2', normal, compile, [''])
+test('GADT3', normal, compile, [''])
+test('GADT4', normal, compile, [''])
+test('GADT5', normal, compile, [''])
+test('GADT6', normal, compile, [''])
+test('GADT7', normal, compile, [''])
+test('GADT8', normal, compile, [''])
+test('GADT9', normal, compile, [''])
+test('GADT10', normal, compile, [''])
+test('GADT11', normal, compile, [''])
+test('GADT12', normal, compile, [''])
+test('GADT13', normal, compile, [''])
+test('GADT14', normal, compile, [''])
+
+test('Class1', normal, compile, [''])
+test('Class2', normal, compile, [''])
+test('Class3', normal, compile, [''])
+
+test('Refl', normal, compile, [''])
+test('Refl2', normal, compile, [''])
+
+test('Rules1', normal, compile, [''])
+
+test('Numerals', normal, compile, [''])
+
+test('ColInference', normal, compile, [''])
+test('ColInference2', normal, compile, [''])
+test('ColInference3', normal, compile, [''])
+test('ColInference4', normal, compile, [''])
+test('ColInference5', normal, compile, [''])
+test('ColInference6', normal, compile, [''])
+
+test('Col', normal, compile, [''])
+test('Col2', normal, compile, [''])
+
+test('ColGivenCheck', normal, compile, [''])
+test('ColGivenCheck2', normal, compile, [''])
+
+test('InstEqContext', normal, compile, [''])
+test('InstEqContext2', normal, compile, [''])
+test('InstEqContext3', normal, compile, [''])
+
+test('InstContextNorm', normal, compile, [''])
+
+test('GivenCheck', normal, compile, [''])
+test('GivenCheckSwap', normal, compile, [''])
+test('GivenCheckDecomp', normal, compile, [''])
+test('GivenCheckTop', normal, compile, [''])
+
+# A very delicate test
+test('Gentle', normal, compile, [''])
+
+test('T1981', normal, compile, [''])
+test('T2238', normal, compile, [''])
+test('OversatDecomp', normal, compile, [''])
+
+test('T2219', normal, compile, [''])
+test('T2627', normal, compile, [''])
+test('T2448', normal, compile, [''])
+test('T2291', normal, compile, [''])
+test('T2639', normal, compile, [''])
+test('T2944', normal, compile, [''])
+test('T3017', normal, compile, ['-ddump-types'])
+test('TF_GADT', normal, compile, [''])
+test('T2203b', normal, compile, [''])
+test('T2767', normal, compile, [''])
+test('T3208a', normal, compile, [''])
+test('T3208b', normal, compile_fail, [''])
+test('T3418', normal, compile, [''])
+test('T3423', normal, compile, [''])
+test('T2850', normal, compile, [''])
+test('T3220', normal, compile, [''])
+test('T3590', normal, compile, [''])
+test('CoTest3', normal, compile, [''])
+test('Roman1', normal, compile, [''])
+test('T4160', normal, compile, [''])
+test('IndTypesPerf',
+     [ # expect_broken(5224),
+       # unbroken temporarily: #5227
+       extra_clean(['IndTypesPerf.o', 'IndTypesPerf.hi',
+                    'IndTypesPerfMerge.o', 'IndTypesPerfMerge.hi'])
+     ] ,
+     run_command,
+     ['$MAKE -s --no-print-directory IndTypesPerf'])
+
+test('T4120', normal, compile_fail, [''])
+test('T3787', reqlib('mtl'), compile, [''])
+test('T3826', normal, compile, [''])
+test('T4200', normal, compile, [''])
+test('T3851', normal, compile, [''])
+test('T4178', normal, compile, [''])
+test('T3023', normal, compile, [''])
+test('T4358', normal, compile, [''])
+test('T4356', normal, compile, [''])
+test('T4484', normal, compile, [''])
+test('T4492', normal, compile, [''])
+test('T4494', normal, compile, [''])
+test('DataFamDeriv', normal, compile, [''])
+test('T1769', if_compiler_lt('ghc', '7.1', expect_fail), compile, [''])
+test('T4497', normal, compile, [''])
+test('T3484', normal, compile, [''])
+test('T3460', normal, compile, [''])
+test('T4935', normal, compile, [''])
+
+test('T4981-V1', normal, compile, [''])
+test('T4981-V2', normal, compile, [''])
+test('T4981-V3', normal, compile, [''])
+
+test('T5002', normal, compile, [''])
+test('PushedInAsGivens', normal, compile, [''])
+
+# Superclass equalities
+test('T4338', normal, compile, [''])
+test('T2715', normal, compile, [''])
+test('T2102', normal, compile, [''])
+test('ClassEqContext', normal, compile, [''])
+test('ClassEqContext2', normal, compile, [''])
+test('ClassEqContext3', normal, compile, [''])
+test('HO', normal, compile, [''])
+
+
diff --git a/testsuite/tests/indexed-types/should_compile/impexp.stderr b/testsuite/tests/indexed-types/should_compile/impexp.stderr
new file mode 100644
index 0000000000..7ebebe9e03
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/impexp.stderr
@@ -0,0 +1,2 @@
+[1 of 2] Compiling Exp              ( Exp.hs, Exp.o )
+[2 of 2] Compiling Imp              ( Imp.hs, Imp.o )
diff --git a/testsuite/tests/indexed-types/should_compile/ind1.hs b/testsuite/tests/indexed-types/should_compile/ind1.hs
new file mode 100644
index 0000000000..48203a1519
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ind1.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- Test type families
+
+module ShouldCompile where
+
+data family T a :: *
+
+data instance T Bool = TBool !Bool
+
+class C a where
+  foo :: (a -> a) -> T a -> T a
+
+instance C Bool where
+  foo f (TBool x) = TBool $ f (not x)
diff --git a/testsuite/tests/indexed-types/should_compile/ind2.hs b/testsuite/tests/indexed-types/should_compile/ind2.hs
new file mode 100644
index 0000000000..de5d9d6a86
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/ind2.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldCompile where
+
+import Ind2_help(C(..))
+
+zipT :: (C a, C b) => T a -> T b -> T (a,b)
+zipT x y = mkT (unT x, unT y)
+
diff --git a/testsuite/tests/indexed-types/should_fail/DerivUnsatFam.hs b/testsuite/tests/indexed-types/should_fail/DerivUnsatFam.hs
new file mode 100644
index 0000000000..d401356326
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/DerivUnsatFam.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving #-}

+

+-- Crashed 6.12

+

+module T1769 where

+

+data family T a

+deriving instance Functor T

diff --git a/testsuite/tests/indexed-types/should_fail/DerivUnsatFam.stderr b/testsuite/tests/indexed-types/should_fail/DerivUnsatFam.stderr
new file mode 100644
index 0000000000..63c1262147
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/DerivUnsatFam.stderr
@@ -0,0 +1,5 @@
+

+DerivUnsatFam.hs:8:1:

+    Can't make a derived instance of `Functor T':

+      Unsaturated data family application

+    In the stand-alone deriving instance for `Functor T'

diff --git a/testsuite/tests/indexed-types/should_fail/GADTwrong1.hs b/testsuite/tests/indexed-types/should_fail/GADTwrong1.hs
new file mode 100644
index 0000000000..7295090439
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/GADTwrong1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies, GADTs, RankNTypes, ScopedTypeVariables #-}
+
+module ShouldFail where
+
+type family Const a
+type instance Const a = ()
+
+data T a where T :: a -> T (Const a)
+
+coerce :: forall a b . a -> b
+coerce x = case T x :: T (Const b) of
+           T y -> y
diff --git a/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr b/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
new file mode 100644
index 0000000000..e565aa6cde
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr
@@ -0,0 +1,18 @@
+
+GADTwrong1.hs:12:19:
+    Could not deduce (a1 ~ b)
+    from the context (() ~ Const a1)
+      bound by a pattern with constructor
+                 T :: forall a. a -> T (Const a),
+               in a case alternative
+      at GADTwrong1.hs:12:12-14
+      `a1' is a rigid type variable bound by
+           a pattern with constructor
+             T :: forall a. a -> T (Const a),
+           in a case alternative
+           at GADTwrong1.hs:12:12
+      `b' is a rigid type variable bound by
+          the type signature for coerce :: a -> b at GADTwrong1.hs:11:1
+    In the expression: y
+    In a case alternative: T y -> y
+    In the expression: case T x :: T (Const b) of { T y -> y }
diff --git a/testsuite/tests/indexed-types/should_fail/Makefile b/testsuite/tests/indexed-types/should_fail/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/indexed-types/should_fail/NoMatchErr.hs b/testsuite/tests/indexed-types/should_fail/NoMatchErr.hs
new file mode 100644
index 0000000000..304e11613e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/NoMatchErr.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- Type error message looks like
+-- 	TF.hs:12:11:
+--    Couldn't match expected type `Memo d'
+--           against inferred type `Memo d1'
+--      NB: `Memo' is a (non-injective) type function
+--
+-- Note the "NB", which helps point out the problem
+
+module Foo where
+
+class Fun d where
+    type Memo d :: * -> *
+    abst :: (d -> a) -> Memo d a
+    appl :: Memo d a -> (d -> a)
+
+f ::  (Fun d) => Memo d a -> Memo d a    -- (1)
+f = abst . appl
+
diff --git a/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
new file mode 100644
index 0000000000..38c8cf6b2f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr
@@ -0,0 +1,13 @@
+

+NoMatchErr.hs:20:12:

+    Could not deduce (Memo d0 ~ Memo d)

+    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

+    NB: `Memo' is a type function, and may not be injective

+    Expected type: Memo d a

+      Actual type: Memo d0 a

+    Expected type: Memo d a -> d0 -> a

+      Actual type: Memo d0 a -> d0 -> a

+    In the second argument of `(.)', namely `appl'

+    In the expression: abst . appl

diff --git a/testsuite/tests/indexed-types/should_fail/NonLinearSigErr.hs b/testsuite/tests/indexed-types/should_fail/NonLinearSigErr.hs
new file mode 100644
index 0000000000..34a9fd3ff6
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/NonLinearSigErr.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- This is actually perfectly ok!
+
+module NonLinearSigErr where
+
+type family E a b
+type instance E a (a :: *) = [a]
diff --git a/testsuite/tests/indexed-types/should_fail/NonLinearSigErr.stderr b/testsuite/tests/indexed-types/should_fail/NonLinearSigErr.stderr
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/NonLinearSigErr.stderr
diff --git a/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.hs b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.hs
new file mode 100644
index 0000000000..d41f86b3a1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module NotRelaxedExamples where
+
+type family F1 a
+type family F2 a
+type family F3 a
+
+type instance F1 Char = F1 (F1 Char)
+type instance F2 [x]  = F2 [x]
+type instance F3 Bool = F3 [Char]
diff --git a/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
new file mode 100644
index 0000000000..dbc83696ee
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/NotRelaxedExamples.stderr
@@ -0,0 +1,18 @@
+
+NotRelaxedExamples.hs:9:1:
+    Nested type family application
+      in the type family application: F1 (F1 Char)
+    (Use -XUndecidableInstances to permit this)
+    In the type synonym instance declaration for `F1'
+
+NotRelaxedExamples.hs:10:1:
+    Application is no smaller than the instance head
+      in the type family application: F2 [x]
+    (Use -XUndecidableInstances to permit this)
+    In the type synonym instance declaration for `F2'
+
+NotRelaxedExamples.hs:11:1:
+    Application is no smaller than the instance head
+      in the type family application: F3 [Char]
+    (Use -XUndecidableInstances to permit this)
+    In the type synonym instance declaration for `F3'
diff --git a/testsuite/tests/indexed-types/should_fail/Over.stderr b/testsuite/tests/indexed-types/should_fail/Over.stderr
new file mode 100644
index 0000000000..bb973eee08
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/Over.stderr
@@ -0,0 +1,10 @@
+
+OverB.hs:7:15:
+    Conflicting family instance declarations:
+      data instance OverA.C [Int] [a] -- Defined at OverB.hs:7:15
+      data instance OverA.C [a] [Int] -- Defined at OverC.hs:7:15
+
+OverB.hs:9:15:
+    Conflicting family instance declarations:
+      type instance OverA.D [Int] [a] -- Defined at OverB.hs:9:15
+      type instance OverA.D [a] [Int] -- Defined at OverC.hs:9:15
diff --git a/testsuite/tests/indexed-types/should_fail/OverA.hs b/testsuite/tests/indexed-types/should_fail/OverA.hs
new file mode 100644
index 0000000000..0f0573782f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/OverA.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module OverA (C, D)
+where
+
+data family C a b :: *
+
+type family D a b :: *
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/OverB.hs b/testsuite/tests/indexed-types/should_fail/OverB.hs
new file mode 100644
index 0000000000..6f1546d19f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/OverB.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module OverB
+where
+import OverA (C, D)
+
+data instance C [Int] [a] = CListList2
+
+type instance D [Int] [a] = Int
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/OverC.hs b/testsuite/tests/indexed-types/should_fail/OverC.hs
new file mode 100644
index 0000000000..01f82d9170
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/OverC.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module OverC
+where
+import OverA (C, D)
+
+data instance C [a] [Int] = C9ListList
+
+type instance D [a] [Int] = Char
diff --git a/testsuite/tests/indexed-types/should_fail/OverD.hs b/testsuite/tests/indexed-types/should_fail/OverD.hs
new file mode 100644
index 0000000000..3bce8de55e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/OverD.hs
@@ -0,0 +1,3 @@
+module OverD where
+import OverB
+import OverC
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs
new file mode 100644
index 0000000000..7235f67e02
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail10.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+class C8 a where
+  data S8 a :: * -> *
+
+instance C8 Int where
+  data S8 Int a = S8Int a
+
+-- must fail: extra arguments must be variables
+instance C8 Bool where
+  data S8 Bool Char = S8Bool
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr
new file mode 100644
index 0000000000..5fe00056b3
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail10.stderr
@@ -0,0 +1,6 @@
+
+SimpleFail10.hs:13:3:
+    Arguments that do not correspond to a class parameter must be variables
+    Instead of a variable, found Char
+    In the associated type instance for `S8'
+    In the instance declaration for `C8 Bool'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail11a.hs
new file mode 100644
index 0000000000..830b05fc75
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11a.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+data family C9 a b :: *
+data instance C9 Int Int = C9IntInt
+-- must fail: conflicting
+data instance C9 Int Int = C9IntInt2
+
+type family D9 a b :: *
+type instance D9 Int Int = Char
+-- must fail: conflicting
+type instance D9 Int Int = Int
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail11a.stderr
new file mode 100644
index 0000000000..23a8fd957d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11a.stderr
@@ -0,0 +1,10 @@
+
+SimpleFail11a.hs:8:15:
+    Conflicting family instance declarations:
+      data instance C9 Int Int -- Defined at SimpleFail11a.hs:8:15-16
+      data instance C9 Int Int -- Defined at SimpleFail11a.hs:6:15-16
+
+SimpleFail11a.hs:13:15:
+    Conflicting family instance declarations:
+      type instance D9 Int Int -- Defined at SimpleFail11a.hs:13:15-16
+      type instance D9 Int Int -- Defined at SimpleFail11a.hs:11:15-16
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11b.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail11b.hs
new file mode 100644
index 0000000000..f6aa7aa3b0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11b.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+data family C9 a b :: *
+data instance C9 Int Int = C9IntInt
+data instance C9 [a] Int = C9ListInt
+-- must fail: conflicting
+data instance C9 [a] Int = C9ListInt2
+
+type family D9 a b :: *
+type instance D9 Int Int = Int
+type instance D9 [a] Int = [a]
+-- must fail: conflicting
+type instance D9 [a] Int = Maybe a
+
+type instance D9 Int [a] = [a]
+type instance D9 Int [b] = [b]  -- must not conflict!
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail11b.stderr
new file mode 100644
index 0000000000..f32fe3a2bb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11b.stderr
@@ -0,0 +1,10 @@
+
+SimpleFail11b.hs:9:15:
+    Conflicting family instance declarations:
+      data instance C9 [a] Int -- Defined at SimpleFail11b.hs:9:15-16
+      data instance C9 [a] Int -- Defined at SimpleFail11b.hs:7:15-16
+
+SimpleFail11b.hs:15:15:
+    Conflicting family instance declarations:
+      type instance D9 [a] Int -- Defined at SimpleFail11b.hs:15:15-16
+      type instance D9 [a] Int -- Defined at SimpleFail11b.hs:13:15-16
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11c.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail11c.hs
new file mode 100644
index 0000000000..21d3f2b4ea
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11c.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+data family C9 a b :: *
+data instance C9 Int Int = C9IntInt
+data instance C9 [a] Int = C9ListInt
+-- must fail: conflicting
+data instance C9 [Int] Int = C9ListInt2
+
+type family D9 a b :: *
+type instance D9 Int Int = Int
+type instance D9 [a] Int = [a]
+-- must fail: conflicting
+type instance D9 [Int] Int = [Bool]
+
+type family E9 a b :: *
+type instance E9 Int   Int = Int
+type instance E9 [a]   Int = [a]
+type instance E9 [Int] Int = [Int]   -- does *not* conflict!
+type instance E9 b     Int = b
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11c.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail11c.stderr
new file mode 100644
index 0000000000..ccc897a626
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11c.stderr
@@ -0,0 +1,10 @@
+
+SimpleFail11c.hs:7:15:
+    Conflicting family instance declarations:
+      data instance C9 [a] Int -- Defined at SimpleFail11c.hs:7:15-16
+      data instance C9 [Int] Int -- Defined at SimpleFail11c.hs:9:15-16
+
+SimpleFail11c.hs:15:15:
+    Conflicting family instance declarations:
+      type instance D9 [Int] Int -- Defined at SimpleFail11c.hs:15:15-16
+      type instance D9 [a] Int -- Defined at SimpleFail11c.hs:13:15-16
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11d.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail11d.hs
new file mode 100644
index 0000000000..b0457a6933
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11d.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+data family C9 a b :: *
+data instance C9 Int Int = C9IntInt
+data instance C9 [a] Int = C9ListInt
+data instance C9 [Int] [a]   = C9ListList2
+-- must fail: conflicting
+data instance C9 [a]   [Int] = C9ListList
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail11d.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail11d.stderr
new file mode 100644
index 0000000000..1847565329
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail11d.stderr
@@ -0,0 +1,5 @@
+
+SimpleFail11d.hs:10:15:
+    Conflicting family instance declarations:
+      data instance C9 [a] [Int] -- Defined at SimpleFail11d.hs:10:15-16
+      data instance C9 [Int] [a] -- Defined at SimpleFail11d.hs:8:15-16
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail12.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail12.hs
new file mode 100644
index 0000000000..0c8ffefefe
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail12.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, Rank2Types #-}
+
+
+module ShouldFail where
+
+type family C a :: *
+-- must fail: rhs is not a tau type
+type instance C Int = forall a. [a]
+
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail12.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail12.stderr
new file mode 100644
index 0000000000..24ac5f10a1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail12.stderr
@@ -0,0 +1,4 @@
+
+SimpleFail12.hs:8:1:
+    Illegal polymorphic or qualified type: forall a. [a]
+    In the type synonym instance declaration for `C'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail13.hs
new file mode 100644
index 0000000000..bc94e2115a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+type family C a :: *
+
+data family D a :: *
+-- must fail: lhs contains a type family application
+data instance D [C a] = DC
+
+type family E a :: *
+-- must fail: lhs contains a type family application
+type instance E [C a] = Int
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
new file mode 100644
index 0000000000..f87d4059ae
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail13.stderr
@@ -0,0 +1,8 @@
+
+SimpleFail13.hs:9:1:
+    Illegal type synonym family application in instance: [C a]
+    In the data type instance declaration for `D'
+
+SimpleFail13.hs:13:1:
+    Illegal type synonym family application in instance: [C a]
+    In the type synonym instance declaration for `E'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail14.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail14.hs
new file mode 100644
index 0000000000..a25d81d3ba
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail14.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple14 where
+
+data T a = T (a~a)
+
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr
new file mode 100644
index 0000000000..e11f9500fb
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail14.stderr
@@ -0,0 +1,6 @@
+
+SimpleFail14.hs:5:15:
+    Predicate used as a type: a ~ a
+    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/SimpleFail15.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail15.hs
new file mode 100644
index 0000000000..586403937b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail15.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+foo :: (a,b) -> (a~b => t) -> (a,b)
+foo p x = p 
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail15.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail15.stderr
new file mode 100644
index 0000000000..8f97746510
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail15.stderr
@@ -0,0 +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)

diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail16.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail16.hs
new file mode 100644
index 0000000000..fc70df1fd8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail16.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+type family F a
+
+foo :: p a -> p a
+foo x = x
+
+bar = foo (undefined :: F ())
+
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
new file mode 100644
index 0000000000..0573e15aea
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail16.stderr
@@ -0,0 +1,6 @@
+
+SimpleFail16.hs:10:12:
+    Couldn't match type `F ()' with `p0 a0'
+    In the first argument of `foo', namely `(undefined :: F ())'
+    In the expression: foo (undefined :: F ())
+    In an equation for `bar': bar = foo (undefined :: F ())
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail1a.hs
new file mode 100644
index 0000000000..a87d5e515d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1a.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeFamilies #-}
+
+data family T1 a :: * -> *
+data instance T1 Int           = T1_1   -- must fail: too few args
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
new file mode 100644
index 0000000000..6bbbb32da9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1a.stderr
@@ -0,0 +1,4 @@
+
+SimpleFail1a.hs:4:1:
+    Family instance has too few parameters; expected 2
+    In the data type instance declaration for `T1'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1b.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.hs
new file mode 100644
index 0000000000..71ede91143
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeFamilies #-}
+
+data family T1 a :: * -> *
+data instance T1 Int Bool Char = T1_3   -- must fail: too many args
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
new file mode 100644
index 0000000000..e4db86bdf1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail1b.stderr
@@ -0,0 +1,4 @@
+
+SimpleFail1b.hs:4:1:
+    Family instance has too many parameters: `T1'
+    In the data type instance declaration for `T1'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs
new file mode 100644
index 0000000000..011426fe3b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Simple2a where
+
+class C a where
+  data Sd a :: *
+  data Sn a :: *
+  type St a :: *
+
+instance C Int where
+  data    Sd a :: *   -- must fail: parse error
+  data    Sd Int = SdC Char
+  newtype Sn Int = SnC Char
+  type    St Int = Char
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
new file mode 100644
index 0000000000..56e06e3145
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2a.stderr
@@ -0,0 +1,5 @@
+
+SimpleFail2a.hs:11:11:
+    Conflicting definitions for `Sd'
+    Bound at: SimpleFail2a.hs:11:11-12
+              SimpleFail2a.hs:12:11-12
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2b.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail2b.hs
new file mode 100644
index 0000000000..031b170a1a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2b.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+
+class C a where
+  data Sd a :: *
+  data Sn a :: *
+  type St a :: *
+
+instance C Int where
+  data    Sd Int = SdC1 Char	-- must fail: conflicting
+  data    Sd Int = SdC2 Char	--            declarations
+  newtype Sn Int = SnC Char
+  type    St Int = Char
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail2b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail2b.stderr
new file mode 100644
index 0000000000..cdb91dea58
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail2b.stderr
@@ -0,0 +1,5 @@
+
+SimpleFail2b.hs:9:11:
+    Conflicting definitions for `Sd'
+    Bound at: SimpleFail2b.hs:9:11-12
+              SimpleFail2b.hs:10:11-12
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail3a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail3a.hs
new file mode 100644
index 0000000000..87f68ab124
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail3a.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+class C1 a where
+  data S1 a :: *
+
+-- must fail: wrong category of type instance
+instance C1 Int where
+  type S1 Int = Bool
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail3a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail3a.stderr
new file mode 100644
index 0000000000..9a93d9fc90
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail3a.stderr
@@ -0,0 +1,5 @@
+
+SimpleFail3a.hs:10:3:
+    Wrong category of family instance; declaration was for a data type
+    In the type synonym instance declaration for `S1'
+    In the instance declaration for `C1 Int'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail3b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail3b.stderr
new file mode 100644
index 0000000000..419fe91492
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail3b.stderr
@@ -0,0 +1,3 @@
+
+SimpleFail3b.hs:10:2:
+    Wrong category of family instance; declaration was for a newtype
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs
new file mode 100644
index 0000000000..de674a39fd
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail4.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+-- must fail: defaults have no patterns
+class C2 a b where
+  type S2 a :: *
+  type S2 Int = Char
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
new file mode 100644
index 0000000000..0f42d5a572
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail4.stderr
@@ -0,0 +1,4 @@
+
+SimpleFail4.hs:8:3:
+    Type declaration in a class must be a kind signature or synonym default:
+    type instance S2 Int = Char
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5a.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.hs
new file mode 100644
index 0000000000..e50250d4e7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+class C3 a where
+  data    S3  a :: *
+  data    S3n a :: *
+  foo3  :: a -> S3 a
+  foo3n :: a -> S3n a
+  bar3  :: S3 a -> a
+  bar3n :: S3n a -> a
+
+instance C3 Int where
+  data    S3  Int  = D3Int
+  newtype S3n Int  = D3Intn ()
+  foo3  _          = D3Int
+  foo3n _          = D3Intn ()
+  bar3  D3Int      = 1
+  bar3n (D3Intn _) = 1
+
+instance C3 Char where
+  data S3 Char = D3Char
+  foo3 _       = D3Char
+  bar3 D3Char  = 'c'
+
+bar3' :: S3 Char -> Char
+bar3' D3Char = 'a'
+
+-- must fail: signature too general
+bar3wrong :: S3 a -> a
+bar3wrong D3Int  = 1
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
new file mode 100644
index 0000000000..861ef5c869
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr
@@ -0,0 +1,10 @@
+
+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
+    Expected type: S3 a
+      Actual type: S3 Int
+    In the pattern: D3Int
+    In an equation for `bar3wrong': bar3wrong D3Int = 1
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5b.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail5b.hs
new file mode 100644
index 0000000000..d05b3bcb36
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5b.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+class C3 a where
+  data    S3  a :: *
+  data    S3n a :: *
+  foo3  :: a -> S3 a
+  foo3n :: a -> S3n a
+  bar3  :: S3 a -> a
+  bar3n :: S3n a -> a
+
+instance C3 Int where
+  data    S3  Int  = D3Int
+  newtype S3n Int  = D3Intn ()
+  foo3  _          = D3Int
+  foo3n _          = D3Intn ()
+  bar3  D3Int      = 1
+  bar3n (D3Intn _) = 1
+
+instance C3 Char where
+  data S3 Char = D3Char
+  foo3 _       = D3Char
+  bar3 D3Char  = 'c'
+
+bar3' :: S3 Char -> Char
+bar3' D3Char = 'a'
+
+-- must fail: Can't match Int against Char
+bar3wrong' D3Int  = 1
+bar3wrong' D3Char = 'a'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr
new file mode 100644
index 0000000000..5a9d279860
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail5b.stderr
@@ -0,0 +1,7 @@
+
+SimpleFail5b.hs:31:12:
+    Couldn't match expected type `Int' with actual type `Char'
+      Expected type: S3 Int
+        Actual type: S3 Char
+    In the pattern: D3Char
+    In an equation for `bar3wrong'': bar3wrong' D3Char = 'a'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail6.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail6.hs
new file mode 100644
index 0000000000..8a39e6042d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail6.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+-- must fail: Repeated type variable
+class C4 a where
+  data S4 a a :: *
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail6.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail6.stderr
new file mode 100644
index 0000000000..c5c7e8a86a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail6.stderr
@@ -0,0 +1,2 @@
+
+SimpleFail6.hs:7:11: Illegal repeated type variable `a'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail7.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail7.hs
new file mode 100644
index 0000000000..3d9a089381
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail7.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+-- must fail: AT must be in class instance
+class C5 a where
+  data S5 a :: *
+data instance S5 Int = S5
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail7.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail7.stderr
new file mode 100644
index 0000000000..04131efe33
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail7.stderr
@@ -0,0 +1,4 @@
+
+SimpleFail7.hs:8:1:
+    Associated type `S5' must be inside a class instance
+    In the data type instance declaration for `S5'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail8.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail8.hs
new file mode 100644
index 0000000000..cefb00f5b0
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail8.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+-- must fail: C6 has no ATs S3 and Map
+class C6 a
+
+instance C6 Integer where
+  data Map Integer v = MapInteger
+  data S3 Integer = S3Integer
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail8.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail8.stderr
new file mode 100644
index 0000000000..88c71b690c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail8.stderr
@@ -0,0 +1,4 @@
+
+SimpleFail8.hs:9:8: Not in scope: type constructor or class `Map'
+
+SimpleFail8.hs:10:8: Not in scope: type constructor or class `S3'
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs
new file mode 100644
index 0000000000..d45c9830a4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
+
+module ShouldFail where
+
+class C7 a b where
+  data S7 b :: *
+
+instance C7 Char (a, Bool) where
+  data S7 (a, Bool) = S7_1
+
+-- must fail: type indexes don't match the instance types
+instance C7 Char (a, Int) where
+  data S7 (b, Int) = S7_2
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
new file mode 100644
index 0000000000..fb04fa8af7
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
@@ -0,0 +1,6 @@
+
+SimpleFail9.hs:13:3:
+    Type indexes must match class instance head
+    Found `(b, Int)' but expected `(a, Int)'
+    In the associated type instance for `S7'
+    In the instance declaration for `C7 Char (a, Int)'
diff --git a/testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.hs b/testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.hs
new file mode 100644
index 0000000000..ce86d7beab
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls #-}
+
+module SkolemOccursLoop where
+
+-- SkelemOccurs tests by Tom and Martin
+
+data T x
+type family F x
+type instance F [x] = [T (F x)]
+
+t :: a -> a -> Bool
+t _ _ = True
+
+f :: a -> F [a]
+f = undefined
+
+test1 :: (F [a] ~ a) => a -> Bool
+test1 x = t x (f x)
+
+--
+
+data S a
+type family G x
+type instance G (S x, y) = S (G (x,y))
+
+g :: a -> G [a]
+g = undefined
+
+test2 :: (G (S a,a) ~ a) => a -> Bool
+-- inferred: G [a] ~ a => a -> Bool
+test2 x = t x (g x)
diff --git a/testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.stderr b/testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.stderr
new file mode 100644
index 0000000000..0900da8e33
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.stderr
@@ -0,0 +1,10 @@
+
+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'
diff --git a/testsuite/tests/indexed-types/should_fail/T1900.hs b/testsuite/tests/indexed-types/should_fail/T1900.hs
new file mode 100644
index 0000000000..efcfbc1391
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T1900.hs
@@ -0,0 +1,73 @@
+{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
+
+module Class4 where
+
+class  (Eq (Depend s)) => Bug s where
+  type Depend s 
+  trans :: Depend s -> Depend s
+  
+instance Bug Int where
+  type Depend Int = ()
+  trans = (+1)
+
+check :: (Bug s) => Depend s -> Bool
+check d = d == trans d
+
+{-
+ Given: (Bug s, Eq (Depend s))
+      = (Bug s, Eq fsk, Depend s ~ fsk)
+
+ Wanted: (Eq alpha,                 (invocation of == at alpha)
+          Depend s ~ alpha          (first arg of ==)
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+          Depend sigma ~ Depend s   (first arg of trans)
+
+          {der}Eq (Depend sigma)    (superclass of Bug sigma)
+
+==>
+ Wanted: (Eq alpha,                 (invocation of == at alpha)
+          Depend s ~ alpha          (first arg of ==)
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+          {der}Eq (Depend sigma)    (superclass of Bug sigma)
+
+==>
+ Wanted: (Eq alpha,                 (invocation of == at alpha)
+          Depend s ~ alpha          (first arg of ==)
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+
+          {der}Eq uf_ahj
+          Depend sigma ~ uf_ahj
+
+==> uf := alpha
+ Wanted: (Eq alpha,                 (invocation of == at alpha)
+          Depend s ~ alpha          (first arg of ==)
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+          {der}Eq alpha)
+==> discharge Eq alpha from {der}
+ Wanted: (Depend s ~ alpha          (first arg of ==)
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+          {der}Eq alpha)
+
+==> use given Depend s ~ fsk
+ Wanted: (alpha ~ fsk
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+          {der}Eq alpha)
+
+==> alpha := fsk
+ Wanted: ({given}alpha ~ fsk
+          Depend sigma ~ alpha      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+          {der}Eq fsk)
+
+==> discharge {der} Eq fsk
+ Wanted: ({given}uf ~ fsk
+          Depend sigma ~ uf      (second arg of ==)
+          Bug sigma,                (invocation of trans at sigma)
+
+-}
diff --git a/testsuite/tests/indexed-types/should_fail/T1900.stderr b/testsuite/tests/indexed-types/should_fail/T1900.stderr
new file mode 100644
index 0000000000..4e3be835c4
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T1900.stderr
@@ -0,0 +1,18 @@
+
+T1900.hs:11:13:
+    No instance for (Num ())
+      arising from the literal `1'
+    Possible fix: add an instance declaration for (Num ())
+    In the second argument of `(+)', namely `1'
+    In the expression: (+ 1)
+    In an equation for `trans': trans = (+ 1)
+
+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
+    NB: `Depend' is a type function, and may not be injective
+    In the first argument of `trans', namely `d'
+    In the second argument of `(==)', namely `trans d'
+    In the expression: d == trans d
diff --git a/testsuite/tests/indexed-types/should_fail/T2157.hs b/testsuite/tests/indexed-types/should_fail/T2157.hs
new file mode 100644
index 0000000000..c9e562051e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2157.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies, LiberalTypeSynonyms #-}
+
+module T2157 where
+
+type S a b = a
+type family F a :: * -> *
+type instance F a = S a
diff --git a/testsuite/tests/indexed-types/should_fail/T2157.stderr b/testsuite/tests/indexed-types/should_fail/T2157.stderr
new file mode 100644
index 0000000000..b28f879663
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2157.stderr
@@ -0,0 +1,4 @@
+
+T2157.hs:7:1:
+    Type synonym `S' should have 2 arguments, but has been given 1
+    In the type synonym instance declaration for `F'
diff --git a/testsuite/tests/indexed-types/should_fail/T2203a.hs b/testsuite/tests/indexed-types/should_fail/T2203a.hs
new file mode 100644
index 0000000000..89ed37e3da
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2203a.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ScopedTypeVariables, TypeFamilies, FlexibleInstances #-}
+
+module T2203a where
+
+class Foo a where
+   type TheFoo a
+   foo :: TheFoo a -> a
+   foo' :: a -> Int
+
+class Bar b where
+   bar :: b -> Int
+
+instance Foo a => Bar (Either a (TheFoo a)) where
+   bar (Left a) = foo' a
+   bar (Right b) = foo' (foo b :: a)
diff --git a/testsuite/tests/indexed-types/should_fail/T2203a.stderr b/testsuite/tests/indexed-types/should_fail/T2203a.stderr
new file mode 100644
index 0000000000..cd12f6a7be
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2203a.stderr
@@ -0,0 +1,5 @@
+
+T2203a.hs:13:19:
+    Illegal type synonym family application in instance:
+        Either a (TheFoo a)
+    In the instance declaration for `Bar (Either a (TheFoo a))'
diff --git a/testsuite/tests/indexed-types/should_fail/T2239.hs b/testsuite/tests/indexed-types/should_fail/T2239.hs
new file mode 100644
index 0000000000..750fdd941c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2239.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE NoMonomorphismRestriction, RankNTypes #-}
+{-# LANGUAGE FunctionalDependencies, MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T2239 where
+
+data A = A
+data B = B
+
+class C a where c :: a -> String
+instance C Bool where c _ = "Bool"
+instance C Char where c _ = "Char"
+
+-- via TFs
+type family TF a
+type instance TF A = Char
+type instance TF B = Bool
+
+tf :: forall a b. (b ~ TF a,C b) => a -> String
+tf a = c (undefined:: b) 
+
+tfa = tf A
+tfb = tf B
+
+-- via FDs
+class FD a b | a -> b
+instance FD A Char
+instance FD B Bool
+
+fd :: forall a b. (FD a b,C b) => a -> String
+fd a = c (undefined:: b) 
+
+fda = fd A
+fdb = fd B
+
+
+class MyEq a b | a->b, b->a
+instance MyEq a a
+
+simpleFD = id :: (forall b. MyEq b Bool => b->b) 
+
+simpleTF = id :: (forall b. b~Bool => b->b)
+
+-- These two both involve impredicative instantiation,
+-- and should fail (in the same way)
+complexFD = id :: (forall b. MyEq b Bool => b->b)
+               -> (forall b. MyEq b Bool => b->b)
+
+complexTF = id :: (forall b. b~Bool => b->b)
+               -> (forall b. b~Bool => b->b)
diff --git a/testsuite/tests/indexed-types/should_fail/T2239.stderr b/testsuite/tests/indexed-types/should_fail/T2239.stderr
new file mode 100644
index 0000000000..b8d5fc7a36
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2239.stderr
@@ -0,0 +1,30 @@
+
+T2239.hs:47:13:
+    Couldn't match expected type `b -> b'
+                with actual type `forall b1. MyEq b1 Bool => b1 -> b1'
+    Expected type: (forall b1. MyEq b1 Bool => b1 -> b1) -> b -> b
+      Actual type: (forall b1. MyEq b1 Bool => b1 -> b1)
+                   -> forall b1. MyEq b1 Bool => b1 -> b1
+    In the expression:
+        id ::
+          (forall b. MyEq b Bool => b -> b)
+          -> (forall b. MyEq b Bool => b -> b)
+    In an equation for `complexFD':
+        complexFD
+          = id ::
+              (forall b. MyEq b Bool => b -> b)
+              -> (forall b. MyEq b Bool => b -> b)
+
+T2239.hs:50:13:
+    Couldn't match expected type `b -> b'
+                with actual type `forall b1. b1 ~ Bool => b1 -> b1'
+    Expected type: (forall b1. b1 ~ Bool => b1 -> b1) -> b -> b
+      Actual type: (forall b1. b1 ~ Bool => b1 -> b1)
+                   -> forall b1. b1 ~ Bool => b1 -> b1
+    In the expression:
+        id ::
+          (forall b. b ~ Bool => b -> b) -> (forall b. b ~ Bool => b -> b)
+    In an equation for `complexTF':
+        complexTF
+          = id ::
+              (forall b. b ~ Bool => b -> b) -> (forall b. b ~ Bool => b -> b)
diff --git a/testsuite/tests/indexed-types/should_fail/T2334.hs b/testsuite/tests/indexed-types/should_fail/T2334.hs
new file mode 100644
index 0000000000..c73402e2d5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2334.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE TypeFamilies #-}
+
+-- Trac #2334
+
+module Test where
+
+data family F r
+
+newtype instance F ()  = F () () deriving Eq
+newtype instance F Int  = H deriving Eq
+
+data instance F Bool = K1
+data instance F Bool = K2
+
+
+
diff --git a/testsuite/tests/indexed-types/should_fail/T2334.stderr b/testsuite/tests/indexed-types/should_fail/T2334.stderr
new file mode 100644
index 0000000000..5bb3e24c22
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2334.stderr
@@ -0,0 +1,17 @@
+
+T2334.hs:9:26:
+    The constructor of a newtype must have exactly one field
+      but `F' has two
+    In the definition of data constructor `F'
+    In the newtype instance declaration for `F'
+
+T2334.hs:10:27:
+    The constructor of a newtype must have exactly one field
+      but `H' has none
+    In the definition of data constructor `H'
+    In the newtype instance declaration for `F'
+
+T2334.hs:13:15:
+    Conflicting family instance declarations:
+      data instance F Bool -- Defined at T2334.hs:13:15
+      data instance F Bool -- Defined at T2334.hs:12:15
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.hs b/testsuite/tests/indexed-types/should_fail/T2544.hs
new file mode 100644
index 0000000000..22f3995286
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2544.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeOperators, TypeFamilies #-}

+

+module T2544 where

+

+data (:|:) a b = Inl a | Inr b

+

+class Ix i where

+   type IxMap i :: * -> *

+   empty  :: IxMap i [Int]

+

+data BiApp a b c = BiApp (a c) (b c)

+

+instance (Ix l, Ix r) => Ix (l :|: r) where

+   type IxMap (l :|: r) = BiApp (IxMap l) (IxMap r)

+   empty = BiApp empty empty
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
new file mode 100644
index 0000000000..6c977bf833
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -0,0 +1,22 @@
+
+T2544.hs:15:18:
+    Could not deduce (IxMap i0 ~ IxMap l)
+    from the context (Ix l, Ix r)
+      bound by the instance declaration at T2544.hs:13:10-37
+    NB: `IxMap' is a type function, and may not be injective
+    Expected type: IxMap l [Int]
+      Actual type: IxMap i0 [Int]
+    In the first argument of `BiApp', namely `empty'
+    In the expression: BiApp empty empty
+    In an equation for `empty': empty = BiApp empty empty
+
+T2544.hs:15:24:
+    Could not deduce (IxMap i1 ~ IxMap r)
+    from the context (Ix l, Ix r)
+      bound by the instance declaration at T2544.hs:13:10-37
+    NB: `IxMap' is a type function, and may not be injective
+    Expected type: IxMap r [Int]
+      Actual type: IxMap i1 [Int]
+    In the second argument of `BiApp', namely `empty'
+    In the expression: BiApp empty empty
+    In an equation for `empty': empty = BiApp empty empty
diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.hs b/testsuite/tests/indexed-types/should_fail/T2627b.hs
new file mode 100644
index 0000000000..13dbd9cb26
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2627b.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GADTs, TypeFamilies, EmptyDataDecls #-}
+
+module T2627b where
+
+data R a b
+data W a b
+data Z
+
+type family Dual a
+type instance Dual Z = Z
+type instance Dual (R a b) = W a (Dual b)
+type instance Dual (W a b) = R a (Dual b)
+
+data Comm a where
+    Rd :: (a -> Comm b) -> Comm (R a b)
+    Wr :: a  -> Comm b  -> Comm (W a b)
+    Fin :: Int -> Comm Z
+
+conn :: (Dual a ~ b, Dual b ~ a) => Comm a -> Comm b -> (Int, Int)
+conn (Rd k) (Wr a r) = conn undefined undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T2627b.stderr b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
new file mode 100644
index 0000000000..a8e232486b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2627b.stderr
@@ -0,0 +1,7 @@
+
+T2627b.hs:20:24:
+    Occurs check: cannot construct the infinite type:
+      a0 = Dual (Dual a0)
+    In the expression: conn undefined undefined
+    In an equation for `conn':
+        conn (Rd k) (Wr a r) = conn undefined undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.hs b/testsuite/tests/indexed-types/should_fail/T2664.hs
new file mode 100644
index 0000000000..d5b04a6380
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2664.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE EmptyDataDecls, TypeFamilies, TypeOperators, ScopedTypeVariables #-}
+module Overflow where
+import Control.Concurrent
+
+data (:*:) a b
+data (:+:) a b
+
+data family PChan a
+data    instance PChan (a :+: b) = E (IO (PChan a)) (IO (PChan b))
+newtype instance PChan (a :*: b) = O (IO (Either (PChan a) (PChan b)))
+
+type family Dual a
+type instance Dual (a :+: b) = Dual a :*: Dual b
+type instance Dual (a :*: b) = Dual a :+: Dual b
+
+class Connect s where
+    newPChan :: (s ~ Dual c, c ~ Dual s) => IO (PChan s, PChan c)
+
+pchoose :: (t -> a) -> MVar a -> IO (t,b) -> IO b
+pchoose = undefined
+
+instance (Connect a, Connect b) => Connect (a :*: b) where
+    newPChan = do
+        v <- newEmptyMVar
+
+        -- This version is in T2664a
+        -- correct implementation:
+        -- return (O $ takeMVar v, E (pchoose Left v newPChan) (pchoose Right v newPChan))
+       
+        -- type error leads to stack overflow (even without UndecidableInstances!)
+        return (O $ takeMVar v, E (pchoose Right v newPChan) (pchoose Left v newPChan))
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
new file mode 100644
index 0000000000..b3b8428a55
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -0,0 +1,18 @@
+
+T2664.hs:31:33:
+    Could not deduce (Dual a ~ Dual b)
+    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))
+      bound by the type signature for
+                 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)
diff --git a/testsuite/tests/indexed-types/should_fail/T2664a.hs b/testsuite/tests/indexed-types/should_fail/T2664a.hs
new file mode 100644
index 0000000000..b7a3033723
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2664a.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE EmptyDataDecls, TypeFamilies, TypeOperators, ScopedTypeVariables #-}
+module Overflow where
+import Control.Concurrent
+
+data (:*:) a b
+data (:+:) a b
+
+data family PChan a
+data    instance PChan (a :+: b) = E (IO (PChan a)) (IO (PChan b))
+newtype instance PChan (a :*: b) = O (IO (Either (PChan a) (PChan b)))
+
+type family Dual a
+type instance Dual (a :+: b) = Dual a :*: Dual b
+type instance Dual (a :*: b) = Dual a :+: Dual b
+
+class Connect s where
+    newPChan :: (s ~ Dual c, c ~ Dual s) => IO (PChan s, PChan c)
+
+pchoose :: (t -> a) -> MVar a -> IO (t,b) -> IO b
+pchoose = undefined
+
+instance (Connect a, Connect b) => Connect (a :*: b) where
+    newPChan = do
+        v <- newEmptyMVar
+        -- correct implementation:
+        return (O $ takeMVar v, E (pchoose Left v newPChan) (pchoose Right v newPChan))
+       
+        -- This version is in T2664
+        -- type error leads to stack overflow (even without UndecidableInstances!)
+        --return (O $ takeMVar v, E (pchoose Right v newPChan) (pchoose Left v newPChan))
diff --git a/testsuite/tests/indexed-types/should_fail/T2677.hs b/testsuite/tests/indexed-types/should_fail/T2677.hs
new file mode 100644
index 0000000000..93288ba40d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2677.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T2677 where
+
+type family A x
+type instance A a = Bool
+type instance A Int = Char
diff --git a/testsuite/tests/indexed-types/should_fail/T2677.stderr b/testsuite/tests/indexed-types/should_fail/T2677.stderr
new file mode 100644
index 0000000000..e1c08e3b15
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2677.stderr
@@ -0,0 +1,5 @@
+
+T2677.hs:7:15:
+    Conflicting family instance declarations:
+      type instance A Int -- Defined at T2677.hs:7:15
+      type instance A a -- Defined at T2677.hs:6:15
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.hs b/testsuite/tests/indexed-types/should_fail/T2693.hs
new file mode 100644
index 0000000000..5b0066e948
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2693.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T2693 where
+
+type family TFn a :: *
+
+f :: Maybe ()
+f = do
+  let Just x = undefined :: Maybe (TFn a)
+  let n = fst x + fst x
+  return ()
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
new file mode 100644
index 0000000000..2072d53296
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -0,0 +1,7 @@
+
+T2693.hs:9:16:
+    Couldn't match type `TFn a0' with `(a1, b0)'
+    Expected type: Maybe (a1, b0)
+      Actual type: Maybe (TFn a0)
+    In the expression: undefined :: Maybe (TFn a)
+    In a pattern binding: Just x = undefined :: Maybe (TFn a)
diff --git a/testsuite/tests/indexed-types/should_fail/T2888.hs b/testsuite/tests/indexed-types/should_fail/T2888.hs
new file mode 100644
index 0000000000..169eebb474
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T2888.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeFamilies #-}
+-- Test for no type indices
+
+module T2888 where
+
+class C w where 
+  data D:: * -> *
diff --git a/testsuite/tests/indexed-types/should_fail/T3092.hs b/testsuite/tests/indexed-types/should_fail/T3092.hs
new file mode 100644
index 0000000000..e3a671e67e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3092.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+module T3092 where
+
+data T a = T1 a
+data instance T Int = T2 Char
+
+type S b = b
+type instance S Int = Char
+ 
diff --git a/testsuite/tests/indexed-types/should_fail/T3092.stderr b/testsuite/tests/indexed-types/should_fail/T3092.stderr
new file mode 100644
index 0000000000..ceea069f8f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3092.stderr
@@ -0,0 +1,10 @@
+
+T3092.hs:5:1:
+    Illegal family instance for `T'
+      (T is not an indexed type family)
+    In the data type instance declaration for `T'
+
+T3092.hs:8:1:
+    Illegal family instance for `S'
+      (S is not an indexed type family)
+    In the type synonym instance declaration for `S'
diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.hs b/testsuite/tests/indexed-types/should_fail/T3330a.hs
new file mode 100644
index 0000000000..c09eb0fd5c
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- A very bogus program (multiple errors) but
+-- sent GHC 6.12 into a loop
+
+module T3330a where
+
+import Control.Monad.Writer
+
+data AnyF (s :: * -> *) = AnyF
+class HFunctor (f :: (* -> *) -> * -> *)
+type family PF (phi :: * -> *) :: (* -> *) -> * -> *
+
+children :: s ix -> (PF s) r ix -> [AnyF s]
+children p x = execWriter (hmapM p collect x)
+
+collect :: HFunctor (PF s) => s ix -> r ix -> Writer [AnyF s] (r ix)
+collect = undefined
+
+hmapM :: (forall ix. phi ix -> r ix -> m (r' ix))
+      -> phi ix -> f r ix -> m (f r' ix)
+hmapM = undefined
+
diff --git a/testsuite/tests/indexed-types/should_fail/T3330a.stderr b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
new file mode 100644
index 0000000000..cfe7f67270
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3330a.stderr
@@ -0,0 +1,9 @@
+
+T3330a.hs:17:34:
+    Couldn't match type `s' with `(->) (s 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:17:1
+    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)
diff --git a/testsuite/tests/indexed-types/should_fail/T3330b.hs b/testsuite/tests/indexed-types/should_fail/T3330b.hs
new file mode 100644
index 0000000000..05d2282304
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3330b.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+-- Bizarrely this made 6.10 loop
+
+module T3330b where
+
+class RFunctor c a b where
+    type Res c a b :: *
+    rmap :: (a -> b) -> c -> Res c a b
+
+instance (a ~ c) => RFunctor c a b where
+    type Res c a b = b
+    rmap f = f
+
+instance (RFunctor c a b, a ~ c) => RFunctor [c] a b where
+    type Res [c] a b = [b]
+    rmap f = map (map f)
diff --git a/testsuite/tests/indexed-types/should_fail/T3330b.stderr b/testsuite/tests/indexed-types/should_fail/T3330b.stderr
new file mode 100644
index 0000000000..927bd5b483
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3330b.stderr
@@ -0,0 +1,5 @@
+
+T3330b.hs:14:10:
+    Conflicting family instance declarations:
+      type Res c a b -- Defined at T3330b.hs:14:10-12
+      type Res [c] a b -- Defined at T3330b.hs:18:10-12
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.hs b/testsuite/tests/indexed-types/should_fail/T3330c.hs
new file mode 100644
index 0000000000..e6c4dfbb30
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE EmptyDataDecls, TypeFamilies, TypeOperators, GADTs, KindSignatures #-}
+
+module T3330c where
+
+data (f :+: g) x = Inl (f x) | Inr (g x)
+
+data R :: (* -> *) -> * where
+  RSum  :: R f -> R g -> R (f :+: g)
+
+class Rep f where
+  rep :: R f
+
+instance (Rep f, Rep g) => Rep (f :+: g) where
+  rep = RSum rep rep
+
+type family Der (f :: * -> *) :: * -> *
+type instance Der (f :+: g) = Der f :+: Der g
+
+plug :: Rep f => Der f x -> x -> f x
+plug = plug' rep where
+
+plug' :: R f -> Der f x -> x -> f x
+plug' (RSum rf rg) (Inl df) x = Inl (plug rf df x)
+
+{-
+rf :: R f1, rg :: R g1
+Given by GADT match: f ~ f1 :+: g1
+
+Second arg has type (Der f x)
+    = (Der (f1:+:g1) x)
+    = (:+:) (Der f1) (Der g1) x
+Hence df :: Der f1 x
+
+Inl {f3,g3,x} (plug {f2,x1} rf df x)  gives rise to
+  result of Inl:   ((:+:) f3 g3 x ~ f x)
+  first arg (rf):  (R f1 ~ Der f2 x1)
+  second arg (df): (Der f1 x ~ x1)
+  result of plug:  (f2 x1 ~ x -> f3 x)
+
+  result of Inl: ((:+:) f3 g3 x ~ f x)
+       by given  ((:+:) f3 g3 x ~ (:+:) f1 g1 x)
+  hence need f3~f1, g3~g1
+
+So we are left with
+   first arg:      (R f1 ~ Der f2 x1)
+   second arg:     (Der f1 x ~ x1)
+   result:         (f2 x1  ~  (->) x (f3 x))
+
+Decompose result:
+          f2 ~ (->) x
+          x1 ~ f1 x
+Hence
+        first:  R f1 ~ Der ((->) x) (f1 x)
+  decompose  : R ~ Der ((->) x)
+               f1 ~ f1 x
+
+
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
new file mode 100644
index 0000000000..4ca19f8a4e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -0,0 +1,18 @@
+
+T3330c.hs:23:43:
+    Couldn't match type `f1' with `f1 x'
+      `f1' is a rigid type variable bound by
+           a pattern with constructor
+             RSum :: forall (f :: * -> *) (g :: * -> *).
+                     R f -> R g -> R (f :+: g),
+           in an equation for `plug''
+           at T3330c.hs:23:8
+    In the first argument of `plug', namely `rf'
+    In the first argument of `Inl', namely `(plug rf df x)'
+    In the expression: Inl (plug rf df x)
+
+T3330c.hs:23:43:
+    Couldn't match type `Der ((->) x)' with `R'
+    In the first argument of `plug', namely `rf'
+    In the first argument of `Inl', namely `(plug rf df x)'
+    In the expression: Inl (plug rf df x)
diff --git a/testsuite/tests/indexed-types/should_fail/T3440.hs b/testsuite/tests/indexed-types/should_fail/T3440.hs
new file mode 100644
index 0000000000..0bf1544009
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3440.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TypeFamilies, GADTs #-}
+
+module T3440 where
+
+type family Fam a :: *
+
+data GADT :: * -> * where
+   GADT :: a -> Fam a -> GADT (Fam a)
+
+unwrap :: GADT (Fam a) -> (a, Fam a)
+unwrap (GADT x y) = (x, y)
diff --git a/testsuite/tests/indexed-types/should_fail/T3440.stderr b/testsuite/tests/indexed-types/should_fail/T3440.stderr
new file mode 100644
index 0000000000..fe61b1da65
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T3440.stderr
@@ -0,0 +1,19 @@
+
+T3440.hs:11:22:
+    Could not deduce (a1 ~ a)
+    from the context (Fam a ~ Fam a1)
+      bound by a pattern with constructor
+                 GADT :: forall a. a -> Fam a -> GADT (Fam a),
+               in an equation for `unwrap'
+      at T3440.hs:11:9-16
+      `a1' is a rigid type variable bound by
+           a pattern with constructor
+             GADT :: forall a. a -> Fam a -> GADT (Fam a),
+           in an equation for `unwrap'
+           at T3440.hs:11:9
+      `a' is a rigid type variable bound by
+          the type signature for unwrap :: GADT (Fam a) -> (a, Fam a)
+          at T3440.hs:11:1
+    In the expression: x
+    In the expression: (x, y)
+    In an equation for `unwrap': unwrap (GADT x y) = (x, y)
diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.hs b/testsuite/tests/indexed-types/should_fail/T4093a.hs
new file mode 100644
index 0000000000..06168f577e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4093a.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}

+module T4093a where

+

+type family Foo x

+type instance Foo () = Maybe ()

+

+hang :: (Foo e ~ Maybe e) => Foo e

+hang = Just ()

diff --git a/testsuite/tests/indexed-types/should_fail/T4093a.stderr b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
new file mode 100644
index 0000000000..0b36936be9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4093a.stderr
@@ -0,0 +1,14 @@
+
+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
+      `e' is a rigid type variable bound by
+          the type signature for hang :: Foo e ~ Maybe e => Foo e
+          at T4093a.hs:8:1
+    Expected type: Foo e
+      Actual type: Maybe ()
+    In the return type of a call of `Just'
+    In the expression: Just ()
+    In an equation for `hang': hang = Just ()
diff --git a/testsuite/tests/indexed-types/should_fail/T4093b.hs b/testsuite/tests/indexed-types/should_fail/T4093b.hs
new file mode 100644
index 0000000000..2d9878541f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4093b.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE GADTs, EmptyDataDecls, ScopedTypeVariables, TypeFamilies #-}

+

+module T4093b where

+

+data C

+data O

+

+type family   EitherCO e a b :: *

+type instance EitherCO C a b = a

+type instance EitherCO O a b = b

+

+data MaybeC ex t where

+  JustC    :: t -> MaybeC C t

+  NothingC ::      MaybeC O t

+

+data Block (n :: * -> * -> *) e x

+

+

+blockToNodeList ::

+  forall n e x. (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

+

+type A e x n = (MaybeC e (n C O), MaybeC x (n O C))

+blockToNodeList b = foldBlockNodesF (f, l) b z 

+  where

+    z :: EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))

+    z = undefined

+

+    f :: n C O -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)

+    f n _ = (JustC n, NothingC)

+

+    l :: n O C -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C C n) (A O C n)

+    l _ = undefined

+

+foldBlockNodesF  :: forall n a b c e x .

+                   ( n C O       -> a -> b

+                   , n O C       -> b -> c)

+                 -> (Block n e x -> EitherCO e a b -> EitherCO x c b)

+foldBlockNodesF _ = undefined

diff --git a/testsuite/tests/indexed-types/should_fail/T4093b.stderr b/testsuite/tests/indexed-types/should_fail/T4093b.stderr
new file mode 100644
index 0000000000..6818e006ef
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4093b.stderr
@@ -0,0 +1,32 @@
+
+T4093b.hs:31:13:
+    Could not deduce (e ~ C)
+    from the context (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)
+      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)-(34,19)
+      `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
+    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)
+    In an equation for `f': f n _ = (JustC n, NothingC)
+    In an equation for `blockToNodeList':
+        blockToNodeList b
+          = foldBlockNodesF (f, l) b z
+          where
+              z ::
+                EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))
+              z = undefined
+              f ::
+                n C O
+                -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
+              f n _ = (JustC n, NothingC)
+              ....
diff --git a/testsuite/tests/indexed-types/should_fail/T4099.hs b/testsuite/tests/indexed-types/should_fail/T4099.hs
new file mode 100644
index 0000000000..1ca3c7a4a5
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4099.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T4099 where
+
+type family T a
+
+foo :: T a -> Int
+foo x = error "urk"
+
+bar1 :: T b -> Int
+bar1 x = foo x
+
+bar2 :: Maybe b -> Int
+bar2 x = foo x
diff --git a/testsuite/tests/indexed-types/should_fail/T4099.stderr b/testsuite/tests/indexed-types/should_fail/T4099.stderr
new file mode 100644
index 0000000000..1f5a917296
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4099.stderr
@@ -0,0 +1,13 @@
+
+T4099.hs:11:14:
+    Couldn't match type `T b' with `T a0'
+    NB: `T' is a type function, and may not be injective
+    In the first argument of `foo', namely `x'
+    In the expression: foo x
+    In an equation for `bar1': bar1 x = foo x
+
+T4099.hs:14:14:
+    Couldn't match type `T a1' with `Maybe b'
+    In the first argument of `foo', namely `x'
+    In the expression: foo x
+    In an equation for `bar2': bar2 x = foo x
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.hs b/testsuite/tests/indexed-types/should_fail/T4174.hs
new file mode 100644
index 0000000000..784c0baa08
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4174.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, EmptyDataDecls #-}
+
+module T4174 where
+
+data True
+data False
+
+data Minor1
+
+data GHC6'8 m
+data GHC6'10 m
+
+type family a :<=: b :: {-Bool-}*
+type instance GHC6'10 m1 :<=: GHC6'8 m2 = False
+
+type a :>=: b = b :<=: a
+
+data Way ghcVersion tablesNextToCode profiling threaded
+
+type family GHCVersion way :: {-GHCVersion-} *
+type instance GHCVersion (Way v n p t) = v
+
+type family Threaded way :: {-Bool-} *
+type instance Threaded (Way v n p t) = t
+
+data Field w s t
+data SmStep
+data RtsSpinLock
+
+field :: String -> m (Field w a b)
+field = undefined
+
+type family WayOf (m :: * -> *) :: *
+
+sync_large_objects :: (Monad m, 
+                       (GHCVersion (WayOf m) :>=: GHC6'10 Minor1) ~ True, 
+                       Threaded (WayOf m) ~ True) 
+                   => m (Field (WayOf m) SmStep RtsSpinLock)
+sync_large_objects = field "sync_large_objects"
+
+testcase :: Monad m => m (Field (Way (GHC6'8 minor) n t p) a b)
+testcase = sync_large_objects
+
+{- Wanted constraints from the occurrence of sync_large_objects
+
+   (WayOf m) ~ (Way (GHC6'8 minor) n t p)
+   a ~ SmStep
+   b ~ RtsSpinLock
+
+   Threaded (WayOf m) ~ True 
+     == Threaded (Way (GHC6'8 minor) n t p) ~ True 
+     == p ~ True   
+
+   (GHCVersion (WayOf m) :>=: GHC6'10 Minor1) ~ True, 
+     == (GHC6'10 Minor1 :<=: GHCVersion (WayOf m)) ~ True, 
+     == (GHC6'10 Minor1 :<=: GHCVersion (Way (GHC6'8 minor) n t p))) ~ True, 
+     == (GHC6'10 Minor1 :<=: GHC6'8 minor) ~ True
+     == False ~ True
+
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr b/testsuite/tests/indexed-types/should_fail/T4174.stderr
new file mode 100644
index 0000000000..2a403786d9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr
@@ -0,0 +1,5 @@
+
+T4174.hs:42:12:
+    Couldn't match type `False' with `True'
+    In the expression: sync_large_objects
+    In an equation for `testcase': testcase = sync_large_objects
diff --git a/testsuite/tests/indexed-types/should_fail/T4174.stderr-ghc-7.0 b/testsuite/tests/indexed-types/should_fail/T4174.stderr-ghc-7.0
new file mode 100644
index 0000000000..81fb603dd8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4174.stderr-ghc-7.0
@@ -0,0 +1,7 @@
+
+T4174.hs:42:12:
+    Couldn't match type `False' with `True'
+    Expected type: True
+      Actual type: GHCVersion (WayOf m) :>=: GHC6'10 Minor1
+    In the expression: sync_large_objects
+    In an equation for `testcase': testcase = sync_large_objects
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.hs b/testsuite/tests/indexed-types/should_fail/T4179.hs
new file mode 100644
index 0000000000..ee54100ccc
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4179.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE TypeFamilies  #-}
+
+module T4179 where
+
+class DoC a where
+     type A2 a
+     type A3 a
+     op :: a -> A2 a -> A3 a
+
+data Con x = InCon (x (Con x))
+type FCon x = x (Con x)
+
+-- should have been changed to this, which works
+-- foldDoC :: Functor f => (f a -> a) -> A2 (FCon f) -> Con f -> a
+-- foldDoC f i (InCon t) = f (fmap (foldDoC f i) t)
+-- this original version causes GHC to hang 
+foldDoC :: Functor f => (f a -> a) -> Con f -> a 
+foldDoC f (InCon t) = f (fmap (foldDoC f) t)
+
+doCon :: (DoC (FCon x)) => Con x -> A2 (FCon x) -> A3 (FCon x) 
+doCon (InCon x) = op x
+
+-- Note that if this is commented out then there's no hang: 
+-- presumably because GHC doesn't have to perform type deduction for foldDoC.
+fCon :: (Functor x, DoC (FCon x)) => Con x -> A2 (FCon x) -> A3 (FCon x) 
+fCon = foldDoC op
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
new file mode 100644
index 0000000000..50c1ad5365
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -0,0 +1,63 @@
+
+T4179.hs:26:16:
+    Could not deduce (DoC (x (A2 (FCon x) -> A3 (FCon x))))
+      arising from a use of `op'
+    from the context (Functor x, DoC (FCon x))
+      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
+    Possible fix:
+      add (DoC (x (A2 (FCon x) -> A3 (FCon x)))) to the context of
+        the type signature for
+          fCon :: (Functor x, DoC (FCon x)) =>
+                  Con x -> A2 (FCon x) -> A3 (FCon x)
+      or add an instance declaration for
+         (DoC (x (A2 (FCon x) -> A3 (FCon x))))
+    In the first argument of `foldDoC', namely `op'
+    In the expression: foldDoC op
+    In an equation for `fCon': fCon = foldDoC op
+
+T4179.hs:26:16:
+    Could not deduce (A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                        ~
+                      A2 (FCon x))
+    from the context (Functor x, DoC (FCon x))
+      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
+    NB: `A2' is a type function, and may not be injective
+    Expected type: A2 (FCon x) -> A3 (FCon x)
+      Actual type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                   -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
+    Expected type: x (A2 (FCon x) -> A3 (FCon x))
+                   -> A2 (FCon x)
+                   -> A3 (FCon x)
+      Actual type: x (A2 (FCon x) -> A3 (FCon x))
+                   -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                   -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
+    In the first argument of `foldDoC', namely `op'
+    In the expression: foldDoC op
+
+T4179.hs:26:16:
+    Could not deduce (A3 (x (A2 (FCon x) -> A3 (FCon x)))
+                        ~
+                      A3 (FCon x))
+    from the context (Functor x, DoC (FCon x))
+      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
+    NB: `A3' is a type function, and may not be injective
+    Expected type: A2 (FCon x) -> A3 (FCon x)
+      Actual type: A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                   -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
+    Expected type: x (A2 (FCon x) -> A3 (FCon x))
+                   -> A2 (FCon x)
+                   -> A3 (FCon x)
+      Actual type: x (A2 (FCon x) -> A3 (FCon x))
+                   -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
+                   -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
+    In the first argument of `foldDoC', namely `op'
+    In the expression: foldDoC op
diff --git a/testsuite/tests/indexed-types/should_fail/T4246.hs b/testsuite/tests/indexed-types/should_fail/T4246.hs
new file mode 100644
index 0000000000..b5c37a68e3
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4246.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies, FlexibleInstances, OverlappingInstances #-}

+module T4246 where

+

+class Stupid a where

+   type F a

+

+instance Stupid a where

+   type F a = a

+

+instance Stupid Int where

+   type F Int = Bool

+

+type family G a :: *

+type instance G Int = Int

+type instance G Int = Bool

diff --git a/testsuite/tests/indexed-types/should_fail/T4246.stderr b/testsuite/tests/indexed-types/should_fail/T4246.stderr
new file mode 100644
index 0000000000..fe1cfce250
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4246.stderr
@@ -0,0 +1,10 @@
+
+T4246.hs:8:9:
+    Conflicting family instance declarations:
+      type F a -- Defined at T4246.hs:8:9
+      type F Int -- Defined at T4246.hs:11:9
+
+T4246.hs:15:15:
+    Conflicting family instance declarations:
+      type instance G Int -- Defined at T4246.hs:15:15
+      type instance G Int -- Defined at T4246.hs:14:15
diff --git a/testsuite/tests/indexed-types/should_fail/T4254.hs b/testsuite/tests/indexed-types/should_fail/T4254.hs
new file mode 100644
index 0000000000..b12ffb4f87
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4254.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeFamilies, FunctionalDependencies, RankNTypes, MultiParamTypeClasses #-}
+module T4254 where
+
+class FD a b | a -> b where 
+  op :: a -> b; 
+  op = undefined 
+
+instance FD Int Bool
+
+ok1   :: forall a b. (a~Int,FD a b) => a -> b
+ok1    = op
+-- Should be OK: op has the right type
+
+ok2   :: forall a b. (a~Int,FD a b,b~Bool) => a -> Bool
+ok2    = op
+-- Should be OK: needs the b~Bool
+
+fails :: forall a b. (a~Int,FD a b) => a -> Bool 
+fails  = op
+-- Could fail: no proof that b~Bool
+-- But can also succeed; it's not a *wanted* constraint
diff --git a/testsuite/tests/indexed-types/should_fail/T4254.stderr b/testsuite/tests/indexed-types/should_fail/T4254.stderr
new file mode 100644
index 0000000000..03aa80bdac
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4254.stderr
@@ -0,0 +1,18 @@
+
+T4254.hs:19:10:
+    Could not deduce (b ~ Bool)
+    from the context (a ~ Int, FD a b)
+      bound by the type signature for
+                 fails :: (a ~ Int, FD a b) => a -> Bool
+      at T4254.hs:19:1-11
+      `b' is a rigid type variable bound by
+          the type signature for fails :: (a ~ Int, FD a b) => a -> Bool
+          at T4254.hs:19:1
+    When using functional dependencies to combine
+      FD Int b,
+        arising from the type signature for
+                       fails :: (a ~ Int, FD a b) => a -> Bool
+        at T4254.hs:19:1-11
+      FD Int Bool, arising from a use of `op' at T4254.hs:19:10-11
+    In the expression: op
+    In an equation for `fails': fails = op
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.hs b/testsuite/tests/indexed-types/should_fail/T4272.hs
new file mode 100644
index 0000000000..3370fc3637
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4272.hs
@@ -0,0 +1,22 @@
+ {-# LANGUAGE TypeFamilies, ScopedTypeVariables, FlexibleContexts #-}  
+module T4272 where
+
+class Family f where
+   terms :: f a -> a
+
+class Family (TermFamily a) => TermLike a where
+   type TermFamily a :: * -> *
+
+laws :: forall a b. TermLike a => TermFamily a a -> b  
+laws t = prune t (terms (undefined :: TermFamily a a))
+
+prune :: TermLike a => TermFamily a a -> TermFamily a a -> b
+prune = undefined  
+
+-- terms :: Family f => f a -> a
+--    Instantiate with f = TermFamily a
+-- terms :: Family (TermFamily a) => TermFamily a a -> a
+-- (terms (undefined::TermFamily a a) :: Family (TermFamily a) => a
+-- So the call to prune forces the equality
+--    TermFamily a a ~ a
+-- which triggers an occurs check
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
new file mode 100644
index 0000000000..792cde92b8
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -0,0 +1,8 @@
+
+T4272.hs:11:16:
+    Occurs check: cannot construct the infinite type:
+      a0 = TermFamily a0 a0
+    In the first argument of `prune', namely `t'
+    In the expression: prune t (terms (undefined :: TermFamily a a))
+    In an equation for `laws':
+        laws t = prune t (terms (undefined :: TermFamily a a))
diff --git a/testsuite/tests/indexed-types/should_fail/T4485.hs b/testsuite/tests/indexed-types/should_fail/T4485.hs
new file mode 100644
index 0000000000..b48e8206f2
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4485.hs
@@ -0,0 +1,66 @@
+-- The behavior of type-inference and OverlappingInstances has changed
+-- between GHC 6.12 and GHC 7.0 such that the following code
+-- type-checks under 6.12, but not 7.0rc2. I assume this change has
+-- something to do with the new type checker in GHC 7, but it is not
+-- clear to me if this change in behavior is intended. Nor am I clear
+-- how to achieve something similar to the old behavior. This is
+-- preventing HSP (and by extension, happstack) from migrating to GHC
+-- 7. I reported this earlier on the mailing lists, but I have further
+-- simplied the test case here.
+
+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses
+  , FlexibleContexts, FlexibleInstances, UndecidableInstances
+  , TypeSynonymInstances, GeneralizedNewtypeDeriving
+  , OverlappingInstances 
+  #-}
+module XMLGenerator where
+
+newtype XMLGenT m a = XMLGenT (m a)
+   deriving (Functor, Monad)
+
+class Monad m => XMLGen m where
+ type XML m
+ data Child m
+ genElement :: String -> XMLGenT m (XML m)
+
+class XMLGen m => EmbedAsChild m c where
+    asChild :: c -> XMLGenT m [Child m]
+
+instance (EmbedAsChild m c, m1 ~ m) => EmbedAsChild m (XMLGenT m1 c)
+
+instance (XMLGen m,  XML m ~ x) => EmbedAsChild m x
+
+data Xml = Xml
+data IdentityT m a = IdentityT (m a)
+instance Monad (IdentityT m)
+instance XMLGen (IdentityT m) where
+    type XML (IdentityT m) = Xml
+
+data Identity a = Identity a
+instance Monad Identity
+
+instance EmbedAsChild (IdentityT IO) (XMLGenT Identity ())
+
+data FooBar = FooBar
+
+instance EmbedAsChild (IdentityT IO) FooBar where
+  asChild b = asChild $ (genElement "foo")
+  -- asChild :: FooBar -> XMLGenT (XMLGenT (IdentityT IO) [Child (IdentitiyT IO)])
+
+{-     ---------- Deriving the constraints ----------
+ asChild :: EmbedAsChild m c => c -> XMLGenT m [Child m]
+ genElement :: XMLGen m => String -> XMLGenT m (XML m)
+
+ Wanted: EmbedAsChild m c, with m = IdentityT IO
+                                c = XMLGenT meta (XML meta)
+         XMLGen meta
+
+  ie     EmbedAsChild (IdentityT IO) (XMLGen meta (XML meta)
+         XMLGen meta
+
+We have instances
+    EmbedAsChild (IdentityT IO) FooBar
+    EmbedAsChild (IdentityT IO) (XMLGenT Identity ())
+    EmbedAsChild m              (XMLGenT m1 c)
+    EmbedAsChild m              x
+-}
diff --git a/testsuite/tests/indexed-types/should_fail/T4485.stderr b/testsuite/tests/indexed-types/should_fail/T4485.stderr
new file mode 100644
index 0000000000..a9e9792cda
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T4485.stderr
@@ -0,0 +1,19 @@
+
+T4485.hs:47:15:
+    Overlapping instances for EmbedAsChild
+                                (IdentityT IO) (XMLGenT m0 (XML m0))
+      arising from a use of `asChild'
+    Matching instances:
+      instance [overlap ok] (m1 ~ m, EmbedAsChild m c) =>
+                            EmbedAsChild m (XMLGenT m1 c)
+        -- Defined at T4485.hs:29:10-68
+      instance [overlap ok] EmbedAsChild
+                              (IdentityT IO) (XMLGenT Identity ())
+        -- Defined at T4485.hs:42:10-58
+    (The choice depends on the instantiation of `m0'
+     To pick the first instance above, use -XIncoherentInstances
+     when compiling the other instance declarations)
+    In the expression: asChild
+    In the expression: asChild $ (genElement "foo")
+    In an equation for `asChild':
+        asChild b = asChild $ (genElement "foo")
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamArity1.hs b/testsuite/tests/indexed-types/should_fail/TyFamArity1.hs
new file mode 100644
index 0000000000..4a35071e2f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/TyFamArity1.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeFamilies #-}
+
+type family T a b :: *
+type instance T Int = IO   -- must fail: too few args
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr b/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr
new file mode 100644
index 0000000000..7ee60167e1
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/TyFamArity1.stderr
@@ -0,0 +1,4 @@
+
+TyFamArity1.hs:4:1:
+    Number of parameters must match family declaration; expected 2
+    In the type synonym instance declaration for `T'
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamArity2.hs b/testsuite/tests/indexed-types/should_fail/TyFamArity2.hs
new file mode 100644
index 0000000000..2bff129925
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/TyFamArity2.hs
@@ -0,0 +1,4 @@
+{-# LANGUAGE TypeFamilies #-}
+
+type family T a :: * -> *
+type instance T Int Float = Char   -- must fail: extra arguments
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr b/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr
new file mode 100644
index 0000000000..30d0526664
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/TyFamArity2.stderr
@@ -0,0 +1,4 @@
+
+TyFamArity2.hs:4:1:
+    Number of parameters must match family declaration; expected 1
+    In the type synonym instance declaration for `T'
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamUndec.hs b/testsuite/tests/indexed-types/should_fail/TyFamUndec.hs
new file mode 100644
index 0000000000..2c81faab2d
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/TyFamUndec.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module ShouldFail where
+
+type family T a
+type instance T (a, [b])     = T (b, b)        -- var occurs more often
+type instance T (a, Maybe b) = T (a, Maybe b)  -- not smaller
+type instance T (a, IO [b])  = T (a, T b)      -- nested tyfam application
diff --git a/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr b/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
new file mode 100644
index 0000000000..2fc8e1b078
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/TyFamUndec.stderr
@@ -0,0 +1,18 @@
+
+TyFamUndec.hs:6:1:
+    Variable occurs more often than in instance head
+      in the type family application: T (b, b)
+    (Use -XUndecidableInstances to permit this)
+    In the type synonym instance declaration for `T'
+
+TyFamUndec.hs:7:1:
+    Application is no smaller than the instance head
+      in the type family application: T (a, Maybe b)
+    (Use -XUndecidableInstances to permit this)
+    In the type synonym instance declaration for `T'
+
+TyFamUndec.hs:8:1:
+    Nested type family application
+      in the type family application: T (a, T b)
+    (Use -XUndecidableInstances to permit this)
+    In the type synonym instance declaration for `T'
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
new file mode 100644
index 0000000000..f2d904d32e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -0,0 +1,72 @@
+setTestOpts(only_compiler_types(['ghc']))
+setTestOpts(omit_ways(['optasm']))
+
+test('SimpleFail1a', normal, compile_fail, [''])
+test('SimpleFail1b', normal, compile_fail, [''])
+test('SimpleFail2a', normal, compile_fail, [''])
+test('SimpleFail2b', normal, compile_fail, [''])
+test('SimpleFail3a', normal, compile_fail, [''])
+test('SimpleFail4', normal, compile_fail, [''])
+test('SimpleFail5a', normal, compile_fail, [''])
+test('SimpleFail5b', normal, compile_fail, [''])
+test('SimpleFail6', normal, compile_fail, [''])
+test('SimpleFail7', normal, compile_fail, [''])
+test('SimpleFail8', normal, compile_fail, [''])
+test('SimpleFail9', normal, compile_fail, [''])
+test('SimpleFail10', normal, compile_fail, [''])
+test('SimpleFail11a', normal, compile_fail, [''])
+test('SimpleFail11b', normal, compile_fail, [''])
+test('SimpleFail11c', normal, compile_fail, [''])
+test('SimpleFail11d', normal, compile_fail, [''])
+test('SimpleFail12', normal, compile_fail, [''])
+test('SimpleFail13', normal, compile_fail, [''])
+test('SimpleFail14', normal, compile_fail, [''])
+test('SimpleFail15', normal, compile_fail, [''])
+test('SimpleFail16', normal, compile_fail, [''])
+test('TyFamArity1', normal, compile_fail, [''])
+test('TyFamArity2', normal, compile_fail, [''])
+test('TyFamUndec', normal, compile_fail, [''])
+
+test('NotRelaxedExamples', normal, compile_fail, [''])
+test('NonLinearSigErr', normal, compile, [''])
+
+test('GADTwrong1', normal, compile_fail, [''])
+
+test('Over',
+     extra_clean(['OverA.hi', 'OverA.o',
+                  'OverB.hi', 'OverB.o',
+                  'OverC.hi', 'OverC.o']),
+     multimod_compile_fail,
+     ['OverD', '-no-hs-main -c -v0'])
+
+test('SkolemOccursLoop', expect_fail, compile_fail, [''])
+
+test('T2334', normal, compile_fail, [''])
+test('T1900', normal, compile_fail, [''])
+test('T2157', normal, compile_fail, [''])
+test('T2203a', normal, compile_fail, [''])
+test('T2627b', normal, compile_fail, [''])
+test('T2693', normal, compile_fail, [''])
+test('T2888', normal, compile, [''])
+test('T3092', normal, compile_fail, [''])
+test('NoMatchErr', normal, compile_fail, [''])
+test('T2677', normal, compile_fail, [''])
+test('T4099', normal, compile_fail, [''])
+test('T4272', normal, compile_fail, [''])
+test('T4246', normal, compile_fail, [''])
+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('T4179', normal, compile_fail, [''])
+test('T4254', normal, compile_fail, [''])
+test('T2239', normal, compile_fail, [''])
+test('T3440', normal, compile_fail, [''])
+test('T4485', normal, compile_fail, [''])
+test('T4174', normal, compile_fail, [''])
+test('DerivUnsatFam', if_compiler_lt('ghc', '7.1', expect_fail), compile_fail, [''])
+test('T2664', normal, compile_fail, [''])
+test('T2664a', normal, compile, [''])
+test('T2544', normal, compile_fail, [''])
+
diff --git a/testsuite/tests/indexed-types/should_run/GMapAssoc.hs b/testsuite/tests/indexed-types/should_run/GMapAssoc.hs
new file mode 100644
index 0000000000..404818ea55
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/GMapAssoc.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Main where
+
+import Prelude hiding (lookup)
+import Data.Char (ord)
+import qualified Data.Map as Map
+
+
+-- Generic maps as ATs
+-- -------------------
+
+class GMapKey k where
+  data GMap k :: * -> *
+  empty       :: GMap k v
+  lookup      :: k -> GMap k v -> Maybe v
+  insert      :: k -> v -> GMap k v -> GMap k v
+
+instance GMapKey Int where
+  data GMap Int v        = GMapInt (Map.Map Int v)
+  empty                  = GMapInt Map.empty
+  lookup k (GMapInt m)   = Map.lookup k m
+  insert k v (GMapInt m) = GMapInt (Map.insert k v m)
+
+instance GMapKey Char where
+  data GMap Char v        = GMapChar (GMap Int v)
+  empty                   = GMapChar empty
+  lookup k (GMapChar m)   = lookup (ord k) m
+  insert k v (GMapChar m) = GMapChar (insert (ord k) v m)
+
+instance GMapKey () where
+  data GMap () v           = GMapUnit (Maybe v)
+  empty                    = GMapUnit Nothing
+  lookup () (GMapUnit v)   = v
+  insert () v (GMapUnit _) = GMapUnit $ Just v
+
+instance (GMapKey a, GMapKey b) => GMapKey (a, b) where
+  data GMap (a, b) v            = GMapPair (GMap a (GMap b v))
+  empty		                = GMapPair empty
+  lookup (a, b) (GMapPair gm)   = lookup a gm >>= lookup b 
+  insert (a, b) v (GMapPair gm) = GMapPair $ case lookup a gm of
+				    Nothing  -> insert a (insert b v empty) gm
+				    Just gm2 -> insert a (insert b v gm2  ) gm
+
+instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
+  data GMap (Either a b) v                = GMapEither (GMap a v) (GMap b v)
+  empty                                   = GMapEither empty empty
+  lookup (Left  a) (GMapEither gm1  _gm2) = lookup a gm1
+  lookup (Right b) (GMapEither _gm1 gm2 ) = lookup b gm2
+  insert (Left  a) v (GMapEither gm1 gm2) = GMapEither (insert a v gm1) gm2
+  insert (Right a) v (GMapEither gm1 gm2) = GMapEither gm1 (insert a v gm2)
+
+-- Test code
+-- ---------
+
+nonsence :: GMap Bool String
+nonsence = undefined
+
+myGMap :: GMap (Int, Either Char ()) String
+myGMap = insert (5, Left 'c') "(5, Left 'c')"    $
+	 insert (4, Right ()) "(4, Right ())"    $
+	 insert (5, Right ()) "This is the one!" $
+	 insert (5, Right ()) "This is the two!" $
+	 insert (6, Right ()) "(6, Right ())"    $
+	 insert (5, Left 'a') "(5, Left 'a')"    $
+	 empty
+main = putStrLn $ maybe "Couldn't find key!" id $ lookup (5, Right ()) myGMap
diff --git a/testsuite/tests/indexed-types/should_run/GMapAssoc.stdout b/testsuite/tests/indexed-types/should_run/GMapAssoc.stdout
new file mode 100644
index 0000000000..27fa244dde
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/GMapAssoc.stdout
@@ -0,0 +1 @@
+This is the one!
diff --git a/testsuite/tests/indexed-types/should_run/GMapTop.hs b/testsuite/tests/indexed-types/should_run/GMapTop.hs
new file mode 100644
index 0000000000..9ce830950b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/GMapTop.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Main where
+
+import Prelude hiding (lookup)
+import Data.Char (ord)
+import qualified Data.Map as Map
+
+
+-- Generic maps as toplevel indexed data types
+----------------------------------------------
+
+data family GMap k :: * -> *
+data instance GMap Int          v = GMapInt    (Map.Map Int v)
+data instance GMap Char         v = GMapChar   (GMap Int v)
+data instance GMap ()           v = GMapUnit   (Maybe v)
+data instance GMap (a, b)       v = GMapPair   (GMap a (GMap b v))
+data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
+
+class GMapKey k where
+  empty       :: GMap k v
+  lookup      :: k -> GMap k v -> Maybe v
+  insert      :: k -> v -> GMap k v -> GMap k v
+
+instance GMapKey Int where
+  empty                  = GMapInt Map.empty
+  lookup k (GMapInt m)   = Map.lookup k m
+  insert k v (GMapInt m) = GMapInt (Map.insert k v m)
+
+instance GMapKey Char where
+  empty                   = GMapChar empty
+  lookup k (GMapChar m)   = lookup (ord k) m
+  insert k v (GMapChar m) = GMapChar (insert (ord k) v m)
+
+instance GMapKey () where
+  empty                    = GMapUnit Nothing
+  lookup () (GMapUnit v)   = v
+  insert () v (GMapUnit _) = GMapUnit $ Just v
+
+instance (GMapKey a, GMapKey b) => GMapKey (a, b) where
+  empty		                = GMapPair empty
+  lookup (a, b) (GMapPair gm)   = lookup a gm >>= lookup b 
+  insert (a, b) v (GMapPair gm) = GMapPair $ case lookup a gm of
+				    Nothing  -> insert a (insert b v empty) gm
+				    Just gm2 -> insert a (insert b v gm2  ) gm
+
+instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
+  empty                                   = GMapEither empty empty
+  lookup (Left  a) (GMapEither gm1  _gm2) = lookup a gm1
+  lookup (Right b) (GMapEither _gm1 gm2 ) = lookup b gm2
+  insert (Left  a) v (GMapEither gm1 gm2) = GMapEither (insert a v gm1) gm2
+  insert (Right a) v (GMapEither gm1 gm2) = GMapEither gm1 (insert a v gm2)
+
+
+-- Test code
+-- ---------
+
+nonsence :: GMap Bool String
+nonsence = undefined
+
+myGMap :: GMap (Int, Either Char ()) String
+myGMap = insert (5, Left 'c') "(5, Left 'c')"    $
+	 insert (4, Right ()) "(4, Right ())"    $
+	 insert (5, Right ()) "This is the one!" $
+	 insert (5, Right ()) "This is the two!" $
+	 insert (6, Right ()) "(6, Right ())"    $
+	 insert (5, Left 'a') "(5, Left 'a')"    $
+	 empty
+main = putStrLn $ maybe "Couldn't find key!" id $ lookup (5, Right ()) myGMap
diff --git a/testsuite/tests/indexed-types/should_run/GMapTop.stdout b/testsuite/tests/indexed-types/should_run/GMapTop.stdout
new file mode 100644
index 0000000000..27fa244dde
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/GMapTop.stdout
@@ -0,0 +1 @@
+This is the one!
diff --git a/testsuite/tests/indexed-types/should_run/Makefile b/testsuite/tests/indexed-types/should_run/Makefile
new file mode 100644
index 0000000000..9101fbd40a
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/Makefile
@@ -0,0 +1,3 @@
+TOP=../../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/indexed-types/should_run/T2985.hs b/testsuite/tests/indexed-types/should_run/T2985.hs
new file mode 100644
index 0000000000..6ae6e12c50
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/T2985.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
+{-# OPTIONS_GHC -Wnot #-}
+
+module Main where
+
+-- See http://article.gmane.org/gmane.comp.lang.haskell.general/16796
+-- and Trac #2985
+
+instance (Num a, Num b, a ~ b) => Num (a,b) where
+    (x,y) * (u,v) = (x*u-y*v, x*v+y*u)
+
+test1 = (1,1) * (2,2)
+main = print test1
diff --git a/testsuite/tests/indexed-types/should_run/T2985.stdout b/testsuite/tests/indexed-types/should_run/T2985.stdout
new file mode 100644
index 0000000000..2ba96498ec
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/T2985.stdout
@@ -0,0 +1 @@
+(0,4)
diff --git a/testsuite/tests/indexed-types/should_run/T4235.hs b/testsuite/tests/indexed-types/should_run/T4235.hs
new file mode 100644
index 0000000000..45ba33df20
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/T4235.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TypeFamilies, StandaloneDeriving, FlexibleInstances, GADTs #-}
+module Main where
+
+import Data.Ix
+
+-- Deriving Enum with phantom type parameter
+data T a = R | S | T deriving( Enum, Show )
+
+-- Tests that deriving works for data families
+data family Foo a
+
+data instance Foo Int
+  = A | B | C | D
+  deriving (Eq, Enum)
+
+f :: Foo Int -> Bool
+f A = True
+f B = False
+f _ = True
+
+-- Tests that deriving works for GADTs
+data Bar a where
+   P :: Int -> Bar Int
+   Q :: Bar Int
+
+deriving instance (Eq (Bar Int))
+
+main = do { print [R .. T]
+          ; print (map f [B .. D])
+          ; print [P 3 == P 3, P 4 == Q] }
diff --git a/testsuite/tests/indexed-types/should_run/T4235.stdout b/testsuite/tests/indexed-types/should_run/T4235.stdout
new file mode 100644
index 0000000000..3b5ac7194f
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/T4235.stdout
@@ -0,0 +1,3 @@
+[R,S,T]
+[False,True,True]
+[True,False]
diff --git a/testsuite/tests/indexed-types/should_run/all.T b/testsuite/tests/indexed-types/should_run/all.T
new file mode 100644
index 0000000000..454e702c0e
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_run/all.T
@@ -0,0 +1,8 @@
+setTestOpts(only_compiler_types(['ghc']))
+setTestOpts(omit_ways(['hpc', 'ghci', 'threaded1', 'threaded2']))
+
+test('T2985', normal, compile_and_run, [''])
+test('T4235', normal, compile_and_run, [''])
+
+test('GMapAssoc', normal, compile_and_run, ['-package containers'])
+test('GMapTop',   normal, compile_and_run, ['-package containers'])