GADT related bug in GHC type checker
Daniel Fischer
daniel.is.fischer at web.de
Tue Jul 13 18:44:24 EDT 2010
On Wednesday 14 July 2010 00:11:00, George Giorgidze wrote:
> Hi,
>
> I have encountered a bug in GHC type checker. I have stripped down my
> code to small manageable example that illustrates the bug:
>
> {-# LANGUAGE GADTs #-}
> {-# OPTIONS -Wall #-}
>
> module StrangeGADT where
>
> data Q a where
> ToQ :: (QA a) => a -> Q a
> Sum :: (QA a, Num a) => Q [a] -> Q a
>
> class QA a where
> toQ :: a -> Q a
> fromQ :: Q a -> a
>
> instance QA Int where
> toQ = ToQ
> fromQ q = case q of
> ToQ a -> a
> Sum as -> sum (fromQ as)
>
> instance QA a => QA [a] where
> toQ = ToQ
> fromQ q = case q of
> ToQ a -> a
> -- Sum _ -> ([] + 13)
>
> The above program typechecks but GHC wrongly warns that last pattern
> match is not exhaustive.
That warning is correct. Uncommenting the Sum case:
*StrangeGADT> fromQ (Sum $ ToQ [[1 :: Int .. 10]])
[]
Of course, to make it work, I needed
instance (Num a) => Num [a] where
(+) = zipWith (+)
<and so on>
fromInteger = repeat . fromInteger
But since that instance is possible, both constructors can appear as
arguments to fromQ for the list instance, hence the warning.
>
> Furthermore, if I uncomment the last line of the code it typechecks
> (without warnings) and does not reject ([] + 13) as type incorrect
> expression.
It's type correct:
Prelude> :t [] + 13
[] + 13 :: (Num [a]) => [a]
It's usable only when a Num instance for a list is in scope, though.
>
> It would be very much appreciated if someone could suggest how to
> circumvent the problem.
For the code you posted, there is no problem to circumvent. GHC behaves
correctly since it works on an open world assumption, it doesn't rely on
the instances in scope but takes other possible instances into account.
>
> Is there a version of GHC that behaves correctly in this case?
>
> Is this yet another instance of GADT related bugs already reported in
> GHC trac? or it is unrelated and I better report it as a separate
> ticket.
>
> Cheers, George
>
More information about the Glasgow-haskell-users
mailing list