Dear Cafe, the following type-correct program does not contain GADT syntax. When I activate GADT language pragma, it does no longer typecheck. {-# language GADTs, ScopedTypeVariables #-} data M a b dw :: (b -> b -> b) -> M a b -> M a b -> M a b dw f x y = x data Bar a b s = Bar { this :: M a (M b s), that :: M b (M a s) } f :: forall p q s . (s -> s -> s) -> Bar p q s -> Bar p q s -> Bar p q s f g x y = let -- diff :: forall p . M p s -> M p s -> M p s diff a b = dw g a b in Bar { this = dw diff (this x)(this y) , that = dw diff (that x)(that y) } I can fix this by declaring the type for `diff` as indicated in the comment. Otherwise, `diff` is not polymorphic (enough), as the error message shows. This behaviour is consistent over ghc-7.8,7.10,8-rc, so it's unlikely to be a bug. But it does seem to go against the claim of "conservative extension of HM" (Sect 6.6 of the ICFP'06 paper, Sect 4.9 of MS-CIS-05-26) http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/ - J.W.