Nesting Functional Dependencies Requires Extraneous Type Variable

[Jason94]

It should be possible to define a class hierarchy like this:

(coalton-toplevel

  (define-class (HasA :t :a (:t -> :a))
    (get-a (Proxy :t -> :a)))

  (define-class (HasA :t :a => WrapsHasA :w :t (:w -> :t))
    (get-two-as (:w -> Tuple :a :a)))
  )

Because, in the definition of WrapsHasA, :a can be determined by :t, that should be fully defined. Instead, Coalton forces WrapsHasA to also declare the inner type variable. Trying to compile the above gives this error:

      error: Unknown type variable
      --> test.lisp:6:25
       |
     6 |    (define-class (HasA :t :a => WrapsHasA :w :t (:w -> :t))
       |                           ^^ Unknown type variable :A

and the only fix is to also encode :a in WrapsHasA, like this:

(coalton-toplevel

  (define-class (HasA :t :a (:t -> :a))
    (get-a (Proxy :t -> :a)))

  (define-class (HasA :t :a => WrapsHasA :w :t :a (:w -> :t))
    (get-two-as (:w -> Tuple :a :a)))

  )

[stylewarning]

What does Haskell do?

@YarinHeffes, What do you think? I could see code breaking if the constraint has variables not present in the qualified type, but maybe it shouldn't actually be a big deal.

[Jason94]

To be fair, Haskell doesn't seem to allow this either. This compiles

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

class HasA t a | t -> a where
  getA :: proxy t -> a

class HasA t a => WrapsHasA w t a | w -> t where
  getTwoAs :: w -> (a, a)

main = putStrLn ""

but this doesn't

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

class HasA t a | t -> a where
  getA :: proxy t -> a

class HasA t a => WrapsHasA w t | w -> t where
  getTwoAs :: w -> (a, a)

main = putStrLn ""
==>
Main.hs:10:14: error: [[GHC-76037](https://errors.haskell.org/messages/GHC-76037)] Not in scope: type variable ‘a’
   |
10 | class HasA t a => WrapsHasA w t | w -> t where

I think in Haskell if you wanted to do it this way, you'd use type families.

However, if you move the HasA restriction from the class to the function definition, it does work:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy

newtype Identity a = Identity a

class HasString t where
  getA :: proxy t -> String

class WrapsHasA w t | w -> t where
  getTwoAs :: w -> (String, String)

instance HasString () where
  getA _ = "Has a string"

instance WrapsHasA (Identity ()) () where
  getTwoAs _ = (s, s)
    where
      s = getA (Proxy :: Proxy ())

main :: IO ()
main = print (getTwoAs (Identity ()))

At that point, you're basically doing what I tried to do in #1717 , just in a typeclass method not a bare function. (Which should become possible in Coalton, too, once that issue gets fixed) So that might be good enough. I'm not exactly sure why Haskell doesn't support this - I can't think of what the problems would be. Possibly it's because you can just move the constraint to the method, and for all practical purposes you have the same thing. And it also has type families. So maybe there's just enough other ways to do the same thing.