oleg | 23 Aug 13:27 2012

Rigid skolem type variable escaping scope


Matthew Steele asked why foo type-checks and bar doesn't:
>   class FooClass a where ...
> 
>   foo :: (forall a. (FooClass a) => a -> Int) -> Bool
>   foo fn = ...
> 
>   newtype IntFn a = IntFn (a -> Int)
> 
>   bar :: (forall a. (FooClass a) => IntFn a) -> Bool
>   bar (IntFn fn) = foo fn

This and further questions become much simpler if we get a bit more
explicit. Imagine we cannot write type signatures like those of foo
and bar (no higher-ranked type signatures). But we can define
higher-rank newtypes. Since we can't give foo the higher-rank
signature, we must re-write it, introducing the auxiliary
newtype FaI.

> {-# LANGUAGE Rank2Types #-}

> class FooClass a where m :: a
>
> instance FooClass Int where m = 10
>
> newtype FaI = FaI{unFaI :: forall a. (FooClass a) => a -> Int}

> foo :: FaI -> Bool
> foo fn = ((unFaI fn)::(Char->Int)) m > 0

(Continue reading)


Gmane