display forms do not see through definitions

[UlfNorell]

From sanzhi...@gmail.com on August 15, 2013 05:34:08

module Bug where

postulate A : Set I : Set

module R (_ : I) where postulate f : A

postulate r : I X : I -> I Q : A -> Set

module Qualified where K = X r open R K

foo : Q f foo = {!!} -- normal form: Q (R.f (X r))

module UnQualified where

open R (X r)

bar : Q f bar = {!!} -- normal form: Q f

It would be much nicer if foo's goal had the same display form as bar's goal when normalized.

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

[UlfNorell]

From nils.anders.danielsson on August 21, 2013 08:51:14

This problem seems related to issue 657 . See also issue 644 .

Status: Accepted
Labels: Display Type-Defect Priority-Medium

[UlfNorell]

From sanzhi...@gmail.com on November 01, 2013 04:01:49

I got notified of a comment which doesn't appear here, but since it's still marked as fixed I wanted to clarify that the bug is still present with a freshly pulled Agda from the carcs repo.

Except my code example might be misleading, since with both the Qualified and UnQualified module loaded in the same file we get "Q . Bug886 .UnQualified._.f" as the normal form for foo's goal, rather than "Q (R.f (X r))" which is what we get without the UnQualified module present.

[UlfNorell]

From andreas....@gmail.com on November 01, 2013 06:11:04

Ah, I deleted my comment since I had interpreted the report wrongly. I did not see that you need to press C-u C-u C-c C-t to see the unwanted printing of the goal. I misinterpreted my "delete-comment" as "undo", but the status changes were not undone by deleting the comment. So, in fact, the issue is open.

Status: Accepted