[Haskell-cafe] Rank2Types in let bindings

[Li-yao Xia]

Hi Olaf,

This is the monomorphism restriction. g is a binding without a 
signature, so it gets specialized. The type annotation is part of the 
body of g, but if you want to generalize g it should be a separate 
declaration

     let g :: forall ...
         g = ...

On 10/5/2021 3:36 PM, Olaf Klinke wrote:
> 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?
> 
> Olaf
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.