Deep pattern matching fails for sized binary trees

[GoogleCodeExporter]

What's the problem? Cut-and-pasted program examples are preferred over
attachments (if reasonably short).

open import Size

data BTree : {i : Size} → Set where
  leaf : ∀ {i} → BTree {↑ i}
  node : ∀ {i} → BTree {i} → BTree {i} → BTree {↑ i}

deepId : ∀ {i} → BTree {i} → BTree {i}
deepId (node leaf leaf) = node leaf leaf
...

Agda complains that

i' != i of type Size
when checking that the pattern leaf has type BTree {↑ i}

However, this is not the intended behavior of pattern matching with sized types.

What version of Agda are you using? On what operating system (if relevant)?

recent darcs version (Aug 2010)

Original issue reported on code.google.com by andreas....@gmail.com on 20 Aug 2010 at 3:44

Attachments:

• SizedBTree.agda

[GoogleCodeExporter]

Original comment by nils.anders.danielsson on 22 Aug 2010 at 8:01

• Added labels: Priority-Medium, Type-Defect

[GoogleCodeExporter]

Fixed by making the size successor injective, if option --sized-types is 
enabled.

Original comment by andreas....@gmail.com on 1 Sep 2010 at 12:42

• Changed state: Fixed

[GoogleCodeExporter]

There are still problems...

-- with explicit ∞ annotation, it works
works : ∀ {i} → BTree {i} → BTree
works (node (node t1 t2) t3) = node (works t1) (node {∞} t2 t3)
works t = t

-- otherwise, fails
fails : ∀ {i} → BTree {i} → BTree
fails (node (node t1 t2) t3) = node (fails t1) (node t2 t3)
fails t = t

Original comment by andreas....@gmail.com on 14 Feb 2012 at 11:53

• Changed state: Accepted
• Added labels: Sized-Types

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 14 Feb 2012 at 11:57

Attachments:

• Issue298b.agda

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 14 Feb 2012 at 1:25

• Changed state: Fixed

[GoogleCodeExporter]

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

• Added labels: SizedTypes
• Removed labels: Sized-Types