We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
A function foo
foo
foo {A} (value : A) {maybeValue : Maybe Nat := nothing} : Nat := 123;
using default arguments compiles, whereas a function bar
bar
trait type SomeTrait A := mkSomeTrait {baz : A -> Nat}; bar {A} {{SomeTrait A}} (value : A) {maybeValue : Maybe Nat := nothing} : Nat := 123;
requiring SomeTrait does not compile and throws an error
SomeTrait
error: The expression nothing {_} has type: Maybe _ but is expected to have type: A
The text was updated successfully, but these errors were encountered:
I've fixed it in #2998.
Before the next release, one can workaround this problem by giving a name to the trait argument. E.g.
bar {A} {{dummy : SomeTrait A}} (value : A) {maybeValue : Maybe Nat := nothing} : Nat := 123;
Sorry, something went wrong.
e45503a
Successfully merging a pull request may close this issue.
A function
foo
using default arguments compiles, whereas a function
bar
requiring
SomeTrait
does not compile and throws an errorThe text was updated successfully, but these errors were encountered: