newtype um ST verursacht Typ Fehler

Question

Wenn ich versuche, den folgenden Code unter GHC 7.4.1 zu laden:

{-# 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 

Es mit der folgenden Meldung fehlschlägt:

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 

Warum dies nicht versagt, wenn M ist nur ein Wrapper um ST?

(. Mein eigentliches Programm hat ein paar Transformatoren auf – gestapelt ist dies nur ein Minimalfall)

---

EDIT: Es scheint, das Hinzufügen eines let behebt das Problem:

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

Wenn jedoch TypeFamilies aktiviert ist (wie es in meinem echten Code ist), schlägt es erneut fehl.

Answer 1

Es ist ein Problem mit den Pattern-Übereinstimmungen + Rankntypes.

GHC sagt m um den Typ ST ??? a wo ??? eine Typvariable ist, die mit irgendetwas vereinheitlichen kann und mit etwas * vereinheitlichen muss. Also geben wir es dann an runST weiter und runST will ein also m vereinheitlicht damit und ??? vereint mit s. Aber warten Sie, jetzt vereinheitlichen wir mit s außerhalb des Bereichs, in dem s definiert ist, ist der Umfang so katastrophal.

Ein einfacheres Beispiel ist

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

Und wieder bekommen wir die gleichen Fehler, weil wir mit der Art der m mit t zu vereinen versuchen, aber t ist in einem zu geringen Umfang.

Die einfachste Lösung ist einfach nicht diese Art Variable polymorphen ein gut und wahr mit

test m = runST (unM m) 

hier unM kehrt zu schaffen ST dass runST mit glücklich ist. Sie können let verwenden, da es standardmäßig polymorph ist, aber seit -XTypeFamilies macht lassen monomorphe wird es explodieren wie Mustererkennung, wie Sie entdeckt haben.

---

** Es scheint, dass m monomorph ist. let ist polymorph ohne Typ Familien so ich vermute, dass das ist, was vor sich geht. Es verhält sich wie es

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

Fehler versuchen Bool und Int zu vereinen, wie Sie von einem monomorphen Typ Variable erwartet. Warum scheint jeder seltsame Typfehler, den ich finde, irgendeine Form der monomorphen Typenvariable zu verbergen.