blob: 99aecad3fbfb94d9b4492e10ae0d3ae6009198ac (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
{-# LANGUAGE GADTs #-}
-- From the ghc-users mailing list
module Foo where
data TValue t where
TList :: [a] -> TValue [a]
instance (Eq b) => Eq (TValue b) where
(==) (TList p) (TList q) = (==) p q
{- My reply to the list
Here's the reasoning (I have done a bit of renaming).
* The TList constructor really has type
TList :: forall a. forall x. (a~[x]) => [x] -> TValue a
* So in the pattern match we have
(Eq b) available from the instance header
TList p :: TValue b
x is a skolem, existentially bound by the pattern
p :: [x]
b ~ [x] available from the pattern match
* On the RHS we find we need (Eq [x]).
* So the constraint problem we have is
(Eq b, b~[x]) => Eq [x]
["Given" => "Wanted"]
Can we prove this? From the two given constraints we can see
that we also have Eq [x], and that certainly proves Eq [x].
Nevertheless, it's a bit delicate. If we didn't notice all the
consequences of the "given" constraints, we might use the top-level Eq
a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq
x, which *isn't* a consequence of (Eq b, b~[x]).
-}
|
