要するに明示的な型宣言をして通るプログラムならば、
型推論でも必ず通るという意味なのかな？