Mismatch between order of matching in clauses and case tree; subject reduction broken

[jespercockx]

While checking a definition by pattern matching, Agda uses left-to-right matching for the previous clauses. After the definition is checked, Agda uses the case tree computed by the coverage checker. Unfortunately, these don't always give the same result. For example, consider the following function:

f : (A : Set) → A → Bool → A ≡ Bool → Bool
f .Bool true true refl = true
f _     _    _    _    = false

The coverage checker will first split on the third argument, then on the fourth, and finally on the second. So when using the standard left-to-right matching, f Bool false x refl computes to false, but the case tree will get stuck on the free variable x instead.

This can be exploited to break subject reduction:

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

record R : Set₁ where
  field
    fun  : (A : Set) → A → Bool → A ≡ Bool → Bool
    rule : ∀ x → fun Bool false x refl ≡ false
open R

test : R
fun test .Bool true true refl = true
fun test _     _    _    _    = false
rule test x = refl

We have that rule test x of type fun Bool false x refl ≡ false computes to refl, but refl is not actually a well-typed term of this type. Indeed, the following fails:

fails : ∀ x → fun test Bool false x refl ≡ false
fails x = refl

Error:

fun test Bool false x refl != false of type Bool
when checking that the expression refl has type
fun test Bool false x refl ≡ false

A very drastic fix would be to only allow left-to-right splitting in the coverage checker, but this would be overly restrictive. A proper fix would probably require interleaving LHS checking, coverage checking, and the construction of the case tree.

Apart from breaking subject reduction, I think this is also worrying because there's no easy way to read the splitting order (and hence the computational meaning) of f from its definition. But this is not the first time we have such a problem. Perhaps we should instead do as Epigram did and record the case tree more explicitly in the definition of a function.

[jespercockx]

Another solution would be to change the matching algorithm used while checking the definition (the one in TypeChecking.Patterns.Match) to be more conservative. In particular, we could replace the current rule

match p v = No
------------------------
match (p:ps) (v:vs) = No

by two rules

match p v = No        match ps vs = Yes sub
-------------------------------------------
match (p:ps) (v:vs) = No

and

match p v = No        match ps vs = No
---------------------------------------
match (p:ps) (v:vs) = No

This would mean we only go to the next clause when all the arguments either match or fail to match (and at least one of them fails). This seems a bit weird at first, but it's really the right thing to do if we want to make matching produce a valid result independent of the splitting order.

I've implemented a basic version of this fix and the test suite seems to pass without problems. Do you think this fix would be acceptable?

[UlfNorell]

I think this makes sense. Before we know what splitting order we'll get in the end the only sensible thing to do is to be conservative. The test suite passing is a good sign.

[andreasabel]

See issue #408.

[Saizan]

Here is something that fails with an internal error at Match.hs:167 :

module _ where

open import Agda.Primitive
open import Relation.Binary.PropositionalEquality

record Category {o h} : Set (lsuc (o ⊔ h)) where
  no-eta-equality
  constructor con
  field
    Obj : Set o
    Hom : Obj → Obj → Set h

  _⇒_ = Hom
  field
    id : ∀ {X : Obj} → Hom X X
    _∘_ : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z
    id-left : ∀ {X Y} (f : Hom X Y) → id ∘ f ≡ f
    id-right : ∀ {X Y} (f : Hom X Y) → f ∘ id ≡ f
    ∘-assoc : ∀ {A B C D} (f : Hom C D) (g : Hom B C) (h : Hom A B)
              → f ∘ (g ∘ h) ≡ (f ∘ g) ∘ h
open Category

record Functor {o1 h1 o2 h2} (C : Category {o1} {h1})(D : Category {o2} {h2})
               : Set (lsuc ((o1 ⊔ h1) ⊔ (o2 ⊔ h2))) where
  no-eta-equality
  constructor con
  private
    module C = Category C
    module D = Category D
  field
    obj      : C .Obj → D .Obj
    hom      : {A B : C .Obj} → (A C.⇒ B) → (obj A) D.⇒ (obj B)
    presId   : {A : C .Obj} → hom (C .id {A}) ≡ D .id {obj A}
    presComp : {A B C : C .Obj} → (f : A C.⇒ B) → (g : B C.⇒ C) →
                 hom (g C.∘ f) ≡ (hom g) D.∘ (hom f)
open Functor

record NaturalTransformation
       {o1 h1 o2 h2} {C : Category {o1} {h1}} {D : Category {o2} {h2}}
       (F G : Functor C D) : Set (h2 ⊔ (h1 ⊔ o1)) where
  constructor con
  private
    module D = Category D
  field
    apply : ∀ {X} → Hom D (F .obj X) (G .obj X)
    natural : ∀ {X Y} (f : Hom C X Y)
              → apply {Y} D.∘ F .hom f ≡ G .hom f D.∘ apply {X}
open NaturalTransformation

Func : ∀ {o1 h1 o2 h2} (C : Category {o1} {h1}) (D : Category {o2} {h2})
       → Category
Func C D .Obj                  = Functor C D
Func C D .Hom                  = NaturalTransformation
Func C D .id {F} .apply        = D .id
Func C D .id .natural f        = trans (D .id-left _) (sym (D .id-right _))
(Func C D ._∘_ f g) .apply     = D ._∘_ (f .apply) (g .apply)
(Func C D ._∘_ f g) .natural h
      = trans (sym (D .∘-assoc _ _ _))
        (trans (cong (D ._∘_ (f .apply)) (g .natural h))
        (trans (D .∘-assoc _ _ _)
        (trans (cong (\ x → D ._∘_ x (g .apply)) (f .natural h))
               (sym (D .∘-assoc _ _ _)))))

Func C D .id-left  f           = { }0
Func C D .id-right f           = { }1
Func C D .∘-assoc f g h        = { }2

[andreasabel]

Did you mean to reopen the issue?

[jespercockx]

Right, when we carelessly continue matching after a failure we may get a comparison between an application and a projection copattern. This shouldn't really count as a mismatch by itself but OTOH it can also never block evaluation of the case tree since these clauses clearly don't belong to the same branch. So maybe it would be fine to return 'No' anyway? I need to do some more thinking...

[andreasabel]

If I understand correctly, we should revert the changes introduced in my patch aeba531 which introduced lazy left-to-right matching. At that time, it fixed #1124. Maybe the preconditions for this bug have been resolved otherwise now.

Currently, some comments in the test file and in Match.hs are no longer accurate. (See the patch.)

[jespercockx]

I tried reverting aeba531 but the original bug of #1124 is still there (now in the form of an __IMPOSSIBLE__ in Reduce.Fast). The original problem there was that we eta-expand terms when matching them against a record constructor, even under uncertain assumptions (i.e. a previous match returned a DontKnow). But we're still doing exactly that, in fact we're now also matching under even more dubious assumptions (when a previous match was No)!

As usual with eta-related problems, the proper solution seems to be to keep track of the types of the things we're matching, and only eta-expand when the type is in fact a record type. Failing that, we could have a simple flag for when we go into speculative/heterogeneous matching mode, and not eta-expand anything when this flag is set.

[jespercockx]

The original problem in this issue is fixed and what remains amounts to "maybe we could implement matching in a nicer way" which is not worth an issue IMHO, so I'm closing this.