New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Order of patterns matters for checking left hand sides #1411

Closed
GoogleCodeExporter opened this Issue Aug 8, 2015 · 3 comments

Comments

Projects
None yet
1 participant
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

open import Common.Prelude
open import Common.Equality

data Fin : Nat → Set where
  fzero : (n : Nat) → Fin (suc n)
  fsuc  : (n : Nat) → (i : Fin n) → Fin (suc n)

data _≅_ {A : Set} (a : A) : {B : Set} (b : B) → Set where
  refl : a ≅ a

postulate
  inj-Fin-≅ : ∀ {n m} {i : Fin n} {j : Fin m} → i ≅ j → n ≡ m

suc-injective : ∀ n m (i : Fin n) (j : Fin m) → fsuc n i ≅ fsuc m j → i 
≅ j
suc-injective n m i j p with inj-Fin-≅ p
suc-injective n .n i j p | refl = {!p!}

-- Splitting of p fails:

-- Refuse to solve heterogeneous constraint i : Fin n =?= j : Fin m
-- when checking that the pattern refl has type fsuc n i ≅ fsuc m j

-- But the type of p is homogeneous:

-- p : fsuc n i ≅ fsuc n j
-- j : Fin n
-- i : Fin n
-- n : Nat

Original issue reported on code.google.com by andreas....@gmail.com on 23 Jan 2015 at 9:58

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

The error is reported when Agda reloads, with clause

  suc-injective n .n i .i refl | refl = ?

The LHS checker splits on the first data constructor, which is refl for het.eq. 
 The unifier complains, and the LHS checker gives up (unlike the coverage 
checker who tries to split on the next constructor).

Seems like the LHS checker was not designed for situations where splitting has 
to occur in a certain order even for a *single clause*.

A possible resign would be that the LHS splitter returns all possible splits 
(maybe lazily), and the LHS checker tries to find the first split that 
satisfies the unifier.  

Original comment by andreas....@gmail.com on 23 Jan 2015 at 2:10

  • Removed labels: Coverage
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Here is a case without with:

{-# OPTIONS -v tc.lhs:10 #-}

open import Common.Prelude
open import Common.Equality

data Fin : Nat → Set where
  fzero : (n : Nat) → Fin (suc n)
  fsuc  : (n : Nat) → (i : Fin n) → Fin (suc n)

data _≅_ {A : Set} (a : A) : {B : Set} (b : B) → Set where
  refl : a ≅ a

works : ∀ n m (i : Fin n) (j : Fin m) → n ≡ m → fsuc n i ≅ fsuc m j 
→ i ≅ j
works n .n i .i refl refl = refl

fails : ∀ n m (i : Fin n) (j : Fin m) → fsuc n i ≅ fsuc m j → n ≡ m 
→ i ≅ j
fails n .n i .i refl refl = refl

-- Refuse to solve heterogeneous constraint i : Fin n =?= j : Fin m
-- when checking that the pattern refl has type fsuc n i ≅ fsuc m j

The order of patterns matters even for the LHS checker, which it should not.

Original comment by andreas....@gmail.com on 23 Jan 2015 at 2:46

  • Changed title: Order of patterns matters for checking left hand sides
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Implemented #1 in patches
https://github.com/agda/agda/commit/7290688799f4d918861210ead1e17536b1393978
https://github.com/agda/agda/commit/47d9e487bfb892769fbe5c3ae4ecaa5611b0c048

Some ranges got worse, see
https://github.com/agda/agda/commit/0c5629c176760259935ccc1799ed44680d2f13fd


Original comment by andreas....@gmail.com on 25 Jan 2015 at 8:30

  • Changed state: Fixed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment