diff --git a/FSharpActivePatterns/bin/REPL.ml b/FSharpActivePatterns/bin/REPL.ml
index 92627dc75..319a4febe 100644
--- a/FSharpActivePatterns/bin/REPL.ml
+++ b/FSharpActivePatterns/bin/REPL.ml
@@ -119,7 +119,7 @@ let run_repl dump_parsetree input_file =
             (match ic with
              | None ->
                List.iter
-                 (fun (n, t) -> fprintf std_formatter "%s : %a" n pp_typ t)
+                 (fun (n, t) -> fprintf std_formatter "%s : %a\n" n pp_typ t)
                  names_and_types;
                print_flush ();
                run_repl_helper run env new_state
diff --git a/FSharpActivePatterns/lib/ast.ml b/FSharpActivePatterns/lib/ast.ml
index 1fe2a60af..4cc306c35 100644
--- a/FSharpActivePatterns/lib/ast.ml
+++ b/FSharpActivePatterns/lib/ast.ml
@@ -4,6 +4,7 @@
 
 open KeywordChecker
 open TypedTree
+open TypesPp
 
 type ident = Ident of string (** identifier *) [@@deriving show { with_path = false }]
 
@@ -99,11 +100,9 @@ type pattern =
   | PVar of ident (** pattern identifier *)
   | POption of pattern option
   (*| Variant of (ident list[@gen gen_ident_small_list]) (** | [Blue, Green, Yellow] -> *) *)
-  | PConstraint of pattern * (typ[@gen gen_typ_sized (n / 4)])
+  | PConstraint of pattern * (typ[@gen gen_typ_primitive])
 [@@deriving show { with_path = false }, qcheck]
 
-let gen_typed_pattern_sized n = QCheck.Gen.(pair (gen_pattern_sized n) (return None))
-
 type is_recursive =
   | Nonrec (** let factorial n = ... *)
   | Rec (** let rec factorial n = ... *)
@@ -151,7 +150,7 @@ and expr =
         [@gen QCheck.Gen.(list_size (0 -- 2) (gen_let_bind_sized (n / 20)))])
       * expr (** [let rec f x = if (x <= 0) then x else g x and g x = f (x-2) in f 3] *)
   | Option of expr option (** [int option] *)
-  | EConstraint of expr * (typ[@gen gen_typ_sized (n / 4)])
+  | EConstraint of expr * (typ[@gen gen_typ_primitive])
 [@@deriving show { with_path = false }, qcheck]
 
 and let_bind =
diff --git a/FSharpActivePatterns/lib/astPrinter.ml b/FSharpActivePatterns/lib/astPrinter.ml
index a0db5cabe..0c8bd4a05 100644
--- a/FSharpActivePatterns/lib/astPrinter.ml
+++ b/FSharpActivePatterns/lib/astPrinter.ml
@@ -8,6 +8,7 @@
 
 open Format
 open Ast
+open TypesPp
 
 let print_bin_op indent fmt = function
   | Binary_equal -> fprintf fmt "%s| Binary Equal\n" (String.make indent '-')
@@ -51,13 +52,18 @@ let rec print_pattern indent fmt = function
     print_pattern (indent + 2) fmt r
   | PVar (Ident name) -> fprintf fmt "%s| PVar(%s)\n" (String.make indent '-') name
   | POption p ->
-    fprintf fmt "%s| POption: " (String.make indent '-');
+    fprintf fmt "%s| POption " (String.make indent '-');
     (match p with
      | None -> fprintf fmt "None\n"
      | Some p ->
        fprintf fmt "Some:\n";
        print_pattern (indent + 2) fmt p)
-  | PConstraint (p, _) -> print_pattern indent fmt p
+  | PConstraint (p, t) ->
+    fprintf fmt "%s| PConstraint\n" (String.make indent ' ');
+    fprintf fmt "%sPattern:\n" (String.make (indent + 2) ' ');
+    print_pattern (indent + 2) fmt p;
+    fprintf fmt "%sType:\n" (String.make (indent + 2) ' ');
+    fprintf fmt "%s| %a\n" (String.make (indent + 2) '-') pp_typ t
 ;;
 
 let print_unary_op indent fmt = function
@@ -69,11 +75,9 @@ let rec print_let_bind indent fmt = function
   | Let_bind (name, args, body) ->
     fprintf fmt "%s| Let_bind:\n" (String.make indent '-');
     fprintf fmt "%sNAME:\n" (String.make (indent + 4) ' ');
-    fprintf fmt "%s| %a\n" (String.make (indent + 4) '-') pp_pattern name;
+    print_pattern (indent + 4) fmt name;
     fprintf fmt "%sARGS:\n" (String.make (indent + 4) ' ');
-    List.iter
-      (fun arg -> fprintf fmt "%s| %a\n" (String.make (indent + 2) '-') pp_pattern arg)
-      args;
+    List.iter (fun arg -> print_pattern (indent + 2) fmt arg) args;
     fprintf fmt "%sBODY:\n" (String.make (indent + 4) ' ');
     print_expr (indent + 2) fmt body
 
@@ -134,7 +138,6 @@ and print_expr indent fmt expr =
   | Lambda (arg1, args, body) ->
     fprintf fmt "%s| Lambda:\n" (String.make indent '-');
     fprintf fmt "%sARGS\n" (String.make (indent + 2) ' ');
-    print_pattern (indent + 4) fmt arg1;
     List.iter (fun pat -> print_pattern (indent + 4) fmt pat) (arg1 :: args);
     fprintf fmt "%sBODY\n" (String.make (indent + 2) ' ');
     print_expr (indent + 4) fmt body
@@ -147,11 +150,11 @@ and print_expr indent fmt expr =
   | LetIn (rec_flag, let_bind, let_bind_list, inner_e) ->
     fprintf
       fmt
-      "%s | %s LetIn=\n"
+      "%s| %sLetIn=\n"
       (String.make indent '-')
       (match rec_flag with
        | Nonrec -> ""
-       | Rec -> "Rec");
+       | Rec -> "Rec ");
     fprintf fmt "%sLet_binds\n" (String.make (indent + 2) ' ');
     List.iter (print_let_bind (indent + 2) fmt) (let_bind :: let_bind_list);
     fprintf fmt "%sINNER_EXPRESSION\n" (String.make (indent + 2) ' ');
@@ -162,7 +165,12 @@ and print_expr indent fmt expr =
      | Some e ->
        fprintf fmt "%s| Option: Some\n" (String.make indent '-');
        print_expr (indent + 2) fmt e)
-  | EConstraint (e, _) -> print_expr indent fmt e
+  | EConstraint (e, t) ->
+    fprintf fmt "%s| EConstraint\n" (String.make indent ' ');
+    fprintf fmt "%sExpr:\n" (String.make (indent + 2) ' ');
+    print_expr (indent + 2) fmt e;
+    fprintf fmt "%sType:\n" (String.make (indent + 2) ' ');
+    fprintf fmt "%s| %a\n" (String.make (indent + 2) '-') pp_typ t
 ;;
 
 let print_statement indent fmt = function
diff --git a/FSharpActivePatterns/lib/inferencer.ml b/FSharpActivePatterns/lib/inferencer.ml
index 082b1dc09..c5710a47b 100644
--- a/FSharpActivePatterns/lib/inferencer.ml
+++ b/FSharpActivePatterns/lib/inferencer.ml
@@ -15,19 +15,21 @@ type error =
   | `Not_allowed_right_hand_side_let_rec
   | `Not_allowed_left_hand_side_let_rec
   | `Args_after_not_variable_let
+  | `Bound_several_times
   ]
 
 let pp_error fmt : error -> _ = function
   | `Occurs_check -> fprintf fmt "Occurs check failed"
   | `Undef_var s -> fprintf fmt "Undefined variable '%s'" s
   | `Unification_failed (fst, snd) ->
-    fprintf fmt "unification failed on %a and %a" pp_typ fst pp_typ snd
+    fprintf fmt "unification failed on %a and %a\n" pp_typ fst pp_typ snd
   | `Not_allowed_right_hand_side_let_rec ->
     fprintf fmt "This kind of expression is not allowed as right-hand side of `let rec'"
   | `Not_allowed_left_hand_side_let_rec ->
     fprintf fmt "Only variables are allowed as left-hand side of `let rec'"
   | `Args_after_not_variable_let ->
     fprintf fmt "Arguments in let allowed only after variable"
+  | `Bound_several_times -> fprintf fmt "Variable is bound several times"
 ;;
 
 (* for treating result of type inference *)
