Testsuite: tabs -> spaces [skip ci]
[ghc.git] / testsuite / tests / gadt / gadt25.hs
1 {-# LANGUAGE GADTs #-}
2
3 -- From the ghc-users mailing list
4
5 module Foo where
6
7 data TValue t where
8 TList :: [a] -> TValue [a]
9
10 instance (Eq b) => Eq (TValue b) where
11 (==) (TList p) (TList q) = (==) p q
12
13 {- My reply to the list
14
15 Here's the reasoning (I have done a bit of renaming).
16
17 * The TList constructor really has type
18 TList :: forall a. forall x. (a~[x]) => [x] -> TValue a
19
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
26
27 * On the RHS we find we need (Eq [x]).
28
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].
34
35
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]).
40
41 -}