Given the program take (A: Type) (f: A -> A): A = f 0 (with dep. to core), the current message is:
error[E032]: expected type `A`, got type `crate.core.nat.Nat`
>>> file.lushui:4:20
|
4 | take (A: Type) (f: A -> A): A = f 0
| - expected due to this
|
>>> file.lushui:4:35
|
4 | take (A: Type) (f: A -> A): A = f 0
| ^ has wrong type
|
error: aborting due to previous error
Which is not bad but I prefer it saying expected type parameter `A`, … and also add a secondary span on the definition site of the parameter like parameter defined here. Also, the phrasing expected due to this does not really work in this context, for my liking. It should be more precise like `f` takes a parameter of type `A` or something like that special-casing pi types here.
Given the program
take (A: Type) (f: A -> A): A = f 0(with dep. tocore), the current message is:Which is not bad but I prefer it saying
expected type parameter `A`, …and also add a secondary span on the definition site of the parameter likeparameter defined here. Also, the phrasingexpected due to thisdoes not really work in this context, for my liking. It should be more precise like`f` takes a parameter of type `A`or something like that special-casing pi types here.