GADT Type Checking GHC 6.10 versus older GHC

21 Nov 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

GADT Type Checking GHC 6.10 versus older GHC

Jason Dagit