val loosen (#t1: Type) (#t2: Type{t1 `subtype_of` t2}) (x: possibly t1) : possibly t2
let loosen (#t1:Type) (#t2:Type{t1 `subtype_of` t2})
    (x:possibly t1) : possibly t2 =
  match x with
  | Ok x' -> Ok x'
  | Err s -> Err s
val loosen (#t1: Type) (#t2: Type{t1 `subtype_of` t2}) (x: possibly t1) : possibly t2
let loosen (#t1: Type) (#t2: Type{t1 `subtype_of` t2}) (x: possibly t1) : possibly t2 =
match x with
| Ok x' -> Ok x'
| Err s -> Err s
Vale.Def.PossiblyMonad.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Vale.Def.PossiblyMonad.fst
Prims.subtype_of Vale.Def.PossiblyMonad.possibly Vale.Def.PossiblyMonad.Ok Prims.string Vale.Def.PossiblyMonad.Err
module Vale.Def.PossiblyMonad

/// Similar to the [maybe] monad in Haskell (which is like the
/// [option] type in F* and OCaml), but instead, we also store the
/// reason for the error when the error occurs.

type possibly 'a =
  | Ok : v:'a -> possibly 'a
  | Err : reason:string -> possibly 'a

unfold let return (#a:Type) (x:a) : possibly a =
  Ok x

unfold let (let+) (#a #b:Type) (x:possibly a) (f:a -> possibly b) : possibly b =
  match x with
  | Err s -> Err s
  | Ok x' -> f x'

unfold let fail_with (#a:Type) (s:string) : possibly a = Err s

unfold let unimplemented (#a:Type) (s:string) : possibly a = fail_with ("Unimplemented: " ^ s)

(** Allows moving to a "looser" monad type, always *)
unfold
let loosen (#t1:Type) (#t2:Type{t1 `subtype_of` t2})
val loosen (#t1: Type) (#t2: Type{t1 `subtype_of` t2}) (x: possibly t1) : possibly t2
x: Vale.Def.PossiblyMonad.possibly t1 -> Vale.Def.PossiblyMonad.possibly t2