bad error message with copatterns

[UlfNorell]

From Daniel.G...@gmail.com on November 11, 2013 20:01:23

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). The error message one gets when using the wrong projection name is not very good.

{-# OPTIONS --copatterns #-} module Bug where

postulate A : Set

record R : Set where field x : A

record S : Set where field y : A

open R

f : S x f = ?

{- Arguments left we cannot split on. TODO: better error message when checking that the clause x f = ? has type S -} 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=950

[UlfNorell]

From andreas....@gmail.com on November 11, 2013 11:09:00

Labels: Type-Defect Priority-High Milestone-2.3.4 Copatterns ErrorReporting CaseSplitting

[UlfNorell]

From andreas....@gmail.com on November 11, 2013 16:26:01

Fixed. Keep these reports coming!

Tue Nov 12 01:22:52 CET 2013 Andreas Abel andreas.abel@ifi.lmu.de

• [ issue 950 ] Better split error messages for copatterns.

Status: Fixed
Owner: andreas....@gmail.com