More tests and wibbles in existing tests.

testsuite/tests/ghc-regress/indexed-types/should_compile/PushedInAsGivens.hs

+{-# 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.
+
+
+

testsuite/tests/ghc-regress/indexed-types/should_compile/SlowComp.hs

+{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, FlexibleContexts #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module SlowComp where
+
+import Control.Monad
+import Control.Monad.State
+
+-------------------------------------------------------------------------------
+-- Usual Peano integers.
+
+
+class NatInt a where
+	natInt :: a -> Int
+
+data D0 n = D0 {d0Arg :: n}
+data D1 n = D1 {d1Arg :: n}
+
+data C0
+data C1
+
+class DPosInt n where posInt :: n -> (Int,Int)
+instance DPosInt () where posInt _ = (0,1)
+instance DPosInt n => DPosInt (D0 n) where
+	posInt a = (dsum,w*2)
+		where
+			(dsum,w) = posInt $ d0Arg a
+instance DPosInt n => DPosInt (D1 n) where
+	posInt a = (dsum+w,w*2)
+		where
+			(dsum,w) = posInt $ d1Arg a
+
+instance NatInt () where natInt _ = 0
+instance DPosInt n => NatInt (D0 n) where natInt a = fst $ posInt a
+instance DPosInt n => NatInt (D1 n) where natInt a = fst $ posInt a
+
+type family DRev a
+type instance DRev a = DRev' a ()
+
+type family DRev' x acc
+type instance DRev' () acc = acc
+type instance DRev' (D0 a) acc = DRev' a (D0 acc)
+type instance DRev' (D1 a) acc = DRev' a (D1 acc)
+
+type family DAddC c a b
+type instance DAddC C0 (D0 a) (D0 b) = D0 (DAddC C0 a b)
+type instance DAddC C0 (D1 a) (D0 b) = D1 (DAddC C0 a b)
+type instance DAddC C0 (D0 a) (D1 b) = D1 (DAddC C0 a b)
+type instance DAddC C0 (D1 a) (D1 b) = D0 (DAddC C1 a b)
+type instance DAddC C1 (D0 a) (D0 b) = D1 (DAddC C0 a b)
+type instance DAddC C1 (D1 a) (D0 b) = D0 (DAddC C1 a b)
+type instance DAddC C1 (D0 a) (D1 b) = D0 (DAddC C1 a b)
+type instance DAddC C1 (D1 a) (D1 b) = D1 (DAddC C1 a b)
+type instance DAddC C0 ()     ()     = ()
+type instance DAddC C1 ()     ()     = D1 ()
+type instance DAddC c  (D0 a) ()     = DAddC c (D0 a) (D0 ())
+type instance DAddC c  (D1 a) ()     = DAddC c (D1 a) (D0 ())
+type instance DAddC c  ()     (D0 b) = DAddC c (D0 b) (D0 ())
+type instance DAddC c  ()     (D1 b) = DAddC c (D1 b) (D0 ())
+
+type family DNorm a
+type instance DNorm () = D0 ()
+type instance DNorm (D0 ()) = D0 ()
+type instance DNorm (D0 (D1 a)) = D1 a
+type instance DNorm (D0 (D0 a)) = DNorm a
+type instance DNorm (D1 a) = D1 a
+
+type family DPlus a b
+type instance DPlus a b = DNorm (DRev (DAddC C0 (DRev a) (DRev b)))
+
+type family DDepth a
+type instance DDepth () = D0 ()
+type instance DDepth (D0 ()) = D0 ()
+type instance DDepth (D1 ()) = D1 ()
+type instance DDepth (D1 (D0 n)) = DPlus ONE (DDepth (D1 n))
+type instance DDepth (D1 (D1 n)) = DPlus ONE (DDepth (D1 n))
+
+type family DLog2 a
+type instance DLog2 a = DDepth a
+
+type ZERO = D0 ()
+
+type ONE = D1 ()
+type TWO = DPlus ONE ONE
+type THREE = DPlus ONE TWO
+type FOUR = DPlus TWO TWO
+type FIVE = DPlus ONE FOUR
+type SIX = DPlus TWO FOUR
+type SEVEN = DPlus ONE SIX
+type EIGHT = DPlus FOUR FOUR
+type NINE = DPlus FOUR FIVE
+type TEN = DPlus EIGHT TWO
+type SIZE8  = EIGHT
+type SIZE9  = NINE
+type SIZE10 = TEN
+type SIZE12 = DPlus SIX SIX
+type SIZE15 = DPlus EIGHT SEVEN
+type SIZE16 = DPlus EIGHT EIGHT
+type SIZE17 = DPlus ONE SIZE16
+type SIZE24 = DPlus SIZE8 SIZE16
+type SIZE32 = DPlus SIZE8 SIZE24
+type SIZE30 = DPlus SIZE24 SIX
+
+-------------------------------------------------------------------------------
+-- Description of CPU.
+
+class CPU cpu where
+	-- register address.
+	type RegAddrSize cpu
+	-- register width
+	type RegDataSize cpu
+	-- immediate width.
+	type ImmSize cpu
+	-- variables in CPU - register indices, command format variables, etc.
+	type CPUVars cpu :: * -> *
+
+data Const size = Const Integer
+
+data Var cpu size where
+	Temp :: Int -> Var cpu size
+	Var :: CPUVars cpu size -> Var cpu size
+
+-------------------------------------------------------------------------------
+-- Command description monad.
+
+data Command cpu where
+	Command :: (Var cpu size) -> (Operation cpu size) -> Command cpu
+
+type RegVar cpu = Var cpu (RegDataSize cpu)
+type Immediate cpu = Const (ImmSize cpu)
+
+data Operation cpu resultSize where
+	Add :: RegVar cpu -> Either (Immediate cpu) (RegVar cpu) -> Operation cpu (RegDataSize cpu)
+	Sub :: RegVar cpu -> Either (Immediate cpu) (RegVar cpu) -> Operation cpu (RegDataSize cpu)
+	
+
+type CDM cpu a = StateT (Int, [Command cpu]) IO a
+
+($=) :: CPU cpu => Var cpu size -> Operation cpu size -> CDM cpu ()
+var $= op = modify $ \(cnt,ops) -> (cnt,ops ++ [Command var op])
+
+tempVar :: CPU cpu => CDM cpu (Var cpu size)
+tempVar = do
+	cnt <- liftM fst get
+	modify $ \(_,cmds) -> (cnt+1,cmds)
+	return $ Temp cnt
+
+op :: CPU cpu => Operation cpu size -> CDM cpu (Var cpu size)
+op operation = do
+	v <- tempVar
+	v $= operation
+	return v
+
+-------------------------------------------------------------------------------
+-- Dummy CPU.
+
+data DummyCPU = DummyCPU
+
+data DummyVar size where
+	DummyFlag :: Flag -> DummyVar ONE
+	DummyReg :: Int -> DummyVar SIZE16
+	DummyZero :: DummyVar SIZE16
+
+data Flag = C | Z | N | V
+
+instance CPU DummyCPU where
+	type RegAddrSize DummyCPU = FIVE
+	type RegDataSize DummyCPU = SIZE16
+	type ImmSize DummyCPU = SIZE12
+	type CPUVars DummyCPU = DummyVar
+
+-------------------------------------------------------------------------------
+-- Long compiling program.
+
+cnst :: Integer -> Either (Immediate DummyCPU) (RegVar DummyCPU)
+cnst x = Left (Const x)
+
+longCompilingProgram :: CDM DummyCPU ()
+longCompilingProgram = do
+-- the number of lines below greatly affects compilation time.
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	x10 <- op $ Add (Var DummyZero) (cnst 10)
+	return ()

testsuite/tests/ghc-regress/indexed-types/should_compile/T4981-V1.hs

+{-# 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

testsuite/tests/ghc-regress/indexed-types/should_compile/T4981-V2.hs

+{-# 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

testsuite/tests/ghc-regress/indexed-types/should_compile/T4981-V3.hs

+{-# 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

testsuite/tests/ghc-regress/indexed-types/should_compile/T5002.hs

+{-# 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
+

testsuite/tests/ghc-regress/indexed-types/should_compile/all.T

@@ -167,3 +167,11 @@ 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, [''])
+test('SlowComp', normal, compile, [''])
\ No newline at end of file

testsuite/tests/ghc-regress/indexed-types/should_fail/NoMatchErr.stderr

-
-NoMatchErr.hs:20:5:
-    Could not deduce (Memo d ~ Memo d0)
-    from the context (Fun d)
-      bound by the type signature for f :: Fun d => Memo d a -> Memo d a
-      at NoMatchErr.hs:20:1-15
-    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 -> Memo d a
-      Actual type: Memo d0 a -> Memo d0 a
-    In the expression: abst . appl
-    In an equation for `f': f = abst . appl
+
+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

testsuite/tests/ghc-regress/typecheck/should_compile/GivenOverlapping.hs

+{-# LANGUAGE FunctionalDependencies, FlexibleContexts #-}
+
+class C a where 
+
+class D a where 
+ dop :: a -> a    
+
+instance C a => D [a] where 
+ dop = undefined
+
+class J a b | a -> b 
+ where j :: a -> b -> () 
+
+instance J Bool Int where 
+ j = undefined
+   
+foo :: D [Int] => ()
+foo = j True (head (dop [undefined]))
+
+main = return ()
+

testsuite/tests/ghc-regress/typecheck/should_compile/SilentParametersOverlapping.hs

+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+
+module SilentParametersOverlapping where 
+
+class C a where 
+  c :: a -> () 
+
+class C a => B a where 
+  b :: a -> () 
+
+instance C [a] where 
+  c x = () 
+
+instance B [(a,b)] where 
+  -- Silent: C [(a,b)] 
+  b x = c [(undefined,undefined)]
+
+-- DV: The silent parameter should not give us a failure to apply the instance!
+
+
+
+
+
+
+
+

testsuite/tests/ghc-regress/typecheck/should_compile/all.T

@@ -346,3 +346,6 @@ test('T4969', normal, compile, [''])
 test('T5120', normal, compile, [''])
 test('mc18', expect_broken_for(4370, ['hpc']), compile, [''])
 test('tc249', normal, compile, [''])
+
+test('GivenOverlapping', normal, compile, [''])
+test('SilentParametersOverlapping', normal, compile, [''])
\ No newline at end of file

testsuite/tests/ghc-regress/typecheck/should_fail/FailDueToGivenOverlapping.hs

+{-# LANGUAGE FlexibleContexts #-}
+
+module FailDueToGivenOverlapping where
+
+class C a where
+
+class D a where 
+ dop :: a -> ()
+
+
+instance C a => D [a] 
+
+-- should succeed since we can't learn anything more for 'a'
+foo :: (C a, D [Int]) => a -> () 
+foo x = dop [x] 
+
+
+class E a where 
+ eop :: a -> () 
+
+instance E [a] where 
+ eop = undefined
+
+-- should fail since we can never be sure that we learnt 
+-- everything about the free unification variable.
+bar :: E [Int] => () -> ()
+bar _ = eop [undefined]

testsuite/tests/ghc-regress/typecheck/should_fail/FailDueToGivenOverlapping.stderr

+
+FailDueToGivenOverlapping.hs:27:9:
+    Overlapping instances for E [t0]
+      arising from a use of `eop'
+    Matching instances:
+      instance E [a] -- Defined at FailDueToGivenOverlapping.hs:21:10-14
+    Matching givens (or their superclasses):
+      (E [Int])
+        bound by the type signature for bar :: E [Int] => () -> ()
+        at FailDueToGivenOverlapping.hs:27:1-23
+    (The choice depends on the instantiation of `t0')
+    In the expression: eop [undefined]
+    In an equation for `bar': bar _ = eop [undefined]

testsuite/tests/ghc-regress/typecheck/should_fail/LongWayOverlapping.hs

+{-# LANGUAGE TypeFamilies, MultiParamTypeClasses
+  , FlexibleContexts, FlexibleInstances, UndecidableInstances
+  , TypeSynonymInstances, GeneralizedNewtypeDeriving
+  , OverlappingInstances 
+  #-}
+
+module LongWayOverlapping where
+
+
+class M a where 
+
+class M a => XMLG a 
+
+instance M [a] 
+
+instance XMLG [m] where     -- Generates an implication wanted:  forall m. M [m]
+
+class M a => EmbAsChild a b where 
+  emb :: b -> [a]
+
+
+instance EmbAsChild [Char] Bool where 
+  emb _ = emb 'c'
+
+
+  -- This one generates an unsolvable EmbAsChild [Char] Char
+
+-- Original problem is: 
+-- [w] EmbAsChild [Char] Char 
+-- [w] forall m. M [m]
+-- Now, by converting the wanted to given and pushing it inside the implication 
+-- we have the following:
+-- [g] EmbAsChild [Char] Char 
+-- [g] M [Char]   <~~ The superclass of the first given! 
+-- [w] M [m] 
+-- And now OOPS we can't solve M [m] because we are supposed to delay our choice 
+-- as much as possible! 
+
+-- DV:
+-- One possible solution is to STOP PUSHING wanteds as givens inside an implication
+-- in a checking context. I think it's the best thing to do and I've implemented it.
+
+-- In inference mode that's ok and the error message is very comprehensible, see
+-- test case PushedInFlatsOverlap.hs 

testsuite/tests/ghc-regress/typecheck/should_fail/LongWayOverlapping.stderr

+
+LongWayOverlapping.hs:23:11:
+    No instance for (EmbAsChild [Char] Char)
+      arising from a use of `emb'
+    Possible fix:
+      add an instance declaration for (EmbAsChild [Char] Char)
+    In the expression: emb 'c'
+    In an equation for `emb': emb _ = emb 'c'
+    In the instance declaration for `EmbAsChild [Char] Bool'

testsuite/tests/ghc-regress/typecheck/should_fail/all.T

@@ -238,3 +238,5 @@ test('tcfail207', normal, compile_fail, [''])
 test('T5084', normal, compile_fail, [''])
 test('tcfail208', normal, compile_fail, [''])
 
+test('FailDueToGivenOverlapping', normal, compile_fail, [''])
+test('LongWayOverlapping', normal, compile_fail, [''])
\ No newline at end of file

testsuite/tests/ghc-regress/typecheck/should_run/tcrun033.hs

 
 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
-             UndecidableInstances, TypeSynonymInstances #-}
-
--- This test made GHC 6.3 build a superclass loop, in
--- the instance ClassA a String declaration
-
-module Main where
-
-class (Sat (a -> b -> String), ClassB b) => ClassA a b
-
-class ClassB a where