Opaque signature matching is too permissive

Version

110.99.5 (Latest)

Operating System

[X] Any
[ ] Linux
[ ] macOS
[ ] Windows
[ ] Other Unix

OS Version

No response

Processor

[X] Any
[ ] Arm (using Rosetta)
[ ] PowerPC
[ ] Sparc
[ ] x86 (32-bit)
[ ] x86-64 (64-bit)
[ ] Other

System Component

Core system

Severity

Minor

Description

SML/NJ does not properly make types abstract when returned from functors.

Transcript

signature SIG = sig type t end

functor Id(X : SIG) :> SIG = X

structure T = struct type t = int end

structure R = Id(T)

val x : R.t = 1

- use "bad.sml";
[opening bad.sml]
signature SIG = sig
  type t
end
functor Id(X: sig
  type t
end) : sig
  type t
end
structure T : sig
  type t = int
end
structure R : SIG
val x = 1 : T.t
-

Expected Behavior

From the SML '97 definition:

Types which are specified as “abstract” in a opaque functor result signa- ture give rise to generation of fresh type names upon each application of the functor, even if the functor body is a constant structure. For example, after the elaboration of structure A = struct type t = int end functor f():> sig type t end = A structure B = f() and C = f(); the two types B.t and C.t are different

- use "bad.sml";
bad.sml:10.5-10.17 Error: pattern and expression in val dec do not agree [overload - bad instantiation]
  pattern:    R.t
  expression:    'Z[INT]
  in declaration:
    x : R.t = 1

Steps to Reproduce

Just type the code snippet

Additional Information

This code is correctly rejected by MLton with the error message:

Pattern and expression disagree.
    pattern:    [R.t]
    expression: [int]
    in: val x: R.t = 1

This code is correctly rejected by PolyML with the error message:

bad.sml:10: error: Pattern and expression have incompatible types.
Pattern: x : R.t : R.t
Expression: 1 : int
Reason:
  Can't unify int (*In Basis*) with
     R.t (*Created from applying functor Id*)
     (Different type constructors)
Found near val x : R.t = 1
Exception- Fail "Static Errors" raised

This code is correctly rejected by Moscow ML with the error message:

File "bad.sml", line 10, characters 14-15:
! val x : R.t = 1
!               ^
! Type clash: expression of type
!   int
! cannot have type
!   t

This code is correctly rejected by MLKit with the error message:

bad.sml, line 10, column 4:
  val x : R.t = 1
      ^^^^^^^^^^^
Type clash,
   type of left-hand side pattern:     t
   type of right-hand side expression: int

This error was the source of a bug in one of our research projects, detected after type-checking with a different compiler.

Email address

skyler DOT soss AT gmail.com

This is a duplicate of Issue #273 in the smlnj (Development) repository. I did some work on this. Here is a copy of the comment I submitted for #273:

I have done some preliminary work on this bug in the legacy version of the compiler. I thought that it might have a fairly trivial fix, but this turns out not to be the case. One complication is that it interacts with the hack I used to implement curried functors. The other problem is that it seems to be happening in the "entity function" that is produced during elaboration of functor declarations. In the Legacy version, the diagnostic messages that are implemented in the compiler/Elaborator/elabmod.sml file do not show what is going on with the entity function, and it is painful to fix or extend the diagnostic messages in the Legacy version. So I propose to get back to debugging this problem once I can do so in my newpp branch of the "development" version (smlnj/smlnj).

Since a new bug report for this problem has been submitted, I will raise the urgency of the bug and will do further work toward a fix. As the #273 comment indicates, the fix involves some fairly deep analysis and relates to the rather ad hoc approach to supporting curried functors and requires further debugging infrastructure related to entity functions in the module implementation. (Eventually this is going to all be reworked, so the fix will likely be specific to the current implementation with all its flaws and limitations.)

See further comments for Issue #273 under smlnj/smlnj.

smlnj / legacy