@@ -357,7 +359,8 @@ end = struct
      ;; *)
 
   let pp_without_freevars fmt t =
-    Map.iteri t ~f:(fun ~key ~data -> fprintf fmt "%s : %a" key pp_typ (Scheme.typ data))
+    Map.iteri t ~f:(fun ~key ~data ->
+      fprintf fmt "%s : %a\n" key pp_typ (Scheme.typ data))
   ;;
 
   (* collect all free vars from environment *)
@@ -468,27 +471,40 @@ let infer_patterns env ~shadow patterns =
       return (new_env, typ :: typs))
 ;;
 
-let extract_names_from_pattern pat =
-  let rec helper = function
-    | PVar (Ident name) -> [ name ]
-    | PList l -> List.concat (List.map l ~f:helper)
-    | PCons (hd, tl) -> List.concat [ helper hd; helper tl ]
-    | PTuple (fst, snd, rest) ->
-      List.concat [ helper fst; helper snd; List.concat (List.map rest ~f:helper) ]
-    | POption (Some p) -> helper p
-    | PConstraint (p, _) -> helper p
-    | POption None -> []
-    | Wild -> []
-    | PConst _ -> []
-  in
-  helper pat
+module StringSet = struct
+  include Stdlib.Set.Make (String)
+
+  let union_disjoint s1 s2 =
+    let* s1 = s1 in
+    let* s2 = s2 in
+    if is_empty (inter s1 s2) then return (union s1 s2) else fail `Bound_several_times
+  ;;
+
+  let union_disjoint_many sets =
+    List.fold ~init:(return empty) ~f:(fun acc set -> union_disjoint acc set) sets
+  ;;
+end
+
+let rec extract_names_from_pattern =
+  let extr = extract_names_from_pattern in
+  function
+  | PVar (Ident name) -> return (StringSet.singleton name)
+  | PList l -> StringSet.union_disjoint_many (List.map l ~f:extr)
+  | PCons (hd, tl) -> StringSet.union_disjoint (extr hd) (extr tl)
+  | PTuple (fst, snd, rest) ->
+    StringSet.union_disjoint_many (List.map ~f:extr (fst :: snd :: rest))
+  | POption (Some p) -> extr p
+  | PConstraint (p, _) -> extr p
+  | POption None -> return StringSet.empty
+  | Wild -> return StringSet.empty
+  | PConst _ -> return StringSet.empty
 ;;
 
 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* pat_names = extract_names_from_pattern pattern >>| StringSet.elements in
   let generalized_schemes =
     List.map pat_names ~f:(fun name ->
       let typ = TypeEnvironment.find_typ_exn env name in
@@ -501,12 +517,11 @@ let infer_match_pattern env ~shadow pattern match_type =
 ;;
 
 let extract_names_from_patterns pats =
-  List.fold pats ~init:[] ~f:(fun acc p ->
-    List.concat [ acc; extract_names_from_pattern p ])
+  StringSet.union_disjoint_many (List.map ~f:extract_names_from_pattern pats)
 ;;
 
 let extract_bind_names_from_let_binds let_binds =
-  List.concat
+  StringSet.union_disjoint_many
     (List.map let_binds ~f:(function Let_bind (pat, _, _) ->
        extract_names_from_pattern pat))
 ;;
@@ -518,7 +533,7 @@ let extract_bind_patterns_from_let_binds let_binds =
 let extend_env_with_bind_names env let_binds =
   (* to prevent binds like let rec x = x + 1*)
   let let_binds =
-    List.filter let_binds ~f:(function Let_bind (_, args, _) -> List.length args <> 0)
+    List.filter let_binds ~f:(function Let_bind (_, args, _) -> not (List.is_empty args))
   in
   let bind_names = extract_bind_patterns_from_let_binds let_binds in
   let* env, _ = infer_patterns env ~shadow:true bind_names in
@@ -661,48 +676,55 @@ let rec infer_expr env = function
     let* subst_final = Substitution.compose subst1 subst2 in
     return (subst_final, typ)
   | Function ((p1, e1), rest) ->
-    let* arg_type = make_fresh_var in
-    let* return_type = make_fresh_var in
-    let* subst, return_type =
-      List.fold
-        ((p1, e1) :: rest)
-        ~init:(return (Substitution.empty, 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 arg_type pat in
-          let env = TypeEnvironment.apply subst2 env in
-          let* subst3, expr_typ = infer_expr env expr in
-          let* subst4 = unify return_type expr_typ in
-          let* subst = Substitution.compose_all [ subst1; subst2; subst3; subst4 ] in
-          return (subst, Substitution.apply subst return_type))
-    in
-    return (subst, Arrow (Substitution.apply subst arg_type, return_type))
+    let* match_t = make_fresh_var in
+    let* return_t = make_fresh_var in
+    infer_matching_expr
+      env
+      ((p1, e1) :: rest)
+      Substitution.empty
+      match_t
+      return_t
+      ~with_arg:true
   | Match (e, (p1, e1), rest) ->
-    let* subst_init, match_type = infer_expr env e in
+    let* subst_init, match_t = infer_expr env e in
     let env = TypeEnvironment.apply subst_init env in
-    let* return_type = make_fresh_var in
-    let* subst, return_type =
-      List.fold
-        ((p1, e1) :: rest)
-        ~init:(return (subst_init, return_type))
-        ~f:(fun acc (pat, expr) ->
-          let* subst1, return_type = acc 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
-          let* subst4 = unify return_type expr_typ in
-          let* subst = Substitution.compose_all [ subst12; subst3; subst4 ] in
-          return (subst, Substitution.apply subst return_type))
-    in
-    return (subst, return_type)
+    let* return_t = make_fresh_var in
+    infer_matching_expr env ((p1, e1) :: rest) subst_init match_t return_t ~with_arg:false
   | EConstraint (e, t) ->
     let* subst1, e_type = infer_expr env e in
     let* subst2 = unify e_type (Substitution.apply subst1 t) in
     let* subst_result = Substitution.compose subst1 subst2 in
     return (subst_result, Substitution.apply subst2 e_type)
 
+and infer_matching_expr env cases subst_init match_t return_t ~with_arg =
+  let* subst, return_t =
+    List.fold
+      cases
+      ~init:(return (subst_init, return_t))
+      ~f:(fun acc (pat, expr) ->
+        let* subst1, return_type = acc in
+        let* env, subst2 =
+          match with_arg with
+          | true ->
+            let* env, pat = infer_pattern env ~shadow:true pat in
+            let* subst2 = unify match_t pat in
+            return (env, subst2)
+          | false -> infer_match_pattern env ~shadow:true pat match_t
+        in
+        let* subst12 = Substitution.compose subst1 subst2 in
+        let env = TypeEnvironment.apply subst12 env in
+        let* subst3, expr_typ = infer_expr env expr in
+        let* subst4 = unify return_type expr_typ in
+        let* subst = Substitution.compose_all [ subst12; subst3; subst4 ] in
+        return (subst, Substitution.apply subst return_type))
+  in
+  let final_typ =
+    match with_arg with
+    | true -> Arrow (Substitution.apply subst match_t, return_t)
+    | false -> return_t
+  in
+  return (subst, final_typ)
+
 and extend_env_with_let_binds env is_rec let_binds =
   List.fold
     let_binds
@@ -729,8 +751,8 @@ and infer_let_bind env is_rec let_bind =
   let* subst2 = unify (Substitution.apply subst1 name_type) bind_type in
   let* subst = Substitution.compose subst1 subst2 in
   let env = TypeEnvironment.apply subst env in
-  let names = extract_names_from_pattern name in
-  let arg_names = extract_names_from_patterns args in
+  let* names = extract_names_from_pattern name >>| StringSet.elements in
+  let* arg_names = extract_names_from_patterns args >>| StringSet.elements in
   let names_types = List.map names ~f:(fun n -> n, TypeEnvironment.find_typ_exn env n) in
   let env = TypeEnvironment.remove_many env (List.concat [ names; arg_names ]) in
   let names_schemes_list =
@@ -744,7 +766,9 @@ let infer_statement env = function
     let let_binds = let_bind :: let_binds in
     let* env = extend_env_with_bind_names env let_binds in
     let* env, _ = extend_env_with_let_binds env Rec let_binds in
-    let bind_names = extract_bind_names_from_let_binds let_binds in
+    let* bind_names =
+      extract_bind_names_from_let_binds let_binds >>| StringSet.elements
+    in
     let bind_names_with_types =
       List.map bind_names ~f:(fun name ->
         match TypeEnvironment.find_exn env name with
@@ -754,7 +778,9 @@ let infer_statement env = function
   | Let (Nonrec, let_bind, let_binds) ->
     let let_binds = let_bind :: let_binds in
     let* env, _ = extend_env_with_let_binds env Nonrec let_binds in
-    let bind_names = extract_bind_names_from_let_binds let_binds in
+    let* bind_names =
+      extract_bind_names_from_let_binds let_binds >>| StringSet.elements
+    in
     let bind_names_with_types =
       List.map bind_names ~f:(fun name ->
         match TypeEnvironment.find_exn env name with
diff --git a/FSharpActivePatterns/lib/inferencer.mli b/FSharpActivePatterns/lib/inferencer.mli
index 952225aa1..f9ed9c1c6 100644
--- a/FSharpActivePatterns/lib/inferencer.mli
+++ b/FSharpActivePatterns/lib/inferencer.mli
@@ -22,6 +22,7 @@ type error =
   | `Not_allowed_right_hand_side_let_rec
   | `Not_allowed_left_hand_side_let_rec
   | `Args_after_not_variable_let
