[Haskell-cafe] -XGADTs changes type for program that does not contain GADT

[Johannes Waldmann]

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.