# GADT Type Checking GHC 6.10 versus older GHC

Simon Peyton-Jones simonpj at microsoft.com
Fri Nov 21 11:57:16 EST 2008

You need a type signature for the case expression.  As Daniel says, this is worth a read

Simon

| -----Original Message-----
| bounces at haskell.org] On Behalf Of Jason Dagit
| Sent: 21 November 2008 16:04
| 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
| _______________________________________________
`