055 の調査のために、再現用の小さなテストプロを作成。
showlist2.hs:
$ cat testcases/showlist2.hs
main = do
putStrLn $ showList [1] ""
where
showList xs = (++) (showlist' xs)
where showlist' [] = "[]"
showlist' [x] = "[" ++ show x ++ "]"
showlist' (x:xs) = "[" ++ foldl (\s t -> s ++ "," ++ show t) (show x) xs ++ "]"
これをコンパイル、実行するとランタイムでエラーする。 なお、これに似た showlist.hs は大丈夫。
showlist.hs:
main = do
putStrLn $ showList [1] ""
where showlist' [] = "[]"
showlist' [x] = "[" ++ show x ++ "]"
showlist' (x:xs) = "[" ++ foldl (\s t -> s ++ "," ++ show t) (show x) xs ++ "]"
showList xs = (++) (showlist' xs)
また、showlist2.hs の showlist' に型注釈をつけたもの（showlist3.hs）も Ok.
エラーするケースでは、showlist' 内部における辞書の解決がおかしいようにみえる。
let 式がネストされているケースの多相の解決（DictPass による辞書渡し形式への変換） に難があるようだ。flesh な type value にすべきところをしていないとか、かも。
うまくいくケースとそうでない場合の core0, core を見比べてみよう。
だめな場合の core を確認すると、DARG0 を渡すべきところで、${Prelude.Char Prelude.Show} を渡しているよう。型注釈をつけた showlist3.hs では、 ${Prelude.Integer Prelude.Show} がその場で生成されているので OK。
ただ、まだ例が大きすぎてみるのが大変だし、被疑個所が特定しづらい。 そこで、もっと小さくしていって、エラーが出る場合と出ない場合の境界をあきらかにしたい。
どうやら、これが最小再現ケースではないかな (t067.hs)：
main = do
putStrLn $ f 1 ""
where
f xs str = str ++ (show' xs)
where show' x = show x
show' はここまで単純でも再現する。でも、let が nest されていて、show' の型が決まらない（多相になる）のは必須だと思われる。
instancee (Show a) => Show [a] の実装において発覚した問題だが、リストは関係なかったよう。また、元の例ではパターンマッチコンパイル結果の case 式が頻出していて、 その複雑な場合に発生する問題かなと恐れたのですが、そうでもなかった。
なお、f はこれ以上単純化する、たとえば、f xs str = show' xs のようにすると、もう、再現しない。
t067.hs の問題の core は次の通り：
---- ddumpCore ----
(Main.main :: (Prelude.IO ())) =
let
(Main.l1.l0.f :: ([Prelude.Show t5] :=> (t5 -> ([Prelude.Char] -> [Prelude.Char])))) =
\(Main.l1.l0.f.DARG0 :: Ä) ->
\(_Main.l1.l0.f.U1 :: ([Prelude.Show t0] :=> t0)) (_Main.l1.l0.f.U2 :: ([Prelude.Show t0] :=> [Prelude.Char])) ->
let
(Main.l1.l0.l0.l0.show' :: ([Prelude.Show t3] :=> (t3 -> [Prelude.Char]))) =
\(Main.l1.l0.l0.l0.show'.DARG0 :: Ä) ->
\(_Main.l1.l0.l0.l0.show'.U1 :: ([Prelude.Show t1] :=> t1)) ->
(((Prelude.show :: ([Prelude.Show t2] :=> (t2 -> [Prelude.Char])))
${Prelude.Char Prelude.Show})
(_Main.l1.l0.l0.l0.show'.U1 :: ([Prelude.Show t1] :=> t1)))
in
(((Prelude.++ :: ([t3] -> ([t3] -> [t3])))
(_Main.l1.l0.f.U2 :: ([Prelude.Show t0] :=> [Prelude.Char])))
(((Main.l1.l0.l0.l0.show' :: ([Prelude.Show t4] :=> (t4 -> [Prelude.Char])))
(Main.l1.l0.f.DARG0 :: Å))
(_Main.l1.l0.f.U1 :: ([Prelude.Show t0] :=> t0))))
in
((Prim.putStrLn :: ([Prelude.Char] -> (Prelude.IO ()))) $
((((Main.l1.l0.f :: ([Prelude.Show t7] :=> (t7 -> ([Prelude.Char] -> [Prelude.Char]))))
${Prelude.Integer Prelude.Show})
(((Prelude.fromInteger :: ([Prelude.Num t8] :=> (Prelude.Integer -> t8)))
${Prelude.Integer Prelude.Num})
(1 :: Prelude.Integer))) ""))
Main.l1.l0.l0.l0.show' のなかで、show に渡されている辞書が、 なぜ唐突に ${Prelude.Char Prelude.Show } なのかということ。
show' の外にある、f を単純にすると再現しないことから、ひとつ上のレベルの変な情報を拾ってしまっている模様。（そういえば、CompositDict を思いつくまえに、変な改造をいれたかな…）
f を少し単純にした t067b.hs のコアは以下のとおり：
---- ddumpCore ----
(Main.main :: (Prelude.IO ())) =
let
(Main.l1.l0.f :: ([Prelude.Show t5] :=> (t5 -> (t6 -> [Prelude.Char])))) =
\(Main.l1.l0.f.DARG0 :: Ä) ->
\(_Main.l1.l0.f.U1 :: ([Prelude.Show t0] :=> t0)) (_Main.l1.l0.f.U2 :: ([Prelude.Show t0] :=> t1)) ->
let
(Main.l1.l0.l0.l0.show' :: ([Prelude.Show t4] :=> (t4 -> [Prelude.Char]))) =
\(Main.l1.l0.l0.l0.show'.DARG0 :: Ä) ->
\(_Main.l1.l0.l0.l0.show'.U1 :: ([Prelude.Show t2] :=> t2)) ->
(((Prelude.show :: ([Prelude.Show t3] :=> (t3 -> [Prelude.Char])))
(Main.l1.l0.l0.l0.show'.DARG0 :: Å))
(_Main.l1.l0.l0.l0.show'.U1 :: ([Prelude.Show t2] :=> t2)))
in
(((Main.l1.l0.l0.l0.show' :: ([Prelude.Show t4] :=> (t4 -> [Prelude.Char])))
(Main.l1.l0.f.DARG0 :: Å))
(_Main.l1.l0.f.U1 :: ([Prelude.Show t0] :=> t0)))
in
((Prim.putStrLn :: ([Prelude.Char] -> (Prelude.IO ()))) $
((((Main.l1.l0.f :: ([Prelude.Show t7] :=> (t7 -> (t8 -> [Prelude.Char]))))
${Prelude.Integer Prelude.Show})
(((Prelude.fromInteger :: ([Prelude.Num t9] :=> (Prelude.Integer -> t9)))
${Prelude.Integer Prelude.Num})
(1 :: Prelude.Integer))) ""))
上手くいっている方は、_Main.l1.l0.f.U2 の型が違う（多相）。 だめな方は、これをなぜか拾っている？？
おお、そうか。_Main.l1.l0.f.U1 と _Main.l1.l0.f.U2 の量化変数がともに t0 になっていて、 まざっているんだと思われる。
Core0 の時点でおかしいので、問題は DictPass ではなく、TrCore あたりにある。
---- ddumpCore ----
(Main.main :: (Prelude.IO ())) =
let
(Main.l1.l0.f :: ([Prelude.Show t5] :=> (t5 -> ([Prelude.Char] -> [Prelude.Char])))) =
\(_Main.l1.l0.f.U1 :: ([Prelude.Show t0] :=> t0)) (_Main.l1.l0.f.U2 :: ([Prelude.Show t0] :=> [Prelude.Char])) ->
ちょっと怖いので、ブランチをわけて修正作業をしよう。あとで。
上記の件で、TrCore を修正。_Main.l1.l0.f.U2 の型から不要な Predicate は消えるようになったが、辞書渡しがおかしいのは変わらず。
$ git diff
diff --git a/compiler/src/TrCore.hs b/compiler/src/TrCore.hs
index 291a029..5abc145 100644
--- a/compiler/src/TrCore.hs
+++ b/compiler/src/TrCore.hs
@@ -6,7 +6,7 @@ import PreDefined (ConstructorInfo, initialConsts)
import Symbol
import Types
import Typing (Assump (..), Pred (..), Qual (..),
- Scheme (..), find, inst)
+ Scheme (..), find, inst, tv)
import qualified Typing as Ty (Expr (..), Literal (..),
Pat (..))
@@ -120,8 +120,9 @@ transVdef (n, Pat.Lambda ns expr) = do
vs = zipWith f ns ts
qf = case qt of
(qf' :=> _) -> qf'
- f n' t' = TermVar n' (qf :=> t')
- as' = [n' :>: Forall [] (qf :=> t') | (n', t') <- zip ns ts]
+ f n' t' = let qf' = filter (\pr -> head (tv pr) `elem` tv t') qf
+ in TermVar n' (qf' :=> t')
+ as' = [n' :>: Forall [] (qf' :=> t') | TermVar n' (qf' :=> t') <- vs]
appendAs as'
expr' <- transExpr expr
appendBind (n, lam' vs expr')
このあたりの実装は、最後あたりに整理しなおさないといけなさそう。 あやふやな理解のまま書いた風なところが多い。
もしかして、DictPass では、Lambda の型を assump からとればいい （TrCore で登録してある）のに、TrCore の古いバージョンと同じやり方で生成しているのでは？
tcExpr e@(Var n (qv :=> t'))) qt にトレースを仕掛けてみると、 ここで問題の "show" 呼び出しを処理するときに与えられる qt が変。
(Var (TermVar "Prelude.show" ([IsIn "Prelude.Show" (TVar (Tyvar "t2" Star))] :=> TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "t2" Star))) (TAp (TCon (Tycon "Prelude.[]" (Kfun Star Star))) (TCon (Tycon "Prelude.Char" Star))))),[] :=> TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TCon (Tycon "Prelude.Char" Star))) (TAp (TCon (Tycon "Prelude.[]" (Kfun Star Star))) (TCon (Tycon "Prelude.Char" Star))))
これでは、show の第一引数の型は Char なので、${Prelude.Char Prelude.Show} が生成される。
仮に、Let の tcExpr 中で、tcBind に state を引き継がないようにすると、 t067.hs は通るようになる（他がだめになるが）。
let の中と外でなにかコンフリクトしている模様。
tcExpr (Let bs e) qt = do st <- get let bs' = tcBind bs (tcCe st) (Just st) e' <- tcExpr e (normQTy qt) return $ Let bs' e'
tcBind にせっかく状態をわたしているのに、そこで更新された tcNum をあとに引き継いでなかった（複数の tcbind 間でも）のを修正。
それで改善するかと思ったが、そうはいかず。 でも、この修正は必要だったとは思われる。
t067.hs 処理のどこで初めて t1 なり t2 が Char になってしまうか捉えるために、 check&stoper を仕掛ける。
-- checkStoper (for 067)
checkStop :: TC ()
checkStop = do
s <- getSubst
let t1 = TVar (Tyvar "t1" Star)
t2 = TVar (Tyvar "t2" Star)
t1' = apply s t1
t2' = apply s t2
trace (show (t1,t1',t2,t2')) $ return ()
when (t1' == tChar) $ error "checkStop t1' = tChar"
when (t2' == tChar) $ error "checkStop t2' = tChar"
tcExpr Lam における unify' 直後の checkStop で停止した：
tcExpr e@(Lam vs ebody) (qs :=> t) = do
trace ("tcExpr 0:" ++ show e ++ " (" ++ show qs ++ " :=> " ++ show t ++ ")") checkStop
_ :=> t' <- getTy e
unify' t' t
trace (show t') $ return ()
trace ("tcExpr 1:" ++ show e ++ " (" ++ show qs ++ " :=> " ++ show t ++ ")") checkStop
qt <- getTy ebody
s <- getSubst
ebody' <- tcExpr ebody (normQTy (apply s qt))
return $ Lam vs ebody'
つかんだ尻尾は以下：
TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "t1" Star))) (TAp (TCon (Tycon "Prelude.[]" (Kfun Star Star))) (TCon (Tycon "Prelude.Char" Star)))
tcExpr 1:
Lam [TermVar "_Main.l1.l0.l0.l0.show'.U1" ([IsIn "Prelude.Show" (TVar (Tyvar "t1" Star))] :=> TVar (Tyvar "t1" Star))]
(App (Var (TermVar "Prelude.show" ([IsIn "Prelude.Show" (TVar (Tyvar "t2" Star))] :=> TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "t2" Star))) (TAp (TCon (\
Tycon "Prelude.[]" (Kfun Star Star))) (TCon (Tycon "Prelude.Char" Star)))))) (Var (TermVar "_Main.l1.l0.l0.l0.show'.U1" ([IsIn "Prelude.Show" (TVar (Tyvar "t1" Star))] :=> TVar (Tyvar "t1"\
Star)))))
([IsIn "Prelude.Show" (TVar (Tyvar "t3" Star))] :=>
TAp (TAp (TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))) (TVar (Tyvar "t3" Star))) (TAp (TCon (Tycon "Prelude.[]" (Kfun Star Star))) (TCon (Tycon "Prelude.Char" Star))))
bunnyc: checkStop t1' = tChar
ここでは、t1 -> [Char] と t3 -> [Char] を unify して、t1 -> Char に なってしまっている。
しらべると、この時点ですでに t3 -> Char となっていた。
なので、こんどは、t3 -> Char になった瞬間を捕まえなくてはいけない。
おっていくと、(++) :: [t3] -> [t3] -> [t3] で、これの引数に "" が与えられているので、 t3 -> Char と置換されるのは正しい。 問題は、show' に出現する show の型にも同じ型変数が用いられ、show :: (Show t3) => t3 -> [Char] となっているところ。
やっぱり、被疑個所は DictPass ではない。
TrCore.appendBind に問題があった。
以下は修正後のコード：
appendBind :: (Id, Expr) -> TRC ()
appendBind (n, e) = do
t <- typeLookup n
st <- get -- this must be after the typeLookup above.
let Rec bs = trcBind st
bs' = bs ++ [(TermVar n t, e)]
put st{trcBind = Rec bs'}
typeLookup にて、Assump から識別子 n の型を検索し、かつ、 量化変数を具体化するのだが、そこで状態 st が更新される。
が、従来のコードは、st <- get を typelookup の前に行っていたため、 その後の put st{...} で、st の内部状態 trcNum が巻き戻ってしまい、 番号の重複につながっていた（t3 が二回生成されて衝突）。
これを直したことで、本件の問題は解決。
もともと ok だった、showlist.hs, showlist3.hs は廃止。