Commit 5c1d923f authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Adapt to being a bit more picky about inference with GADTs

This means adding a few type signature, and some tests failing
(as they should) rather than succeeding
parent 8bc6c4a6
......@@ -11,12 +11,12 @@ test('gadt3', normal, compile, [''])
test('gadt4', skip_if_fast, compile_and_run, [''])
test('gadt5', skip_if_fast, compile_and_run, [''])
test('gadt6', normal, compile, [''])
test('gadt7', normal, compile, [''])
test('gadt7', normal, compile_fail, [''])
test('gadt8', normal, compile, [''])
test('gadt9', normal, compile, [''])
test('gadt10', normal, compile_fail, [''])
test('gadt11', normal, compile_fail, [''])
test('gadt13', normal, compile, [''])
test('gadt13', normal, compile_fail, [''])
test('gadt14', normal, compile, [''])
test('gadt15', normal, compile, [''])
test('gadt16', normal, compile, [''])
......@@ -73,7 +73,7 @@ test('data2', normal, compile, [''])
test('termination', normal, compile, [''])
test('set', normal, compile, [''])
test('scoped', normal, compile, [''])
test('gadt-escape1', normal, compile, [''])
test('gadt-escape1', normal, compile_fail, [''])
# New ones from Dimitrios
......
......@@ -12,6 +12,9 @@ hval = Hidden (ExpInt 0) (ExpInt 1)
-- With the type sig this is ok, but without it maybe
-- should be rejected becuase the result type is wobbly
-- weird1 :: ExpGADT Int
--
-- And indeed it is rejected by GHC 7.8 because OutsideIn
-- doesn't unify under an equality constraint.
weird1 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a
-- Hidden t (ExpInt (co :: t ~ Int) _ :: ExpGADT t) (a :: ExpGADT t)
......
gadt-escape1.hs:19:58:
Couldn't match type `t' with `ExpGADT Int'
`t' is untouchable
inside the constraints (t1 ~ Int)
bound by a pattern with constructor
ExpInt :: Int -> ExpGADT Int,
in a case alternative
at gadt-escape1.hs:19:43-50
`t' is a rigid type variable bound by
the inferred type of weird1 :: t at gadt-escape1.hs:19:1
Expected type: t
Actual type: ExpGADT t1
Relevant bindings include
weird1 :: t (bound at gadt-escape1.hs:19:1)
In the expression: a
In a case alternative: Hidden (ExpInt _) a -> a
In the expression:
case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
......@@ -2,6 +2,9 @@
-- This should fail, because there is no annotation on shw,
-- but it succeeds in 6.4.1
--
-- It fails again with 7.8 because Outside in doesn't
-- unify under an equality constraint
module ShouldFail where
......
gadt13.hs:15:13:
Couldn't match expected type `t'
with actual type `String -> [Char]'
`t' is untouchable
inside the constraints (t1 ~ Int)
bound by a pattern with constructor
I :: Int -> Term Int,
in an equation for `shw'
at gadt13.hs:15:6-8
`t' is a rigid type variable bound by
the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1
Relevant bindings include
shw :: Term t1 -> t (bound at gadt13.hs:15:1)
In the expression: ("I " ++) . shows t
In an equation for `shw': shw (I t) = ("I " ++) . shows t
......@@ -11,7 +11,8 @@ data T a where
i1 :: T a -> a -> Int
i1 t y = (\t1 y1 -> case t1 of K -> y1) t y
-- No type signature; should type-check
-- No type signature; should not type-check,
-- because we can't unify under the equalty constraint for K
i1b t y = (\t1 y1 -> case t1 of K -> y1) t y
i2 :: T a -> a -> Int
......
gadt7.hs:16:38:
Couldn't match expected type `t' with actual type `t1'
`t1' is untouchable
inside the constraints (t2 ~ Int)
bound by a pattern with constructor
K :: T Int,
in a case alternative
at gadt7.hs:16:33
`t1' is a rigid type variable bound by
the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
`t' is a rigid type variable bound by
the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
Relevant bindings include
i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)
y :: t1 (bound at gadt7.hs:16:7)
y1 :: t1 (bound at gadt7.hs:16:16)
In the expression: y1
In a case alternative: K -> y1
In the expression: case t1 of { K -> y1 }
......@@ -225,10 +225,13 @@ deriving instance Show a => Show (Alt a b)
instance Rec (PHom (->) (->)) (FAlt a) (Alt a) where
_in = mkPHom f g where
f,g :: FAlt a (Alt a) s -> Alt a s
f FZero = Zero
f (FSucc1 a b) = Succ1 a b
g (FSucc2 a b) = Succ2 a b
out = mkPHom f g where
f,g :: Alt a s -> FAlt a (Alt a) s
f Zero = FZero
f (Succ1 a b) = FSucc1 a b
g (Succ2 a b) = FSucc2 a b
......@@ -252,8 +255,11 @@ type PairUpResult a = K2 [(a, a)] (a, [(a, a)])
pairUp :: Alt a Fst -> [(a, a)]
pairUp xs = let (K21 xss) = (fstPHom (fold (mkPHom phi psi))) xs in xss
where
phi FZero = K21 []
phi :: FAlt y (K2 v (r,[(y,r)])) s -> K2 [(y,r)] (y,z) s
phi FZero = K21 []
phi (FSucc1 x1 (K22 (x2, xss))) = K21 ((x1, x2):xss)
psi :: FAlt y (K2 z w) s -> K2 [x] (y,z) s
psi (FSucc2 x (K21 xss)) = K22 (x, xss)
main = print (Succ1 (0::Int) $ Succ2 1 $ Succ1 2 $ Succ2 3 $ Succ1 4 $ Succ2 5 Zero)
......@@ -23,4 +23,5 @@ f = ap (ETwice . twice)
foo :: ETwice
foo = ETwice (5 :: Int)
bar :: IO ()
bar = ap print (f foo)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment