Edwin Brady
Edwin Brady
> I'm not going to defend the design decision 'names which are in scope in a type are also always in > scope in the body of the corresponding definition'...
I wonder if we should also find a way to do record access by dots. I couldn't see how to fix the syntax to support it, but the Haskell people...
The strange behaviour is probably because in `TestStruct`, `ExtraStruct` isn't a pointer. A `Struct` on the Idris side needs to be a pointer to the struct on the C side....
Internally, these exist, but there's no syntax yet. There is a possible complication - implicits might appear in a different order than the lambdas, so perhaps there needs to be...
@gallais It would be nice to do that, yes. I don't think there's any reason not to - I could never make it work in Idris 1 because the design...
The error message is bad, but there are definitely two possible results: one from the first Node, one from the second. There's no guarantee they'd be the same.
I haven't checked if it affects this issue, but recently I found and fixed a problem with 'import public', so maybe this is okay now?
I know some people are keen on this sort of thing (I'm occasionally asked about it). Usually the reasoning is about wanting to make the code look more like the...
Idris 1 works a bit harder to disambiguate, but there should at least be an error message that explains what the ambiguity is.
I've labelled this with "Feature request" - we ought to have them really. If anyone wants pointers on where to start implementing it, please let me know.