newtype wokół ST powoduje błąd typu

Question

Kiedy próbuję załadować następujący kod pod GHC 7.4.1:

{-# LANGUAGE RankNTypes #-} 

import Control.Monad.ST 

newtype M s a = M { unM :: ST s a } 

runM :: (forall s. M s a) -> a 
runM (M m) = runST m 

nie powiedzie się z następującym komunikatem:

test.hs:9:14: 
    Couldn't match type `s0' with `s' 
     because type variable `s' would escape its scope 
    This (rigid, skolem) type variable is bound by 
     a type expected by the context: ST s a 
    The following variables have types that mention s0 
     m :: ST s0 a (bound at test.hs:9:9) 
    In the first argument of `runST', namely `m' 
    In the expression: runST m 
    In an equation for `runM': runM (M m) = runST m 

Dlaczego to się nie uda, gdy M to tylko opakowanie o numerze ST?

(. Mój rzeczywisty program ma kilka transformatorów ułożone na – to tylko minimalny przypadek)

---

EDIT: Wydaje dodanie let rozwiązuje problem:

runM m = let M m' = m in runST m 

Jednakże, jeśli TypeFamilies jest włączony (jak to jest w moim prawdziwym kodzie), to znowu się nie powiedzie.

Answer 1

To jest problem z dopasowaniem wzorców + rangami.

Podpowiedzi GHC m mają typ ST ??? a, gdzie ??? jest zmienną typu, która może się zjednoczyć z czymkolwiek i musi się zjednoczyć z czymś *. Przekazujemy go następnie do runST i runST, aby uzyskać jednolitą całość z ST s a i ujednolicić z ??? z s. Ale poczekaj, teraz łączymy się z s poza zakresem, w którym s jest zdefiniowanym zasięgiem tak katastrofy.

Prostsza przykładem jest

test (M m) = (m :: forall t . ST t a) `seq`() 

I znowu mamy ten sam błąd, ponieważ staramy się zjednoczyć z typem m wykorzystaniem t, ale t jest w zbyt małym zakresie.

Najprostszym rozwiązaniem jest po prostu nie do stworzenia tego typu zmiennej z

test m = runST (unM m) 

tutaj unM Zwraca dobre i prawdziwe polimorficzny ST że runST jest zadowolony. Możesz użyć parametru let, ponieważ jest on domyślnie polimorficzny, ale ponieważ -XTypeFamilies sprawi, że będzie monomorficzny, wyskoczy jak dopasowywanie do wzorca, jak odkryłeś.

---

** Wygląda na to, że m jest monomorficzny. let jest polimorficzna bez rodzin typów, więc podejrzewam, że to właśnie się dzieje. Zachowuje się jakby to

test :: forall a. (forall t. M t a) ->() 
test (M m) = (m :: ST Bool a) `seq` (m :: ST Int a) `seq`() 

Błędy próbuje ujednolicić Bool i Int jak można oczekiwać od zmiennej typu jednokształtny. Dlaczego każdy błąd dziwnego typu wydaje mi się ukrywać jakąś postać monomorficznej zmiennej typu ..