1 {-# LANGUAGE GADTs #-}

3 -- From the ghc-users mailing list

13 {- My reply to the list

15 Here's the reasoning (I have done a bit of renaming).

17 * The TList constructor really has type

18 TList :: forall a. forall x. (a~[x]) => [x] -> TValue a

20 * So in the pattern match we have

21 (Eq b) available from the instance header

22 TList p :: TValue b

23 x is a skolem, existentially bound by the pattern

24 p :: [x]

25 b ~ [x] available from the pattern match

27 * On the RHS we find we need (Eq [x]).

29 * So the constraint problem we have is

30 (Eq b, b~[x]) => Eq [x]

31 ["Given" => "Wanted"]

32 Can we prove this? From the two given constraints we can see

33 that we also have Eq [x], and that certainly proves Eq [x].

36 Nevertheless, it's a bit delicate. If we didn't notice all the

37 consequences of the "given" constraints, we might use the top-level Eq

38 a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq

39 x, which *isn't* a consequence of (Eq b, b~[x]).

41 -}