Copatterns do not work in parametrized modules

[UlfNorell]

From Daniel.G...@gmail.com on November 05, 2013 20:22:14

What's the problem? Cut-and-pasted program examples are preferred over attachments (if reasonably short). While playing some more with copatterns I found the following bug. If a record is defined under a module telescope then an internal error occurs if one tries to copattern match in the same module:

{-# OPTIONS --copatterns #-}

module Bug where

module _ (A : Set) where

record Box : Set where constructor box field unbox : A

open Box

postulate x : A

ex : Box ex = box x -- works

{- ex' : Box unbox ex' = x -- doesn't work -- -}

-- uncommenting this definition will cause the following error {- An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Substitute.hs:326 -}

postulate A : Set

ex' : Box A Box.unbox ex' = x A -- works 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=940

[UlfNorell]

From andreas....@gmail.com on November 06, 2013 01:56:52

Labels: Type-Defect Priority-High Milestone-2.3.4 Copatterns Modules

[UlfNorell]

From andreas....@gmail.com on November 06, 2013 05:52:14

Fixed. Again a problem with module free variables, but I am slowly learning how to handle them...

Summary: Copatterns do not work in parametrized modules (was: Defining records under module telescopes breaks copatterns)
Status: Fixed
Owner: andreas....@gmail.com