Local rewrite matches and smart with

[NathanielB123]

WORK IN PROGRESS!

Todos:

• Fix bugs
• Stress test --smart-with, --without-K more (we reject the examples I have come up with so far, but it wouldn't surprise me if there are ways to get around this...)
• Throw an error (or warning?) when we use the inspect idiom (with ... in eq) as --smart-with makes it redundant
• Better error messages
• Investigate mysterious loop in my NbE for type theory in type theory example
• Fix (and re-enable) display forms for with functions

[NathanielB123]

While working on the normalisation proof (trying to figure out how to encode pi-typed values), I thought of a counter-example to my neutral LHS and no overlaps condition:

{-# OPTIONS --smart-with #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

foo : (f : Nat → Nat → Nat) (x : Nat) → f x ≡ (λ y → f y y) → f x x ≡ 42
foo f x p rewrite p = refl

I think this demonstrates that allowing closures on the RHS of rewrites doesn't really work. Not exactly sure how I want to encode the restriction (or how it will look when translated to Agda), but in principle we could inspect the normal form of the RHS, looking for any occurrence of lam not guarded by a stuck elimination rule (i.e. we also need to rule out inl (λ ... → ...), but I think map (λ ... → ...) xs, stuck on xs, is fine).

In the NbE proof, this would mean that pi-typed values would only need to quantify over variable-thinnings (i.e. we can introduce new variables into the context, but not new convertibility assumptions).

[NathanielB123]

I have now implemented the above-described check (currently noClosures in Rewriting.hs). I think this shouldn't be too restrictive in practice, but we shall see...

[NathanielB123]

Ouch, there is a similar counter-example which I don't yet prevent, using copatterns:

{-# OPTIONS --smart-with #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

record Weird : Set where
  no-eta-equality
  constructor mk
  field
    app : Nat → Nat
open Weird

wah : (f : Nat → Weird) → Weird
wah f .app x = f x .app x

foo : (f : Nat → Weird) (x : Nat) → f x ≡ wah f → f x .app x ≡ 42
foo f x p rewrite p = refl

I am not immediately sure what the fix here should be. I need to think about how copatterns should work in NbE.

EDIT: I think it makes sense to reject this example because all underapplied applications (in this case wah f) are basically closures. It's pretty-much identical to

{-# OPTIONS --smart-with #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data Unit : Set where
  ⟨⟩ : Unit

wah : (Nat → Unit → Nat → Nat) → Unit → Nat → Nat
wah f ⟨⟩ y = f y ⟨⟩ y

foo : (f : Nat → Unit → Nat → Nat) (x : Nat) → f x ≡ wah f → f x ⟨⟩ x ≡ 42
foo f x p rewrite p = refl

[NathanielB123]

Yet another counter-example:

{-# OPTIONS --smart-with #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Agda.Builtin.Nat

data ⊥ : Set where

data Branch : Set where
  branch : (Nat → Branch) → Branch

rec : Branch → ⊥
rec (branch f) = rec (f 0)

foo : (f : Nat → Branch) (bad : ⊥) → f 0 ≡ branch f → rec (f 0) ≡ bad
foo f bad p rewrite p = refl

I think this demonstrates that all pi-typed terms should be considered closures (which is perhaps not so surprising).

It's interesting to consider that this example is still problematic without eta for functions though. If we try to apply the NbE proof to a type theory with rewriting but without eta for functions, we find that we can no longer interpret rec, because rec on branch f where f is neutral really relies on neutrals being closed under application (i.e. f being neutral implies rec (f 0) is neutral). In the presence of rewrites, this no longer holds (f 0 is merely pre-neutral, so we need to try and rewrite it before applying rec).

Luckily, Agda has eta for functions, so the much more obvious route is to just consider f to be a closure and reject the rewrite.

[NathanielB123]

    loop block t (rew:rews) es
     | let n = rewArity rew, length es >= n = do
...
     | otherwise = loop (block `mappend` NotBlocked Underapplied ()) t rews es

This is... not ideal

[NathanielB123]

Btw, for --smart-with this to work properly with cubical (e.g. allow with abstracting after interval abstractions, properly reconstructing the boundary), we need to support Path types with @rewrites in their codomain. This is a little scary (a lot of the prior local rewrite rule infrastructure assumed @rewrite could only occur prenex in iterated pi-types.

[NathanielB123]

Another edge case.....

{-# OPTIONS --smart-with #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

data ⊥ : Set where

data Foo : Set
record Bar : Set

data Foo where
  b : Bar → Foo

record Bar where
  inductive
  no-eta-equality
  field
    app : Nat → Foo
open Bar

rec : Foo → ⊥
rec (b f) = rec (f .app 0)


ohNo : (x : Bar) → x .app 0 ≡ b x → Nat
ohNo x p rewrite p = {!!}

Projections are considered size-preserving...

My current thinking:

• For eta-equality records, not catching this is definitely a bug (we need to eta-expand)
• For no-eta records, in NbE with rewriting, it doesnt really make sense for projections to preserve size.
  • We could do some hack like considering all elements of inductive record types as potential closures, but this feels pretty overkill.
  • We could modify the termination checker with --smart-with enabled, but this is the sort of edge-case that will be awful to maintain into the future and also this would force --smart-with to be coinfective to retain termination guaranteees
  • We could maybe try to fix this a different way: perhaps generalise the occurs check on the RHS to consider x .app 0 occuring in b x. i.e. rather than the full LHS occuring, we check for the LHS with all inductive projections and applications stripped off (mirroring the rule in the termination checker). Intuitively, this seems like a nice direction but I'm not sure how to justify such a strategy from the perspective of NbE modulo rewriting

[NathanielB123]

Ok I think there is a much simpler strategy actually.
In x .app 0 ~> b x, we should actually consider x to be a closure, because it is underapplied (due to the rewrite rule itself). In practice, we can account for this by checking for closures under a rewrite rule from the LHS to a fresh variable (i.e. x .app 0 ~> fresh)