依存型を使っていると destruct が ill-typed term を作って失敗することがあるんですが，その原因が何なのかがよくわからないので似たような現象を起こす小さな例を探しています。pattern でおそらく同様の原因によるものと思われるエラーが出る例を作りま…