title: agda - type of expression with mutual Lists not found
body: <p>In Agda 2.5.1.1 on Windows, after the code below is loaded (it corresponds to the tutorial <a href="https://github.com/k0001/tut-agda/blob/master/SetsParametric.agda" rel="nofollow noreferrer">https://github.com/k0001/tut-agda/blob/master/SetsParametric.agda</a>), the C-c C-d type-checking does find the type <code>List₁ _A_2 _B_3</code> for the <code>[]</code> expression, but no reasonable type for any more structured expression like <code>true ∷ []</code> , just underscore and number is returned, like <code>_5</code> . Any ideas what the reason could be, please?</p>
  
  <p>The previous exercises of the tutorial work well.</p>
  
  <pre><code> 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
  </code></pre>