Hello ghc folks,
The following GADT program fails to typecheck, although I think it really
should be fine, so I'm reporting this as a bug. I'm sorry, but I haven't
been able to simplify the foo function any more without causing the error
to go away. :(
> {-# OPTIONS_GHC -fglasgow-exts #-}
> module Main where
>
> data Foo a b where
> Foo :: Int -> Foo a b
>
> data Patch a b where
> PP :: Foo a b -> Patch a b
> Lis :: PL a b -> Patch a b
>
> data PL a b where
> U :: Patch a b -> PL a b
> Nil :: PL x x
> (:-) :: PL c d -> PL d e -> PL c e
>
> data Pair alpha omega where
> (:.) :: Patch a i -> Patch i o -> Pair a o
>
> foo :: Pair a b -> Maybe (Pair a b)
> foo (Lis (U x :- y) :. Lis Nil) = Just (PP x :. Lis y)
^^^^
Oddly enough, the code *does* typecheck if we change the above line to
foo (Lis (U a :- b) :. Lis Nil) = Just (Lis (U a) :. Lis b)
which differs only in here............ ^^^^^^^^
It's a strange bug, and is quite an inconvenience. Could this be a result
of the wobbly types used for GADTs? It seems to me that this is a pretty
dead safe bit of code--after all (PP x) and (Lis (U x)) have precisely the
same type!
I get the following error:
test.lhs:27:44:
Couldn't match `Foo a b' against `Patch a1 d'
Expected type: Foo a b
Inferred type: Patch a1 d
In the first argument of `PP', namely `x'
In the first argument of `(:.)', namely `PP x'
when running with
Glasgow Haskell Compiler, Version 6.4, for Haskell 98, compiled by GHC version
6.4
using the ghc compiler in debian sarge.
--
David Roundy
http://www.darcs.net
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
