Open fabianhjr opened 4 years ago
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.
@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)
Could the style in https://github.com/edwinb/Idris2/blob/master/libs/base/Data/Nat.idr#L191 work for you?
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)
div : (n, d: a) -> Not (d = Semiring.zero) -> a
Steps to Reproduce
Expected Behavior
Typecheck (Like Idris1)
Observed Behavior
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.