Lack of subject reduction with REWRITE

[GoogleCodeExporter]

module No-subject-reduction where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

{-# BUILTIN REWRITE _≡_ #-}

data Unit : Set where
  unit : Unit

module _ {A B : Set} {f g : A → B} (f≡g : ∀ x → f x ≡ g x) where

  private

    id : Unit → A → B → B
    id unit _ x = x

    f≡g′ : ∀ u x → id u x (f x) ≡ g x
    f≡g′ unit = f≡g

    {-# REWRITE f≡g′ #-}

    ext′ : ∀ u → (λ x → id u x (f x)) ≡ g
    ext′ u = refl

  ext : f ≡ g
  ext = ext′ unit

id₁ : Unit → Unit
id₁ unit = unit

id₂ : Unit → Unit
id₂ unit = unit

id₁≡id₂ : id₁ ≡ id₂
id₁≡id₂ = ext (λ { unit → refl })

-- The normal form of id₁≡id₂ is refl, but refl is not a type-correct
-- term of type id₁ ≡ id₂, so the REWRITE machinery breaks subject
-- reduction:

rejected : id₁ ≡ id₂
rejected = refl

Original issue reported on code.google.com by nils.anders.danielsson on 26 Feb 2015 at 3:03

[GoogleCodeExporter]

The same trick can be used to break normalisation in open contexts:

module _ (p : false ≡ true) where

  block : {A : Set} → Unit → A → A
  block unit x = x

  r : ∀ u → block u false ≡ true
  r unit = p

  {-# REWRITE r #-}

  r′ : ∀ u → block u false ≡ true
  r′ u = refl

  lazy : false ≡ true
  lazy = r′ unit

T : Bool → Set
T true  = Bool
T false = Bool → Bool

module _ (p : false ≡ true) where

  bool : (Bool → Bool) → Bool
  bool = subst T (lazy p)

  fun : Bool → (Bool → Bool)
  fun = subst T (sym (lazy p))

  omega : Bool → Bool
  omega = λ x → fun x x

  loop : Bool
  loop = omega (bool omega)

-- omega = λ p x → x x
-- loop = λ p → <BLACKHOLE>

Original comment by ulf.nor...@gmail.com on 26 Feb 2015 at 4:39

[GoogleCodeExporter]

If I may say so: duh. Rewriting was never meant to be sound, and it is meant for experimentation purposes only (or for situations where you have strong meta-theoretic arguments that the resulting theory is sound, I guess). Breaking strong normalization is very easy:

foo : unit ≡ unit
foo = refl

{-# REWRITE foo #-} 

Breaking subject reduction is not much harder:

Foo : Unit → Set
Foo unit = Unit

Bar : Unit → Unit → Set
Bar unit = Foo

bar : ∀ x y → Bar x y ≡ Unit
bar unit unit = refl

{-# REWRITE bar #-}

test : ∀ x y → Bar x y
test _ _ = unit

works : ∀ x → Foo x
works x = test unit x

To fix this, we would have to implement a confluence checker and a termination checker for the complete set of rewrite rules.

Original comment by jesper.c...@gmail.com on 26 Feb 2015 at 5:08

• Changed state: WontFix

[jespercockx]

We should revisit this test case now that we actually have a confluence checker.