search

rowandavies / sml-cidre

SML Checker for Intersection and Datasort Refinements (pronounced "cider")
http://www.cs.cmu.edu/~rowan/sorts.html
Other
20 stars 2 forks source link

Maddening non-local errors #3

Closed robsimmons closed 12 years ago

robsimmons commented 12 years ago

https://github.com/robsimmons/l10/tree/bug2

has an error that can be fixed (as Rowan showed) by sort annotations

https://github.com/robsimmons/l10/compare/bug2...bug2-fix

but the workaround that Rob figured out really demonstrates the hideously non-local nature of this bug: a seemingly meaningless addition of the sort distinction between decl and decl_t in syntax.sml caused errors in parse.sml.

https://github.com/robsimmons/l10/compare/bug2...bug2-workaround

The nature of the error messages in the "bug2" branch is evident from a careful reading of bidirectional typechecking, but the reason that this change triggered it whereas "bug2-workaround" did not is mysterious from a user perspective.

robsimmons commented 12 years ago

The only critical changes in bug2-workaround are in syntax.sml, others are just fixing up the type errors (and fixing some other issues that show up downstream, since I wanted the bug2-workaround branch to actually check without errors)

rowandavies commented 12 years ago

Regarding the proposal for a syntax like ([[ Decl.decl ]]) instead of giving the full instantiated sort.

I recall now why I didn't go that way. It's because it doesn't allow you to instantiate the same sort scheme multiple ways and then construct the intersection of the resulting sorts, which sometimes you need to do. E.g., you may need to instantiate the sort scheme for Stream.lazy to:

 (unit -> Decl.decl Stream.front) -> Decl.decl Stream.stream

& (unit -> Decl.class Stream.front) -> Decl.class Stream.stream

Having a construct that's not fully general may wrongly give the impression that you can't do instantiations like this. To make it fully general we'd need to extend it to something like:

([[ Decl.decl, Decl.class ]])

and with multiple sort variables you might have something like:

(_[[ Decl.decl, Decl.class ] [ Decl.class, Decl.declt ]])

I think this could work, but I'd like to think about it some more. The instantiations that happen when reconstructing sorts from pattern-residuals seem to be the hardest case - if we have a solution for those, it should also fix the other issues related to instantiations.