Opaque signature matching is too permissive

[Skyb0rg007]

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