GADT Type Checking GHC 6.10 versus older GHC
Jason Dagit
dagit at codersbase.com
Fri Nov 21 11:04:18 EST 2008
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
More information about the Glasgow-haskell-users
mailing list