CODEWITHSUNDEEP
haskell
B. Mehta
B. Mehta

Reputation: 425

Undecidable functional dependencies

I'm reading through Clowns to the left of me, Jokers to the right and playing around with the Dissection class, and I came across a coverage condition error. Code:

{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies #-}
import Data.Bifunctor
import GHC.Generics

data Add2 p q x y = L2 (p x y) | R2 (q x y)

instance (Bifunctor p, Bifunctor q) => Bifunctor (Add2 p q) where
  bimap f g (L2 p) = L2 (bimap f g p)
  bimap f g (R2 q) = R2 (bimap f g q)

class (Functor p, Bifunctor p') => Diss p p' | p -> p' where

instance (Diss p p', Diss q q') => Diss (p :+: q) (Add2 p' q')

GHC error message:

cj.hs:13:10: error:
    • Illegal instance declaration for ‘Diss (p :+: q) (Add2 p' q')’
        The coverage condition fails in class ‘Diss’
          for functional dependency: ‘p -> p'’
        Reason: lhs type ‘p :+: q’ does not determine rhs type ‘Add2 p' q'’
        Un-determined variables: p', q'
        Using UndecidableInstances might help
    • In the instance declaration for ‘Diss (p :+: q) (Add2 p' q')’
   |
13 | instance (Diss p p', Diss q q') => Diss (p :+: q) (Add2 p' q')
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

I'm struggling to understand the reason given: I feel that the type p :+: q should determine the rhs type because of the dependencies p -> p' and q -> q' implied by the constraints Diss p p' and Diss q q'. Enabling UndecidableInstances does remove the error, but I'd like to understand why it's necessary in this case.

Upvotes: 2

Views: 123

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 152707

The GHC documentation has this to say about a similar scenario:

class Mul a b c | a b -> c where
  (.*.) :: a -> b -> c

instance Mul Int Int Int where (.*.) = (*)
instance Mul Int Float Float where x .*. y = fromIntegral x * y
instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

(Answerer's note: as with your example, you might think here that in the Mul a b c => Mul a [b] [c] instance, since a b determines c, it ought to also be the case that a [b] clearly determines [c].)

The third instance declaration does not obey the coverage condition; and indeed the (somewhat strange) definition:

f = \ b x y -> if b then x .*. [y] else y

makes instance inference go into a loop, because it requires the constraint Mul a [b] b.

So the coverage condition is explicitly about ruling out cases like yours that look benign but may potentially not be.

Upvotes: 3

Related Questions