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