diff options
author | David Terei <davidterei@gmail.com> | 2011-07-20 11:09:03 -0700 |
---|---|---|
committer | David Terei <davidterei@gmail.com> | 2011-07-20 11:26:35 -0700 |
commit | 16514f272fb42af6e9c7674a9bd6c9dce369231f (patch) | |
tree | e4f332b45fe65e2a7a2451be5674f887b42bf199 /testsuite/tests/gadt/gadt25.hs | |
parent | ebd422aed41048476aa61dd4c520d43becd78682 (diff) | |
download | haskell-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.hs | 41 |
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 |