bug in GADT typechecking

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

bug in GADT typechecking

David Roundy
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
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

Re: bug in GADT typechecking

Andres Loeh-2
> > {-# 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............   ^^^^^^^^

Looks to me as if ghc is right to complain. PP takes a Foo, but U takes
a Patch. Therefore the x that's matched on the lhs is a Patch, not a Foo.

> 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'

> Glasgow Haskell Compiler, Version 6.4, for Haskell 98, compiled by GHC version 6.4

FWIW, same error with ghc-6.5 from a few weeks ago.

Cheers,
  Andres
_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
Reply | Threaded
Open this post in threaded view
|

Same for ghc-6.5 from two days ago was Re: bug in GADT typechecking

Shae Matijs Erisson
Andres Loeh <[hidden email]> writes:

> > Glasgow Haskell Compiler, Version 6.4, for Haskell 98, compiled by GHC
> > version 6.4
> FWIW, same error with ghc-6.5 from a few weeks ago.

Same error from a ghc-cvs build from two days ago.
--
Shae Matijs Erisson - http://www.ScannedInAvian.com/ - Sockmonster once said:
You could switch out the unicycles for badgers, and the game would be the same.

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs