%hide not hiding specifications?

[nicolabotta]

The code

> module Algebra

> %default total

> %hide Semigroup
> %hide (<+>)

> class Semigroup t where  
>   (<+>) : t -> t -> t 
>   associative : {a, b, c : t} -> a <+> (b <+> c) = (a <+> b) <+> c

does not type check:

- + Errors (1)
 `-- (no file) line 0 col -1:
     FoldableProperties.lidr:8:7:Algebra.<+> already defined

Am I doing something wrong? How can I hide the prelude declaration of (<+>)?

On a side track: why do the prelude type classes Semigroup and Monoid not require associativity of (<+>) and neutrality of neutral?

[ahmadsalim]

I think this should work, so I think this is a confirmed bug.

[ahmadsalim]

With regards to the proofs of associativity and neutrality, I believe that there was some discussion that it might be hard in practice to prove this for many monoids with propositional equality, and so someone recommended to have Verified* versions instead. I can't remember exactly what happened for the rest.

[nicolabotta]

With regards to the proofs of associativity and neutrality, I believe that there was some discussion that it might be hard in practice to prove this for many monoids with propositional equality, and so someone recommended to have Verified* versions instead. I can't remember exactly what happened for the rest.

I understand the difficulties, but I think that instead of calling Monoid something that does not need to be a monoid (and VerifiedMonoid something that is just a monoid) it would be better to call monoids Monoid and things that do not need to be monoids something else. Idris is one of the few languages that allow programmers to encode precise notions as data types. Let's use it to call things as they are!

[ahmadsalim]

@nicolabotta I was unfortunately not a decision maker in that library design idea, and so I am only reenumerating what I was told :).