The to_c function below is rejected due to a type error when compiling with the GADTs extension that I want to use for an unrelated code fragment that is not shown here.
newtype Church = Church { unC :: forall a. (a -> a) -> a -> a }
to_c :: Int -> Church
to_c 0 = let f0 f c = c in Church f0
to_c n =
let fn f c = iterate f c !! n in Church fn
Error message:
Couldn't match type ‘a0’ with ‘a’ because type variable ‘a’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context:
(a -> a) -> a -> a
Expected type: (a -> a) -> a -> a
Actual type: (a0 -> a0) -> a0 -> a0
In the first argument of ‘Church’, namely ‘fn’
I can rewrite the function in direct recursive style that will type check and also work; however, I was curious as to why this iterative approach is defective and whether it can be salvaged with some clever type annotations.
This really doesn't have anything to do with GADTs, only, the -XGADTs extension also implies -XMonoLocalBinds, and that's the real problem here. What it does is, because the local binding fn has no explicit signature it wants to give it a type that is no more polymorphic than the environment... i.e. in this case not polymorphic at all. But of course, it must be polymorphic so it can actually be used in the Church type, so that's no good.
You can still give an explicit polymorphic signature:
{-# LANGUAGE RankNTypes, MonoLocalBinds #-}
newtype Church = Church { unC :: forall a. (a -> a) -> a -> a }
to_c :: Int -> Church
-- to_c 0 = ... -- the base case is redundant.
to_c n =
let fn :: (a -> a) -> a -> a
fn f c = iterate f c !! n
in Church fn
but an easier solution is to just don't make any binding at all, then -XMonoLocalBinds doesn't come into play:
to_c :: Int -> Church
to_c n = Church (\f c -> iterate f c !! n)
...or, if you do make a binding, do it within the Church constructor, because there the environment is already polymorphic:
to_c n = Church (let fn f c = iterate f c !! n in fn)