Minor fixes

src/DblParser/Desugar.ml

@@ -632,11 +632,10 @@ and tr_explicit_inst (fld : Raw.field) =
   | FldName n ->
     let pe =
       match n with
-      | NLabel         -> Error.fatal (Error.desugar_error fld.pos)
-      | NVar      x    -> make (EVar (NPName x))
-      | NOptionalVar x -> Error.fatal (Error.desugar_error fld.pos)
-      | NImplicit n    -> make (EImplicit (NPName n))
-      | NMethod   n    -> Error.fatal (Error.desugar_error fld.pos)
+      | NLabel       -> Error.fatal (Error.desugar_error fld.pos)
+      | NVar x | NOptionalVar x -> make (EVar (NPName x))
+      | NImplicit n  -> make (EImplicit (NPName n))
+      | NMethod   n  -> Error.fatal (Error.desugar_error fld.pos)
     in
     Either.Right (make (n, make (EPoly(pe, [], []))))
   | FldNameVal(n, e) ->

src/DblParser/YaccParser.mly

@@ -69,7 +69,7 @@ var_id
 name
 : KW_LABEL  { NLabel       }
 | LID       { NVar $1      }
-| QLID       { NOptionalVar $1 }
+| QLID      { NOptionalVar $1 }
 | TLID      { NImplicit $1 }
 | KW_METHOD LID { NMethod $2   }
 ;

src/TypeInference/Pattern.ml

@@ -331,25 +331,28 @@ and check_pattern_schemes ~env ~scope pats schs =
 
   | [], _ :: _ | _ :: _, [] -> assert false
 
+(** Infer type-scheme of given formal optional argument. Returns extended
+  environment, a pattern that represents an argument, its scheme, and the
+  effect of pattern-matching *)
 let infer_optional_arg_scheme env (arg : S.arg) =
-match arg with
-| ArgAnnot(pat, sch) ->
-  let sch_pos = sch.sch_pos in
-  let sch = Type.tr_scheme env sch in
-  assert (T.Scheme.is_monomorphic sch);
-  let sch = T.Scheme.of_type 
-    (PreludeTypes.mk_Option ~env ~pos:sch_pos sch.sch_body)
-  in
-  let scope = Env.scope env in
-  let (env, pat, _, r_eff) =
-    check_scheme ~env ~scope pat sch in
-  (env, pat, sch, r_eff)
-| ArgPattern pat ->
-  let tp = Env.fresh_uvar env T.Kind.k_type in
-  let tp = (PreludeTypes.mk_Option ~env ~pos:pat.pos tp) in
-  let scope = Env.scope env in
-  let (env, pat, _, r_eff) = check_type ~env ~scope pat tp in
-  (env, pat, T.Scheme.of_type tp, r_eff)
+  match arg with
+  | ArgAnnot(pat, sch) ->
+    let sch_pos = sch.sch_pos in
+    let sch = Type.tr_scheme env sch in
+    assert (T.Scheme.is_monomorphic sch);
+    let sch = T.Scheme.of_type 
+      (PreludeTypes.mk_Option ~env ~pos:sch_pos sch.sch_body)
+    in
+    let scope = Env.scope env in
+    let (env, pat, _, r_eff) =
+      check_scheme ~env ~scope pat sch in
+    (env, pat, sch, r_eff)
+  | ArgPattern pat ->
+    let tp = Env.fresh_uvar env T.Kind.k_type in
+    let tp = (PreludeTypes.mk_Option ~env ~pos:pat.pos tp) in
+    let scope = Env.scope env in
+    let (env, pat, _, r_eff) = check_type ~env ~scope pat tp in
+    (env, pat, T.Scheme.of_type tp, r_eff)
 
 let infer_arg_scheme env (arg : S.arg) =
   match arg with

src/TypeInference/Pattern.mli

@@ -23,12 +23,6 @@ val check_type :
 val infer_arg_scheme :
   Env.t -> S.arg -> Env.t * T.pattern * T.scheme * ret_effect
 
-(** Infer type-scheme of given formal optional argument. Returns extended
-  environment, a pattern that represents an argument, its scheme, and the
-  effect of pattern-matching *)
-val infer_optional_arg_scheme :
-  Env.t -> S.arg -> Env.t * T.pattern * T.scheme * ret_effect
-
 (** Check if given argument has given type scheme. Returns extended
   environment, translated argument as pattern, and the effect of
   pattern-matching *)

src/TypeInference/PreludeTypes.ml

@@ -38,7 +38,7 @@ let mk_Some ~env ~pos tp_arg expr_arg : T.expr =
       let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
       match
         List.find_index
-          (fun (ctor_decl : T.ctor_decl) -> String.compare ctor_decl.ctor_name "Some" == 0)
+          (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name = "Some")
           adt_ctors
       with
       | Some idx ->
@@ -60,7 +60,7 @@ let mk_None ~env ~pos option_tp : T.expr =
       let { Module.adt_proof; adt_args; adt_ctors; adt_type } = adt_info in
       match
         List.find_index
-          (fun (ctor_decl : T.ctor_decl) -> String.compare ctor_decl.ctor_name "None" == 0)
+          (fun (ctor_decl : T.ctor_decl) -> ctor_decl.ctor_name = "None")
           adt_ctors
       with
       | Some idx ->

src/TypeInference/TypeUtils.ml

@@ -48,8 +48,7 @@ let open_scheme ~pos (env : Env.t) (sch : T.scheme) =
         let (env, x) =
           match name with
           | T.NLabel -> Env.add_the_label_sch env sch
-          | T.NVar x  -> Env.add_poly_var env x sch
-          | T.NOptionalVar x -> Env.add_mono_var env x sch.sch_body
+          | T.NVar x | T.NOptionalVar x -> Env.add_poly_var env x sch
           | T.NImplicit n -> Env.add_poly_implicit env n sch ignore
           | T.NMethod   n ->
             let owner = method_owner_of_scheme ~pos ~env sch in

test/ok/ok0109_optionalParams.fram → test/ok/ok0111_optionalParams.fram

@@ -7,17 +7,18 @@ let a = f
 let b = f {x=2}
 
 let g {?x : Int} () = 
-match x with
-| Some n => n + 2
-| None => 42
-end
+  match x with
+  | Some n => n + 2
+  | None => 42
+  end
 let c = g ()
 let d = g {x=2} ()
 let e = g {?x = Some 2} ()
 
-let h {?x} () = match x with
-| Some n => n
-| None => None
-end
+let h {?x} () =
+  match x with
+  | Some n => n
+  | None => None
+  end
 
-let a = h {x=Some 2}
+let a = h {x=Some 2}