Is GADT extension destroying polymorphism?

Question

Is the extension GADT in Haskell destroying polymorphism, even in code that don't use GADTs ?

Here's a example which works and don't use GADT

{-# LANGUAGE RankNTypes #-}
--{-# LANGUAGE GADTs #-}

newtype Fix1 f i = In1 { unFix1 :: f (Fix1 f) i }
mcata1 ::      (forall r k. (forall j. r j -> t j) -> f r k -> t k) 
            -> Fix1 f i
            -> t i
mcata1 f (In1 x) = f (mcata1 f) x


newtype Ret i = Ret {unRet :: (i -> Int) -> Int}


-- recusive type
data BushR i = NBR | CBR i (BushR (BushR i))

-- initial algebra
data BushF r i = NB | CB i (r (r i))
type Bush i = Fix1 BushF i

bsumm = mcata1 alg
  where alg :: forall i r. (forall j. r j -> Ret j) -> BushF r i -> Ret i
        alg r NB = Ret (const 0)
        alg r (CB x xs) = Ret (\f -> 
                f x + bsum xs (\ys -> bsum ys f))
                        where
                                bsum  = unRet . r

If GADTs is enabled we get a compile error

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

newtype Fix1 f i = In1 { unFix1 :: f (Fix1 f) i }
mcata1 ::      (forall r k. (forall j. r j -> t j) -> f r k -> t k) 
            -> Fix1 f i
            -> t i
mcata1 f (In1 x) = f (mcata1 f) x


newtype Ret i = Ret {unRet :: (i -> Int) -> Int}


-- recusive type
data BushR i = NBR | CBR i (BushR (BushR i))

-- initial algebra
data BushF r i = NB | CB i (r (r i))
type Bush i = Fix1 BushF i

bsumm = mcata1 alg
  where alg :: forall i r. (forall j. r j -> Ret j) -> BushF r i -> Ret i
        alg r NB = Ret (const 0)
        alg r (CB x xs) = Ret (\f -> 
                f x + bsum xs (\ys -> bsum ys f)) -- error
                        where
                                bsum  = unRet . r
-- • Occurs check: cannot construct the infinite type: i1 ~ r i1
--   Expected type: r (r i1)
--     Actual type: r i1
-- • In the first argument of ‘bsum’, namely ‘ys’
--   In the expression: bsum ys f
--   In the second argument of ‘bsum’, namely ‘(\ ys -> bsum ys f)’
-- • Relevant bindings include

which can be fixed by duplicating bindings

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}

newtype Fix1 f i = In1 { unFix1 :: f (Fix1 f) i }
mcata1 ::      (forall r k. (forall j. r j -> t j) -> f r k -> t k) 
            -> Fix1 f i
            -> t i
mcata1 f (In1 x) = f (mcata1 f) x


newtype Ret i = Ret {unRet :: (i -> Int) -> Int}


-- recusive type
data BushR i = NBR | CBR i (BushR (BushR i))

-- initial algebra
data BushF r i = NB | CB i (r (r i))
type Bush i = Fix1 BushF i

bsumm = mcata1 alg
  where alg :: forall i r. (forall j. r j -> Ret j) -> BushF r i -> Ret i
        alg r NB = Ret (const 0)
        alg r (CB x xs) = Ret (\f -> 
                f x + bsum xs (\ys -> bsum2 ys f))
                        where
                                bsum   = unRet . r
                                bsum2  = unRet . r

Is there a deep reason for that ?

Answer 1

Enabling GADTs we implicitly also enable MonoLocalBinds which prevents some forms of let- and where- type generalizations.

This affects types whose type variables are partly quantified (i below), and partly free (r below).

where bsum :: forall i. r i -> (i -> Int) -> Int
      bsum = unRet . r

A simple solution is to provide an explicit type annotation so to force the wanted generalization.

The docs provide a rationale for MonoLocalBinds, showing why it makes sense to restrict generalization in some cases. A blog post from 2010 provides further discussion.

A relevant quote by Simon Peyton-Jones from the blog (slightly reformatted, and using the same links as in the original blog):

Why did we make it?

It’s a long story, but the short summary is this: I don’t know how to build a reliable, predictable type inference engine for a type system that has both

• (a) generalisation of local let/where and
• (b) local type equality assumptions, such as those introduced by GADTs.

The story is told in our paper “Let should not be generalised” and, at greater length, in the journal version “Modular type inference with local assumptions”.