Type signature is too general; missing constraint?

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 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.

链接地址: http://www.djcxy.com/p/43038.html

上一篇: 为什么我的自定义类型的地图实现不正确？

下一篇: 类型签名过于笼统; 缺少约束？