[Haskell-cafe] Rank2Types in let bindings

Olaf Klinke olf at aatal-apotheke.de
Tue Oct 5 19:36:36 UTC 2021

Dear Cafe,

apologies if this is a duplicate question. I want to define an element of 
a Rank-2 type, use its specialization and then return the general thing. 
Apparently this is not possible without a newtype.

{-# LANGUAGE RankNTypes #-}
newtype General = General {
    useGeneral :: forall a. Integral a => a -> Bool

doesNotWork :: General
doesNotWork = let
         g = even :: forall a. Integral a => a -> Bool
         b = specializeGeneral g
         in General g

doesWork :: General
doesWork = let
         g = General even
         b = specializeGeneral (useGeneral g)
         in g

specializeGeneral :: (Int -> Bool) -> Bool
specializeGeneral p = p 5

I was under the impression that one can always use a more general type 
where a more special type is needed. In `doesNotWork` above, despite the 
explicit Rank-2 type annotation, usage in `specializeGeneral` apparently 
makes the compiler infer the type of `g` to be (Int -> Bool) and complains 
that `a` can not me matched with `Bool`. What gets me is that the compiler 
error is at `General g`, so the compiler must have ignored my Rank-2 type 
annotation. Should it be allowed to do that?


More information about the Haskell-Cafe mailing list