Nested coalton-lisp-coalton forgets the type of variable

[ghost]

(asdf:load-system :coalton)
(in-package :coalton-user)

(coalton (let ((x 5)) (lisp Integer (x) (coalton x))))

Produces the error:

;    error: Unknown variable X
;     --> repl:1:9
;      |
;    1 |  (COALTON X)
;      |           ^ unknown variable X

This might be expected looking at the Design Document:

(coalton-toplevel

  (declare num-square ((Num :a) => :a -> :a))
  (define (num-square x)
    "Returns the square of an object of any type with a defined instance of num."
    (* x x))

  (define (print-num-square1 x)
    (lisp String (x)
      (cl:format cl:nil "~a squared = ~a" x (coalton (num-square (lisp :a () x)))))))

And using a nested lisp form does let the Integer case compile:

(coalton (let ((x 5)) (lisp Integer (x) (coalton (lisp Integer () x)))))

But with parametric types or typeclasses, there's no way to refer to the original type. This was the original reason I used a nested Coalton: So that Lisp code could dispatch to the appropriate implementation of a class.

The example I think only works because of type defaulting:

Coalton will only default if one or more of the predicates is a numeric type class (Num, Quantizable, Reciprocable, Complex, Remainder, Integral). Coalton will default an ambiguous variable to either Integer, Double-Float, or Single-Float;

If a non-special class is used, the trick doesn't work:

(coalton-toplevel
  (define-class (Foo :a)
    (foo (:a -> Integer)))
  (define-instance (Foo String) (define (foo _) 0))
  (define-instance (Foo Integer) (define (foo _) 1))

  (declare bar ((Foo :a) => :a -> Integer))
  (define (bar x)
    (let ((x 5))
      (lisp Integer (x)
        (coalton
         (foo
          (lisp
              :a () x)))))
    )
  )

fails with error:

  style-warning: 
    warn: Unused variable
      --> /Users/mira/repos/lisp/scratch/coalton-interop-test.lisp:11:21
        |
     11 |    (declare bar ((Foo :a) => :a -> Integer))
        |                       ^ variable defined here
    help: prefix the variable with '_' to declare it unused
     11 |   (declare bar ((Foo _:a) => :a -> Integer))
        |                      --

  error: 
    during macroexpansion of (COALTON (FOO #)). Use COMMON-LISP:*BREAK-ON-SIGNALS*
    to intercept.

     error: Unable to codegen
      --> /Users/mira/repos/lisp/scratch/coalton-interop-test.lisp:1:10
       |
     1 |    (asdf:load-system :coalton)
       |  ____________^
       | | ___________-
     2 | || (in-package :coalton-user)
       | ||___________________________- Add a type assertion with THE to resolve ambiguity
       | |____________________________^ expression has type ∀ #T824. (FOO #T824) => INTEGER with unresolved constraint (FOO #T824)

The :a in the nested lisp form does not refer to the top-level bar signature's :a. It's a freshly-generated type. The style warning is complaining the typeclass dictionary isn't used, because it's forgotten. Then because the top-level x is forgotten, there's no way to get its type or to unify a fresh type with it. So the inner coalton fails to codegen because it can't access the unused dictionary. So it seems like this function can't be written.

Should there be a dynamic-scoped type context set on (lisp) entry so the type isn't forgotten?

[ghost]

Alternatively: Some way to turn the typeclass dictionary into a value, pass it to (lisp), and call a typeclass-based method using it. Both approaches could make sense to implement, even together.

Or turn any type into a value and let (coalton) accept it as an optional parameter.

[YarinHeffes]

To add to this, the following block compiles,

(coalton-toplevel

  (define (check-num x)
    ((fn (x) (+ x x)) (lisp :a (x) x))))

but this block does not,

(coalton-toplevel

  (define (check-eq x)
    ((fn (x) (== x x)) (lisp :a (x) x))))

erroring instead with,

error: Ambiguous predicate
  --> repl:4:8
   |
 4 |         (== X X))
   |          ^^ Ambiguous predicate EQ :A
   [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]

Maybe the inferences applied to the Num type class can be generalized under the hood.

For what it's worth, I implemented an interface between types and classes defined in Lisp and in Coalton in order to hook my Coalton project into a Lisp codebase. The entire interface is contained in this file, in case you find it helpful.

[eliaslfox]

The example I think only works because of type defaulting:

This is correct.

Should there be a dynamic-scoped type context set on (lisp) entry so the type isn't forgotten?

The inner macro expansion of coalton is a separate call to the compiler that won't share type information with the outer call. I think the inner call will be expanded after the outer coalton-toplevel has finished compiling.

Alternatively: Some way to turn the typeclass dictionary into a value, pass it to (lisp), and call a typeclass-based method using it. Both approaches could make sense to implement, even together.

We could expose a primitive for doing this.

I'm not sure if it would work for your use case, but it's often possible to have the compiler generate specialized implementations of generic methods automatically. These can then safely be passed to lisp code. See the implementation of sort and sortBy for vectors which combines cl:sort with the Ord type class.