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

No error for bad sorts in tuple patterns #7

Open robsimmons opened 12 years ago

robsimmons commented 12 years ago
(*[ 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.

robsimmons commented 12 years ago

A related error is that this doesn't check, even though, intuitively (speaking as a user) it should:

(*[ val f: unit -> true -> true ]*)
fun f x = 
   let
      val (q (*[ <: true -> true ]*), _) = ((fn x => x), 3) 
   in q end

Workaround:

(*[ val f: unit -> true -> true ]*)
fun f x = 
   let
      val (q , _) (*[ <: (true -> true) * int ]*) = ((fn x => x), 3) 
   in q end