Closes #776. Applications with annotation arguments were previously disallowed in implicit equations. This allows calling such functions, including monadic functions with annotation arguments (e.g. applying a "function" of type Maybe<(ResultTy ::= ArgTy; anno::AnnoTy)>).
Documentation
This adds comments in the explaining the code for handling annotations.
This implements the expected behavior, so it does not need any documentation for users.
Changes
Closes #776. Applications with annotation arguments were previously disallowed in implicit equations. This allows calling such functions, including monadic functions with annotation arguments (e.g. applying a "function" of type
Maybe<(ResultTy ::= ArgTy; anno::AnnoTy)>).Documentation
This adds comments in the explaining the code for handling annotations.
This implements the expected behavior, so it does not need any documentation for users.