idris-lang
`typebind` operators seems to have too narrow translation
Pinging @andrevidela as probably the only implementor of the feature
Steps to Reproduce
Consider a couple of non-standard typebind operators op and op' and their non-typebind equivalents po and po'. They have different types on the first argument and in the input type of a function in the second argument.
import Data.Nat
%default total
export infix 0 `po`, `po'`
export typebind infixr 0 `op`, `op'`
op, po : (mty : Type) -> (ty -> Type) -> Type
g : Maybe Nat `po` \res => 5 `LT` res
f : (res : Maybe Nat) `op` (5 `LT` res)
op', po' : (mty : Type) -> (mty = Maybe ty) => (ty -> Type) -> Type
g' : Maybe Nat `po'` \res => 5 `LT` res
f' : (res : Maybe Nat) `op'` (5 `LT` res)
Expected Behavior
I'd expect all examples, especially, pairs of op and po, and op' and po', to work in the same way.
Observed Behavior
Error: While processing type of f. When unifying:
Maybe Nat
and:
Nat
Mismatch between: Maybe Nat and Nat.
BadTypeBind:12:36--12:39
08 |
09 | op, po : (mty : Type) -> (ty -> Type) -> Type
10 |
11 | g : Maybe Nat `po` \res => 5 `LT` res
12 | f : (res : Maybe Nat) `op` (5 `LT` res)
^^^
Error: While processing type of f'. When unifying:
Maybe Nat
and:
Nat
Mismatch between: Maybe Nat and Nat.
BadTypeBind:17:6--17:42
13 |
14 | op', po' : (mty : Type) -> (mty = Maybe ty) => (ty -> Type) -> Type
15 |
16 | g' : Maybe Nat `po'` \res => 5 `LT` res
17 | f' : (res : Maybe Nat) `op'` (5 `LT` res)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Analysis
Well, strictly speaking, accoring to the documentation, this is expected behaviour, since (name : type) `op` expr goes to type `op` (\name : type => expr), i.e. the type of the lambda argument is also filled.
I feel that the correct translation is to have no type ascription in the lambda (i.e. to have _ or ? there), since if they must be the same, it will be derived from the signature of op, but if they are not the same by the signature of op, it still should work.
BTW, small very related question is why only infixr are allowed for typebind operators? I think, the just infix should be supported too.
Yeah this is expected behaviour. The error message should be better.
In this case we can detect the problem as we are defining op since the syntax extension is already in scope. Something like:
error: Inappropriate type for typebind operator
08 |
09 | op, po : (mty : Type) -> (ty -> Type) -> Type
10 | ^^^ ^^
Typebind operators require the second argument to depend
on the first. If that is not the case, consider using
autobind instead. Possible solutions:
- declare the operator as "export autobind infixr 0 `op`"
- make the second argument depend on the first: "op : (mty : Type) -> (mty -> Type) -> Type"
However, I've not taken the time to implement it because doing it this way is brittle. It does not work across modules and making it an error would prevent the valid use of the function using normal function application op a b as well as other valid overloads of op. I'm hoping someone can come up with a better idea.
why only infixr are allowed for typebind operators?
To mimic pi-syntax as much as possible. Currently -> behave close to (but not exactly like) infixr -2 ->. This is an artificial limitation and it will be lifted the day someone write a DSL for a library but is stopped by this limitation from completing it.
