Closed sgodwincs closed 1 month ago
Here is a version without std-lib and without abstract
:
{-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality using (_≡_; refl)
open import Agda.Builtin.List using (List; _∷_)
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 (λ x → Idx.suc (ρ x))
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 ρ x = Expr.var (ρ x)
postulate
_;_ : {Γ Γ' Γ'' : Ctx} → Subst Γ Γ' → Subst Γ' Γ'' → Subst Γ Γ''
-- (σ ; σ') x = subst σ' (σ x)
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 = {!!}
This works as expected in Agda 2.5 and starts failing in 2.6.0.
Bisection points to commit 031c69df6ca2e4ae203a5809df0277c587f4f1a4 @jespercockx
Date: Thu May 31 10:46:49 2018 +0200 [ rewriting ] Make non-linear matching more type-directed
The code has evolved quite a bit, but there is a fishy bit that is still here from the original commit: https://github.com/agda/agda/commit/031c69df6ca2e4ae203a5809df0277c587f4f1a4#r141318594
https://github.com/agda/agda/blob/c7541afeda1cabf4cdc5218fce5d4577ebf5f7af/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs#L349-L353
k
here is the context of variables bound by lambdas in the higher-order pattern. It is represented as a telescope. This feels unusual and is maybe wrong. Telescopes are extended on the left (B --> Sigma A B
) while context are extended on the right (A --> Sigma A B
). When going under a binder, we need to extend on the right, so telescopes seem wrong, and contexts would be right for the bound variables, if I am not mistaken.
The symptom is:
{-# OPTIONS -v rewriting:60 #-}
...
rewrote comp σ (ren ρ) idx
to subst (λ {τ} z → var (ρ τ)) (σ τ)
This is ill-typed, correct would be subst (λ z {τ} → var (ρ z)) (σ idx)
, so it seems that the lambdas are assembled in the wrong order.
telescopes seem wrong, and contexts would be right for the bound variables
PR incoming that implements this, fixing the issue...
Is there a workaround available for this other than reverting to 2.5?
Not sure what exactly you are intending to do, but you could try opaque/unfolding
instead of abstract/REWRITE
(if you want to control the unfolding of substitution composition).
Using Agda v2.6.4.3 and agda-stdlib v2.0, I'm encountering the following error
when trying to typecheck the following:
The problem goes away if I don't use
REWRITE
.(Was recommended to file bug report from chat)