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@. 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