Uncaught Bind exception in compiler with opaque signature matching

[JohnReppy]

Version

110.99.4 (Latest)

Operating System

• Any
• Linux
• macOS
• Windows
• Other Unix

OS Version

No response

Processor

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

System Component

Core system

Severity

Minor

Description

The elaborator raises a Bind exception when dealing with a structure that has type errors and an opaque signature.

Transcript

% sml bug.sml
Standard ML of New Jersey (64-bit) v110.99.4 [built: Tue Aug 01 16:07:38 2023]
[opening bug.sml]
[autoloading]
[library $SMLNJ-BASIS/basis.cm is stable]
[library $SMLNJ-BASIS/(basis.cm):basis-common.cm is stable]
[autoloading done]
bug.sml:41.32-43.37 Error: types of rules do not agree [circularity]
  earlier rule(s): ('Z -> 'Y) result -> 'Y result
  this rule: ('Z -> 'Y) result -> ('Z -> 'Y) result
  in rule:
    err => err
bug.sml:1.2-52.6 Error: value type in structure does not match signature spec
    name: field
  spec:   string
           -> 'a ?.JSONDecode.decoder
           -> ('a -> 'b) ?.JSONDecode.decoder -> 'b ?.JSONDecode.decoder
  actual: string
           -> 'a ?.JSONDecode.decoder
           -> ('a -> 'a) ?.JSONDecode.decoder -> 'a ?.JSONDecode.decoder

uncaught exception Bind [nonexhaustive binding failure]
  raised at: ../compiler/Elaborator/elaborate/elabmod.sml:624.13-624.67
             ../compiler/Elaborator/elaborate/elabmod.sml:1363.32
             ../compiler/Basics/stats/stats.sml:198.40
             ../compiler/TopLevel/interact/evalloop.sml:45.54
             ../compiler/TopLevel/interact/evalloop.sml:306.20-306.23

Expected Behavior

There should not be an uncaught Bind exception.

Steps to Reproduce

Here is the source that reproduces the bug:

structure JSONDecode :> sig

    datatype 'a result = Err of exn | Ok of 'a

    type 'a decoder

    (* decode a required field *)
    val field : string -> 'a decoder -> ('a -> 'b) decoder -> 'b decoder

  end = struct

    datatype value
      = OBJECT of (string * value) list
      | ARRAY of value list
      | NULL
      | BOOL of bool
      | INT of IntInf.int
      | FLOAT of real
      | STRING of string

    exception FieldNotFound of value * string
    exception NotObject of value

    fun lookupField (v as OBJECT fields) = let
          fun find lab = (case List.find (fn (l, v) => (l = lab)) fields
                 of NONE => raise FieldNotFound(v, concat["no definition for field \"", lab, "\""])
                  | SOME(_, v) => v
                (* end case *))
          in
            find
          end
      | lookupField v = raise NotObject v

    datatype 'a result = Err of exn | Ok of 'a

    datatype 'a decoder = D of value -> 'a result

    (* decode a required field *)
    fun field key (D valueDecoder) (D objDecoder) = let
          fun decoder jv = (case valueDecoder (lookupField jv key)
                 of Ok fld => (case objDecoder jv
                       of Ok mkObj => Ok(mkObj fld)
                        | err => err
                      (* end case *))
                  | err => err
                (* end case *))
                  handle ex => Err ex
          in
            D decoder
          end

  end

Additional Information

Note that changing the :> to : for the signature ascription causes the bug to disappear.

Email address

jhr@cs.uchicago.edu

[dmacqueen]

This issue (bug) seems to be closely related to issue 285 (Bind exception after a static signature matching error). Here is a much simpler test case that produces the Bind exception behavior.

signature S = 
sig
  val f : 'a -> 'b
end;

structure A :> S =   (* opaque ascription required *)
struct
  fun f x = x
end;

[dmacqueen]

There is a fairly mild fix to elabmod.sml and sigmatch.sml involving having SigMatch.matchStr return an option result which would be NONE in the case that the signature match fails, instead of a "bogus" record. This fix eliminates the uncaught Bind exceptions in Issues $285 and #289, but it has an unexpected side effect of not allowing the legacy compiler to bootstrap with an unbound lambda var exception during the init phase when compiling dummy.sml. So this weird side effect would need to be fixed before the fix could be committed.

[dmacqueen]

Committed a second, successful fix for #285 and #289. This fix introduces another severity constructor for ErrorMsg.severity, "TERMINAL". When this severity is passed to the ErrorMsg.error function, the error message is printed and ErrorMsg.Error is raised, terminating compilation. So for the two modes of signature matching failure represented by #285 (unmatched spec) and #289 (val spec type mismatch), there is no attempt to recover after the error by returning a bogus result from sigMatch. WARNING: there are several other signature matching failure modes whose treatment has not changed, so there may be other cases where recovery is attempted after a signature match failure, leading to an uncaught BIND exception in the function constrStr function in ElabMod. A full fix needs to deal with all signature match failure modes in Elaborator/modules/sigmatch.sml.