Создание типа Rank2Type в монаде

Итак, я поверхностно понимаю Rank2Types, но когда я попробую следующее

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f :: IO (Process a a)
f = return . auto $ id

GHC кашляет

Couldn't match type `MachineT m0 (Is a0) a0'
              with `forall (m :: * -> *). Monad m => MachineT m (Is a) a'
Expected type: IO (Process a a)
  Actual type: IO (MachineT m0 (Is a0) a0)
In the expression: return . auto $ id
In an equation for `f': f = return . auto $ id
Failed, modules loaded: none.

Итак, насколько я вижу, GHC не позволит мне поставить forall в Монаду. Существует ли принципиальная логическая причина квантификации, или это просто ограничение GHC? Или я просто делаю что-то глупое?

Ответы

Ответ 1

В качестве примера можно привести следующие действия:

{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}

import Data.Machine

f = (return :: (forall a. Process a a) -> IO (forall a. Process a a)) (auto id)

Как говорит Карл, вы должны аннотировать функции, которые вы хотите использовать нецелесообразно, например return здесь. Даже тогда работа с нечистыми типами в GHC несколько хрупка. Я бы не рекомендовал его. Причинами ограничений являются просто то, что сложно выполнить вывод типа при наличии нечистоплотных типов, и, кроме того, язык поверхности Haskell не имеет надлежащего синтаксиса для указания типа, в котором вы хотите создать полиморфную функцию.

Общим решением является обернуть содержимое в newtype:

data PolyProcess = PP (forall a. Process a a)

f' :: IO PolyProcess
f' = return $ PP $ auto $ id