Impredicativity woes

Main.purs

module Main where

import Prelude
import Data.Maybe (Maybe(..), fromMaybe)
import Unsafe.Coerce (unsafeCoerce)

type Id = forall a. a -> a
newtype ID = ID Id

mkID :: Id -> ID
mkID = ID

runID :: ID -> Id
runID (ID id') = id'

aThing' :: Maybe ID
aThing' = Nothing

runAThing' :: Id
runAThing' = runID (fromMaybe (mkID id) aThing')

choose :: forall f b. Functor f => f Id -> f (b -> b)
choose faa = faa <#> \a -> a

aThing :: Maybe (forall a. a -> a)
aThing = (Just :: Id -> Maybe Id) id

runAThing :: forall z. z -> z
runAThing = (fromMaybeId :: Maybe (z -> z) -> (z -> z)) (choose aThing :: Maybe (z -> z)) where
  fromMaybeId :: Maybe (z -> z) -> z -> z
  fromMaybeId = (fromMaybe :: (z -> z) -> Maybe (z -> z) -> (z -> z)) (id :: z -> z)