mapping over RankNTypes functions-CodePudding

Using rankN from here:

{-# LANGUAGE RankNTypes #-}
rankN :: (forall n. Num n => n -> n) -> (Int, Double)
rankN f = (f 1, f 1.0)

Why can't do map rankN [negate]? Is there some way to make it possible?

I think I now (mostly) understand the RankNTypes, and see I can do both rankN ( 1) and rankN negate.

(And why does map rankN [negate] give a weird error Couldn't match type ‘n’ with ‘Integer’, when I don't think there are any Integers involved?)

Also, I just checked :t map rankN. It gives the dreaded Couldn't match type ‘a’ with ‘n -> n’ because type variable ‘n’ would escape its scope. This (rigid, skolem) type variable is bound by.... I see how that error comes about in some cases, but don't really understand why it would apply here.

Thanks, and sorry if this is a dup. (But I couldn't find the answer amongst all the other RankNTypes questions.)

CodePudding user response：

The reason that it does not work by default is because the type of map is (a -> b) -> [a] -> [b], but you cannot instantiate that a to a type involving forall, in this case forall n. Num n => n -> n. Such instantiation is called impredicative, which was not supported (reliably) by GHC for a long time.

Since GHC 9.2.1 there is a new reliable implementation of the ImpredicativeTypes extension, which does allow you to instantiate impredicatively:

GHCi, version 9.2.0.20210821: https://www.haskell.org/ghc/  :? for help
ghci> :set -XImpredicativeTypes
ghci> :t rankN
rankN :: (forall n. Num n => n -> n) -> (Int, Double)
ghci> :t map rankN 
map rankN :: [forall n. Num n => n -> n] -> [(Int, Double)]
ghci> :t map rankN [negate]
map rankN [negate] :: [(Int, Double)]
ghci> map rankN [negate]
[(-1,-1.0)]