Make the backward functions not fail

[sonmarcho]

trafficstars

For now the backward functions can fail (they use the Result type). The problem comes from enumerations containing mutable borrows. For instance:

fn id<'a, T>(x : &'a mut Option<T>) -> Option<&'a mut T> {
  match x with
  | None => None,
  | Some(x) => Some(x),
}

A pure model is given by (note that the backward function consumes an option):

def id {T} (x : Option T) : Result (Option T x (Option T -> Result (Option T))) :=
  match x with
  | none => ok (None, fun _ => ok None)
  | some x =>
    let back x :=
      -- We need to extract the given back value from the option
      match x with
      | none =>
        -- This case shouldn't happen if the backward function is called correctly,
        -- but yet we have to take it into account and are stuck.
        -- We have to fail somehow.
        fail
      | some x =>
        -- Here we simply propagate
        ok (some x)
   ok (x, back)

The main issue comes from the fact that we sometimes have to match over an enumeration to extract a given back value from it. If the enumeration doesn't have the proper variant (which shouldn't happen if the backward function is used properly, but that we can't forbid just through typing) then we have an issue because we need to propagate something. However, we could use the fact that we still have the "old" values available to account for this case:

def id {T} (x : Option T) : Result (Option T x (Option T -> Option T)) :=
  match x with
  | none => ok (None, fun _ => None)
  | some x =>
    let back x' :=
      -- We need to extract the given back value from the option
      match x' with
      | none => x -- Simply propagate the old value!
      | some x' => some x' -- Normal case
   (ok x, back)