Implicits in Interface Functions cause Typecheck Error

[fabianhjr]

Steps to Reproduce

module Test

interface Foo a where
  bar : a -> {auto ok: ()} -> a 

Expected Behavior

Typecheck (Like Idris1)

Observed Behavior

1/1: Building Test (Test.idr)
Test.idr:4:3--5:1:While processing left hand side of bar at Test.idr:4:3--5:1:
ok is not a valid implicit argument in bar

Edit: maybe related to #8, however I couldn't change it to a constraint as a workaround since I was restricting the domain of a division to nonzero elements.

[rgrover]

The following rewrite doesn't give a type error:

module Foo

interface Foo a where
  bar : {auto ok: ()} -> a -> a

perhaps the implicit argument needs to be the first.

[fabianhjr]

@rgrover, the issue is that I was working on div/mod and wanted to remove the ring's zero:

div : (n, d: a) -> {auto ok: d `NEQ` Semiring.zero} -> a

(I did check the issue #8 with the constraint workaround suggestion)

[rgrover]

Could the style in https://github.com/edwinb/Idris2/blob/master/libs/base/Data/Nat.idr#L191 work for you?

[fabianhjr]

Well, it would typecheck but so would any usages of div that didn't verify that they weren't dividing by zero. (Or ask for such a proof explicitly when it could attempt to derive it)

[rgrover]

div : (n, d: a) -> Not (d = Semiring.zero) -> a