rowandavies / sml-cidre Goto Github PK

This diff:

robsimmons/l10@6925910

goes from no errors to one error in the code, seeming to indicate that projections aren't being handled correctly

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

is a branch that demonstrates this strange bug:

CIDRE: basis construction error:

/Users/rjsimmon/r/l10/sml/check-types.sml:641.9-641.48 Error: 
           Decl.DB (pos, (db, props', hd worlds'))
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Sort mismatch: t
      expecting: decl_t
------------------------------------------------------------------
/Users/rjsimmon/r/l10/sml/check-types.sml:639.23-639.59 Error: 
           val worlds' = #2 (tc_worlds DictX.empty [ world ])
                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Sort mismatch: (t * (symbol * t list)) list
      expecting: (t * (symbol * (term & term_t) list)) list
------------------------------------------------------------------

I just realized that the names of the lexeme constructors are externally visible, so this old syntax change can lead to confusing error messages. Easily fixed, but my working set's stack and queue are both at capacity right now, so I'm putting this here as something soothing to do later.

The grammar in section 7.8 of the thesis includes a "topsort [type]" construct, but it seems this is not legal syntax in the current version of Cidre. Am I right that Cidre only supports "top" refinements (0-ary intersections) for pure datatypes, and specifically that it does not have them for function types?

For example, suppose we begin by defining some function with a restricted domain:

(*[ datasort true = true ]*)

(*[ idTrue <: true -> true ]*)
fun idTrue true = true

Now, I would expect the following code to fail to sort-check,

(*[ bad <: bool ]*)
val bad = idTrue false

and indeed Cidre gives an error:

  val bad = idTrue false
                   ^^^^^
  Sort mismatch: bool
      expecting: true

That makes sense: even though the sort bool is equivalent to the "top" refinement at type bool, we shouldn't be able to give idTrue false (which evaluates to an exception) the top sort due to the value restriction. However, if we had "topsort" at function types, then I would expect a thunked variation of this example to go through:

(*[ okaymaybe <: topsort[unit -> bool] ]*)
val okaymaybe = fn () => idTrue false

This is not (currently!) legal Cidre syntax, though. We could try the following:

(*[ alsobad <: unit -> bool ]*)
val alsobad = fn () => idTrue false

But this won't help (again the checker will complain), because the sort unit -> bool is not actually equivalent to the top refinement at type unit -> bool (and in general, we need not have that topsort[A -> B] = topsort[A] -> topsort[B] in the presence of effects).

Does this sound right? If so, then maybe you could read this as a feature request... ;-)

Truly a "Expected: ?.vector, got: ?.vector" esque error, courtesy of https://github.com/robsimmons/l10/blob/bug6/sml/splitting.sml#L67-70 (which does normal-sml-typecheck). If you can't tell, from the annotation, I played around with this one for awhile, to my increasing disbelief ;-).

