<div dir="ltr"><div dir="ltr"><div>Hi François,</div><div><br></div><div>Thank you for your message. This seems to be a bug in Agda, I've reported it here: <a href="https://github.com/agda/agda/issues/3431">https://github.com/agda/agda/issues/3431</a>.</div><div><br></div><div>Best regards,</div><div>Jesper</div><div><br></div><div>ps: I wouldn't necessarily recommend a combination of --rewriting with universe level hackery as an introduction to Agda, but I guess you know that already ;)<br></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Tue, Dec 4, 2018 at 10:33 AM François Thiré <<a href="mailto:franth2@gmail.com">franth2@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>