[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é
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20181204/73d01409/attachment.html>