Overlapping implementation again

[nicolabotta]

The program

> %default total
> %auto_implicits off
> %access public export

> postulate Real    : Type 
> postulate plus    : Real -> Real -> Real
> postulate mult    : Real -> Real -> Real
> postulate fromNat : Nat -> Real

> implementation Num Real where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

fails to type check with

- + Errors (1)
 `-- ./Testing/implementation1.lidr line 10 col 17:
     Overlapping implementation: Num Integer already defined

which seems an Idris error. Most likely related to #4279 but here in a perhaps more obvious form. Why is it still so difficult to use interfaces? Is there something obviously wrong with the example above? Is the error message is perhaps misleading?

[ahmadsalim]

@nicolabotta This does seem strange indeed. At least the error message is wrong.

I would assume that you can only define interfaces on concrete type constructors, and not postulates.

[nicolabotta]

@ahmadsalim Defining interfaces in terms of postulated features should be fine as long as these features are not accessed at run time. Notiuce that replacing

> implementation Num Real where

with

> implementation [Lala] Num Real where

makes the code type check. Thus, this seems to be just an Idris bug, not a problem with postulates!