Implement inference of polymorphic patterns in Match. Fix types pretty printer.

FSharpActivePatterns/lib/inferencer.ml

@@ -317,7 +317,6 @@ module TypeEnvironment : sig
   val remove : t -> string -> t
   val remove_many : t -> string list -> t
   val pp_without_freevars : formatter -> t -> unit
-
   (* val pp : formatter -> t -> unit *)
 end = struct
   open Base
@@ -485,6 +484,22 @@ let extract_names_from_pattern pat =
   helper pat
 ;;
 
+let infer_match_pattern env ~shadow pattern match_type =
+  let* env, pat_typ = infer_pattern env ~shadow pattern in
+  let* subst = unify pat_typ match_type in
+  let env = TypeEnvironment.apply subst env in
+  let pat_names = extract_names_from_pattern pattern in
+  let generalized_schemes =
+    List.map pat_names ~f:(fun name ->
+      let typ = TypeEnvironment.find_typ_exn env name in
+      let env = TypeEnvironment.remove env name in
+      let generalized_typ = generalize env typ in
+      name, generalized_typ)
+  in
+  let env = TypeEnvironment.extend_many env generalized_schemes in
+  return (env, subst)
+;;
+
 let extract_names_from_patterns pats =
   List.fold pats ~init:[] ~f:(fun acc p ->
     List.concat [ acc; extract_names_from_pattern p ])
@@ -673,8 +688,7 @@ let rec infer_expr env = function
         ~init:(return (subst_init, return_type))
         ~f:(fun acc (pat, expr) ->
           let* subst1, return_type = acc in
-          let* env, pat = infer_pattern env ~shadow:true pat in
-          let* subst2 = unify match_type pat in
+          let* env, subst2 = infer_match_pattern env ~shadow:true pat match_type in
           let* subst12 = Substitution.compose subst1 subst2 in
           let env = TypeEnvironment.apply subst12 env in
           let* subst3, expr_typ = infer_expr env expr in

FSharpActivePatterns/lib/typesPp.ml

@@ -15,14 +15,18 @@ let pp_typ fmt typ =
        | _ -> fprintf fmt "%a -> %a" helper fst helper snd)
     | Type_list typ -> fprintf fmt "%a list" helper typ
     | Type_tuple (first, second, rest) ->
-      fprintf fmt "(";
       Format.pp_print_list
         ~pp_sep:(fun fmt () -> fprintf fmt " * ")
-        helper
+        (fun fmt typ ->
+          match typ with
+          | Arrow _ -> fprintf fmt "(%a)" helper typ
+          | _ -> helper fmt typ)
         fmt
-        (first :: second :: rest);
-      fprintf fmt ")"
-    | TOption t -> fprintf fmt "%a option" helper t
+        (first :: second :: rest)
+    | TOption t ->
+      (match t with
+       | Type_tuple _ | Arrow _ -> fprintf fmt "(%a) option" helper t
+       | t -> fprintf fmt "%a option" helper t)
   in
   helper fmt typ;
   fprintf fmt "\n"

FSharpActivePatterns/tests/inference.t

@@ -15,8 +15,8 @@
 
   $ ../bin/REPL.exe -fromfile manytests/do_not_type/015tuples.ml
   Type checking failed: Only variables are allowed as left-hand side of `let rec'
-  Type checking failed: unification failed on ('_0 * '_1)
-   and (int * int * int)
+  Type checking failed: unification failed on '_0 * '_1
+   and int * int * int
 
   $ ../bin/REPL.exe -fromfile manytests/do_not_type/099.ml
   Type checking failed: Only variables are allowed as left-hand side of `let rec'
@@ -62,33 +62,31 @@
   addi : ('_0 -> bool -> int) -> ('_0 -> bool) -> '_0 -> int
   main : int
   $ ../bin/REPL.exe -fromfile manytests/typed/009let_poly.ml
-  temp : (int * bool)
+  temp : int * bool
   $ ../bin/REPL.exe -fromfile manytests/typed/010sukharev.ml
-  _1 : int -> int -> (int * '_1) -> bool
+  _1 : int -> int -> int * '_1 -> bool
   _2 : int
   _3 : (int * string) option
   _4 : int -> '_14
   _42 : int -> bool
-  _6 : '_26 option -> '_26
-  id1 : '_40 -> '_40
-  id2 : '_41 -> '_41
+  _5 : int
+  _6 : '_30 option -> '_30
+  id1 : '_44 -> '_44
+  id2 : '_45 -> '_45
   int_of_option : int option -> int
-  Type checking failed: unification failed on string
-   and int
-
   $ ../bin/REPL.exe -fromfile manytests/typed/015tuples.ml
-  feven : ('_33 * int -> int) -> int -> int
+  feven : '_33 * (int -> int) -> int -> int
   fix : (('_1 -> '_5) -> '_1 -> '_5) -> '_1 -> '_5
-  fixpoly : (('_21 -> '_25 * '_21 -> '_25) -> '_21 -> '_25 * ('_21 -> '_25 * '_21 -> '_25) -> '_21 -> '_25) -> ('_21 -> '_25 * '_21 -> '_25)
-  fodd : (int -> int * '_41) -> int -> int
+  fixpoly : (('_21 -> '_25) * ('_21 -> '_25) -> '_21 -> '_25) * (('_21 -> '_25) * ('_21 -> '_25) -> '_21 -> '_25) -> ('_21 -> '_25) * ('_21 -> '_25)
+  fodd : (int -> int) * '_41 -> int -> int
   main : int
-  map : ('_9 -> '_11) -> ('_9 * '_9) -> ('_11 * '_11)
+  map : ('_9 -> '_11) -> '_9 * '_9 -> '_11 * '_11
   meven : int -> int
   modd : int -> int
-  tie : (int -> int * int -> int)
+  tie : (int -> int) * (int -> int)
   $ ../bin/REPL.exe -fromfile manytests/typed/016lists.ml
   append : '_67 list -> '_67 list -> '_67 list
-  cartesian : '_98 list -> '_105 list -> ('_98 * '_105) list
+  cartesian : '_98 list -> '_105 list -> '_98 * '_105 list
   concat : '_81 list list -> '_81 list
   iter : ('_87 -> unit) -> '_87 list -> unit
   length : '_3 list -> int