[Agda] Type-checking errors with meta variables

[Jesper Cockx]

Hi François,

Thank you for your message. This seems to be a bug in Agda, I've reported
it here: https://github.com/agda/agda/issues/3431.

Best regards,
Jesper

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 ;)

On Tue, Dec 4, 2018 at 10:33 AM François Thiré <franth2 at gmail.com> wrote:

> Dear mailing list,
>
> I am not really familiar with the Agda system, but I want to use it to
> make some experiments.
>
> 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?
>
> I am using the version 2.6.0 of Agda.
>
> {-# OPTIONS --rewriting #-}
>
> module test where
>
> open import Level
> open import Agda.Builtin.Equality
> {-# BUILTIN REWRITE _≡_ #-}
>
> 1ℓ : Level
> 1ℓ = suc zero
>
> postulate
>   prod  : {ℓ ℓ′ : Level} → (A : Set ℓ) → (B : Set ℓ′) → Set (ℓ ⊔ ℓ′)
>
>   p : Set 1ℓ → Set 1ℓ
>   q : Set 1ℓ → Set 1ℓ
>   f : ∀ (c : Set 0ℓ) → p (Lift 1ℓ c) → q (Lift 1ℓ c)
>   g : ∀ (a : Set 1ℓ) → ∀ (b : Set 1ℓ) → p (prod a b)
>   a : Set 0ℓ
>   b : Set 0ℓ
>
>   canL : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → (B : Set ℓ′)  → (prod (Lift ℓ″
> A) B) ≡ Lift (ℓ″ ⊔ ℓ′) (prod A B)
>   canR : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → (B : Set ℓ′)  → (prod A (Lift
> ℓ″ B)) ≡ Lift (ℓ ⊔ ℓ″) (prod A B)
>   canT : {ℓ ℓ′ ℓ″ : Level} → (A : Set ℓ) → Lift ℓ″ (Lift ℓ′ A) ≡ Lift (ℓ″
> ⊔ ℓ′) A
>
> {-# REWRITE canL #-}
> {-# REWRITE canR #-}
> {-# REWRITE canT #-}
>
> ali : q (Lift 1ℓ (prod a b))
> ali = f (prod a b) (g (Lift 1ℓ a) (Lift 1ℓ b))
> {- ali = f (prod a b) (g (Lift 1ℓ ?) (Lift 1ℓ b)) FAILS -}
>
> For this last line, the error message is:
>
> Set₁ != Set
> when checking that the expression g (Lift 1ℓ ?) (Lift 1ℓ b) has
> type p (Lift 1ℓ (prod a b))
>
> Best wishes,
>
> François Thiré
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181204/78dc9e1d/attachment.html>