GHC accepts derived instances that violate functional dependencies

Summary

Instances generated using DerivingVia are accepted even though equivalent handwritten instances are rejected due to violation of the (liberal) coverage condition.

Steps to reproduce

This module demonstrates the problem:

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

module DerivingViaBug where

class C a b | b -> a

newtype A t a = A a
instance C t (A t a)

data T = T
  deriving (C a) via (A () T)

The above program is accepted. But if we write the C a T instance manually, rather than deriving it, the program is rejected:

data T = T
instance C a T

src/DerivingViaBug.hs:13:10: error:
    • Illegal instance declaration for ‘C a T’
        The coverage condition fails in class ‘C’
          for functional dependency: ‘b -> a’
        Reason: lhs type ‘T’ does not determine rhs type ‘a’
        Un-determined variable: a
    • In the instance declaration for ‘C a T’
   |
13 | instance C a T
   |          ^^^^^

Expected behavior

The simplest solution to this problem would be to reject the derived instance. However, this introduces a bit of an inconsistency between functional dependencies and associated types. Consider the following similar program, which uses associated types instead of functional dependencies:

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module DerivingViaBug where

class C a where
  type F a

newtype A t a = A a
instance C (A t a) where
  type F (A t a) = t

data T = T
  deriving (C) via (A () T)

This program is accepted, and the behavior is reasonable. The derived instance is

instance C T where
  type F T = F (A () T)

so F T is ultimately (). To achieve analogous behavior for functional dependencies, it seems like a reasonable derived instance could be

instance C () T

which can be constructed by applying the substitution {t ↦ (), a ↦ T} to the original C t (A t a) instance declaration. I haven’t thought about it enough to say whether or not that would cause more problems than it would solve, however.

Environment

• GHC version used: 8.6.5
• Operating System: macOS 10.14.5 (18F132)
• System Architecture: x86_64