It used to be, because GHC used to implement so-called "deep skolemisation". See Section 4.6.2 of http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/putting.pdf
Deep skolemisation was an unfortunate casualty of the push to add impredicative polymoprhism. However, as I mentioned in an earlier email, I'm currently planning to take impredicative polymorphism *out*, which means that deep skolemisation might come back *in*. Simon | -----Original Message----- | From: [email protected] [mailto:[email protected]] On | Behalf Of Bas van Dijk | Sent: 24 November 2009 13:34 | To: Haskell Cafe | Subject: [Haskell-cafe] Pointfree rank-2 typed function | | Hello, | | Given this program: | | ------------------------------------------------------------ | {-# LANGUAGE Rank2Types #-} | | newtype Region s a = Region a | | unRegion :: forall a s. Region s a -> a | unRegion (Region x) = x | | runRegionPointfull :: forall a. (forall s. Region s a) -> a | runRegionPointfull r = unRegion r | ------------------------------------------------------------ | | Is it possible to write the rank-2 typed function 'runRegionPointfull' | in pointfree style? | | Unfortunately the following doesn't typecheck: | | runRegionPointfree :: forall a. (forall s. Region s a) -> a | runRegionPointfree = unRegion | | Couldn't match expected type `forall s. Region s a' | against inferred type `Region s a1' | In the expression: unRegion | In the definition of `runRegionPointfree': | runRegionPointfree = unRegion | | Why can't the typechecker match `forall s. Region s a' and `Region s a1'? | | Thanks, | | Bas | _______________________________________________ | Haskell-Cafe mailing list | [email protected] | http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
