Skip to content

Commit a3b1cae

Browse files
fix(typecheck): generalize parametric enum ctor schemes via shared param tyvars (#128) (#188)
register_type_decl's TyEnum branch built result_ty tyvars with an anonymous fresh_tyvar 0 and never bound the declared param names, so (a) field types and the result type used disconnected vars and (b) generalize was a no-op at level 0 -> imported parametric ctor schemes (prelude Ok/Err/Some) were monomorphic with shared vars, collapsing payload types across use-sites on the import path. Bind param names to fresh tyvars one level deeper so result and field types share them, generalize at the outer level, and scope the param names so they don't leak into sibling type decls. Fixes stdlib/result.affine; stdlib 14->15/19; 233/233 dune test, zero regression. Refs #128 Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent c332b60 commit a3b1cae

1 file changed

Lines changed: 35 additions & 21 deletions

File tree

lib/typecheck.ml

Lines changed: 35 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1527,35 +1527,49 @@ let register_type_decl (ctx : context) (td : type_decl) : unit result =
15271527
let* () = check_kind ctx ty KType in
15281528
Ok ty
15291529
| TyEnum variants ->
1530-
(* Register each variant as a constructor *)
1531-
let result_ty = match td.td_type_params with
1530+
(* Register each variant as a constructor.
1531+
1532+
Bind the declared type-param names (e.g. T, E) to fresh tyvars in
1533+
the type env so that BOTH the result type and the field types
1534+
resolve to the *same* variables (previously the result tyvars were
1535+
anonymous `fresh_tyvar 0` and each field `T` became its own
1536+
unrelated var via lower_type_expr's TyVar fallback).
1537+
1538+
The param tyvars are created one level deeper than the current
1539+
context so that `generalize` (which quantifies vars with
1540+
level > ctx.level) actually quantifies them — at level 0 it was a
1541+
no-op, leaving imported ctor schemes monomorphic with shared vars
1542+
(the import-path bug behind result.affine's Unify ((_->_), T)). *)
1543+
let param_names =
1544+
List.map (fun (tp : type_param) -> tp.tp_name.name) td.td_type_params
1545+
in
1546+
enter_level ctx;
1547+
let param_tvs = List.map (fun n ->
1548+
let tv = fresh_tyvar ctx.level in
1549+
Hashtbl.replace ctx.type_env n tv;
1550+
tv
1551+
) param_names in
1552+
let result_ty = match param_tvs with
15321553
| [] -> TCon td.td_name.name
1533-
| params ->
1534-
let tparams = List.map (fun tp ->
1535-
match tp.tp_name.name with
1536-
| _ ->
1537-
let tv = fresh_tyvar 0 in
1538-
(* Note: In a full impl we'd map param name to tv in a local env *)
1539-
tv
1540-
) params in
1541-
TApp (TCon td.td_name.name, tparams)
1554+
| tvs -> TApp (TCon td.td_name.name, tvs)
15421555
in
1543-
List.iter (fun (vd : variant_decl) ->
1556+
let ctors = List.map (fun (vd : variant_decl) ->
15441557
let ctor_ty = List.fold_right (fun field_te acc ->
15451558
TArrow (lower_type_expr ctx field_te, QOmega, acc, EPure)
15461559
) vd.vd_fields result_ty in
1547-
(* If it has type params, we should really bind a TForall scheme *)
1548-
let sc = match td.td_type_params with
1560+
(vd.vd_name.name, ctor_ty)
1561+
) variants in
1562+
exit_level ctx;
1563+
(* Don't let this decl's param names leak into sibling type decls. *)
1564+
List.iter (fun n -> Hashtbl.remove ctx.type_env n) param_names;
1565+
List.iter (fun (name, ctor_ty) ->
1566+
let sc = match param_names with
15491567
| [] -> { sc_tyvars = []; sc_effvars = []; sc_rowvars = []; sc_body = ctor_ty }
15501568
| _ -> generalize ctx ctor_ty
15511569
in
1552-
Hashtbl.replace ctx.constructor_env vd.vd_name.name ctor_ty;
1553-
(* Also bind as a variable for ExprVar references *)
1554-
if vd.vd_fields = [] then
1555-
bind_scheme ctx vd.vd_name.name sc
1556-
else
1557-
bind_scheme ctx vd.vd_name.name sc
1558-
) variants;
1570+
Hashtbl.replace ctx.constructor_env name ctor_ty;
1571+
bind_scheme ctx name sc
1572+
) ctors;
15591573
Ok (TCon td.td_name.name)
15601574
| TyExtern ->
15611575
(* Opaque host-supplied type. Register a TCon so user code can name it

0 commit comments

Comments
 (0)