Inferencia de tipo GHC infortunios

Question

Pregunta. ¿Hay alguna forma de hacer que este código funcione sin una firma de tipo explícita?

Código. En primer lugar, tengo una clase alterna MonadTrans en la práctica, mucho más agradable, inspirada en Data.Newtype. Parece que este,

{-# LANGUAGE FlexibleContexts, TypeFamilies #-} 

module Alt.Control.Monad.Trans where 

import Control.Monad 

class (Monad , Monad (BaseMonad)) => MonadTrans (:: * -> *) where 
    type BaseMonad :: * -> * 
    lift :: (BaseMonad) α -> α 

Entonces, tengo una clase A con el método foo, y si alguna mónada base de M es un A, entonces cualquier mónada transformado T M es también un A. En el código,

class A where 
    foo :: String -> () 

instance (A (BaseMonad), MonadTrans) => A where 
    foo n = lift $ foo n 

Sin embargo, si ahora quiero crear un acceso directo para foo con su primer argumento sustituido, entonces necesito una firma de tipo explícita o desbordamientos de pila contexto del compilador.

minimize_call :: A => () 
minimize_call = foo "minimize" 

información posible para ayudar a la inferencia. Digamos que tenemos un tipo asociado B :: * -> *. Estoy pensando que quiero decir que el compilador B satisface B t /= t, B (B t) /= B t, etc. es decir B es de alguna manera "monotónico" - que perseguir tipos asociados es equivalente a eliminar newtype wrappers, y debe saber que no puede eliminar newtype wrappers para siempre , por lo tanto, es necesario agregar el contexto A a la firma.

Answer 1

Sí, hay una manera. Proporcione una instancia con conexión a tierra para A y agregue NoMonomorphismRestriction al idioma pragma (además del también requerido FlexibleInstances y UndecidableInstances).

Sin embargo, la clase A será inutilizable. No hay forma de que el compilador sepa que nunca habrá una instancia MonadTrans con BaseMonad m = m. Por lo tanto, no puede seleccionar una instancia, nunca, porque no puede saber si usar la instancia de aquí o de otra.

{-# LANGUAGE FlexibleContexts, TypeFamilies, FlexibleInstances, UndecidableInstances, NoMonomorphismRestriction #-} 

module Trans (MonadTrans(..), A(..), minimize_call) where 

import Control.Monad 

class (Monad m, Monad (BaseMonad m)) => MonadTrans (m :: * -> *) where 
    type BaseMonad m :: * -> * 
    lift :: (BaseMonad m) α -> m α 

class A m where 
    foo :: String -> m() 


data Foo a = Bork 

instance Monad Foo where 
    return _ = Bork 
    _ >>= _ = Bork 

instance A Foo where 
    foo _ = Bork 


instance (A (BaseMonad m), MonadTrans m) => A m where 
    foo n = lift $ foo n 

-- minimize_call :: A m => m() 
minimize_call = foo "minimize" 

compila con ghc 6.12, 7.0, 7.2 y 7.4. Sin la firma, minimize_call debe obtener un tipo monomórfico, a menos que el MR esté apagado. Eso no puede funcionar de todos modos porque la restricción A m no es defectible. Entonces, el MR debe estar apagado. Pero luego el verificador de tipos todavía persigue su propia cola tratando de probar que la restricción es satisfactoria. Con solo la instancia de elevación, no puede. Si proporciona un ancla, puede.

Pero proporcionar un tipo de firma es mucho mejor.