CODEWITHSUNDEEP
haskellghctype-inferencetypeclassassociated-types
gatoatigrado
gatoatigrado

Reputation: 16850

GHC type inference woes

Question. Is there any way to make this code work without an explicit type signature?

Code. First, I have a in-practice-much-nicer alternate MonadTrans class, inspired by Data.Newtype. It looks like this,

{-# LANGUAGE FlexibleContexts, TypeFamilies #-}

module Alt.Control.Monad.Trans where

import Control.Monad

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

Then, I have a class A with method foo, and if some base monad M is an A, then any transformed monad T M is also an A. In code,

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

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

However, if I now want to create a shortcut for foo with its first argument substituted, then I need an explicit type signature, or the compiler's context stack overflows.

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

Possible info to help inference. Let's say we have an associated type B :: * -> *. I'm thinking that I want to tell the compiler B satisfies B t /= t, B (B t) /= B t, etc. i.e. B is somehow "monotonic" -- that chasing associated types is equivalent to removing newtype wrappers, and it should know that it cannot remove newtype wrappers forever, hence adding the context A to the signature is necessary.

Upvotes: 5

Views: 215

Answers (1)

Daniel Fischer
Daniel Fischer

Reputation: 183873

Yes, there is a way. Provide a grounded instance for A, and add NoMonomorphismRestriction to the language pragma (in addition to the also required FlexibleInstances and UndecidableInstances).

However, the A class will be unusable. There is no way for the compiler to know that there never will be a MonadTrans instance with BaseMonad m = m. Thus it cannot select an instance, ever, because it cannot know whether to use the instance from here or another one.

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

compiles with ghc 6.12, 7.0, 7.2 and 7.4. Without the signature, minimize_call must get a monomorphic type, unless the MR is turned off. That can't work anyway because the constraint A m is not defaultable. So therefore the MR must be turned off. But then the type checker still chases its own tail trying to prove the constraint is satisfiable. With only the lifting instance, it can't. If you provide an anchor, it can.

But providing a type signature is much much better.

Upvotes: 3

Related Questions