diff --git a/testsuite/tests/warnings/w01.reference b/testsuite/tests/warnings/w01.reference
index 730da03c9ac1..317c6a4a58e3 100644
--- a/testsuite/tests/warnings/w01.reference
+++ b/testsuite/tests/warnings/w01.reference
@@ -9,7 +9,7 @@ Here is an example of a value that is not matched:
 0
 File "w01.ml", line 36, characters 0-1:
 Warning 10: this expression should have type unit.
-File "w01.ml", line 20, characters 8-9:
-Warning 27: unused variable y.
 File "w01.ml", line 43, characters 2-3:
 Warning 11: this match case is unused.
+File "w01.ml", line 20, characters 8-9:
+Warning 27: unused variable y.
diff --git a/typing/btype.ml b/typing/btype.ml
index 5216deb9a43d..dd5e993a2ed6 100644
--- a/typing/btype.ml
+++ b/typing/btype.ml
@@ -62,6 +62,34 @@ let default_mty = function
     Some mty -> mty
   | None -> Mty_signature []
 
+(**** Definitions for backtracking ****)
+
+type change =
+    Ctype of type_expr * type_desc
+  | Ccompress of type_expr * type_desc * type_desc
+  | Clevel of type_expr * int
+  | Cname of
+      (Path.t * type_expr list) option ref * (Path.t * type_expr list) option
+  | Crow of row_field option ref * row_field option
+  | Ckind of field_kind option ref * field_kind option
+  | Ccommu of commutable ref * commutable
+  | Cuniv of type_expr option ref * type_expr option
+  | Ctypeset of TypeSet.t ref * TypeSet.t
+
+type changes =
+    Change of change * changes ref
+  | Unchanged
+  | Invalid
+
+let trail = Weak.create 1
+
+let log_change ch =
+  match Weak.get trail 0 with None -> ()
+  | Some r ->
+      let r' = ref Unchanged in
+      r := Change (ch, r');
+      Weak.set trail 0 (Some r')
+
 (**** Representative of a type ****)
 
 let rec field_kind_repr =
@@ -69,25 +97,25 @@ let rec field_kind_repr =
     Fvar {contents = Some kind} -> field_kind_repr kind
   | kind                        -> kind
 
-(*
-let rec repr =
-  function
-    {desc = Tlink t'} ->
-      (*
-         We do no path compression. Path compression does not seem to
-         improve notably efficiency, and it prevents from changing a
-         [Tlink] into another type (for instance, for undoing a
-         unification).
-      *)
-      repr t'
-  | {desc = Tfield (_, k, _, t')} when field_kind_repr k = Fabsent ->
-      repr t'
-  | t -> t
-*)
+let rec repr_link compress t d =
+ function
+   {desc = Tlink t' as d'} ->
+     repr_link true t d' t'
+ | {desc = Tfield (_, k, _, t') as d'} when field_kind_repr k = Fabsent ->
+     repr_link true t d' t'
+ | t' ->
+     if compress then begin
+       log_change (Ccompress (t, t.desc, d)); t.desc <- d
+     end;
+     t'
 
-(* Path compression must be undone by backtracking *)
-let repr_link' = ref (fun _ -> assert false)
-let repr t = !repr_link' 0 t t.desc t
+let repr t =
+  match t.desc with
+   Tlink t' as d ->
+     repr_link false t d t'
+ | Tfield (_, k, _, t') as d when field_kind_repr k = Fabsent ->
+     repr_link false t d t'
+ | _ -> t
 
 let rec commu_repr = function
     Clink r when !r <> Cunknown -> commu_repr !r
@@ -599,18 +627,6 @@ let extract_label l ls = extract_label_aux [] l ls
                   (*  Utilities for backtracking    *)
                   (**********************************)
 
-type change =
-    Ctype of type_expr * type_desc
-  | Ccompress of type_expr * type_desc * type_desc
-  | Clevel of type_expr * int
-  | Cname of
-      (Path.t * type_expr list) option ref * (Path.t * type_expr list) option
-  | Crow of row_field option ref * row_field option
-  | Ckind of field_kind option ref * field_kind option
-  | Ccommu of commutable ref * commutable
-  | Cuniv of type_expr option ref * type_expr option
-  | Ctypeset of TypeSet.t ref * TypeSet.t
-
 let undo_change = function
     Ctype  (ty, desc) -> ty.desc <- desc
   | Ccompress  (ty, desc, _) -> ty.desc <- desc
@@ -622,23 +638,9 @@ let undo_change = function
   | Cuniv  (r, v) -> r := v
   | Ctypeset (r, v) -> r := v
 
-type changes =
-    Change of change * changes ref
-  | Unchanged
-  | Invalid
-
 type snapshot = changes ref * int
-
-let trail = Weak.create 1
 let last_snapshot = ref 0
 
-let log_change ch =
-  match Weak.get trail 0 with None -> ()
-  | Some r ->
-      let r' = ref Unchanged in
-      r := Change (ch, r');
-      Weak.set trail 0 (Some r')
-
 let log_type ty =
   if ty.id <= !last_snapshot then log_change (Ctype (ty, ty.desc))
 let link_type ty ty' =
@@ -725,19 +727,3 @@ let undo_compress (changes, old) =
 	    ty.desc <- desc; r := !next
 	| _ -> ())
 	log
-
-let rec repr_link n t d =
- function
-   {desc = Tlink t' as d'} ->
-     repr_link (succ n) t d' t'
- | {desc = Tfield (_, k, _, t') as d'} when field_kind_repr k = Fabsent ->
-     repr_link (succ n) t d' t'
- | t' ->
-     if n > 1 then begin
-       log_change (Ccompress (t, t.desc, d)); t.desc <- d
-     end;
-     t'
-
-let () = repr_link' := repr_link
-
-let repr t = repr_link 0 t t.desc t
diff --git a/typing/typecore.ml b/typing/typecore.ml
index 02354ac9b377..7d4fdf186810 100644
--- a/typing/typecore.ml
+++ b/typing/typecore.ml
@@ -3670,9 +3670,8 @@ and type_statement env sexp =
 and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   (* ty_arg is _fully_ generalized *)
   let patterns = List.map (fun {pc_lhs=p} -> p) caselist in
-  let erase_either =
-    List.exists contains_polymorphic_variant patterns
-    && contains_variant_either ty_arg
+  let contains_polyvars = List.exists contains_polymorphic_variant patterns in
+  let erase_either = contains_polyvars && contains_variant_either ty_arg
   and has_gadts = List.exists (contains_gadt env) patterns in
 (*  prerr_endline ( if has_gadts then "contains gadt" else "no gadt"); *)
   let ty_arg =
@@ -3696,7 +3695,18 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   in
 (*  if has_gadts then
     Format.printf "lev = %d@.%a@." lev Printtyp.raw_type_expr ty_res; *)
-  begin_def (); (* propagation of the argument *)
+  (* Do we need to propagate polymorphism *)
+  let propagate =
+    !Clflags.principal || do_init || (repr ty_arg).level = generic_level ||
+    let rec is_var spat =
+      match spat.ppat_desc with
+        Ppat_any | Ppat_var _ -> true
+      | Ppat_alias (spat, _) -> is_var spat
+      | _ -> false in
+    match caselist with
+      [{pc_lhs}] when is_var pc_lhs -> false
+    | _ -> true in
+  if propagate then begin_def (); (* propagation of the argument *)
   let ty_arg' = newvar () in
   let pattern_force = ref [] in
 (*  Format.printf "@[%i %i@ %a@]@." lev (get_current_level())
@@ -3740,11 +3750,15 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
   (* `Contaminating' unifications start here *)
   List.iter (fun f -> f()) !pattern_force;
   (* Post-processing and generalization *)
-  List.iter (iter_pattern (fun {pat_type=t} -> unify_var env t (newvar())))
-    patl;
-  List.iter (fun pat -> unify_pat env pat (instance env ty_arg)) patl;
-  end_def ();
-  List.iter (iter_pattern (fun {pat_type=t} -> generalize t)) patl;
+  let unify_pats ty = List.iter (fun pat -> unify_pat env pat ty) patl in
+  if propagate then begin
+    List.iter
+      (iter_pattern (fun {pat_type=t} -> unify_var env t (newvar()))) patl;
+    unify_pats (instance env ty_arg);
+    end_def ();
+    List.iter (iter_pattern (fun {pat_type=t} -> generalize t)) patl;
+  end
+  else if erase_either then unify_pats (instance env ty_arg);
   (* type bodies *)
   let in_function = if List.length caselist = 1 then in_function else None in
   let cases =
@@ -3789,14 +3803,19 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
     else
       Partial
   in
-  let ty_arg_check =
-    (* Hack: use for_saving to copy variables too *)
-    Subst.type_expr (Subst.for_saving Subst.identity) ty_arg in
-  add_delayed_check
-    (fun () ->
-      List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
-        pat_env_list;
-      check_unused ~lev env (instance env ty_arg_check) cases);
+  let unused_check ty_arg () =
+    List.iter (fun (pat, (env, _)) -> check_absent_variant env pat)
+      pat_env_list;
+    check_unused ~lev env (instance env ty_arg) cases
+  in
+  if contains_polyvars then
+    let ty_arg_check =
+      (* Hack: use for_saving to copy variables too *)
+      Subst.type_expr (Subst.for_saving Subst.identity) ty_arg in
+    add_delayed_check (unused_check ty_arg_check)
+  else
+    unused_check ty_arg ();
+  (* Check for unused cases, do not delay because of gadts *)
   if do_init then begin
     end_def ();
     (* Ensure that existential types do not escape *)