[project @ 2001-05-03 08:35:33 by simonpj]
authorsimonpj <unknown>
Thu, 3 May 2001 08:35:33 +0000 (08:35 +0000)
committersimonpj <unknown>
Thu, 3 May 2001 08:35:33 +0000 (08:35 +0000)
Add two more fundep tests

ghc/tests/typecheck/should_compile/tc110.hs
ghc/tests/typecheck/should_compile/tc125.hs [new file with mode: 0644]
ghc/tests/typecheck/should_compile/tc126.hs [new file with mode: 0644]

index 1422d89..e0c9ba8 100644 (file)
@@ -13,6 +13,12 @@ primDup = undefined
 
 dup () = call primDup
 
+--     call :: Call c h => c -> h
+--
+--     call primDup :: h  with  {Call (Int -> IO Int) h}
+--     Hence h must be fixed by the environment
+--     Reduce at top level to {Call (IO Int) h'}
+
 class Call    c h | c -> h where
     call  :: c -> h
 
diff --git a/ghc/tests/typecheck/should_compile/tc125.hs b/ghc/tests/typecheck/should_compile/tc125.hs
new file mode 100644 (file)
index 0000000..89bb66a
--- /dev/null
@@ -0,0 +1,36 @@
+{-# OPTIONS -fglasgow-exts #-}
+
+-- !!! Functional dependency test. Hugs [Apr 2001] fails to typecheck this
+-- We should infer this type for foo
+--     foo :: Q (S (S Z)) (S Z)
+
+module ShouldCompile where
+
+data Z = Z
+data S a = S a
+
+class Add a b c | a b -> c where add :: a -> b -> c
+
+instance Add Z a a
+instance Add a b c => Add (S a) b (S c)
+
+class Mul a b c | a b -> c where mul :: a -> b -> c
+
+instance Mul Z a Z
+instance (Mul a b c, Add b c d) => Mul (S a) b d
+
+data Q a b = Q a b
+
+-- Problem here.  This is the addition of rational
+-- numbers: (a/b) + (c/d) = (ad+bc)/bd
+
+instance (Mul a d ad,
+          Mul b c bc,
+          Mul b d bd,
+          Add ad bc ad_bc) => Add (Q a b) (Q c d) (Q ad_bc bd)
+
+z = Z
+sz = S Z
+ssz = S (S Z)
+
+foo = add (Q sz sz) (Q sz sz)
diff --git a/ghc/tests/typecheck/should_compile/tc126.hs b/ghc/tests/typecheck/should_compile/tc126.hs
new file mode 100644 (file)
index 0000000..841acf0
--- /dev/null
@@ -0,0 +1,44 @@
+{-# OPTIONS -fglasgow-exts #-}
+
+-- !!! Functional dependency test. Hugs [Apr 2001] fails to typecheck this
+-- Rather bizarre example submitted by Jonathon Bell
+
+module ShouldCompile where
+
+module Foo where
+
+class Bug f a r | f a -> r where
+   bug::f->a->r
+
+instance                Bug (Int->r) Int      r
+instance (Bug f a r) => Bug f        (c a)    (c r) 
+
+f:: Bug(Int->Int) a r => a->r
+f = bug (id::Int->Int)
+
+g1 = f (f [0::Int])
+-- Inner f gives result type 
+--     f [0::Int] :: Bug (Int->Int) [Int] r => r
+-- Which matches the second instance declaration, giving r = [r']
+--     f [0::Int] :: Bug (Int->Int) Int r' => r'
+-- Wwich matches the first instance decl giving r' = Int
+--     f [0::Int] :: Int
+-- The outer f now has constraint
+--     Bug (Int->Int) Int r
+-- which makes r=Int
+-- So g1::Int
+
+g2 = f (f (f [0::Int]))
+-- The outer f repeats the exercise, so g2::Int
+-- This is the definition that Hugs rejects
+
+-- Here is a similar definition rejected by Hugs
+-- It complains that the instances are not consistent with the
+-- functional dependencies, which isn't true, because
+--     (c a) does not unify with (c' a', c' b')
+
+class Foo f a r | f a->r where
+      foo::f->a->r
+
+instance Foo (a->r)     (c a)    (c r)
+instance Foo ((a,b)->r) (c a,c b)(c r)