Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Polymorphic "flip" fails in 7.10

Tags:

haskell

ghc

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.

like image 854
crockeea Avatar asked Dec 25 '22 20:12

crockeea


1 Answers

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.

like image 57
Reid Barton Avatar answered Jan 08 '23 04:01

Reid Barton