Is it possible to use church encodings without breaking equational reasoning?

Question

Mind this program:

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (sum)

type List h = forall t . (h -> t -> t) -> t -> t

sum_ :: (Num a) => List a -> a
sum_ = \ list -> list (+) 0

toList :: [a] -> List a
toList = \ list cons nil -> foldr cons nil list

sum :: (Num a) => [a] -> a
-- sum = sum_ . toList        -- does not work
sum = \ a -> sum_ (toList a)  -- works

main = print (sum [1,2,3])

Both definitions of sum are identical up to equational reasoning. Yet, compiling the second definition of works, but the first one doesn't, with this error:

tmpdel.hs:17:14:
    Couldn't match type ‘(a -> t0 -> t0) -> t0 -> t0’
                  with ‘forall t. (a -> t -> t) -> t -> t’
    Expected type: [a] -> List a
      Actual type: [a] -> (a -> t0 -> t0) -> t0 -> t0
    Relevant bindings include sum :: [a] -> a (bound at tmpdel.hs:17:1)
    In the second argument of ‘(.)’, namely ‘toList’
    In the expression: sum_ . toList

It seems that RankNTypes breaks equational reasoning. Is there any way to have church-encoded lists in Haskell without breaking it??

Answer 1

I have the impression that ghc percolates all for-alls as left as possible:

forall a t. [a] -> (a -> t -> t) -> t -> t)

and

forall a. [a] -> forall t . (h -> t -> t) -> t -> t

can be used interchangeably as witnessed by:

toList' :: forall a t. [a] -> (a -> t -> t) -> t -> t
toList' = toList

toList :: [a] -> List a
toList = toList'

Which could explain why sum's type cannot be checked. You can avoid this sort of issues by packaging your polymorphic definition in a newtype wrapper to avoid such hoisting (that paragraph does not appear in newer versions of the doc hence my using the conditional earlier).

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (sum)

newtype List h = List { runList :: forall t . (h -> t -> t) -> t -> t }

sum_ :: (Num a) => List a -> a
sum_ xs = runList xs (+) 0

toList :: [a] -> List a
toList xs = List $ \ c n -> foldr c n xs

sum :: (Num a) => [a] -> a
sum = sum_ . toList

main = print (sum [1,2,3])