Typeclass Definition "Forgets" constraints on functionally dependent type parameter

[Jason94]

I have two typeclasses with functionally dependent type parameters. The simplest case, with no type constraints compiles:

  (define-class (Collection_ :m :a (:m -> :a))
    (new-collection_
     (Unit -> :m))
    (add_
     (:a -> :m -> :m)))
  
  (define-class (EqCollection_ :m :a (:m -> :a))
    (contains-elt?_
     (:a -> :m -> Boolean))))

  (define-instance (Collection_ (List :a) :a)
    (define new-collection_ (const Nil))
    (define add_ Cons))
  
  (define-instance (Eq :a => EqCollection_ (List :a) :a)
    (define (contains-elt?_ elt lst)
      (some? (l:find (== elt) lst))))

as does the case where there is a type constraint on the "outer" type parameter:

  (define-class ((Collection_ :m :a) => EqCollection_ :m :a (:m -> :a))
    (contains-elt?_
     (:a -> :m -> Boolean))))

However, the case where there is constraint on the :a itself fails to compile:

  (define-class (Eq :a => EqCollection_ :m :a (:m -> :a))
    (contains-elt?_
     (:a -> :m -> Boolean))))
  
  (define-instance (Eq :a => EqCollection_ (List :a) :a)
    (define (contains-elt?_ elt lst)
      (some? (l:find (== elt) lst))))
==>
error: Instance missing context
--> <macroexpansion>:7:19
|
7 | (DEFINE-INSTANCE (EQ :A => EQCOLLECTION_ (LIST :A) :A)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ No instance for EQ :A

Something is happening here where it's not "seeing" that in the instance, :a is an Eq. I think the problem is with the instance definition, not the typeclass definition, because it correctly doesn't compile without the Eq typeclass either:

  (define-class (Eq :a => EqCollection_ :m :a (:m -> :a))
    (contains-elt?_
     (:a -> :m -> Boolean))))
  
  (define-instance (EqCollection_ (List :a) :a)
    (define (contains-elt?_ _ _)
      False))
==>
  error: Instance missing context
  --> <macroexpansion>:7:19
   |
 7 |    (DEFINE-INSTANCE (EQ :A => EQCOLLECTION_ (LIST :A) :A)
   |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ No instance for EQ :a

I tested this in both main and the branch in #1315 , getting the same results, so I believe this is independent from #1050. I'm not sure if that PR is the appropriate place to address this - @YarinHeffes.

Interestingly, it does work if you define the typeclass over a concrete type that is an Eq. This compiles properly:

  (define-instance (Eq :a => EqCollection_ (List :a) :a)
    (define (contains-elt?_ elt lst)
      (some? (l:find (== elt) lst))))

  (define-instance (EqCollection_ (List Integer) Integer)
    (define (contains-elt?_ elt lst)
      (some? (l:find (== elt) lst))))

From a practical standpoint I don't know if this is a huge deal, but it does keep library designers from preventing silly things like this:

  (define-instance (EqCollection_ (List :a) :a)
    (define (contains-elt?_ _ _)
      False))

Finally, as a sanity check that this should even be possible, I checked and in Haskell putting Eq over a does work there. (Not that Coalton has to have the same type system as Haskell in all cases, but since this seemed like a bug and not a feature I thought that was a reasonable point of comparison:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

data MyList a = Cons a (MyList a) | Nil
  deriving Show
  
class Collection m a | m -> a where
  new :: m
  add :: a -> m -> m

class (Eq a, Collection m a) => EqCollection m a | m -> a where 
  containsElt :: a -> m -> Bool
  
instance Collection (MyList a) a where
  new = Nil
  add = Cons

instance Eq a => EqCollection (MyList a) a where
  containsElt _ Nil = False
  containsElt a (Cons h rem) =
    if (a == h)
    then True
    else containsElt a rem 
    
data MyNotEqType = A | B deriving Show

-- Does not compile:
-- Main.hs:35:10: error:
--     • No instance for (Eq MyNotEqType)
--         arising from the superclasses of an instance declaration
--     • In the instance declaration for
--         ‘EqCollection (MyList MyNotEqType) MyNotEqType’
--   |
-- 35 | instance EqCollection (MyList MyNotEqType) MyNotEqType where
instance EqCollection (MyList MyNotEqType) MyNotEqType where
  containsElt _ _ = False
  
main :: IO ()
main = do
  let lst :: MyList Int = add 4 $ add 12 Nil
  putStrLn $ show $ containsElt (10 :: Int) lst

[YarinHeffes]

This issue doesn't seem to be related to functional dependencies. I can reproduce it with the following,

(coalton-toplevel
  (define-class (C :col :elem))
  (define-class (Eq :elem => EqC :col :elem))
  (define-instance (C (List :elem) :elem))
  (define-instance (Eq :elem => EqC (List :elem) :elem)))

and the same error comes from

(coalton-toplevel
  (define-class (C :col :elem))
  (define-class (Eq :elem => EqC :col :elem))
  (define-instance (C (List :elem) :elem))
  (define-instance (EqC (List :elem) :elem)))

See #1342.

---

Side-note: You can define classes on non-* kinded type variables. E.g.

(define-class (Collection :m :a)
  (new-collection (Unit -> :m :a))
  (add (:a -> :m :a -> :m :a)))

(define-instance (Collection List :a)
  (define new-collection (const Nil))
  (define add Cons))

allowing you to avoid functional dependencies for this particular use-case.

[Jason94]

This issue doesn't seem to be related to functional dependencies. I can reproduce it with the following,

(coalton-toplevel
  (define-class (C :col :elem))
  (define-class (Eq :elem => EqC :col :elem))
  (define-instance (C (List :elem) :elem))
  (define-instance (Eq :elem => EqC (List :elem) :elem)))

and the same error comes from

(coalton-toplevel
  (define-class (C :col :elem))
  (define-class (Eq :elem => EqC :col :elem))
  (define-instance (C (List :elem) :elem))
  (define-instance (EqC (List :elem) :elem)))

See #1342.

Side-note: You can define classes on non-* kinded type variables. E.g.

(define-class (Collection :m :a)
  (new-collection (Unit -> :m :a))
  (add (:a -> :m :a -> :m :a)))

(define-instance (Collection List :a)
  (define new-collection (const Nil))
  (define add Cons))

allowing you to avoid functional dependencies for this particular use-case.

Thanks! I'll try rebasing my collections code on your PR and see if it works.

This particular code is incomplete, but it's motivated by a desire to define a further typeclass representing maps ("KeyedCollection" in this case) which are also collections of tuples. To be able to get this to typecheck, I had to add the functional dependencies to the Collection class. I'd love to keep the Collection definition to: (Collection :m) though, so I'm definitely open to better designs.

(coalton-toplevel
  (define-type (ListMap :k :v)
    (ListMap (List (Tuple :k :v))))

<functions omitted>

  (define-class (KeyedCollection_ :m)
    (add-keyed_
     (:k -> :v -> :m :k :v -> :m :k :v))
    (contains-key_
     (Eq :k => :k -> :m :k :v -> Boolean))
    (get-val_
     (Eq :k => :k -> :m :k :v -> Optional :v))))

(coalton-toplevel
  (define-instance (KeyedCollection_ ListMap)
    (define add-keyed_ add-keyed-lstmp)
    (define contains-key_ contains-key-lstmp)
    (define get-val_ get-val-lstmp))

  (define-instance (Collection_ (ListMap :k :v) (Tuple :k :v))
    (define new-collection_ new-collection-lstmp)
    (define add_ add-lstmp))