summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/gadt25.hs
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]).

-}