[Agda] Records & dependent pattern matching

[gallais at EnsL.org]

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