Type signature is too general; missing constraint?

Question

So I tried to ask a general "how do you debug type-level programming problems?" question, and it seems either the question is too general to answer, or maybe it's impossible to debug such things. :-}

On this particular day, the problem that's irking me is a moderately large, complex program. I've managed to boil it down to a reasonably small core that still goes wrong. Here we go:

{-#
  LANGUAGE
    GADTs, MultiParamTypeClasses,
    FlexibleInstances, FlexibleContexts, RankNTypes,
    KindSignatures
#-}

module Minimal where

-------------------------------------------------------------------------------

data Union (t :: * -> *) (ts :: * -> *) x

class Member (x :: * -> *) (ys :: * -> *) where
instance Member x (Union x ys) where
instance (Member x ys) => Member x (Union y ys) where

-------------------------------------------------------------------------------

data ActM (effects :: * -> *) x
instance Monad (ActM effects) where

-------------------------------------------------------------------------------

data Reader i x where
  Get :: Reader i i

get :: Member (Reader i) req => ActM req i
get = undefined

runReader :: i -> ActM (Union (Reader i) req) x -> ActM req x
runReader = undefined

(Aside: I look at that list of language extensions and think to myself "maybe this is just a terrible idea!")

Anyway, the really interesting part is at the bottom. We see that

runReader :: i -> ActM (Union (Reader i) req) x -> ActM req x

In other words, for any i, runReader takes an action in the ActM monad that has Reader i as one of its possible effects, and returns an action in the ActM monad without that possible effect. Simple, right?

Now if I pass (say) a Char as the first argument, then the reader type is fixed to Char:

runReader 'X' :: ActM (Union (Reader Char) req) x -> ActM req x

So far, so good. If I just return some data, all is fine:

runReader 'X' (return True) :: ActM req Bool

(Reassuringly, I also get the correct value as the result!)

But now, what about the get function?

get :: Member (Reader i) req => ActM req i

So get is an action in the ActM monad for any set of effects that includes Reader i. And that means that if I pass it to runReader then I get...

runReader 'X' get :: Member (Reader x) (Union (Reader Char) req) => ActM req x

...wait, what?!? Why hasn't the compiler figured out that x must be Char?

Indeed, if I add an explicit type signature that says

runReader 'X' get :: ActM req Char

then it compiles perfectly (and, incidentally, I get the right value output, which is nice). So where am I missing a constraint?

The instance Member x (Union x ys) requires that both the xs be the same to begin with to match - the compiler will not deduce this information. You would have to write (x ~ x') => Member x (Union x' xs) but this would be overlapping with the other instance - I believe you need a cleverer way of computing membership. — user2407038
Is that really enough extensions? Those two Member instances look awfully suspicious -- like maybe you'll need OverlappingInstances or perhaps even IncoherentInstances for those to "work". If you've got IncoherentInstances on, well... I think the official party line with that extension is, "Good luck, don't complain to us.". — Daniel Wagner
@DanielWagner That's odd... OverlappingInstances is supposed to be in there. I'm not sure how it ended up missing. I must have accidentally dropped it while building my minimal example. — MathematicalOrchid
@user2407038 I was surprised to learn that you can actually write x ~ y in a type signature! You learn something new every day... — MathematicalOrchid

Daniel Wagner Daniel Wagner · Accepted Answer · 2016-05-09T21:33:27

The compiler hasn't figured out that x must be Char because it isn't true. For example, one might write

type ReadsBool req = Union (Reader Bool) req
type ReadsCharAndBool req = Union (Reader Char) (ReadsBool req)

and then you have:

runReader 'X' (get :: ReadsCharAndBool req) :: ActM (ReadsBool req) Bool

So congratulations, now you know why mtl's MonadReader class has the fundep it does: for type inference reasons, one often wants the monad to uniquely determine what kind of thing you can get from it.

Type signature is too general; missing constraint?

1 Answers