<div dir="ltr"><div dir="ltr"><div dir="ltr"><div>Dear mailing list,</div><div><br></div><div>I am not really familiar with the Agda system, but I want to use it to make some experiments.</div><div><br></div><div>On the relatively small example below, I have a definition that is well-typed when everything is instantiated. However, if I replace the second occurrence of "a" by a hole, Agda refuses to elaborate the term and gives me an error. I don't understand why Agda is giving me this error message and is there a way to overcome this problem?<br></div><div><br></div><div>I am using the version 2.6.0 of Agda.<br></div><div><br></div><div><span style="font-family:monospace,monospace">{-# OPTIONS --rewriting #-}<br><br>module test where<br><br>open import Level<br>open import Agda.Builtin.Equality<br>{-# BUILTIN REWRITE _≡_ #-}<br><br>1ℓ : Level<br>1ℓ = suc zero<br><br>postulate<br>  prod  : {ℓ ℓ′ : Level} → (A : Set ℓ) → (B : Set ℓ′) → Set (ℓ ⊔ ℓ′)<br><br>  p : Set 1ℓ → Set 1ℓ<br>  q : Set 1ℓ → Set 1ℓ<br>  f : ∀ (c : Set 0ℓ) → p (Lift 1ℓ c) → q (Lift 1ℓ c)<br>  g : ∀ (a : Set 1ℓ) → ∀ (b : Set 1ℓ) → p (prod a b)<br>  a : Set 0ℓ<br>  b : Set 0ℓ<br><br>  canL : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → (B : Set ℓ′)  → (prod (Lift ℓ″ A) B) ≡ Lift (ℓ″ ⊔ ℓ′) (prod A B)<br>  canR : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → (B : Set ℓ′)  → (prod A (Lift ℓ″ B)) ≡ Lift (ℓ ⊔ ℓ″) (prod A B)<br>  canT : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → Lift ℓ″ (Lift ℓ′ A) ≡ Lift (ℓ″ ⊔ ℓ′) A<br><br>{-# REWRITE canL #-}<br>{-# REWRITE canR #-}<br>{-# REWRITE canT #-}<br><br>ali : q (Lift 1ℓ (prod a b))<br>ali = f (prod a b) (g (Lift 1ℓ a) (Lift 1ℓ b))<br>{- ali = f (prod a b) (g (Lift 1ℓ ?) (Lift 1ℓ b)) FAILS -}</span></div><div><br></div><div>For this last line, the error message is:</div><div><br></div><div><span style="font-family:monospace,monospace">Set₁ != Set<br>when checking that the expression g (Lift 1ℓ ?) (Lift 1ℓ b) has<br>type p (Lift 1ℓ (prod a b))</span></div><div><br></div><div>Best wishes,</div><div><br></div><div>François Thiré<br></div></div></div></div>