def my_id(x:a) -> a given (a, b) = x
> Type error:Ambiguous type variables: [_.1]
def my_id2(x:a) -> a given (a, b:Type) = x
:p my_id2 1.0
> Type error:Ambiguous type variables: [_.2]
now
def my_id(x:a) -> a given (a, b) = x
> Type error:Couldn't infer type of unannotated binder b
def my_id2(x:a) -> a given (a, b:Type) = x
:p my_id2 1.0
> Type error:Couldn't infer implicit argument b of my_id2
>
> :p my_id2 1.0
> ^^^^^^^^^^
These two cases -- unannotated binders and implicit args -- account for most of the inference variables we create, so those were the error messages I focused on. Now that the machinery is in place we can improve the rest of them incrementally as they occur.
Previously:
now
These two cases -- unannotated binders and implicit args -- account for most of the inference variables we create, so those were the error messages I focused on. Now that the machinery is in place we can improve the rest of them incrementally as they occur.