subclass constraints and fundeps not checking right?

[stylewarning]

I'm not 100% sure if my diagnosis is correct below, but I think this is an error.

I was doing some work splitting a type class and got to a situation where I believe some constraints are unambiguous, but Coalton considered them ambiguous:

(coalton-toplevel
  (define-class (RandomAccessBase :f :t (:f -> :t))
    (make (UFix -> :t -> :f))
    (length (:f -> UFix)))

  (define-class (RandomAccessBase :f :t => RandomAccessReadable :f :t (:f -> :t))
    (unsafe-set! (:f -> UFix -> :t -> Unit)))

All is good and well, and now we want to implement a function on RandomAccessReadable.

(coalton-toplevel
  (declare aref (RandomAccessReadable :f :t => :f -> UFix -> (Optional :t)))
  (define (aref storage index)
    (if (and (<= 0 index) (< index (length storage)))
        (Some (unsafe-aref storage index))
        None))

With the declaration, we get an error:

;     error: Explicit type is missing inferred predicate
;     --> blah:70:11
;       |
;    70 |    (define (aref storage index)
;       |             ^^^^ Declared type RANDOMACCESSREADABLE :A :B ⇒ (:A → UFIX → (OPTIONAL :B)) is missing inferred predicate RANDOMACCESSBASE :A :C
;   
;   
;     (in form starting at line: 68, column: 0, position: 2795)

Without the declaration, Coalton infers the following:

COALTON-USER> (type-of 'aref)
∀ :A :B :C. (RANDOMACCESSBASE :A :B) (RANDOMACCESSREADABLE :A :C) ⇒ (:A → UFIX → (OPTIONAL :C))

Since the functional dependency forces :b given :a, Coalton is mistakenly not unifying (?) :b and :c.

[YarinHeffes]

Currently, it seems that type variable substitutions are only generated from functional dependencies when the variables in question are applied to the same class predicate.

coalton/src/typechecker/context-reduction.lisp

Line 306 in 7fc91f8

:when (and (eq (ty-predicate-class pred) (ty-predicate-class expr-pred))

[YarinHeffes]

Currently, it seems that type variable substitutions are only generated from functional dependencies when the variables in question are applied to the same class predicate.

coalton/src/typechecker/context-reduction.lisp

Line 306 in 7fc91f8

:when (and (eq (ty-predicate-class pred) (ty-predicate-class expr-pred))

This turned out not to be the issue. Rather, the issue was that superclasses were not considered when resolving functional dependencies in the typechecker.