The monomorphic library contains the following snippet (which should hopefully compile in 7.8):
{-# LANGUAGE DataKinds, ExistentialQuantification, FlexibleContexts, GADTs #-}
{-# LANGUAGE ImpredicativeTypes, PolyKinds, RankNTypes, TypeFamilies #-}
{-# LANGUAGE TypeOperators, UndecidableInstances #-}
class Monomorphicable k where
type MonomorphicRep k :: *
withPolymorphic :: Monomorphicable k
=> MonomorphicRep k -> (forall a. k a -> b) -> b
withPolymorphic k trans = undefined
-- | Flipped version of 'withPolymorphic'.
liftPoly :: Monomorphicable k
=> (forall a. k a -> b) -> MonomorphicRep k -> b
liftPoly = flip withPolymorphic
However in 7.10, GHC complains:
Couldn't match type ‘k2 a0 -> b’ with ‘forall (a :: k0). k1 a -> b’
Expected type: MonomorphicRep k2 -> (k2 a0 -> b) -> b
Actual type: MonomorphicRep k1
-> (forall (a :: k0). k1 a -> b) -> b
Relevant bindings include
liftPoly :: (forall (a :: k). k2 a -> b) -> MonomorphicRep k2 -> b
(bound at Data/Type/Monomorphic.hs:45:1)
In the first argument of ‘flip’, namely ‘withPolymorphic’
In the expression: flip withPolymorphic
Of course if I changed the definition of liftPoly
to
liftPoly a b = withPolymorphic b a
then 7.10 is happy. What's going on here? Is 7.10 supposed to be stricter when dealing with polymorphic functions somehow? It doesn't appear to be the monomorphism restriction since everything has a signature.
The type of flip
is
flip :: (x -> y -> z) -> (y -> x -> z)
To type check liftPoly
, we have to instantiate the variable y
at the polymorphic type forall a. k a -> b
. This is an instance of impredicative polymorphism.
As the page at https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism says,
We've made various attempts to support impredicativity, so there is a flag
-XImpredicativeTypes
. But it doesn't work, and is absolutely unsupported. If you use it, you are on your own; I make no promises about what will happen.
So, don't be too surprised when the behavior of ImpredicativeTypes
changes between versions of GHC.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With