diff --git a/Changes b/Changes
index 0d543cf85..32996c727 100644
--- a/Changes
+++ b/Changes
@@ -76,6 +76,9 @@ Bug fixes:
   (Nicolas Braud-Santoni, report by Eric Cooper)
 - PR#4832: Filling bigarrays may block out runtime
   (Markus Mottl)
+- PR#5663: program rejected due to nongeneralizable type variable that
+    appears nowhere
+  (Jacques Garrigue, report by Stephen Weeks)
 - PR#5887: move the byterun/*.h headers to byterun/caml/*.h to avoid header
     name clashes
   (Jérôme Vouillon and Adrien Nader and Peter Zotov)
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 18b2ed3b5..69930774d 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -454,38 +454,6 @@ let rec filter_row_fields erase = function
                     (**************************************)
 
 
-exception Non_closed0
-
-let rec closed_schema_rec ty =
-  let ty = repr ty in
-  if ty.level >= lowest_level then begin
-    let level = ty.level in
-    ty.level <- pivot_level - level;
-    match ty.desc with
-      Tvar _ when level <> generic_level ->
-        raise Non_closed0
-    | Tfield(_, kind, t1, t2) ->
-        if field_kind_repr kind = Fpresent then
-          closed_schema_rec t1;
-        closed_schema_rec t2
-    | Tvariant row ->
-        let row = row_repr row in
-        iter_row closed_schema_rec row;
-        if not (static_row row) then closed_schema_rec row.row_more
-    | _ ->
-        iter_type_expr closed_schema_rec ty
-  end
-
-(* Return whether all variables of type [ty] are generic. *)
-let closed_schema ty =
-  try
-    closed_schema_rec ty;
-    unmark_type ty;
-    true
-  with Non_closed0 ->
-    unmark_type ty;
-    false
-
 exception Non_closed of type_expr * bool
 
 let free_variables = ref []
@@ -4205,6 +4173,40 @@ let cyclic_abbrev env id ty =
         false
   in check_cycle [] ty
 
+(* Check for non-generalizable type variables *)
+exception Non_closed0
+let visited = ref TypeSet.empty
+
+let rec closed_schema_rec env ty =
+  let ty = expand_head env ty in
+  if TypeSet.mem ty !visited then () else begin
+    visited := TypeSet.add ty !visited;
+    match ty.desc with
+      Tvar _ when ty.level <> generic_level ->
+        raise Non_closed0
+    | Tfield(_, kind, t1, t2) ->
+        if field_kind_repr kind = Fpresent then
+          closed_schema_rec env t1;
+        closed_schema_rec env t2
+    | Tvariant row ->
+        let row = row_repr row in
+        iter_row (closed_schema_rec env) row;
+        if not (static_row row) then closed_schema_rec env row.row_more
+    | _ ->
+        iter_type_expr (closed_schema_rec env) ty
+  end
+
+(* Return whether all variables of type [ty] are generic. *)
+let closed_schema env ty =
+  visited := TypeSet.empty;
+  try
+    closed_schema_rec env ty;
+    visited := TypeSet.empty;
+    true
+  with Non_closed0 ->
+    visited := TypeSet.empty;
+    false
+
 (* Normalize a type before printing, saving... *)
 (* Cannot use mark_type because deep_occur uses it too *)
 let rec normalize_type_rec env visited ty =
diff --git a/typing/ctype.mli b/typing/ctype.mli
index 7bec693d8..84e3f3ca3 100644
--- a/typing/ctype.mli
+++ b/typing/ctype.mli
@@ -245,7 +245,7 @@ val cyclic_abbrev: Env.t -> Ident.t -> type_expr -> bool
 val is_contractive: Env.t -> type_expr -> bool
 val normalize_type: Env.t -> type_expr -> unit
 
-val closed_schema: type_expr -> bool
+val closed_schema: Env.t -> type_expr -> bool
         (* Check whether the given type scheme contains no non-generic
            type variables *)
 
