今日のお仕事終わり！

type と type scheme で行き来できるようなもんだしな。それと同じで type とふわふわ type 用意して、ふやふわ type から type にせんと型付けできないところとふわふわ type でも型付けできるとこ用意すればええだけか

よく考えれば System-F の instantiation / generalizing も stage 化みたいなものか

いやでもこれ普通の declarative でも stage つければ書けるか

つまりリテラル直書きで使う際は柔軟な推論してくれるが、一回変数とかに当てはめると型が固定化されるみたいなやつ

具体的には、

#let x: (a: Int, b: String) = (1, "str") // ok
#let y = (1, "str")
#let z: (a: Int, b: String) = y // ng, y is inferred to `(?1: Int, ?2: String)`

bidirectional typing だと、ある範囲では柔軟な推論をしてくれるけど、ある程度になると型が固定化されるみたいな型システムも割と柔軟に書けることに気づいた