Type Family Shenanigans in GHCi

Here's my code: ``` {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds, FlexibleContexts, UndecidableInstances #-} module Foo where import Data.Singletons.Prelude import Data.Type.Equality data TP a b -- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs type family Same (b :: Bool) (r :: k) (rq :: [k]) :: k where Same bool r (x ': xs) = Same (bool :&& (r == x)) r xs Same bool r '[] = TP bool r data NotEqualFailure -- converts a True result to a type type family EqResult tp where EqResult (TP 'True r) = r EqResult (TP 'False r) = NotEqualFailure data Zq q i type family Foo rq type instance Foo (Zq q i) = i type R = EqResult (Same 'True (Foo (Zq Double Int)) (Map (TyCon1 Foo) '[Zq Double Int, Zq Float Int])) f :: R f = 3 ``` This doesn't compile in GHC 7.8.3: ``` No instance for (Num NotEqualFailure) arising from a use of ‘f’ In the expression: f In an equation for ‘it’: it = f ``` but if I comment out `f` and start GHCi: ``` > :kind! R R :: * = Int ``` So GHC can't seem to decide if the elements in my list are equal or not. If they are equal, `EqResult` should return the common type (`Int` here), otherwise it returns `NotEqualFailure`. Can anyone explain what's going on here? Let me know if you also think this looks like a bug, and I'll file it on the GHC trac. If you can figure out a way to write "EqResult (Same ...)" in a different way, it might get around this issue. EDIT I rewrote the type family, but unfortunately I'm having essentially the same problem. The code is smaller and simpler now. ``` {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, FlexibleContexts, UndecidableInstances #-} module Foo where import Data.Singletons.Prelude import Data.Singletons.Prelude.List import Data.Type.Equality -- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs type family Same rq where Same (x ': xs) = EqResult (And (Map ((TyCon2 (==)) $ x) xs)) x data NotEqualFailure -- converts a True result to a type type family EqResult b v where EqResult 'True r = r EqResult 'False r = NotEqualFailure type R = Same '[Int, Int] f :: R f = 3 ``` GHCi can still resolve `R` to `Int`, but GHC can't resolve the type family for `EqResult` at all now (before it incorrectly resolved it to `NotEqualFailure`). Note that this example works if I change the size of the list to one, i.e. `'[Int]`. EDIT 2 I removed all external libraries, and got everything to work. This solution is probably the smallest, but I still want to know why the larger examples appear to break GHC. ``` {-# LANGUAGE TypeFamilies, DataKinds, UndecidableInstances #-} module Foo where type family Same (rq :: [*]) :: * where Same (x ': xs) = EqTo x xs --tests if x==y for all x\in xs type family EqTo y xs where EqTo y '[] = y EqTo y (y ': xs) = EqTo y xs EqTo y (x ': xs) = NotEqualFailure data NotEqualFailure type R = Same '[Int, Int] f :: R f = 3 ```