+  | `Bound_several_times
   ]
 
 val pp_error : formatter -> error -> unit
diff --git a/FSharpActivePatterns/lib/parser.ml b/FSharpActivePatterns/lib/parser.ml
index 4d83c29ab..c649e24a3 100644
--- a/FSharpActivePatterns/lib/parser.ml
+++ b/FSharpActivePatterns/lib/parser.ml
@@ -25,15 +25,9 @@ let peek_sep1 =
   match c with
   | None -> return None
   | Some c ->
-    if is_ws c
-       || Char.equal c '('
-       || Char.equal c ')'
-       || Char.equal c ','
-       || Char.equal c ']'
-       || Char.equal c ':'
-       || Char.equal c ';'
-    then return (Some c)
-    else fail "need a delimiter"
+    (match c with
+     | '(' | ')' | ']' | ';' | ':' | ',' -> return (Some c)
+     | _ -> if is_ws c then return (Some c) else fail "need a delimiter")
 ;;
 
 let skip_ws_sep1 = peek_sep1 *> skip_ws
@@ -260,9 +254,9 @@ let p_pat =
     let atom = choice [ p_pat_const; p_parens self; p_parens (p_constraint_pat self) ] in
     let semicolon_list = p_semicolon_list_pat (self <|> atom) <|> atom in
     let opt = p_option semicolon_list make_option_pat <|> semicolon_list in
-    let tuple = p_tuple_pat opt <|> opt in
-    let cons = p_cons_list_pat tuple in
-    cons)
+    let cons = p_cons_list_pat opt in
+    let tuple = p_tuple_pat cons <|> cons in
+    tuple)
 ;;
 
 let p_let_bind p_expr =
@@ -372,8 +366,7 @@ let p_expr =
     let letin_expr = p_letin (p_expr <|> if_expr) <|> if_expr in
     let option = p_option letin_expr make_option_expr <|> letin_expr in
     let apply = p_apply option <|> option in
-    let tuple = p_tuple make_tuple_expr apply <|> apply in
-    let unary = choice [ unary_chain p_not tuple; unary_chain unminus tuple ] in
+    let unary = choice [ unary_chain p_not apply; unary_chain unminus apply ] in
     let factor = chainl1 unary (mul <|> div) in
     let term = chainl1 factor (add <|> sub) in
     let cons_op = chainr1 term cons in
@@ -386,7 +379,8 @@ let p_expr =
     let comp_and = chainl1 bit_or log_and in
     let comp_or = chainl1 comp_and log_or in
     let inf_oper = p_inf_oper_expr comp_or <|> comp_or in
-    let p_function = p_function (p_expr <|> inf_oper) <|> inf_oper in
+    let tuple = p_tuple make_tuple_expr inf_oper <|> inf_oper in
+    let p_function = p_function (p_expr <|> tuple) <|> tuple in
     let ematch = p_match (p_expr <|> p_function) <|> p_function in
     let efun = p_lambda (p_expr <|> ematch) <|> ematch in
     efun)
diff --git a/FSharpActivePatterns/lib/prettyPrinter.ml b/FSharpActivePatterns/lib/prettyPrinter.ml
index e4eeb1117..5233b4031 100644
--- a/FSharpActivePatterns/lib/prettyPrinter.ml
+++ b/FSharpActivePatterns/lib/prettyPrinter.ml
@@ -70,26 +70,18 @@ and pp_expr fmt expr =
     fprintf fmt "]"
   | Tuple (e1, e2, rest) ->
     fprintf fmt "(";
-    pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt ", ") pp_expr fmt (e1 :: e2 :: rest);
+    pp_print_list
+      ~pp_sep:(fun fmt () -> fprintf fmt ", ")
+      pp_parens_expr
+      fmt
+      (e1 :: e2 :: rest);
     fprintf fmt ")"
   | Function ((pat1, expr1), cases) ->
-    let cases =
-      List.map
-        (function
-          | a, b -> a, b)
-        cases
-    in
     fprintf fmt "function ";
     List.iter
       (fun (pat, expr) -> fprintf fmt "| %a -> (%a) \n" pp_pattern pat pp_expr expr)
       ((pat1, expr1) :: cases)
   | Match (value, (pat1, expr1), cases) ->
-    let cases =
-      List.map
-        (function
-          | p, e -> p, e)
-        cases
-    in
     fprintf fmt "match (%a) with \n" pp_expr value;
     List.iter
       (fun (pat, expr) -> fprintf fmt "| %a -> (%a) \n" pp_pattern pat pp_expr expr)
@@ -137,7 +129,8 @@ and pp_args fmt args =
 and pp_let_bind fmt = function
   | Let_bind (name, args, body) ->
     fprintf fmt "%a %a = %a " pp_pattern name pp_args args pp_expr body
-;;
+
+and pp_parens_expr fmt expr = fprintf fmt "(%a)" pp_expr expr
 
 let pp_statement fmt = function
   | Let (rec_flag, let_bind, let_bind_list) ->
diff --git a/FSharpActivePatterns/lib/tests/qcheck_utils.ml b/FSharpActivePatterns/lib/tests/qcheck_utils.ml
index fd6cde746..6084e6655 100644
--- a/FSharpActivePatterns/lib/tests/qcheck_utils.ml
+++ b/FSharpActivePatterns/lib/tests/qcheck_utils.ml
@@ -22,6 +22,13 @@ let shrink_lt =
   | String_lt x -> QCheck.Shrink.string x >|= fun a' -> String_lt a'
 ;;
 
+let exprs_from_let_binds let_binds =
+  List.map
+    (function
+      | Let_bind (_, _, e) -> e)
+    let_binds
+;;
+
 let rec shrink_let_bind =
   let open QCheck.Iter in
   function
@@ -55,7 +62,7 @@ and shrink_expr =
     <+> (shrink_expr i >|= fun a' -> If_then_else (a', t, None))
     <+> (shrink_expr t >|= fun a' -> If_then_else (i, a', None))
   | LetIn (rec_flag, let_bind, let_bind_list, inner_e) ->
-    return inner_e
+    of_list (inner_e :: exprs_from_let_binds (let_bind :: let_bind_list))
     <+> (shrink_let_bind let_bind
          >|= fun a' -> LetIn (rec_flag, a', let_bind_list, inner_e))
     <+> (QCheck.Shrink.list ~shrink:shrink_let_bind let_bind_list
@@ -101,7 +108,7 @@ and shrink_expr =
     of_list [ e; Option None ] <+> (shrink_expr e >|= fun a' -> Option (Some a'))
   | Option None -> empty
   | Variable _ -> empty
-  | EConstraint (e, _) -> return e
+  | EConstraint (e, t) -> return e <+> shrink_expr e >|= fun a' -> EConstraint (a', t)
 
 and shrink_pattern =
   let open QCheck.Iter in
@@ -143,13 +150,26 @@ let shrink_construction =
   let open QCheck.Iter in
   function
   | Expr e -> shrink_expr e >|= fun a' -> Expr a'
-  | Statement s -> shrink_statement s >|= fun a' -> Statement a'
+  | Statement s ->
+    shrink_statement s
+    >|= (fun a' -> Statement a')
+    <+>
+      (match s with
+      | Let (_, let_bind, let_binds) ->
+        of_list (exprs_from_let_binds (let_bind :: let_binds)) >|= fun a' -> Expr a')
 ;;
 
 let arbitrary_construction =
   QCheck.make
     gen_construction
-    ~print:(Format.asprintf "%a" print_construction)
+    ~print:
+      (let open Format in
+       asprintf "%a" (fun fmt c ->
+         let pp = print_construction in
+         fprintf fmt "Generated:\n%a" pp c;
+         match parse (Format.asprintf "%a\n" pp c) with
+         | Ok parsed -> fprintf fmt "Parsed:\n%a" pp parsed
+         | Error e -> fprintf fmt "Parsing error:\n%s\n" e))
     ~shrink:shrink_construction
 ;;
 
diff --git a/FSharpActivePatterns/lib/typedTree.ml b/FSharpActivePatterns/lib/typedTree.ml
index 44aee06e8..93079c14d 100644
--- a/FSharpActivePatterns/lib/typedTree.ml
+++ b/FSharpActivePatterns/lib/typedTree.ml
@@ -4,8 +4,6 @@
 
 type binder = int [@@deriving show { with_path = false }, qcheck]
 
-let gen_primitive = QCheck.Gen.oneofl [ "int"; "bool"; "string"; "unit" ]
-
 type typ =
   | Primitive of (string[@gen gen_primitive])
   | Type_var of binder
@@ -13,7 +11,10 @@ type typ =
   | Type_list of typ
   | Type_tuple of typ * typ * typ list
   | TOption of typ
-[@@deriving show { with_path = false }, qcheck]
+
+let gen_typ_primitive =
+  QCheck.Gen.(oneofl [ "string"; "int"; "unit"; "bool" ] >|= fun t -> Primitive t)
+;;
 
 let arrow_of_types first_types last_type =
   let open Base in
@@ -33,7 +34,7 @@ end
 type binder_set = VarSet.t [@@deriving show { with_path = false }]
 
 (* binder_set here -- list of all type vars in context (?) *)
-type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }]
+type scheme = Scheme of binder_set * typ
 
 let int_typ = Primitive "int"
 let bool_typ = Primitive "bool"
diff --git a/FSharpActivePatterns/lib/typedTree.mli b/FSharpActivePatterns/lib/typedTree.mli
index b3e5dc4bf..e5ad1655a 100644
--- a/FSharpActivePatterns/lib/typedTree.mli
+++ b/FSharpActivePatterns/lib/typedTree.mli
@@ -12,8 +12,7 @@ type typ =
   | Type_tuple of typ * typ * typ list
   | TOption of typ
 
-val gen_typ_sized : int -> typ QCheck.Gen.t
-val pp_typ : Format.formatter -> typ -> unit
+val gen_typ_primitive : typ QCheck.Gen.t
 val arrow_of_types : typ list -> typ -> typ
 
 module VarSet : sig
@@ -23,7 +22,7 @@ module VarSet : sig
 end
 
 type binder_set = VarSet.t
-type scheme = Scheme of binder_set * typ [@@deriving show { with_path = false }]
+type scheme = Scheme of binder_set * typ
 
 val int_typ : typ
 val bool_typ : typ
diff --git a/FSharpActivePatterns/lib/typesPp.ml b/FSharpActivePatterns/lib/typesPp.ml
index 6873b0048..840c717dd 100644
--- a/FSharpActivePatterns/lib/typesPp.ml
+++ b/FSharpActivePatterns/lib/typesPp.ml
@@ -5,29 +5,25 @@
 open TypedTree
 open Format
 
-let pp_typ fmt typ =
-  let rec helper fmt = function
-    | Primitive s -> fprintf fmt "%s" s
-    | Type_var var -> fprintf fmt "'_%d" var
-    | Arrow (fst, snd) ->
-      (match fst with
-       | Arrow _ -> fprintf fmt "(%a) -> %a" helper fst helper snd
-       | _ -> fprintf fmt "%a -> %a" helper fst helper snd)
-    | Type_list typ -> fprintf fmt "%a list" helper typ
-    | Type_tuple (first, second, rest) ->
-      Format.pp_print_list
-        ~pp_sep:(fun fmt () -> fprintf fmt " * ")
-        (fun fmt typ ->
-          match typ with
-          | Arrow _ -> fprintf fmt "(%a)" helper typ
-          | _ -> helper fmt typ)
-        fmt
-        (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"
+let rec pp_typ fmt = function
+  | Primitive s -> fprintf fmt "%s" s
+  | Type_var var -> fprintf fmt "'_%d" var
+  | Arrow (fst, snd) ->
+    (match fst with
+     | Arrow _ -> fprintf fmt "(%a) -> %a" pp_typ fst pp_typ snd
+     | _ -> fprintf fmt "%a -> %a" pp_typ fst pp_typ snd)
+  | Type_list typ -> fprintf fmt "%a list" pp_typ typ
+  | Type_tuple (first, second, rest) ->
+    Format.pp_print_list
+      ~pp_sep:(fun fmt () -> fprintf fmt " * ")
+      (fun fmt typ ->
+        match typ with
+        | Arrow _ -> fprintf fmt "(%a)" pp_typ typ
+        | _ -> pp_typ fmt typ)
+      fmt
+      (first :: second :: rest)
+  | TOption t ->
+    (match t with
+     | Type_tuple _ | Arrow _ -> fprintf fmt "(%a) option" pp_typ t
+     | t -> fprintf fmt "%a option" pp_typ t)
 ;;
diff --git a/FSharpActivePatterns/tests/inference.t b/FSharpActivePatterns/tests/inference.t
index 9603112a8..b2739faf7 100644
--- a/FSharpActivePatterns/tests/inference.t
+++ b/FSharpActivePatterns/tests/inference.t
@@ -1,31 +1,25 @@
   $ ../bin/REPL.exe -fromfile manytests/do_not_type/001.ml
   Type checking failed: Undefined variable 'fac'
   $ ../bin/REPL.exe -fromfile manytests/do_not_type/002if.ml
-  Type checking failed: unification failed on int
-   and bool
+  Type checking failed: unification failed on int and bool
   
   $ ../bin/REPL.exe -fromfile manytests/do_not_type/003occurs.ml
   Type checking failed: Occurs check failed
   $ ../bin/REPL.exe -fromfile manytests/do_not_type/004let_poly.ml
-  Type checking failed: unification failed on bool
-   and int
+  Type checking failed: unification failed on bool and int
   
-  Type checking failed: unification failed on string
-   and int
+  Type checking failed: unification failed on string and int
   
   $ ../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'
   Type checking failed: Undefined variable 'x'
-  Type checking failed: unification failed on '_1 option
-   and '_0 -> '_0
+  Type checking failed: unification failed on '_1 option and '_0 -> '_0
   
-  Type checking failed: unification failed on unit
-   and '_2 -> '_2
+  Type checking failed: unification failed on unit and '_2 -> '_2
   
   $ ../bin/REPL.exe -fromfile manytests/typed/001fac.ml
   fac : int -> int