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