Bug: Functional Dependencies that Introduce new Type Variables Shouldn't Overdefine

[Jason94]

Adding typeclass constraints to a function declaration should compile if they add new type variables, even if they're technically redundant because of functional dependencies and class chains.

For example, suppose you want to have a monad that always has access to a builtin default type, like this:

(define-class ((Default :d) (Monad :m) => HasDefault :d :m (:m -> :d)))

(declare pure-default1 (HasDefault :d :m => :m :d))
(define pure-default1
  (pure (default)))

That works well, but now you have to write this weird typeclass instance that has this extra tvar everywhere, even in some cases where you may not actually use a :d in the function declaration. You can create a typeclass that encodes the :d, taking advantage of the functional dependency on the original class:

(define-class (HasDefault :d :m => SuperMonad :m))

Now here is the error. It should be possible to recover the :d from just a SuperMonad :m instance, like this:

  (declare proxy-for-d ((HasDefault :d :m) (SuperMonad :m) => Proxy (:m :a) -> Proxy :d))
  (define (proxy-for-d _)
    Proxy)

But this gives the error:

error: Declared context is too general
  --> test.lisp:10:23
    |
 10 |    (declare proxy-for-d ((HasDefault :d :m) (SuperMonad :m) => Proxy (:m :a) -> Proxy :d))
    |                         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the substitution :D +-> :D is determined for (HasDefault :D :M) (SuperMonad :M) => Proxy (:M :A) -> Proxy :D by functional dependencies.

---

The motivating use case for this is the way Coalton-IO uses functional dependencies to handle threading. It has a generic Runtime :rt :t class, where :t is the underlying thread and :rt is a phantom type that provides an implementation of the necessary functionality to do things with those threads. Then it has a "SuperMonad" type class, Threads, that just looks like this:

  (define-class ((MonadIo :m) (Runtime :rt :t) => Threads :rt :t :m (:m -> :rt)))

  (inline)
  (declare runtime-for (Threads :rt :t :m => Proxy (:m :a) -> Proxy :rt))
  (define (runtime-for _)
    Proxy)

This works, but because the runtime type doesn't have any valid instances of it and a lot of functions never need to use the :t, it leads to a lot of cluttered function signatures like this:

(declare new-mvar (Threads :rt :t :m => :a -> :m (MVar :a)))

I tried to use the technique above to make Threads like SuperMonad, so I could write something simpler, but I encountered this error:

(declare new-mvar (Threads :m => :a -> :m (MVar :a)))

---

Full test file:

(cl:in-package :cl-user)

(defpackage #:test
  (:use
   #:coalton
   #:coalton-prelude
   #:coalton/types))

(in-package :test)

(named-readtables:in-readtable coalton:coalton)

(coalton-toplevel

  (define-class ((Default :d) (Monad :m) => HasDefault :d :m (:m -> :d)))
  (define-class (HasDefault :d :m => SuperMonad :m))

  (declare pure-default1 (HasDefault :d :m => :m :d))
  (define pure-default1
    (pure (default)))

  (declare proxy-for-d ((HasDefault :d :m) (SuperMonad :m) => Proxy (:m :a) -> Proxy :d))
  (define (proxy-for-d _)
    Proxy)
  )