Spurious coverage error in normal ML checking (cmlib v0.4.0)

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

Spurious coverage error in normal ML checking (cmlib v0.4.0) #10

Open robsimmons opened 12 years ago

robsimmons commented 12 years ago

Ironically, I think it's in your code (pqueue-lazy-paring.sml).

- Cidre.make "/Users/rjsimmon/.smackage/lib/cmlib/v0.4.0/cmlib.mlb";

gives me two warnings - one of them is where I'd added a nonexhaustive match ignore annotation (see issue #9), but the other, in pqueue-lazy-pairing.sml, doesn't seem to be noticed by MLton when it's checking the same file and doesn't make much sense to me in either case.

robsimmons commented 12 years ago

Bizarrely, SML/NJ also warns about this file (MLton does not), so it may be an imprecision in the definition instead of an outright bug.