coalton-lang / coalton

Coalton is an efficient, statically typed functional programming language that supercharges Common Lisp.
https://coalton-lang.github.io/
MIT License
1.15k stars 70 forks source link

Unexpected control stack exhaustion in recursive method definition #973

Closed macrologist closed 1 year ago

macrologist commented 1 year ago

The following typechecks and compiles (as it should):


  (define-instance (Eq :a => Eq (PSeq :a))
    (define (== a b)
      ;; because they're immutable, if they happen to be identical then == is true
      (or (lisp Boolean (a b) (cl:eq a b))
          (match (Tuple a b)
            ((Tuple (LeafArray va) (LeafArray vb))
             (== va vb))
            ((Tuple (RelaxedNode ha _ csta subsa)
                    (RelaxedNode hb _ cstb subsb))
             (and (== ha hb)
                  (== csta cstb)
                  (== subsa subsb))) ;; <----- the mere presence of this step breaks everything at run time
            (_ False)))

But the mere presence of the above-indicated step (which compares two objects of type (Vector (PSeq :a))) results in control stack exhaustion even when that case should never have been encountered:

E.g. the following will trigger control stack exhaustion:

COALTON-NATIVE-TESTS> (coalton (let ((x (the (pseq:Pseq Integer) (pseq:new)))) 
                                 (== x x)))

The x is totally empty, the recursive step should never be encountered. If you insert a trace statement at the top of the == implementation, it will not even print out when == is called.

However, removing the recursive step will behave correctly on cases that do not require that step: the empty sequences will be compared correctly and the trace statement will print out as expected.

macrologist commented 1 year ago

(incidentally, I'm not using the above implementation b/c I realized it tests the wrong things - but the bug remains valid)