search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

bad interaction with copattern and modules #937

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From Daniel.G...@gmail.com on November 04, 2013 15:10:23

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

open import Data.Nat open import Data.Product

ex : Σ ℕ (λ n → 0 < n) proj₁ ex = 1 proj₂ ex = s≤s z≤n -- works

ex' : Σ ℕ (λ n → 0 < n) proj₁ ex' = 1 proj₂ ex' = ? -- works as expected

module { : Set} where ex'' : Σ ℕ (λ n → 0 < n) proj₁ ex'' = 1 proj₂ ex'' = s≤s z≤n -- works

ex''' : Σ ℕ (λ n → 0 < n) proj₁ ex''' = 1 proj₂ ex''' = ? -- does not work, -- when reducing the goal shows: 1 ≤ proj₁ ex'''

This program works, but if one replaces the second equation with a hole then Agda will not accept this term as an solution. Furthermore when one checks the goal of this hole proj₁ ex', will not reduce to 1. This happens when the definition is under a module with a telescope (even if the binders in the telescope are not used as in the example). What version of Agda are you using? On what operating system (if relevant)? Latest darcs

Original issue: http://code.google.com/p/agda/issues/detail?id=937

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 04, 2013 09:23:56

I am looking into this. My fix for issue 907 seems to be incomplete.

Owner: andreas....@gmail.com
Labels: Type-Defect Priority-High Copatterns

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 04, 2013 09:40:52

Funny. If I type (0 < proj₁ ex''') into the goal and normalize it, I get the expected 1 <= 1.

Labels: Meta Interaction

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 04, 2013 17:20:11

Fixed. In Split.hs, splitting on copattern did not apply the function symbol (here: ex''') to the free variables of the section (here: {_}), breaking reduction. The reason that ex'' did work was due to another bug, which cancelled with this first one: clauses added temporarily were not lifted to the toplevel (out of the module telescope).

That was a long hunt...

Status: Fixed

UlfNorell commented 10 years ago

From andreas....@gmail.com on November 05, 2013 03:15:11

A similar problem was in the coverage checker (and it also needs to reduce with the clauses!).

T : (b : Bool) → Set T true = Nat T false = Bool → Nat

test : Σ Bool T proj₁ test = false proj₂ test true = zero proj₂ test false = suc zero -- Error: unreachable clause

This is fixed now.

Labels: -Meta -Interaction PatternMatching Coverage