From 847f3fe67e2226ceed97778395942ff9e38792b3 Mon Sep 17 00:00:00 2001
From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 18 May 2026 03:49:04 +0100
Subject: [PATCH] fix(typecheck): instantiate constructor schemes per use-site
 in patterns (#128)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

check_pattern's PatCon read the monomorphic constructor_env entry and
wrapped it as a 0-tyvar scheme, so every occurrence of a constructor
shared one set of type variables. Two `Ok(_)` patterns in a single
match (e.g. result.affine `apply`'s tuple match) thus forced both
payloads to the same type, yielding `Unify ((_ -> _), T)`.

Now prefer the polymorphic scheme bound in name_types (set via
bind_scheme for builtin Ok/Err/Some/None/RuntimeError and user
variants) and instantiate it fresh per occurrence — exactly as
lookup_var does for ordinary identifiers — falling back to the
constructor_env entry only when no scheme is registered.

Correctness/soundness fix. Full suite 233/233, zero regression.
(result.affine remains blocked on a separate import-path issue:
imported parametric ctor schemes are built with fresh_tyvar 0 then
generalize, a no-op at level 0 — tracked for the next slice.)
Refs #128.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 lib/typecheck.ml | 28 +++++++++++++++++++++++-----
 1 file changed, 23 insertions(+), 5 deletions(-)

diff --git a/lib/typecheck.ml b/lib/typecheck.ml
index 3de2e3d6..0cd344c6 100644
--- a/lib/typecheck.ml
+++ b/lib/typecheck.ml
@@ -488,11 +488,29 @@ let rec check_pattern (ctx : context) (pat : pattern) (expected : ty)
     let* bindings_list = check_patterns ctx pats elem_tys in
     Ok (List.concat bindings_list)
   | PatCon ({ name; _ }, sub_pats) ->
-    (* Look up the constructor type *)
-    begin match Hashtbl.find_opt ctx.constructor_env name with
-      | Some ctor_ty ->
-        let ctor_ty' = instantiate ctx.level
-          { sc_tyvars = []; sc_effvars = []; sc_rowvars = []; sc_body = ctor_ty } in
+    (* Resolve the constructor's type, freshly instantiated *per use-site*.
+       Prefer the polymorphic scheme bound in [name_types] (set via
+       [bind_scheme] for both builtin Ok/Err/Some/None/RuntimeError and
+       user-declared variants) so every occurrence gets independent type
+       variables — exactly as [lookup_var] does for ordinary identifiers.
+       Fall back to the monomorphic [constructor_env] entry only when no
+       scheme is registered. Previously this read [constructor_env] alone
+       and wrapped it as a 0-tyvar scheme, so all occurrences *shared* one
+       set of variables: two `Ok(_)` patterns in one match then forced both
+       payloads to the same type (`Unify ((_ -> _), T)` in result.affine). *)
+    let ctor_ty_opt =
+      match Hashtbl.find_opt ctx.name_types name with
+      | Some sc -> Some (instantiate ctx.level sc)
+      | None ->
+        (match Hashtbl.find_opt ctx.constructor_env name with
+         | Some ctor_ty ->
+           Some (instantiate ctx.level
+             { sc_tyvars = []; sc_effvars = []; sc_rowvars = [];
+               sc_body = ctor_ty })
+         | None -> None)
+    in
+    begin match ctor_ty_opt with
+      | Some ctor_ty' ->
         (* Constructor type should be T1 -> T2 -> ... -> ResultType *)
         let rec peel_arrows ty pats acc =
           match pats with