From 6a1750e1e980733316c22ed3792cdd3b4fa4989a Mon Sep 17 00:00:00 2001 From: Christoph Knittel Date: Sat, 7 Nov 2026 10:05:37 +0000 Subject: [PATCH] Expand chains of type aliases without repeated occur checks MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Why: Each alias in `type t1<'a> = t0<('a, int)>`, `type t2<'a> = t1<('a, int)>`, … was checked by expanding the whole chain several times, and every expansion step ran occur checks over arguments that grow along the chain: 200 aliases allocated 850M words and took 1.6 s. They now allocate 19M words and take 0.15 s. Binding the fresh parameters of an expanded alias skips the occur check, since nothing can contain them yet. The constraint check skips type constructors whose parameters are distinct variables, which accept any arguments, and the cycle check forgets the expansions it memorized. Review: What remains superlinear? Expansions memorize each alias in one list shared along the chain, and looking an alias up scans it, a small cubic term: 800 aliases take 6.7 s, 290M words. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kbf3gK1dcjbe97yY1wRMgs Signed-off-by: Christoph Knittel --- changes/type-alias-chain.polish.md | 1 + compiler/ml/ctype.ml | 57 +++++++++++++++---- compiler/ml/typedecl.ml | 32 ++++++++--- .../constraint_failed_recursive.res.expected | 10 ++++ .../fixtures/constraint_failed_recursive.res | 2 + 5 files changed, 84 insertions(+), 18 deletions(-) create mode 100644 changes/type-alias-chain.polish.md create mode 100644 tests/build_tests/super_errors/expected/constraint_failed_recursive.res.expected create mode 100644 tests/build_tests/super_errors/fixtures/constraint_failed_recursive.res diff --git a/changes/type-alias-chain.polish.md b/changes/type-alias-chain.polish.md new file mode 100644 index 0000000000..41bf72972d --- /dev/null +++ b/changes/type-alias-chain.polish.md @@ -0,0 +1 @@ +- Speed up type checking of long chains of parameterized type aliases. diff --git a/compiler/ml/ctype.ml b/compiler/ml/ctype.ml index 4a3eabb159..ee2376e15d 100644 --- a/compiler/ml/ctype.ml +++ b/compiler/ml/ctype.ml @@ -1118,9 +1118,28 @@ let instance_label fixed lbl = (**** Instantiation with parameter substitution ****) -let unify' = +let unify_var' = (* Forward declaration *) - ref (fun _env _ty1 _ty2 -> raise (Unify [])) + ref (fun ~fresh:_ _env _ty1 _ty2 -> raise (Unify [])) + +(* Whether the instantiated parameters [params'] of [params] are + distinct variables created by the instantiation, which no other type + can contain yet. A parameter that is not generic is not copied, and a + constrained parameter can be a type that contains another one. *) +let fresh_params params params' = + let rec distinct = function + | [] -> true + | p :: rest -> (not (List.memq p rest)) && distinct rest + in + List.for_all2 + (fun p p' -> + p' != repr p + && + match p'.desc with + | Tvar _ -> true + | _ -> false) + params params' + && distinct params' let subst env level priv abbrev ty params args body = if List.length params <> List.length args then raise (Unify []); @@ -1138,8 +1157,13 @@ let subst env level priv abbrev ty params args body = abbreviations () := abbrev; let params', body' = instance_parameterized_type params body in abbreviations () := ref Mnil; - !unify' env body0 body'; - List.iter2 (!unify' env) params' args; + !unify_var' ~fresh:false env body0 body'; + (* Fresh parameters can't occur in the arguments, so binding them + needs no occur check. The check would traverse each argument, and + expanding a chain of aliases whose arguments grow at each step + would become quadratic. *) + let fresh = fresh_params params params' in + List.iter2 (!unify_var' ~fresh env) params' args; current_level () := old_level; body' with Unify _ as exn -> @@ -2660,16 +2684,19 @@ let unify_gadt ~newtype_level:lev (env : Env.t ref) ty1 ty2 = Type_pairs.clear (unify_eq_set ()); raise e -let unify_var env t1 t2 = +(* [fresh]: [t1] is a variable that [t2] can't contain, so the occur + checks are skipped. *) +let unify_var ~fresh env t1 t2 = let t1 = repr t1 and t2 = repr t2 in if t1 == t2 then () else match (t1.desc, t2.desc) with - | Tvar _, Tconstr _ when deep_occur t1 t2 -> unify (ref env) t1 t2 + | Tvar _, Tconstr _ when (not fresh) && deep_occur t1 t2 -> + unify (ref env) t1 t2 | Tvar _, _ -> ( let reset_tracing = check_trace_gadt_instances env in try - occur env t1 t2; + if not fresh then occur env t1 t2; update_level env t1.level t2; link_type t1 t2; reset_trace_gadt_instances reset_tracing @@ -2679,7 +2706,9 @@ let unify_var env t1 t2 = raise (Unify expanded_trace)) | _ -> unify (ref env) t1 t2 -let _ = unify' := unify_var +let _ = unify_var' := unify_var + +let unify_var env t1 t2 = unify_var ~fresh:false env t1 t2 let unify_pairs env ty1 ty2 pairs = current_univar_pairs () := pairs; @@ -4179,14 +4208,20 @@ let cyclic_abbrev env id ty = (match p with | Path.Pident p -> Ident.same p id | _ -> false) - || List.memq ty seen + || Type_set.mem ty seen || - try check_cycle (ty :: seen) (expand_abbrev_opt env ty) with + try check_cycle (Type_set.add ty seen) (expand_abbrev_opt env ty) with | Cannot_expand -> false | Unify _ -> true) | _ -> false in - check_cycle [] ty + let cyclic = check_cycle Type_set.empty ty in + (* The check expands the whole chain of abbreviations, and all the + expansions would stay memorized in the types of the declaration, + making each later traversal of them (generalization, for example) + go over the whole chain again. *) + cleanup_abbrev (); + cyclic (* Check for non-generalizable type variables *) exception Non_closed0 diff --git a/compiler/ml/typedecl.ml b/compiler/ml/typedecl.ml index 2ffd1258d7..78db6ce506 100644 --- a/compiler/ml/typedecl.ml +++ b/compiler/ml/typedecl.ml @@ -800,6 +800,20 @@ let generalize_decl decl = module Type_set = Btype.Type_set module Type_map = Btype.Type_map +(* Whether the parameters of [path] are distinct variables, so that the + constructor accepts any arguments. *) +let has_unconstrained_params env path = + match Env.find_type path env with + | decl -> + let params = List.map Ctype.repr decl.type_params in + let rec distinct_vars = function + | [] -> true + | p :: rest -> + Btype.is_Tvar p && (not (List.memq p rest)) && distinct_vars rest + in + distinct_vars params + | exception Not_found -> false + let rec check_constraints_rec env loc visited ty = let ty = Ctype.repr ty in if Type_set.mem ty !visited then () @@ -807,13 +821,17 @@ let rec check_constraints_rec env loc visited ty = visited := Type_set.add ty !visited; match ty.desc with | Tconstr (path, args, _) -> - let args' = List.map (fun _ -> Ctype.newvar ()) args in - let ty' = Ctype.newconstr path args' in - (try Ctype.enforce_constraints env ty' with - | Ctype.Unify _ -> assert false - | Not_found -> raise (Error (loc, Unavailable_type_constructor path))); - if not (Ctype.matches env ty ty') then - raise (Error (loc, Constraint_failed (ty, ty'))); + (* Unifying with the constrained instance expands both types fully, + which is costly for long chains of aliases. Without constraints + every instance matches. *) + if not (has_unconstrained_params env path) then ( + let args' = List.map (fun _ -> Ctype.newvar ()) args in + let ty' = Ctype.newconstr path args' in + (try Ctype.enforce_constraints env ty' with + | Ctype.Unify _ -> assert false + | Not_found -> raise (Error (loc, Unavailable_type_constructor path))); + if not (Ctype.matches env ty ty') then + raise (Error (loc, Constraint_failed (ty, ty')))); List.iter (check_constraints_rec env loc visited) args | Tpoly (ty, tl) -> let _, ty = Ctype.instance_poly ~fixed:false tl ty in diff --git a/tests/build_tests/super_errors/expected/constraint_failed_recursive.res.expected b/tests/build_tests/super_errors/expected/constraint_failed_recursive.res.expected new file mode 100644 index 0000000000..64cf97cb74 --- /dev/null +++ b/tests/build_tests/super_errors/expected/constraint_failed_recursive.res.expected @@ -0,0 +1,10 @@ + + We've found a bug for you! + /.../fixtures/constraint_failed_recursive.res:2:11-19 + + 1 │ type rec t<'a> = 'a constraint 'a = int + 2 │ and bad = t + 3 │ + + Constraints are not satisfied in this type. + Type t should be an instance of t \ No newline at end of file diff --git a/tests/build_tests/super_errors/fixtures/constraint_failed_recursive.res b/tests/build_tests/super_errors/fixtures/constraint_failed_recursive.res new file mode 100644 index 0000000000..042ab6960f --- /dev/null +++ b/tests/build_tests/super_errors/fixtures/constraint_failed_recursive.res @@ -0,0 +1,2 @@ +type rec t<'a> = 'a constraint 'a = int +and bad = t