Using Agda v2.6.4.3 and agda-stdlib v2.0, I'm encountering the following error
Expected a hidden argument, but found a visible argument
when checking that the type
{Γ Γ' Γ'' : Ctx} (ρ : Rename Γ' Γ'') (σ : Subst Γ Γ') {τ₁ τ₂ : Ty}
(e : Expr (τ₁ ∷ Γ) τ₂) →
subst (λ x → var (Rename.cons zero (λ x₁ → suc (ρ x₁)) x))
(subst (var zero • (λ idx → Rename.rename suc (σ idx))) e)
≡
subst
(var zero • (λ idx → Rename.rename suc (σ idx)) ；
(λ x → var (Rename.cons zero (λ x₁ → suc (ρ x₁)) x)))
e →
abstraction
(subst (var zero • (λ idx → var (suc (ρ idx))))
(subst (var zero • (λ idx → Rename.rename suc (σ idx))) e))
≡
abstraction
(subst
(var zero •
(λ idx → Rename.rename suc (subst (λ z {τ} → var (ρ τ)) (σ idx))))
e)
of the generated with function is well-formed
(https://agda.readthedocs.io/en/v2.6.4/language/with-abstraction.html#ill-typed-with-abstractions)
when trying to typecheck the following:
{-# OPTIONS --rewriting #-}
module MWE where
open import Data.Fin using (Fin)
open import Data.List using (List; _∷_)
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (refl; _≡_)
data Ty : Set where
arr : Ty → Ty → Ty
Ctx : Set
Ctx = List Ty
data Idx : Ctx → Ty → Set where
zero : {Γ : Ctx} {τ : Ty} → Idx (τ ∷ Γ) τ
suc : {Γ : Ctx} {τ₁ τ₂ : Ty} → Idx Γ τ₂ → Idx (τ₁ ∷ Γ) τ₂
data Expr (Γ : Ctx) : Ty → Set where
var : {τ : Ty} → Idx Γ τ → Expr Γ τ
abstraction : {τ₁ τ₂ : Ty} → Expr (τ₁ ∷ Γ) τ₂ → Expr Γ (Ty.arr τ₁ τ₂)
module Rename where
Rename : Ctx → Ctx → Set
Rename Γ Γ' = {τ : Ty} → Idx Γ τ → Idx Γ' τ
cons : {Γ Γ' : Ctx} {τ : Ty} → Idx Γ' τ → Rename Γ Γ' → Rename (τ ∷ Γ) Γ'
cons idx ρ Idx.zero = idx
cons idx ρ (Idx.suc idx') = ρ idx'
ext : {Γ Γ' : Ctx} {τ : Ty} → Rename Γ Γ' → Rename (τ ∷ Γ) (τ ∷ Γ')
ext ρ = cons Idx.zero (Idx.suc ∘ ρ)
rename : {Γ Γ' : Ctx} {τ : Ty} → Rename Γ Γ' → Expr Γ τ → Expr Γ' τ
rename ρ (Expr.var idx) = Expr.var (ρ idx)
rename ρ (Expr.abstraction e) = Expr.abstraction (rename (ext ρ) e)
open Rename using (Rename)
Subst : Ctx → Ctx → Set
Subst Γ Γ' = {τ : Ty} → Idx Γ τ → Expr Γ' τ
infixr 6 _•_
_•_ : {Γ Γ' : Ctx} {τ : Ty} → Expr Γ' τ → Subst Γ Γ' → Subst (τ ∷ Γ) Γ'
_•_ e σ Idx.zero = e
_•_ e σ (Idx.suc idx) = σ idx
⟰ : {Γ Γ' : Ctx} {τ : Ty} → Subst Γ Γ' → Subst Γ (τ ∷ Γ')
⟰ σ idx = Rename.rename Idx.suc (σ idx)
ext : {Γ Γ' : Ctx} {τ : Ty} → Subst Γ Γ' → Subst (τ ∷ Γ) (τ ∷ Γ')
ext σ = Expr.var Idx.zero • ⟰ σ
subst : {Γ Γ' : Ctx} {τ : Ty} (σ : Subst Γ Γ') → Expr Γ τ → Expr Γ' τ
subst σ (Expr.var idx) = σ idx
subst σ (Expr.abstraction e) = Expr.abstraction (subst (ext σ) e)
ren : {Γ Γ' : Ctx} → Rename Γ Γ' → Subst Γ Γ'
ren ρ = Expr.var ∘ ρ
abstract
infixr 5 _；_
_；_ : {Γ Γ' Γ'' : Ctx} → Subst Γ Γ' → Subst Γ' Γ'' → Subst Γ Γ''
(σ ； σ') x = subst σ' (σ x)
abstract
seq-def : {Γ Γ' Γ'' : Ctx} {τ : Ty} (σ : Subst Γ Γ') (σ' : Subst Γ' Γ'') (idx : Idx Γ τ) → (σ ； σ') idx ≡ subst σ' (σ idx)
seq-def σ σ' idx = refl
{-# BUILTIN REWRITE _≡_ #-}
{-# REWRITE seq-def #-}
subst-ren : {Γ Γ' Γ'' : Ctx} {τ : Ty} (ρ : Rename Γ' Γ'') (σ : Subst Γ Γ') (e : Expr Γ τ) → subst (ren ρ) (subst σ e) ≡ subst (σ ； (ren ρ)) e
subst-ren ρ σ (Expr.var idx) = refl
subst-ren ρ σ (Expr.abstraction e) with subst-ren (Rename.ext ρ) (ext σ) e
... | x = ?
The problem goes away if I don't use REWRITE.
(Was recommended to file bug report from chat)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4