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

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Fri Feb 12 12:47:15 UTC 2016

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)

- J.W.

More information about the Haskell-Cafe mailing list