CIDRE: basis construction error: 

    /Users/rjsimmon/r/l10/sml/splitting.sml:68.3-68.6 Error: 
        (map (*[ <: (Term.term_t -> t) -> Term.term_t conslist -> t conslist
         ^^^
      Sort mismatch: ('a -> 'b) -> 'a conslist -> 'b conslist & ('a -> 'b) -> 'a list -> 'b list
          expecting: (term_t -> t) -> term_t conslist -> t conslist & (term_t -> t) -> term_t list -> t list

Of course, it results from the interaction of polymorphism abstract types that turn out to be invariant.

The workaround is basically expanding the definition of map (see https://github.com/robsimmons/l10/blob/master/sml/splitting.sml#L67-68), but... seriously? That's what map is there for.

The ARRAY and VECTOR signatures are pretty clearly out of date.

Also, the default refinement of 'a vector isn't covariant when it should be. (But obviously not for 'a array!) The same is probably true for other type constructors that are opaque in the standard basis signatures.

Also, are there any other of the signatures related to "basic" (compiler implemented) types that haven't been properly compared to the standard basis spec?

(*[ datasort true = true ]*)

fun f x = 
   let (*[ val q: true ]*) 
      val (q, _) = (false, 3) 
   in q end

Rowan says the problem here is that it doesn't identify that I need to now be checking against (true * int). Ideally it would know to check against (true * int), but it should at least give a warning.

I've just fixed some bugs that were resulting in abstract sort constructors (and their intersections) in signatures not being assigned the variances implied by what what the signature designates.

In the process I decided that it would be good to double check that the variances of pre-existing sortnames aren't being clobbered. It turns out they can't be, because you can't ever specify sorts that refine a manifest type that was previously opaquely defined.

So, this issue is that CIDRE should support some way of doing this. Perhaps there should be multiple ways, following SML:
a) sharing specs that follow sharing type t1=t2 with (*[ and sortdef s1=s2 and ... ]*)
b) where type sigexps that similarly modify signatures
c) ([* sortdef s1 = s2 ]*) transparent sort specs.

Then it would be natural to support signatures that weaken what's known about the refinements. Alternatively, we could just consider that we have sufficient modularity at the level of types, and automatically propagate sorts along with the type that they refine.

Regardless, if CIDRE does in the future support such things, it would be good to revisit the propagation of variance for abstract sort constructors. Currently this is done by imperatively improving the variance of sortnames that are subsorts of sortnames that have a variance ascribed. If such improvements were done to sortnames that were defined prior to the current signature it would be bad.

Consider:

(*[ datasort true = true ]*)

(*[ f <: true -> true list ]*)
fun f true = [true]

(*[ g <: true -> true ref ]*)
fun g true = ref true

(*[ passes <: true list & bool list ]*)
val passes = f true

(*[ fails <: true ref & bool ref ]*)
val fails = g true

Naturally, the unsafe annotation fails <: true ref & bool ref fails...

  val fails = g true
              ^^^^^^
  Sort mismatch: true ref
      expecting: true ref & bool ref

but I was a bit surprised that the safe annotation passes <: true list & bool list passes the sort-checker, even though the definition of passes syntactically violates the value restriction.

Is there a simple explanation for what exactly Cidre is doing? I guess it probably has something to do with the fact that the sort true list (which can be synthesized for the application f true) is a subsort of true list & bool list, but the sort true ref is not a subsort of true ref & bool ref?

I meant to write sml/refine.mlb, the file sml/refine.cm doesn't exist. This probably shouldn't throw me back to my shell, however.

bash-3.2$ ../sml-cidre/bin/sml-cidre sml/refine.sml
Standard ML of New Jersey 110.72
with SML-CIDRE 0.99999

Quickstart:   Cidre.make "filenm.cm";

val it = "a piece of" : string
- Cidre.make "sml/refine.cm";
Error: file not found: sml/refine.cm
bash-3.2$

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.

I already annotate code that I expect to fail in libraries, it would be nice if CIDRE would suppress these errors where requested.

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

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

robsimmons/l10@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.

robsimmons/l10@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.

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

Causes Crash to be raised. Not a clue.

bash-3.2$ ../sml-cidre/bin/sml-cidre
Standard ML of New Jersey 110.72
with SML-CIDRE 0.99999

Quickstart:   Cidre.make "filenm.cm";

val it = "a piece of" : string
- Cidre.check "sml/refine.mlb";
CIDRE: MLB sml/refine.mlb 
..snip..
check-types.sml checked in 0.703s
Impossible: RefDec.patSort_to_Sorts(2): 
applying:  t * t stream -> t front
    to:  decl_t * decl_t stream
patSort: SORTps(decl_t * decl_t stream)

Elab
             non-gc         system             gc      wallclock
              0.003          0.000          0.000          0.003

uncaught exception CRASH
  raised at: ../sml-cidre/src/Common/Crash.sml:11.8-11.13
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../sml-cidre/src/Common/Comp.sml:68.47
             ../Manager/ParseElab.sml:182.80
             ../Manager/ParseElab.sml:189.54
             ../Cidre/Cidre.sml:220.63-220.65
             ../Cidre/Cidre.sml:302.64