summaryrefslogtreecommitdiff
path: root/testsuite/tests/gadt/gadt25.hs
diff options
context:
space:
mode:
authorDavid Terei <davidterei@gmail.com>2011-07-20 11:09:03 -0700
committerDavid Terei <davidterei@gmail.com>2011-07-20 11:26:35 -0700
commit16514f272fb42af6e9c7674a9bd6c9dce369231f (patch)
treee4f332b45fe65e2a7a2451be5674f887b42bf199 /testsuite/tests/gadt/gadt25.hs
parentebd422aed41048476aa61dd4c520d43becd78682 (diff)
downloadhaskell-16514f272fb42af6e9c7674a9bd6c9dce369231f.tar.gz
Move tests from tests/ghc-regress/* to just tests/*
Diffstat (limited to 'testsuite/tests/gadt/gadt25.hs')
-rw-r--r--testsuite/tests/gadt/gadt25.hs41
1 files changed, 41 insertions, 0 deletions
diff --git a/testsuite/tests/gadt/gadt25.hs b/testsuite/tests/gadt/gadt25.hs
new file mode 100644
index 0000000000..99aecad3fb
--- /dev/null
+++ b/testsuite/tests/gadt/gadt25.hs
@@ -0,0 +1,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]).
+
+-} \ No newline at end of file