[Agda] Records & dependent pattern matching

[Andreas Abel]

Hi Guillaume,

Agda 2.2.8 compiles matching against record patterns away into using 
projections.  This means that on the l.h.s., you get just a variable 
instead of a record pattern, and on the r.h.s. projections of this 
variable are used instead of the pattern components.

Trying to split on pr in this situation yields an error:

fail2 : ∀ {n : ℕ} (T : CTree (suc n)) → 0Tree (proj₁ T) → ℕ
fail2 T pr = {!pr!}

Cannot pattern match on constructor 0leaf, since the inferred
indices [leaf zero] cannot be unified with the expected indices
[proj₁ T'] for some T', n
when checking that the expression ? has type ℕ

In your situation (fail) the error handling of Agda is not very good: 
it performs the splits but then discovers it is illegal.

What you can do break up the pair in the definition (as you did in 
'success'), or you can use a product type that is a data instead of a 
record.

Cheers,
Andreas

On 12/29/10 3:38 PM, gallais @ EnsL.org wrote:
> Hi all,
>
> I was trying to make my code (written using the 2.2.6) 2.2.8 compatible and
> I faced a problem which (I guess) comes from the way records are treated
> in the last version of Agda.
> Here is a simplified version of my problem:
>
> ===============================================================
>
> module failure where
>
> open import Data.Nat
> open import Data.Fin
> open import Data.Product
>
> -- First: define a datatype for binary trees
> data Tree (n : ℕ) : Set where
>    leaf : ∀ (p : Fin n) → Tree n
>    node : ∀ (T₁ T₂ : Tree n) → Tree n
>
> -- Then: define 2 properties on it
> data Comb {n : ℕ} : Tree n → Set where
>    cleaf : ∀ (p : Fin n) → Comb (leaf p)
>    cnode : ∀ (p : Fin n) (T : Tree n) → Comb T → Comb (node (leaf p) T)
>
> data 0Tree {n : ℕ} : Tree (suc n) → Set where
>    0leaf : 0Tree (leaf zero)
>    0node : ∀ (T₁ T₂ : Tree (suc n)) (pr₁ : 0Tree T₁) (pr₂ : 0Tree T₂) →
> 0Tree (node T₁ T₂)
>
> -- Define the set of Trees that verifies the first property
> CTree : ∀ (n : ℕ) → Set
> CTree n = Σ (Tree n) Comb
>
> -- Try to define a function on Trees that are Combs&  that verifies
> the 0Tree property
> fail : ∀ {n : ℕ} (T : CTree (suc n)) → 0Tree (proj₁ T) → ℕ
> fail (T , HT) pr = {!!}
>
> ===============================================================
>
> When I try to pattern match on pr, agda yields at me!:(
>
> Not supported: Dot patterns inside record patterns, unless
> accompanied by data type patterns
> when checking that the clause fail (.(leaf zero) , HT) 0leaf = ?
> has type {n : ℕ} (T : CTree (suc n)) → 0Tree (proj₁ T) → ℕ
>
> I could, of course, inline everything (see success) and, then, define
> fail as an alias
> of success but... it's kind of ugly, isn't it?
>
> ===============================================================
>
> success : ∀ {n : ℕ} (T : Tree (suc n)) (pr₁ : Comb T) (pr₂ : 0Tree T) → ℕ
> success T pr₁ pr₂ = {!!}
>
> ===============================================================
>
> Is there an elegant way to solve this problem? Is it normal that this
> pattern-matching
> isn't accepted any more?
>
> Cheers,
>
> --
> guillaume
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/