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

Case splitting emits hidden record patterns that should remain implicit. #635

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

Comments

Projects
None yet
2 participants
@GoogleCodeExporter
Copy link

GoogleCodeExporter commented Aug 8, 2015

On recent Agda:

module Splitting where

record Monoid : Set₁ where
  field
    Carrier : Set
    empty : Carrier
    times : Carrier → Carrier → Carrier
    equal : Carrier → Carrier → Set

record MonoidMorphism (M₁ M₂ : Monoid) : Set where
  constructor monMor
  module M₁ = Monoid M₁
  module M₂ = Monoid M₂
  field
    f : M₁.Carrier → M₂.Carrier
    .identity : M₂.equal (f M₁.empty) M₂.empty

f : ∀ {M₁ M₂ : Monoid} → MonoidMorphism M₁ M₂ → MonoidMorphism 
M₁ M₂
f x = {!x!}

case splitting on x in that hole produces this monstrosity:

f {.Splitting.recCon-NOT-PRINTED Carrier empty times equal} 
{.Splitting.recCon-NOT-PRINTED Carrier₁ empty₁ times₁ equal₁} (monMor f 
identity) = ?


Original issue reported on code.google.com by pumpkingod@gmail.com on 10 May 2012 at 7:34

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

I think there are two issues here, really. The case splitter for some reason 
decides that it needs to provide the implicit arguments as patterns to be able 
to match on monMor (something to do with eta expansion?), which isn't true. And 
second, because there is no way to match on records with no constructors, we're 
getting some weird internal representation of the constructor filled in for 
those implicit patterns.

Original comment by pumpkingod@gmail.com on 14 May 2012 at 2:34

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by nils.anders.danielsson on 21 May 2012 at 12:34

  • Changed state: Accepted
  • Added labels: Type-Defect
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 20 Sep 2012 at 9:36

  • Added labels: Milestone-2.3.2, Pattern-Matching
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by nils.anders.danielsson on 8 Oct 2012 at 4:47

  • Added labels: Priority-High
  • Removed labels: Milestone-2.3.2
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Original comment by andreas....@gmail.com on 19 Oct 2012 at 8:04

  • Added labels: PatternMatching
  • Removed labels: Pattern-Matching
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

In issue 473 eager eta-expansion of implicit patterns of record type was 
introduced.  Maybe that should be done on demand only.

Original comment by andreas....@gmail.com on 29 Oct 2012 at 6:11

  • Added labels: Eta
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Issue 810 has been merged into this issue.

Original comment by andreas....@gmail.com on 4 Mar 2013 at 10:22

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Issue 810 has been merged into this issue.

Original comment by stevan.a...@gmail.com on 5 Mar 2013 at 12:57

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fixed by only eta-expanding implicit patterns of record type with a constructor.
This weakens the fix for issue 473 a bit.  Let's see if this becomes a 
problem...

Original comment by andreas....@gmail.com on 21 Mar 2013 at 10:19

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

The example from Issue 810 still doesn't work (should I open a new issue?):

record Cont : Set₁ where
  constructor _◃_
  field
    Sh  : Set
    Pos : Sh → Set

open Cont

data W (C : Cont) : Set where
  sup : (s : Sh C) (k : Pos C s → W C) → W C

-- If I case split on w:
bogus : {C : Cont} → W C → Set
bogus w = {!!}

-- I get this:
bogus′ : {C : Cont} → W C → Set
bogus′ {Sh ◃ Pos} (sup s k) = {!!}

Original comment by stevan.a...@gmail.com on 22 Mar 2013 at 2:16

@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Well, yes, but it does not crash Agda.  It just makes interactive case 
annoying, because you have to clean up manually.  But this is my experience 
with case-splitting anyway.

To fix this properly, one would have to check wether the expanded record 
pattern contains has introduced variables that are used in later patterns (e.g. 
in dot patterns).  If not, it can be folded back into an implicit pattern. 

Original comment by andreas....@gmail.com on 22 Mar 2013 at 2:44

  • Changed title: Case splitting emits hidden record patterns that should remain implicit.
  • Changed state: Accepted
  • Added labels: Priority-Medium, Type-Enhancement
  • Removed labels: Priority-High, Type-Defect
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

-- This issue is still open and annoying.

open import Common.Prelude renaming (Nat to ℕ; _+_ to _+ℕ_)
open import Common.Product
open import Common.Equality

postulate
  _≤ℕ_ : (n m : ℕ) → Set
  maxℕ : (n m : ℕ) → ℕ

When : (b : Bool) (P : Set) → Set
When true P = P
When false P = ⊤

infix 30 _⊕_
infix 20 _+_
infix 10 _≤_
infix 10 _<_

infixr 4 _,_

mutual

  data Cxt : Set where
    ∘   : Cxt
    _,_ : (Δ : Cxt) (b : Size Δ) → Cxt

  data Var : (Δ : Cxt) → Set where
    vz : ∀{Δ b}             → Var (Δ , b)
    vs : ∀{Δ b} (i : Var Δ) → Var (Δ , b)

  data Base (Δ : Cxt) : Set where
    zero : Base Δ
    ∞    : Base Δ
    var  : Var Δ → Base Δ

  record Size (Δ : Cxt) : Set where
    inductive
    constructor _⊕_
    field h : Base Δ
          n : ℕ

↑ : ∀{Δ} (a : Size Δ) → Size Δ
↑ (h ⊕ n) = h ⊕ suc n

_+_ : ∀{Δ} (a : Size Δ) (m : ℕ) → Size Δ
(h ⊕ n) + m = h ⊕ (n +ℕ m)

