`Unsafe.cast` causes Compiler bug

[Skyb0rg007]

Version

110.99.7.1 (Latest)

Operating System

• Any
• Linux
• macOS
• Windows
• Other Unix

OS Version

Ubuntu on WSL2

Processor

• Any
• Arm (using Rosetta)
• PowerPC
• Sparc
• x86 (32-bit)
• x86-64 (64-bit)
• Other

System Component

Core system

Severity

Minor

Description

Using Unsafe.cast to implement polymorphic recursion cases the error Error: Compiler bug: Contract: UsageMap on v358 on current version of SML/NJ.
See gist here

Transcript

$  sml < val-rec-polyrec2.sml
Standard ML of New Jersey [Version 110.99.7.1; 64-bit; January 17, 2025]
- = [autoloading]
[library $SMLNJ-BASIS/basis.cm is stable]
[library $SMLNJ-BASIS/(basis.cm):basis-common.cm is stable]
[autoloading done]
Error: Compiler bug: Contract: UsageMap on v358
...

Expected Behavior

$ /usr/bin/sml < val-rec-polyrec2.sml
Standard ML of New Jersey v110.79 [built: Sat Oct 26 12:27:04 2019]
- = [autoloading]
[library $SMLNJ-BASIS/basis.cm is stable]
[library $SMLNJ-BASIS/(basis.cm):basis-common.cm is stable]
[autoloading done]
datatype 'a nested = Epsilon | Nest of 'a * 'a list nested
val sumListWith = fn : ('a -> int) -> 'a list -> int
val go = fn : ('a -> int) * 'a nested * int -> int
val sum = fn : int nested -> int
val nested = Nest (1,Nest ([#,#,#],Nest #)) : int nested
val nestedSum = 45 : int

Steps to Reproduce

See gist

Additional Information

No response

Email address

skyler DOT soss AT gmail DOT com

[Skyb0rg007]

This seems to be trigged by Unsafe.cast-ing a function: I can remove the error by changing:

val go' = Unsafe.cast go (* Compiler bug *)
fun go' args = go (Unsafe.cast args) (* Compiler bug *)
fun go' (f, n, i) = go (Unsafe.cast f, Unsafe.cast n, i) (* Compiler bug *)

into

fun go' (f, n, i) = go (f o Unsafe.cast, Unsafe.cast n, i) (* Okay *)

[dmacqueen]

Not surprised that you can cause a compiler bug using Unsafe.cast!

Did you know that you can define a Y combinator in SML with the
aid of a recursive type similar to

datatype t = T of t -> t

?

That is, iso-recursive types are powerful enough to define a
useable form of Y combinator. One might think that equi-recrusive types are needed for this (e.g. \mu t. t -> t).

So the SML type system is actually powerful enough that recursion is derivable.

[JohnReppy]

This looks to be a bug in CPS contraction that results in a variable escaping the scope of its binding.

[Skyb0rg007]

@dmacqueen

So the SML type system is actually powerful enough that recursion is derivable.

Yes, but not powerful enough to derive polymorphic recursion like the example in the gist.
I haven't played around with it, but maybe one could implement it using SML/NJ's functor extensions. It's possible with recursive modules (ex. as supported by Moscow ML).
Eventually I can try and expose the full System Fω to the surface language as it's supposedly supported by FLINT, but that's a PR for another day.

[JohnReppy]

I believe that I understand the cause of this bug. It has to do with being a bit overaggressive about the cast operation. I need to think a bit about what the best solution is.

[JohnReppy]

I have fixed this issue for 110.99.8 by treating CAST as an opaque operation in the optimizer. This change may cost some optimization opportunities, but it should avoid downstream breakage.