agda - 相互式の式の型が見つかりません

Question

WindowsのAgda 2.5.1.1では、以下のコードをロードした後（チュートリアルhttps://github.com/k0001/tut-agda/blob/master/SetsParametric.agdaに対応）、Cc Cdの型チェックで[]の型がList₁ _A_2 _B_3になります式はtrue ∷ []のような構造化された式には合理的な型はなく、アンダースコアと数字だけが返されます（_5など）。どのような理由があるのでしょうか？

以前のチュートリアルの演習はうまくいきました。

module Sets.Parametric where 

open import Sets.Enumerated using (Bool; true; false; ⊤; tt) 

data List₁ (A B : Set) : Set 
data List₂ (A B : Set) : Set 
data List₁ (A B : Set) where 
    [] :     List₁ A B 
    _∷_ : A → List₂ A B → List₁ A B 

data List₂ (A B : Set) where 
    _∷_ : B → List₁ A B → List₂ A B 

Answer 1

非オーバーロードされたコンストラクタはinferrable、ひいては[]の種類が推測されているが、オーバーロードされたコンストラクタはチェック可能ですので、あなたはタイプtrue ∷ []を推論することはできません - だけList₂ Bool Aに対してそれを確認してください。

そうでないと、オーバーロードされたコンストラクタの型指定による解決が複雑になります。例えば。 _∷_のタイプは最初の引数に依存する可能性があり、_∷_がList₁またはList₂に属するかどうかを計算すると、延期される可能性のある2つの可能性のある統一問題（List₁とList₂の1つ）ユーザが何を意味するのかが明らかになるまでメモリに座ってください。 Agdaはすでに多くのメタ変数を生成していますが、この数を増やす理由はなく、型のチェックが複雑になりすぎてこの便利な機能ではありません。