diff --git a/typing/typeclass.ml b/typing/typeclass.ml
index 0096628a7..27569bf0f 100644
--- a/typing/typeclass.ml
+++ b/typing/typeclass.ml
@@ -153,23 +153,26 @@ let rec abbreviate_class_type path params cty =
   | Cty_arrow (l, ty, cty) ->
       Cty_arrow (l, ty, abbreviate_class_type path params cty)
 
+(* Check that all type variables are generalizable *)
+(* Use Env.empty to prevent expansion of recursively defined object types;
+   cf. typing-poly/poly.ml *)
 let rec closed_class_type =
   function
     Cty_constr (_, params, _) ->
-      List.for_all Ctype.closed_schema params
+      List.for_all (Ctype.closed_schema Env.empty) params
   | Cty_signature sign ->
-      Ctype.closed_schema sign.csig_self
+      Ctype.closed_schema Env.empty sign.csig_self
         &&
-      Vars.fold (fun _ (_, _, ty) cc -> Ctype.closed_schema ty && cc)
+      Vars.fold (fun _ (_, _, ty) cc -> Ctype.closed_schema Env.empty ty && cc)
         sign.csig_vars
         true
   | Cty_arrow (_, ty, cty) ->
-      Ctype.closed_schema ty
+      Ctype.closed_schema Env.empty ty
         &&
       closed_class_type cty
 
 let closed_class cty =
-  List.for_all Ctype.closed_schema cty.cty_params
+  List.for_all (Ctype.closed_schema Env.empty) cty.cty_params
     &&
   closed_class_type cty.cty_type
 
diff --git a/typing/typemod.ml b/typing/typemod.ml
index fd8c6187c..53b402440 100644
--- a/typing/typemod.ml
+++ b/typing/typemod.ml
@@ -845,15 +845,19 @@ let rec path_of_module mexp =
 
 (* Check that all core type schemes in a structure are closed *)
 
-let rec closed_modtype = function
+let rec closed_modtype env = function
     Mty_ident p -> true
   | Mty_alias p -> true
-  | Mty_signature sg -> List.for_all closed_signature_item sg
-  | Mty_functor(id, param, body) -> closed_modtype body
+  | Mty_signature sg ->
+      let env = Env.add_signature sg env in
+      List.for_all (closed_signature_item env) sg
+  | Mty_functor(id, param, body) ->
+      let env = Env.add_module ~arg:true id (Btype.default_mty param) env in
+      closed_modtype env body
 
-and closed_signature_item = function
-    Sig_value(id, desc) -> Ctype.closed_schema desc.val_type
-  | Sig_module(id, md, _) -> closed_modtype md.md_type
+and closed_signature_item env = function
+    Sig_value(id, desc) -> Ctype.closed_schema env desc.val_type
+  | Sig_module(id, md, _) -> closed_modtype env md.md_type
   | _ -> true
 
 let check_nongen_scheme env str =
@@ -861,11 +865,11 @@ let check_nongen_scheme env str =
     Tstr_value(rec_flag, pat_exp_list) ->
       List.iter
         (fun {vb_expr=exp} ->
-          if not (Ctype.closed_schema exp.exp_type) then
+          if not (Ctype.closed_schema env exp.exp_type) then
             raise(Error(exp.exp_loc, env, Non_generalizable exp.exp_type)))
         pat_exp_list
   | Tstr_module {mb_expr=md;_} ->
-      if not (closed_modtype md.mod_type) then
+      if not (closed_modtype env md.mod_type) then
         raise(Error(md.mod_loc, env, Non_generalizable_module md.mod_type))
   | _ -> ()
 
@@ -1489,7 +1493,7 @@ let type_module_type_of env smod =
   (* PR#6307: expand aliases at root and submodules *)
   let mty = Mtype.remove_aliases env mty in
   (* PR#5036: must not contain non-generalized type variables *)
-  if not (closed_modtype mty) then
+  if not (closed_modtype env mty) then
     raise(Error(smod.pmod_loc, env, Non_generalizable_module mty));
   tmty, mty