Added monomorphism restriction to undefined values.

What does this mean? Basically undefined values can't be created for
types that contain free type variables, so for example: undefined :
list(int) is good, but undefined : list('a) is bad. The reason we want
to do this is because we can't compile them away statically, and this
leads to situations where type-checkable code fails in the rewriter
and gives horribly confusing error messages that don't relate to code
the user wrote at all.

As an example the following used to typecheck, but fail in the
rewriter with a confusing error message, whereas now the typechecker
should reject all cases which would trigger that failure in rewriting.

val test : forall ('a:Type). list('a) -> unit effect {wreg, undef}

function test xs = {
  xs_mut = xs;
  xs_mut = undefined; (* We don't know what kind of undefined 'a is *)
  ()
}

There's a slight hitch, namely that in the undefined_type functions
created by the -undefined_gen option, we do want to allow functions
that have polymorphic undefined values, so that we can generate
undefined generators for polymorphic datatypes such as:

union option ('a:Type) = {
  Some : 'a,
  None
}

These functions are always have a specific form that allows the
rewriter to succesfully remove the polymorphic undefined value for the
'a argument for Sone. As such there's a flag in the typechecking
environment for polymorphic undefineds that is enabled when it sees a
function with the undefined_ name prefix.

Also: Fixed some test cases that were broken due to escape effect being added to assert.

1 files changed, 1 insertions, 1 deletions

diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail2.ml
index 39fc25d3..efcfc8b9 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail2.ml
@@ -181,7 +181,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_tuple exps -> parens (separate_map (comma ^^ space) doc_exp exps)
   | E_if (if_exp, then_exp, else_exp) ->
      group (separate space [string "if"; doc_exp if_exp; string "then"; doc_exp then_exp; string "else"; doc_exp else_exp])
-  | E_list exps -> string "E_list"
+  | E_list exps -> string "[|" ^^ separate_map (comma ^^ space) doc_exp exps ^^ string "|]"
   | E_cons (exp1, exp2) -> string "E_cons"
   | E_record fexps -> string "E_record"
   | E_loop (While, cond, exp) ->