[Haskell-cafe] Strange "ambiguity" problems thanks to GADTs

[wren romano]

Hi all,

In my latest project I've been using a bunch of GADTs, which
unfortunately disables let-polymorphism (i.e., where-polymorphism) in
the most annoying way. For the most part I've been able to hack around
that limitation via judicious use of ScopedTypeVariables, but I've run
into an issue that I can't for the life of me figure out why GHC
doesn't like it.

I have something like the following function, where @a@ and @b@ happen
to be GADTs:

    foo :: (A a, B b) => a i -> M (b i)
    foo a =
        case view a of
        ...
        SomePattern a1 a2 -> do
            b1 <- foo a1
            b2 <- foo a2
            return . unview $ SomePattern b1 b2

It seems to me that the recursive calls should work just fine, using
the same @b@ as we'll ultimately be returning. However, for some
reason GHC complains about the recursive calls using some other @b0@
can can't deduce @B b0@ from @B b at . Why doesn't GHC unify these two
types? How can I force them to unify without adding type annotations
at every recursive call?

-- 
Live well,
~wren