Well, yes, printing does not REALLY work in goals...

[UlfNorell]

From andreas....@gmail.com on November 14, 2013 00:28:33

git clone git@github.com:andreasabel/cubical.git -b 0.0.0.2

Load cubical/src/Control/Decoration.agda

Look at the goals. Try to make sense of them...

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

[UlfNorell]

From nils.anders.danielsson on November 14, 2013 02:13:47

$ git clone git@github.com:andreasabel/cubical.git -b 0.0.0.2 [...] Permission denied (publickey). fatal: Could not read from remote repository.

Please make sure you have the correct access rights and the repository exists. $

Status: InfoNeeded

[UlfNorell]

From nils.anders.danielsson on November 14, 2013 02:13:54

Owner: andreas....@gmail.com

[UlfNorell]

From ulf.nor...@gmail.com on November 14, 2013 03:00:06

I had no problems checking it out. Do you have your github account set up properly?

[UlfNorell]

From nils.anders.danielsson on November 14, 2013 06:17:56

You shouldn't need a GitHub account to access a bug report. The following command works for me:

git clone https://github.com/andreasabel/cubical.git -b 0.0.0.2

Status: New

[UlfNorell]

From sanzhi...@gmail.com on November 14, 2013 08:44:03

Indeed, a lot of problems come from projections applied to compound expressions, especially for some infix ones like ~.

A workaround that often helps is declaring the corresponding module in a let or where, so that display forms (I think) turn the application into a dereference from the module.

So I wonder if pretty-printing could do that automatically, putting the module declarations in a let in the type of the goal.

Ideally that'd turn

(.Relation.Binary.Setoid.preorder (setoid (F, (G, (Data.Product.Σ .A (λ v → C))))) .Relation.Binary.Preorder.∼ FunctorOps.map (ops F) (FunctorOps.map (ops G) (, (proj₁ ax))) (FunctorOps.map (ops F) g (f (proj₂ ax)))) (FunctorOps.map (ops F) ((λ {.x} → FunctorOps.map (ops G) (, (proj₁ ax))) ∘ g) (f (proj₂ ax)))

into

let module pre = .Relation.Binary.Preorder (.Relation.Binary.Setoid.preorder (setoid (F, (G, (Data.Product.Σ .A (λ v → C)))))) module opsF = FunctorOps (ops F) module opsG = FunctorOps (ops G) in opsF.map (opsG.map (, (proj₁ ax))) (opsF.map g (f (proj₂ ax)))) pre.~ (opsF.map ((λ {.x} → opsG.map (, (proj₁ ax))) ∘ g) (f (proj₂ ax)))

Which is better imo, and the user might then copy those modules into the source so that their definition doesn't appear in the goals anymore, hopefully.

It's not a very principled approach but since the title was very open ended I thought It could be interesting to mention.

[UlfNorell]

From andreas....@gmail.com on November 14, 2013 16:57:10

What bothers me here is that Agda turns my

map F

into

FunctorOps.map (ops F)

and propositional equality into that monster

(.Relation.Binary.Setoid.preorder (setoid (F, (G, (Data.Product.Σ .A (λ v → C))))) .Relation.Binary.Preorder.∼

and then using ~ infix for the wrong arguments (the last thing is issue 632 ).

For propositional equality there would possibly a fix involving changing the standard library such that \equiv-Reasoning is defined directly and not in terms of more general constructors, like preorder reasoning for setoids.

[UlfNorell]

From andreas....@gmail.com on November 14, 2013 17:04:30

Owner: ---

[UlfNorell]

From ulf.nor...@gmail.com on November 29, 2013 08:47:44

Could you try to construct a small self-contained example of the map issue to make it easier to analyse the problem? Is it related to issue 657 or issue 886 ?

Status: InfoNeeded
Owner: ulf.nor...@gmail.com
Labels: Priority-High