型シグネチャがあまりにも一般的です。制約がありませんか？

Question

私は一般的な "how do you debug type-level programming problems?"という質問をしてみました。答えがあまりにも一般的なものか、そういうものをデバッグすることは不可能かもしれません。 ： - }

この特定の日に、私を悩ませている問題は、適度に大きい、複雑なプログラムです。私はまだそれが間違って合理的に小さなコアにそれを沸騰させることができた。ここに私達は行く：

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

（脇：私は言語拡張のリストを見て、自分自身に考えて、「多分これはただひどいアイデアです！」）

とにかく、本当に興味深い部分がです下。私たちは、言い換えれば

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

が、その可能性効果を任意のiため、runReaderが可能な効果の一つとしてReader iを持ってActMモナドでアクションを取り、なしActMモナドでアクションを返すことがわかり。シンプル、そう？私は最初の引数として（例えば）Charを渡した場合

さて、その後、リーダータイプがCharに固定されています

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

これまでのところ、とても良いです。私はいくつかのデータを返す場合は、すべての罰金です：

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

（！安心させる、私はまた、結果として正しい値を取得）

しかし、今、何get機能は？

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

のでgetはReader iが含ま効果の任意のセットのためのActMモナドでのアクションです。そして、それは私がrunReaderに渡した場合、私は待って... ...

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

を得ることを意味し、何？！？なぜコンパイラは、xをにする必要がありますかと考えていませんでしたChar？私は

runReader 'X' get :: ActM req Char 

を言う明示的な型シグネチャを追加する場合

確かに、それは（ちなみに、私はいいです右の出力値を、取得、および）完全にコンパイルされます。だからどこに制約がありませんか？

Answer 1

xは、真ではないため、Charである必要があります。例えば、一つは

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

を書くかもしれないし、次にあなたが持っている：型推論の理由から、人はしばしばモナドがしたい：mtl's MonadReader classはそれがないfundepを持っている理由

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

のでお祝いを、今、あなたは知っていますどのようなことができるのかを一意に決めるget