REML signature matching by melsman · Pull Request #204 · melsman/mlkit

melsman · 2026-02-12T11:17:49Z

Make it possible to specify REML types in signatures and have them checked against an implementation.

Copilot

Pull request overview

This pull request implements REML signature matching, enabling the compiler to check that REML types specified in signatures match their implementations during transparent signature matching. The implementation adds a new CHECK_REML lambda expression construct that performs bidirectional type checking to ensure type schemes are compatible.

Changes:

Introduces CHECK_REML lambda expression construct for runtime type scheme validation during transparent signature matching
Updates the constrain function in CompilerEnv to identify and return type schemes containing region variables that require checking
Adds comprehensive handling of CHECK_REML throughout the lambda compilation pipeline (traversal functions, optimizer, type checker)

Reviewed changes

Copilot reviewed 28 out of 28 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/Compiler/Lambda/LambdaExp.sml	Adds CHECK_REML constructor and helper functions (contains_regvars, regvarsType) to Lambda expression type
src/Compiler/Lambda/LAMBDA_EXP.sml	Adds CHECK_REML to signature with helper functions for region variable extraction
src/Compiler/Regions/SpreadExpression.sml	Implements CHECK_REML type checking logic with bidirectional unification and error reporting
src/Compiler/Lambda/CompilerEnv.sml	Updates constrain to collect type schemes needing checks and return them for CHECK_REML generation
src/Compiler/Lambda/COMPILER_ENV.sml	Updates constrain signature to return check list
src/Compiler/Lambda/CompileDec.sml	Generates CHECK_REML expressions for transparent signature constraints
src/Manager/IntModules.sml	Updates constrain calls to handle new return signature
src/Compiler/Lambda/OptLambda.sml	Adds CHECK_REML handling in optimizer passes (lvar tracking, inlining checks)
src/Compiler/Lambda/LambdaStatSem.sml	Adds type checking for CHECK_REML expressions
src/Compiler/Lambda/LambdaBasics.sml	Adds CHECK_REML cases to all lambda traversal functions
src/Compiler/Lambda/EliminateEq.sml	Adds CHECK_REML handling in equality elimination pass
src/Compiler/Regions/RType.sml	Improves error handling to preserve DeepError exceptions during unification
src/Compiler/Regions/RTYPE.sig	Fixes typo in comment ("iff on" -> "iff one")
src/Tools/Tester/Tester.sml	Adds support for "noopt" test flag to disable optimizer
test/explicit_regions/mod.sml	Test case showing implementation type less general than specification
test/explicit_regions/mod2.sml	Test case showing specification type less general than implementation
test/explicit_regions/mod3.sml	Test case with implicit vs explicit region variables
test/explicit_regions/*.log.ok	Expected compiler output for new test cases
test/explicit_regions/all.tst	Adds new test entries and standardizes test flags
test/explicit_regions/Makefile	Updates FLAGS and adds new test sources
src/Common/*.sml	Removes trailing semicolons from signature definitions for consistency

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-02-12T11:23:31Z

test/explicit_regions/mod.sml

@@ -0,0 +1,12 @@
+(* Transparent signature matching: It is checked that the type of an implementation is
+ * is at least as general as the specified type. *)


The comment has a duplicate word "is". The sentence reads "the type of an implementation is is at least as general" but should read "the type of an implementation is at least as general".

Suggested change

* is at least as general as the specified type. *)

* at least as general as the specified type. *)

Copilot · 2026-02-12T11:23:32Z

test/explicit_regions/mod3.sml

@@ -0,0 +1,12 @@
+(* Transparent signature matching: It is checked that the type of an implementation is
+ * is at least as general as the specified type. *)


The comment has a duplicate word "is". The sentence reads "the type of an implementation is is at least as general" but should read "the type of an implementation is at least as general".

Suggested change

* is at least as general as the specified type. *)

* at least as general as the specified type. *)

Copilot · 2026-02-12T11:23:32Z

test/explicit_regions/Makefile

 SMLSOURCES=er*.sml param.sml rec.sml tup.sml call.sml call2.sml ty1.sml err_expty1.sml err_expty2.sml \
  err_expty3.sml err_patty1.sml err_funty1.sml err_funty2.sml err_funty3.sml expty1.sml expty2.sml \
-  disputs.sml disputs2.sml server.sml
+  disputs.sml disputs2.sml server.sml mod.sml mod2.sml


The test file mod3.sml is included in the test suite (all.tst line 91) but is missing from the SMLSOURCES variable in the Makefile. This means that mod3.sml won't be included when generating all.sml for combined testing. Add "mod3.sml" to the SMLSOURCES list on line 6.

Suggested change

disputs.sml disputs2.sml server.sml mod.sml mod2.sml

disputs.sml disputs2.sml server.sml mod.sml mod2.sml mod3.sml

Copilot · 2026-02-12T11:23:32Z

test/explicit_regions/all.tst

+mod.sml               ccl ecte                 (* Transparent signature matching: spec type at least as general as impl type *)
+mod2.sml              ccl ecte                 (* Transparent signature matching: impl type at least as general as spec type *)
+mod3.sml              ccl ecte                 (* Transparent signature matching: impl type at least as general as spec type *)


The FLAGS variable no longer includes "-no_basislib -no_opt" which were previously present. However, these flags are still explicitly specified for individual test files in all.tst (as "nobasislib noopt"). The new module signature matching tests (mod.sml, mod2.sml, mod3.sml) on lines 89-91 of all.tst don't include these flags. For consistency with other tests in the file, consider adding "nobasislib noopt" to these three test entries, or explain why these tests require the basis library and optimizer.

Suggested change

mod.sml ccl ecte (* Transparent signature matching: spec type at least as general as impl type *)

mod2.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *)

mod3.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *)

mod.sml ccl ecte nobasislib noopt (* Transparent signature matching: spec type at least as general as impl type *)

mod2.sml ccl ecte nobasislib noopt (* Transparent signature matching: impl type at least as general as spec type *)

mod3.sml ccl ecte nobasislib noopt (* Transparent signature matching: impl type at least as general as spec type *)

Copilot

Pull request overview

Copilot reviewed 36 out of 36 changed files in this pull request and generated 5 comments.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-02-13T20:07:07Z

test/explicit_regions/all.tst

+mod.sml               ccl ecte                   (* Transparent signature matching: spec type at least as general as impl type *)
+mod2.sml              ccl ecte                   (* Transparent signature matching: impl type at least as general as spec type *)
+mod3.sml              ccl ecte                   (* Transparent signature matching: impl type at least as general as spec type *)
+mod4.sml              ccl ecte
+mod5.sml                                         (* ok matching *)


All other tests in this file run with "noopt" to keep compilation deterministic, but the new mod*.sml entries omit it. If the optimiser affects typing/log output for these cases, the expected *.log.ok files may become brittle. Consider adding "noopt" to mod.sml–mod5.sml entries for consistency and stability (while keeping basislib enabled as needed).

Suggested change

mod.sml ccl ecte (* Transparent signature matching: spec type at least as general as impl type *)

mod2.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *)

mod3.sml ccl ecte (* Transparent signature matching: impl type at least as general as spec type *)

mod4.sml ccl ecte

mod5.sml (* ok matching *)

mod.sml ccl ecte noopt (* Transparent signature matching: spec type at least as general as impl type *)

mod2.sml ccl ecte noopt (* Transparent signature matching: impl type at least as general as spec type *)

mod3.sml ccl ecte noopt (* Transparent signature matching: impl type at least as general as spec type *)

mod4.sml ccl ecte noopt

mod5.sml noopt (* ok matching *)

Copilot · 2026-02-13T20:07:08Z

.github/workflows/main.yml

          mkdir phantomjs
          cd phantomjs
-          wget -q https://bitbucket.org/ariya/phantomjs/downloads/phantomjs-2.1.1-linux-x86_64.tar.bz2
+          wget -q https://github.com/melsman/phantomjs-bin/raw/refs/heads/main/phantomjs-2.1.1-linux-x86_64.tar.bz2


The PhantomJS download URL is pinned to the moving branch ref "/refs/heads/main/". That can break CI if the upstream repository changes history or the file is moved. Prefer pinning to an immutable commit SHA or a versioned release artifact, and ideally verify with a checksum.

Suggested change

wget -q https://github.com/melsman/phantomjs-bin/raw/refs/heads/main/phantomjs-2.1.1-linux-x86_64.tar.bz2

wget -q https://github.com/melsman/phantomjs-bin/releases/download/v2.1.1/phantomjs-2.1.1-linux-x86_64.tar.bz2

Copilot · 2026-02-13T20:07:08Z

src/Tools/Tester/Tester.sml

 	val compile_command_base = kitexe ^
          (if !logdirect then " " else " --log_to_file ") ^
 	  (if opt "nobasislib" then "-no_basislib " else "") ^
+          (if opt "noopt" then "-no_opt " else "") ^
 	  (if opt "tc" (*Time Compiler*) then "--timings " else "") ^


The tester only recognizes the new token "noopt". The repo still contains .tst files using the documented token "nooptimiser" (e.g., test/all.tst, test/parallelism/all.tst), so those tests will not actually disable the optimiser. Consider supporting both tokens (treat "nooptimiser" as an alias of "noopt") to keep existing tests and documentation working.

Copilot · 2026-02-13T20:07:08Z

src/Compiler/Lambda/LambdaExp.sml

          | TYPED (lamb,_,_)            => safe raiseOk lamb
          | PRIM(prim,lambs)            => (safe_prim prim; app (safe raiseOk) lambs)
          | FRAME _                     => ()
+          | CHECK_REML _                => raise NotSafe


CHECK_REML is treated as unsafe here. Since safeLambdaExp is used by the optimiser and link-time discharge logic, marking CHECK_REML as unsafe can prevent the optimiser from dropping the injected let _ = CHECK_REML ... wrappers, allowing CHECK_REML to reach backends (notably the JS backend) and fail compilation. CHECK_REML is intended as a compile-time/type-check-only node, so it should be considered safe (or eliminated before optimisation/backend).

Suggested change

| CHECK_REML _ => raise NotSafe

| CHECK_REML _ => ()

Copilot · 2026-02-13T20:07:09Z

src/Compiler/Backend/JS/ExpToJs2.sml

    end
  | L.RAISE (e,_) => resolveS (toj1 C P e) (fn e' => fn k => J.Throw e')
  | L.TYPED (e,_,_) => toj C P e
+  | L.CHECK_REML _ => die "REML check not supported by JS backend"


The JS backend currently aborts on CHECK_REML. CHECK_REML nodes are injected during transparent signature constraints for explicit-region types, and JS compilation goes through CompileToLamb without running the regions/SpreadExpression pass that eliminates CHECK_REML. This makes such programs fail with an internal error. Consider compiling CHECK_REML as a no-op (unit) or ensuring CHECK_REML is eliminated earlier in the JS pipeline after the static check has been performed.

Suggested change

| L.CHECK_REML _ => die "REML check not supported by JS backend"

| L.CHECK_REML _ => E junit

progress

9972db2

Copilot AI review requested due to automatic review settings February 12, 2026 11:17

melsman self-assigned this Feb 12, 2026

Copilot started reviewing on behalf of melsman February 12, 2026 11:18 View session

melsman added enhancement reml Work particularly related to REML labels Feb 12, 2026

Copilot AI reviewed Feb 12, 2026

View reviewed changes

melsman added 17 commits February 12, 2026 12:23

fix js backend

6686017

fixes of typos in tests

7018882

fix action

dc52953

fix action

f21fc9f

fix action

8d56ac5

fix action

55b89e6

fix action

163cd34

fix action

a7f0d48

fix action

8494bea

fix action

23e7bf3

fix action

1dcc993

fix action

42175d7

fix action

e1cfaf7

fix action

faed872

fix action

32e3a25

fix action

43c4178

fixes

4d95a92

melsman requested a review from Copilot February 13, 2026 19:52

Copilot started reviewing on behalf of melsman February 13, 2026 19:53 View session

Copilot AI reviewed Feb 13, 2026

View reviewed changes

melsman merged commit 341aac4 into master Feb 13, 2026
10 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

REML signature matching#204

REML signature matching#204
melsman merged 18 commits intomasterfrom
reml-sigmatch

melsman commented Feb 12, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Feb 12, 2026

Uh oh!

Copilot AI Feb 12, 2026

Uh oh!

Copilot AI Feb 12, 2026

Uh oh!

Copilot AI Feb 12, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Feb 13, 2026

Uh oh!

Copilot AI Feb 13, 2026

Uh oh!

Copilot AI Feb 13, 2026

Uh oh!

Copilot AI Feb 13, 2026

Uh oh!

Copilot AI Feb 13, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

		@@ -0,0 +1,12 @@
		(* Transparent signature matching: It is checked that the type of an implementation is
		* is at least as general as the specified type. *)

	* is at least as general as the specified type. *)
	* at least as general as the specified type. *)

	disputs.sml disputs2.sml server.sml mod.sml mod2.sml
	disputs.sml disputs2.sml server.sml mod.sml mod2.sml mod3.sml

	wget -q https://github.com/melsman/phantomjs-bin/raw/refs/heads/main/phantomjs-2.1.1-linux-x86_64.tar.bz2
	wget -q https://github.com/melsman/phantomjs-bin/releases/download/v2.1.1/phantomjs-2.1.1-linux-x86_64.tar.bz2

	\| L.CHECK_REML _ => die "REML check not supported by JS backend"
	\| L.CHECK_REML _ => E junit

Conversation

melsman commented Feb 12, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Feb 12, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 12, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 12, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 12, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Feb 13, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant