I am studying pure type systems, particularly the calculus of constructions, and trying to use an encoding for recursive types on it, which, according to Philip Wadler, is possible. As an example, I'm using the Morte Haskell library to encode Scott numerals as given by Cardelli.
A summary of the encoding is as such: given a (positive) recursive type...
$$\mu X.F\ X$$
...we may encode it as a type on System F as...
$$Lfix\ X.F\ X\ =\ \Lambda X.(F\ X\rightarrow X)\rightarrow X$$
...or, using pure type systems' notation (with an explicit $F$)...
$$Lfix\ =\ \Pi F: *\rightarrow*.\Pi X: *.(F\ X\rightarrow X)\rightarrow X$$
...since $F$ is a type constructor ($*$ is the type of types).
In order to encode such, we need to declare three functions, $fold$, $in$ and $out$, according to Wadler, and used by Cardelli on the encoding for Scott numerals.
fold : All X. (F X -> X) -> T -> X
fold = \X. \k: F X -> X. \t:T. t X k
in : F T -> T
in = \s: F T. \X. \k: F X -> X. k (F (fold X k) s).
(Where $T$ is $Lfix\ X. F\ X$.)
It's trivial to write the $fold$ function as given. But when trying to write the $in$ function, it doesn't seem to typecheck. The expression $(fold\ X\ k)$ has type $T\rightarrow X$, and $(F\ (fold\ X\ k)\ s)$ should be of type $F\ X$. Then we infer that $F$ should be of type $(T\rightarrow X)\rightarrow F\ T\rightarrow F\ X$ (looks like a fmap). This doesn't typecheck, because F is a type constructor (of type $*\rightarrow*$).
This doesn't look like a typo... am I missing something?
