Expected a hidden argument, but found a visible argument in with-abstraction when using REWRITE

[sgodwincs]

Expected a hidden argument, but found a visible argument in with-abstraction when using REWRITE

[andreasabel]

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.

[andreasabel]

Bisection points to commit 031c69d @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: 031c69d#r141318594

agda/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs

Lines 349 to 353 in c7541af

	PLam i p' -> case unEl t of
	Pi a b -> do
	let body = raise 1 v `apply` [Arg i (var 0)]
	k' = ExtendTel a (Abs (absName b) k)
	match r gamma k' (absBody b) (absBody p') body

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.

[andreasabel]

telescopes seem wrong, and contexts would be right for the bound variables

PR incoming that implements this, fixing the issue...

[sgodwincs]

Is there a workaround available for this other than reverting to 2.5?

[andreasabel]

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