My understanding of OutsideIn leads me to believe that GHC 7.8 has the behavior
closer to that spec. See Section 5.2 of that paper
(http://research.microsoft.com/en-us/um/people/simonpj/Papers/constraints/jfp-outsidein.pdf),
which is a relatively accessible explanation of this phenomenon.
Given the following code:
{-# LANGUAGE GADTs #-}
data Any a where
AInt :: Int - Any Int
-- demo 1 does not compile
{-
demo1 a = do case a of
(AInt i) - print i
Couldn't match expected type ‘t’ with actual type ‘IO ()’
‘t’ is untouchable
inside the constraints (t1 ~ Int)
I just hit a similar error the other day. I think the gist of it is that
there are two perfectly good types, and neither is more general than the
other. A slightly different example shows why more clearly:
foo (AInt i) = (3 :: Int)
Now, what type should this have?
foo :: Any a - a
foo :: Any
Hi.
Daniel is certainly right to point out general problems with GADT
pattern matching and principal types. Nevertheless, the changing
behaviour of GHC over time is currently a bit confusing to me.
In GHC-6.12.3, Doaitse's program fails with three errors (demo1,
demo2, demo4, all the GADT
