Skip to content
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

Rewriting/NonLinMatch.hs:192:9-54: Irrefutable pattern failed for pattern (Just (_, ct)) #3211

Closed
andreasabel opened this issue Sep 4, 2018 · 15 comments

Comments

@andreasabel
Copy link
Contributor

@andreasabel andreasabel commented Sep 4, 2018

Just got this error:

src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:192:9-54: Irrefutable pattern failed for pattern (Just (_, ct))

Here is a shrunk test case:

{-# OPTIONS --rewriting #-}

module _ (Form : Set) where

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

data Cxt : Set where
  _∙_ : (Γ : Cxt) (A : Form)  Cxt

data _≤_ : (Γ Δ : Cxt) → Set where
  id≤ : {Γ}  Γ ≤ Γ
  lift : {A Γ Δ} (τ : Γ ≤ Δ)  (Γ ∙ A) ≤ (Δ ∙ A)

postulate
  lift-id≤ : {Γ A}  lift id≤ ≡ id≤ {Γ ∙ A}

{-# REWRITE lift-id≤ #-}

Works fine in Agda-2.5.4.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Sep 5, 2018

It seems the problem occurs when the head symbol of a rewrite rule is the constructor of a parametrized datatype: the type is not applied to its parameters. Since rewriting is now type-directed, this becomes a problem. I'm not sure if it would be safe to just drop the parameters though, perhaps it would be better to reconstruct them and make them part of the pattern. But then we would also have to reconstruct them when actually applying the rewrite rule...

Is there actually a compelling use case for adding rewrite rules to a constructor? So far it was allowed since it didn't take any extra effort, but it seems with type-directed rewriting that's no longer the case.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Sep 5, 2018

Fixed by applying the type of the constructor to the parameters when adding the rewrite rule. This may create some weird effects in corner cases, for example adding a rewrite rule for [] of type List Bool will actually fire for [] at any type List A, but other than that I don't see anything serious that could go wrong.

@andreasabel

This comment has been minimized.

Copy link
Contributor Author

@andreasabel andreasabel commented Sep 5, 2018

Is there actually a compelling use case for adding rewrite rules to a constructor?

Well, I use it for a poor man's version of non-free datatypes. I found it convenient for OPEs, but one could also have a poor man's version of the integers like that.

@nad

This comment has been minimized.

Copy link
Contributor

@nad nad commented Sep 6, 2018

This may create some weird effects in corner cases

If you decide to go ahead with this, then I think it should be documented.

Is it impossible to rule out the weird cases?

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Sep 6, 2018

Well, rewriting in general is not really documented anywhere. I should really get around to that sometime.

To rule out the weird cases, we would have to reconstruct the constructor's parameters before applying the rewrite rule, which is problematic because reduce doesn't take a type. So no, I don't think it is possible to rule out these weird cases (unless we rule out constructors as head symbols altogether).

@nad

This comment has been minimized.

Copy link
Contributor

@nad nad commented Sep 6, 2018

Can't you raise an error when problematic rules are declared? A rule for [] : List Bool might not be OK, but perhaps ∀ {a} {A : List a} → [] {A = A} ≡ <whatever> is.

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Sep 6, 2018

Hm, I guess we could reconstruct the parameters when adding the rewrite rule, and refuse the rule unless all of the parameters are variables.

@jespercockx jespercockx reopened this Sep 6, 2018
@nad

This comment has been minimized.

Copy link
Contributor

@nad nad commented Sep 6, 2018

Distinct variables? What about the variables' types?

@andreasabel

This comment has been minimized.

Copy link
Contributor Author

@andreasabel andreasabel commented Sep 7, 2018

I am afraid the original issue isn't really fixed, at least when this rewrite rule is considered for firing, Agda still crashes:

{-# OPTIONS --rewriting #-}

module _ (Form : Set) where

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

data Cxt : Set where
  _∙_ : (Γ : Cxt) (A : Form)  Cxt

data _≤_ : (Γ Δ : Cxt) → Set where
  id≤ : {Γ}  Γ ≤ Γ
  lift : {A Γ Δ} (τ : Γ ≤ Δ)  (Γ ∙ A) ≤ (Δ ∙ A)

postulate
  lift-id≤ : {Γ A}  lift id≤ ≡ id≤ {Γ ∙ A}

{-# REWRITE lift-id≤ #-}

_•_ : {Γ Δ Φ} (τ : Γ ≤ Δ) (σ : Δ ≤ Φ)  Γ ≤ Φ
id≤ • σ = σ
lift τ • id≤ = lift τ
lift τ • lift σ = lift (τ • σ)

yields:

src/full/Agda/TypeChecking/Rewriting.hs:349:9-20: Irrefutable pattern failed for pattern Def f []
@andreasabel

This comment has been minimized.

Copy link
Contributor Author

@andreasabel andreasabel commented Sep 8, 2018

Next crash:

{-# OPTIONS --rewriting #-}

module _ (Base : Set) where

open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-}

cong :  {a b} {A : Set a} {B : Set b}
       (f : A  B) {x y}  x ≡ y  f x ≡ f y
cong f refl = refl

data Form : Set where
  Atom : (P : Base)  Form
  _⇒_ : (A B : Form)  Form

data Cxt : Set where
  ε : Cxt
  _∙_ : (Γ : Cxt) (A : Form)  Cxt

infixl 4 _∙_
infix 3 _≤_

data _≤_ : (Γ Δ : Cxt) → Set where
  id≤ : {Γ}  Γ ≤ Γ
  weak : {A Γ Δ} (τ : Γ ≤ Δ)  Γ ∙ A ≤ Δ
  lift : {A Γ Δ} (τ : Γ ≤ Δ)  Γ ∙ A ≤ Δ ∙ A

postulate lift-id≤ : {Γ A}  lift id≤ ≡ id≤ {Γ ∙ A}
{-# REWRITE lift-id≤ #-}

Mon : (P : Cxt  Set)  Set
Mon P = {Γ Δ} (τ : Γ ≤ Δ)  P Δ  P Γ

infix 2 _⊢_

data _⊢_ (Γ : Cxt) : (A : Form) → Set where
  impI   : {A B} (t : Γ ∙ A ⊢ B)  Γ ⊢ A ⇒ B

Tm = λ A Γ  Γ ⊢ A

monD : {A}  Mon (Tm A)
-- monD : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Tm A Δ → Tm A Γ  -- Works
-- monD : ∀{A Γ Δ} (τ : Γ ≤ Δ) → Δ ⊢ A → Γ ⊢ A    -- Works
monD τ (impI t)    = impI (monD (lift τ) t)

monD-id : {Γ A} (t : Γ ⊢ A)  monD id≤ t ≡ t
monD-id (impI t) = cong impI (monD-id t)  -- REWRITE lift-id≤

-- -}

Error:

src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:388:17-80: Irrefutable pattern failed for pattern Just (_,
                                                                    ct)

Debugging:

OPTIONS -v rewriting.match:90

show the ill-typed match problem which leads to the crash:

matching  (id≤ Γ)   with    id≤  of type  Cxt

The type Cxt is the wrong one.

@andreasabel andreasabel self-assigned this Sep 8, 2018
andreasabel added a commit that referenced this issue Sep 8, 2018
@andreasabel

This comment has been minimized.

Copy link
Contributor Author

@andreasabel andreasabel commented Sep 8, 2018

Still broken for opening of parametrized module:

{-# OPTIONS --rewriting #-}

module _ (Base : Set) where

open import Agda.Builtin.Equality public
{-# BUILTIN REWRITE _≡_ #-}

cong :  {a b} {A : Set a} {B : Set b}
       (f : A  B) {x y}  x ≡ y  f x ≡ f y
cong f refl = refl

module Formulas (Base : Set) where

  data Form : Set where
    Atom : (P : Base)  Form
    _⇒_ : (A B : Form)  Form

  data Cxt : Set where
    ε : Cxt
    _∙_ : (Γ : Cxt) (A : Form)  Cxt

  infixl 4 _∙_
  infix 3 _≤_

  data _≤_ : (Γ Δ : Cxt) → Set where
    id≤ : {Γ}  Γ ≤ Γ
    lift : {A Γ Δ} (τ : Γ ≤ Δ)  Γ ∙ A ≤ Δ ∙ A

  postulate lift-id≤ : {Γ A}  lift id≤ ≡ id≤ {Γ ∙ A}
  {-# REWRITE lift-id≤ #-}

  Mon : (P : Cxt  Set)  Set
  Mon P = {Γ Δ} (τ : Γ ≤ Δ)  P Δ  P Γ

open Formulas Base 

infix 2 _⊢_

data _⊢_ (Γ : Cxt) : (A : Form) → Set where

  impI   : {A B} (t : Γ ∙ A ⊢ B)  Γ ⊢ A ⇒ B

Tm = λ A Γ  Γ ⊢ A

monD : {A}  Mon (Tm A)
monD τ (impI t)    = impI (monD (lift τ) t)

monD-id : {Γ A} (t : Γ ⊢ A)  monD id≤ t ≡ t
monD-id (impI t) = cong impI (monD-id t)  -- REWRITE lift-id≤

(Same error.)

jespercockx added a commit that referenced this issue Oct 9, 2018
@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Oct 9, 2018

I implemented the check that @nad suggested (checking generality+linearity of the parameters before throwing them away). However, now the last two examples of @andreasabel are rejected without throwing an internal error, and I cannot reconstruct a good test case. Could you take a look if you can reconstruct the internal error?

@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented Nov 15, 2018

Closing due to a lack of response.

@jespercockx jespercockx added this to the 2.6.1 milestone Mar 16, 2019
@andreasabel andreasabel modified the milestones: 2.6.1, 2.6.0 Mar 16, 2019
@andreasabel

This comment has been minimized.

Copy link
Contributor Author

@andreasabel andreasabel commented Mar 16, 2019

I tried to fix this using constructor parameter construction in rewrite rules and during matching of rewrite rules. However, when we initially call try to rewrite a constructor expression, we have no way to reconstruct the parameters, as we are not given the type of this expression.

Thus, constructor rewriting defined and used in parametrized modules will not be supported in Agda-2.6.0.

andreasabel added a commit that referenced this issue Mar 16, 2019
@jespercockx

This comment has been minimized.

Copy link
Member

@jespercockx jespercockx commented May 31, 2019

Since the original internal error is fixed, I'm closing this issue and opening a new one for rewriting of constructors of parametrized datatypes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.