Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why can't the Show instance be derived for MaybeT?

Tags:

haskell

If I define the monad transformer type for Identity, it is able to derive the Show instance.

newtype IdentityT f a =
  IdentityT { runIdentityT :: f a }
  deriving (Show)

will derive

instance Show (f a) => Show (IdentityT f a)

But if I define the monad transformer type for Maybe

newtype MaybeT m a =
  MaybeT { runMaybeT :: m (Maybe a) }
  deriving (Show)

I get the error

• No instance for (Show (m (Maybe a)))
        arising from the first field of ‘MaybeT’ (type ‘m (Maybe a)’)

Since Maybe a has a Show instance, I would expect it to work and derive

instance Show (m (Maybe a)) => Show (MaybeT m a)

Why can't it?

like image 673
robertjlooby Avatar asked Jun 24 '17 19:06

robertjlooby


2 Answers

GHC uses a heuristics to determine if an instance guarantees search termination. By termination here, we mean that, when searching for an instance we will not loop forever. Concretely,this must be forbidden

instance Show a => Show a where ...

as well as this

instance Show [a] => Show a where ...

GHC roughly requires that constraints in the instance context (the part before the =>) must be "smaller" than the constraint in the head (after the =>). So, it accepts this:

instance Show a => Show [a] where ...

since a contains one type constructor less than [a].

It also accepts this:

instance Show (f a) => Show (IdentityT f a) where ...

since f a contains one type constructor less than IdentityT f a.

However,

instance Show (f (Maybe a)) => Show (MaybeT f a) where ...

uses the same number of constructors! Hence, it is not accepted to be sure it will not cause a loop. After all, later on, we might meet

instance Show (MaybeT f a)) => Show (f (Maybe a)) where ...

and it's clear that at least one of these two instances must be rejected to guarantee termination. GHC chooses to reject both of them.

UndecidableInstances relaxes this restriction. GHC will accept both instances, and now the burden is on us to avoid loops.

like image 115
chi Avatar answered Nov 14 '22 02:11

chi


I think we can see the issue by following GHC's suggestions (I'm using 8.2.1) until we hit a dead end:

Prelude> :{
Prelude| newtype MaybeT m a =
Prelude|   MaybeT { runMaybeT :: m (Maybe a) }
Prelude|   deriving (Show)
Prelude| :}

<interactive>:12:13: error:
    • No instance for (Show (m (Maybe a)))
        arising from the first field of ‘MaybeT’ (type ‘m (Maybe a)’)
      Possible fix:
        use a standalone 'deriving instance' declaration,
          so you can specify the instance context yourself
    • When deriving the instance for (Show (MaybeT m a))
Prelude> :set -XStandaloneDeriving 
Prelude> deriving instance Show (m (Maybe a)) =>  Show (MaybeT m a)

<interactive>:17:19: error:
    • The constraint ‘Show (m (Maybe a))’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the stand-alone deriving instance for
        ‘Show (m (Maybe a)) => Show (MaybeT m a)’

Okay, so Show wasn't derivable for MaybeT likely because that constraint would have been disallowed, as it's the sort of constraint the typechecker can't prove termination about. You can read more about what "no smaller than instance head" means in this answer: https://stackoverflow.com/a/17866970/176841

like image 26
jberryman Avatar answered Nov 14 '22 02:11

jberryman