# 067: showlist2.hs がランタイムに abend 
[↑up](bunny_notes)

- issued: 2020-05-08
- 分類： A サンプルコードが fail
- status: Closed (2020-05-13)

## 概要

[055](bissue055) の調査のために、再現用の小さなテストプロを作成。

showlist2.hs:

$$<pre>{
$ 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:

$$<pre>{
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 を見比べてみよう。

## 調査ログ
### 2020-05-12

だめな場合の core を確認すると、DARG0 を渡すべきところで、${Prelude.Char Prelude.Show} を渡しているよう。型注釈をつけた showlist3.hs では、
${Prelude.Integer Prelude.Show} がその場で生成されているので OK。

ただ、まだ例が大きすぎてみるのが大変だし、被疑個所が特定しづらい。
そこで、もっと小さくしていって、エラーが出る場合と出ない場合の境界をあきらかにしたい。

どうやら、これが最小再現ケースではないかな (t067.hs)：

$$<pre>{
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 式が頻出していて、
その複雑な場合に発生する問題かなと恐れたのですが、そうでもなかった。 

なお、$<verb>{f} はこれ以上単純化する、たとえば、$<verb>{f xs str = show' xs}
のようにすると、もう、再現しない。

t067.hs の問題の core は次の通り：

$$<pre>{
---- 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)))  ""))
$$}

$<verb>{Main.l1.l0.l0.l0.show'} のなかで、show に渡されている辞書が、
なぜ唐突に $<verb>{${Prelude.Char Prelude.Show}} なのかということ。

show' の外にある、f を単純にすると再現しないことから、ひとつ上のレベルの変な情報を拾ってしまっている模様。（そういえば、CompositDict を思いつくまえに、変な改造をいれたかな…）

f を少し単純にした t067b.hs のコアは以下のとおり：

$$<pre>{
---- 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 あたりにある。

$$<pre>{
---- 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 修正

上記の件で、TrCore を修正。_Main.l1.l0.f.U2 の型から不要な Predicate は消えるようになったが、辞書渡しがおかしいのは変わらず。

$$<pre>{
$ 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 の古いバージョンと同じやり方で生成しているのでは？

### DictPass 調査（継続）

$<verb>{tcExpr e@(Var n (qv :=> t'))) qt} にトレースを仕掛けてみると、
ここで問題の "show" 呼び出しを処理するときに与えられる qt が変。

$$<pre>{
(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 の中と外でなにかコンフリクトしている模様。

$$<pre>{
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 間でも）のを修正。

それで改善するかと思ったが、そうはいかず。
でも、この修正は必要だったとは思われる。

### 2020-05-13

t067.hs 処理のどこで初めて t1 なり t2 が Char になってしまうか捉えるために、
check&stoper を仕掛ける。

$$<pre>{
-- 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 で停止した：

$$<pre>{
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'
$$}

つかんだ尻尾は以下：

$$<pre>{
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 に問題があった。

以下は修正後のコード：

$$<pre>{
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 が二回生成されて衝突）。

これを直したことで、本件の問題は解決。

- showlist2.hs : sample194
- t067.hs : sample195

もともと ok だった、showlist.hs, showlist3.hs は廃止。