[Agda] Type-checking errors with meta variables

[François Thiré]

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é

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

Post by François Thiré
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 -}
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
https://lists.chalmers.se/mailman/listinfo/agda