GitLab

Summary

The GHC user's guide mentions in 9.8.2.2.2. Adding functional dependencies, for class D a b | a -> b where ...:

The compiler, on the other hand, is responsible for ensuring that the set of instances that are in scope at any given point in the program is consistent with any declared dependencies. For example, the following pair of instance declarations cannot appear together in the same scope because they violate the dependency for D, even though either one on its own would be acceptable:

instance D Bool Int where ...
instance D Bool Char where ...

This leaves out what happens when polymorphic types are used in instances, and some of the behavior of functional dependencies in that case is not what I would expect judging by the documentation, but I suspect that they work as intended.

To illustrate:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}

module FunDeps where

class C a b | a -> b where
  foo :: a -> b

-- It is unclear to me why I can write both of these instances together - it
-- seems as though this should violate the dependency
instance C a a where
  foo = id

instance C a () where
  foo = const ()

-- understandably not fine, due to Overlapping instances
-- ex0 = foo () :: ()

-- fine
ex1 = foo 'x' :: Char

-- also fine
-- However, the User's guide says "The notation `a -> b` [...] indicates that the `a`
-- parameter uniquely determines the `b` parameter, and might be read as “a determines b.”"
-- From this I would expect that an expression like `foo 'x'` has a uniquely determined
-- type, but evidently, this is not so, since it can have both type `Char` and `()`.
ex2 = foo 'x' :: ()

-- not fine, with confusing error message
-- Why does it expect the argument of `foo` to be of type `()` when, with
-- an annotation, it accepts a `Char` argument?
-- In fact, it looks like it selected the `C a a` instance and from it determined that
-- it needs to solve a `C Char ()` constraint, which seems paradoxical.
-- Naively I would expect GHC to talk about an ambiguous type variable, which
-- is what happens if the functional dependency is removed.
ex3 = foo 'x'

{-
FunDeps.hs:25:7: error:
    • Couldn't match type ‘Char’ with ‘()’
        arising from a functional dependency between:
          constraint ‘C Char ()’ arising from a use of ‘foo’
          instance ‘C a a’ at FunDeps.hs:9:10-14
    • In the expression: foo 'x'
      In an equation for ‘ex3’: ex3 = foo 'x'
   |
25 | ex3 = foo 'x'
   |       ^^^^^^^
-}

Another interesting aspect is that entering () :: C Bool () => () in GHCi will produce the exact same warning twice, though I don't know if that's expected behavior:

<interactive>:45:7: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘C Bool ()’ matches
        instance C a () -- Defined at FunDeps.hs:15:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In an expression type signature: C Bool () => ()
      In the expression: () :: C Bool () => ()
      In an equation for ‘it’: it = () :: C Bool () => ()

<interactive>:45:7: warning: [-Wsimplifiable-class-constraints]
    • The constraint ‘C Bool ()’ matches
        instance C a () -- Defined at FunDeps.hs:15:10
      This makes type inference for inner bindings fragile;
        either use MonoLocalBinds, or simplify it using the instance
    • In an expression type signature: C Bool () => ()
      In the expression: () :: C Bool () => ()
      In an equation for ‘it’: it = () :: C Bool () => ()

Environment

• GHC version used: 8.11.0.20200127