_-_ : ∀{Δ} (a : Size Δ) (m : ℕ) → Size Δ
(h ⊕ n) - m = h ⊕ (n ∸ m)

ClosedSize = Size ∘

data _≤_ : (a b : ClosedSize) → Set where
  leZZ : ∀{n m} (p : n ≤ℕ m) → zero ⊕ n ≤ zero ⊕ m
  leZ∞ : ∀{n m}               → zero ⊕ n ≤ ∞ ⊕ m
  le∞∞ : ∀{n m} (p : n ≤ℕ m) → ∞ ⊕ n ≤ ∞ ⊕ m

_<_ : (a b : ClosedSize) → Set
a < b = ↑ a ≤ b

max : (a b : ClosedSize) → ClosedSize
max (zero ⊕ n) (zero ⊕ n') = zero ⊕ maxℕ n n'
max (zero ⊕ n) (∞ ⊕ n') = ∞ ⊕ n'
max (zero ⊕ n) (var () ⊕ n')
max (∞ ⊕ n) (zero ⊕ n') = ∞ ⊕ n
max (∞ ⊕ n) (∞ ⊕ n') =  ∞ ⊕ maxℕ n n'
max (∞ ⊕ n) (var () ⊕ n')
max (var () ⊕ n)

-- Closed size valuation
mutual

  data Val (chk : Bool) : (Δ : Cxt) → Set where
    ∘    : Val chk ∘
    _,_<_∣_ : ∀{Δ} (ξ : Val chk Δ) (a : ClosedSize) b (p : When chk (a < eval ξ b)) → Val chk (Δ , b)

  lookup : ∀{Δ chk} (ξ : Val chk Δ) (x : Var Δ) → ClosedSize
  lookup (ξ , a < b ∣ p) vz     = a
  lookup (ξ , a < b ∣ p) (vs x) = lookup ξ x

  evalBase : ∀{Δ chk} (ξ : Val chk Δ) (a : Base Δ) → ClosedSize
  evalBase ξ zero    = zero ⊕ 0
  evalBase ξ ∞       = ∞ ⊕ 0
  evalBase ξ (var x) = lookup ξ x

  eval : ∀{Δ chk} (ξ : Val chk Δ) (a : Size Δ) → ClosedSize
  eval ξ (h ⊕ n) = evalBase ξ h + n

UVal = Val false  -- unsound valuation
SVal = Val true   -- sound valuation

update : ∀{Δ} (ρ : UVal Δ) (x : Var Δ) (f : ClosedSize → ClosedSize) 
→ UVal Δ
update (ρ , a < b ∣ _) vz     f = ρ , f a < b ∣ _
update (ρ , a < b ∣ _) (vs x) f = update ρ x f , a < b ∣ _

data _≤V_ {chk chk'} : ∀ {Δ} (ρ : Val chk Δ) (ξ : Val chk' Δ) → Set 
where
  ∘  : ∘ ≤V ∘
  _,_ : ∀{Δ} {ρ : Val chk Δ} {ξ : Val chk' Δ} {a a' b p q}
         --  {a a' : ClosedSize}
         -- {b : Size Δ}
         -- {p : When chk (a < eval ρ b)}
         -- {q : When chk' (a' < eval ξ b)}
    (r : ρ ≤V ξ) (s : a ≤ a') → (ρ , a < b ∣ p) ≤V (ξ , a' < b ∣ q)

lemma-str :  ∀ {Δ} (x : Var Δ) {n} {a} {ρ : UVal Δ} {ξ : SVal Δ}
  → (p : ρ ≤V ξ)
  → (q : a < lookup ξ x + n)
  → update ρ x (max (↑ a - n)) ≤V ξ
lemma-str vz     (p , s) q = {!q!}  -- Splitting on q produces a lot of noice
lemma-str (vs x) (p , s) q = {!!}

Original comment by andreas....@gmail.com on 28 May 2015 at 10:25

  • Added labels: CaseSplitting, Priority-High
  • Removed labels: Priority-Medium
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015

Fixed by 
https://github.com/agda/agda/commit/566f5c3028909feb489a275ae5cb5543213f6507.

The expanded implicit record patterns are still there, but not printed after 
case splitting.  It would be nice to get rid of them, as they also pollute the 
context (hence name space).

Possible plan:
- expand implicit record patterns (ImplicitP)
- check LHS
- store LHS in expanded form
- contract implicit record patterns
- store LHS also in contracted form
- check RHS, such that meta variable contexts do not have all these names from 
record patterns
- check coverage in expanded form (needed for unifier)
- start case splitting from expanded form (needed for unifier), but contract 
before printing

The last point is a bit problematic, because variable names in expanded and 
contracted form might refer to different things.

It would be better to only expand when the unifier wants to place a dot pattern 
as part of an implicit record pattern.

Original comment by andreas....@gmail.com on 29 May 2015 at 9:34

  • Changed state: Fixed
@GoogleCodeExporter

This comment has been minimized.

Copy link

GoogleCodeExporter commented Aug 8, 2015


open import Common.Prelude
open import Common.Equality
open import Common.Product

test : (p : Bool × Bool) → proj₁ p ≡ true → Set
test _ e = {!e!}

-- Splitting on e gives
-- test r refl = ?
-- proj₁ r != true of type Bool
-- when checking that the pattern refl has type proj₁ r ≡ true

Original comment by andreas....@gmail.com on 20 Jul 2015 at 3:05

  • Changed state: Accepted
@jespercockx

This comment has been minimized.

Copy link
Contributor

jespercockx commented Jan 6, 2016

Fixed by the new unifier: 9b56c07

@jespercockx jespercockx closed this Jan 6, 2016

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment