title: Do OCaml 'underscore types' (e.g. '_a) introduce the possibility of runtime type errors / soundness violations?
body: <p>I was reading a little bit about the value restriction in Standard ML and tried translating the example to OCaml to see what it would do. It seems like OCaml produces these types in contexts where SML would reject a program due to the value restriction. I've also seen them in other contexts like empty hash tables that haven't been "specialized" to a particular type yet.</p>
  
  <p><a href="http://mlton.org/ValueRestriction" rel="nofollow">http://mlton.org/ValueRestriction</a></p>
  
  <p>Here's an example of a rejected program in SML:</p>
  
  <pre><code>val r: 'a option ref = ref NONE
  val r1: string option ref = r
  val r2: int option ref = r
  val () = r1 := SOME "foo"
  val v: int = valOf (!r2)
  </code></pre>
  
  <p>If you enter the first line verbatim into the SML of New Jersey repl you get
  the following error:</p>
  
  <pre><code>- val r: 'a option ref = ref NONE;
  stdIn:1.6-1.33 Error: explicit type variable cannot be generalized at its binding declaration: 'a
  </code></pre>
  
  <p>If you leave off the explicit type annotation you get</p>
  
  <pre><code>- val r = ref NONE
  
  stdIn:1.6-1.18 Warning: type vars not generalized because of
     value restriction are instantiated to dummy types (X1,X2,...)
  val r = ref NONE : ?.X1 option ref
  </code></pre>
  
  <p>What exactly is this dummy type? It seems like it's completely inaccessible and fails to unify with anything</p>
  
  <pre><code>- r := SOME 5;
  
  stdIn:1.2-1.13 Error: operator and operand don't agree [overload conflict]
    operator domain: ?.X1 option ref * ?.X1 option
    operand:         ?.X1 option ref * [int ty] option
    in expression:
      r := SOME 5
  </code></pre>
  
  <p>In OCaml, by contrast, the dummy type variable is accessible and unifies with the first thing it can.</p>
  
  <pre><code># let r : 'a option ref = ref None;;
  val r : '_a option ref = {contents = None}
  
  # r := Some 5;;
  - : unit = ()
  # r ;;
  - : int option ref = {contents = Some 5}
  </code></pre>
  
  <p>This is sort of confusing and raises a few questions.</p>
  
  <p>1) Could a conforming SML implementation choose to make the "dummy" type above accessible? </p>
  
  <p>2) How does OCaml preserve soundness without the value restriction? Does it make weaker guarantees than SML does?</p>
  
  <p>3) The type <code>'_a option ref</code> seems less polymorphic than <code>'a option ref</code>. Why isn't <code>let r : 'a option ref = ref None;;</code> (with an explicit annotation) rejected in OCaml?</p>