Does Cidre have "top" refinements at non-datatypes?

[noamz]

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... ;-)