GADT Type Checking GHC 6.10 versus older GHC

[Simon Peyton-Jones]

You need a type signature for the case expression.  As Daniel says, this is worth a read
http://haskell.org/haskellwiki/Upgrading_packages%23Changes_to_GADT_matching#Changes_to_GADT_matching

Simon


| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
| bounces at haskell.org] On Behalf Of Jason Dagit
| Sent: 21 November 2008 16:04
| To: glasgow-haskell-users at haskell.org
| Subject: GADT Type Checking GHC 6.10 versus older GHC
|
| Hello,
|
| Here is an example where ghc 6.8.x was fine, but now 6.10 complains.
|
| \begin{code}
| type CommuteFunction = forall x y. (Prim :< Prim) C(x y) -> Perhaps
| ((Prim :< Prim) C(x y))
|
| commute_split :: CommuteFunction
| commute_split (Split patches :< patch) =
|     toPerhaps $ do (p1 :< ps) <- cs (patches :< patch)
|                    case sort_coalesceFL ps of
|                             p :>: NilFL -> return (p1 :< p)
|                             ps' -> return (p1 :< Split ps')
|     where cs :: ((FL Prim) :< Prim) C(x y) -> Maybe ((Prim :< (FL Prim)) C(x y))
|           cs (NilFL :< p1) = return (p1 :< NilFL)
|           cs (p:>:ps :< p1) = do p1' :< p' <- commutex (p :< p1)
|                                  p1'' :< ps' <- cs (ps :< p1')
|                                  return (p1'' :< p':>:ps')
| commute_split _ = Unknown
| \end{code}
|
| Now with ghc 6.10 we get this error:
|     GADT pattern match with non-rigid result type `Maybe a'
|       Solution: add a type signature
|     In a case alternative: p :>: NilFL -> return (p1 :< p)
|     In the expression:
|         case sort_coalesceFL ps of {
|           p :>: NilFL -> return (p1 :< p)
|           ps' -> return (p1 :< Split ps') }
|     In the second argument of `($)', namely
|         `do (p1 :< ps) <- cs (patches :< patch)
|             case sort_coalesceFL ps of {
|               p :>: NilFL -> return (p1 :< p)
|               ps' -> return (p1 :< Split ps') }'
|
| You can see more context here:
| http://darcs.net/src/Darcs/Patch/Prim.lhs  around line 472
|
| My understanding was that from 6.6 to 6.8, GADT type checking was
| refined to fill some gaps in the soundness.  Did that happen again
| between 6.8 and 6.10 or is 6.10 being needlessly strict here?
|
| Thanks,
| Jason
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users