Undependable Dependencies

Consider

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


data Hither = Hither  deriving (Eq, Show, Read)		-- just three
data Thither = Thither  deriving (Eq, Show, Read)	-- distinct
data Yon = Yon  deriving (Eq, Show, Read)		-- types

class Whither a b  | a -> b  where
  whither :: a -> b -> b

-- instance Whither Int Hither  where	-- rejected: FunDep conflict
--   whither _ y = y			-- with Thither instance, so

instance {-# OVERLAPPING #-} (b ~ Hither) => Whither Int b  where
  whither _ y = y

instance {-# OVERLAPS #-} Whither a Thither  where
  whither _ y = y
instance {-# OVERLAPPABLE #-} (b ~ Yon) => Whither a b  where
  whither _ y = y

f :: Whither Int b => Int -> b -> b
f = whither

g :: Whither Bool b => Bool -> b -> b
g = whither

Should those three instances be accepted together? In particular, the published work on FDs (including the FDs through CHRs paper) says the Thither instance should behave as if:

instance (beta ~ Thither) => Whither a beta  where ...

(in which beta is a unification variable and the ~ constraint is type improvement under the FD.) But now the instance head is the same as the Yon instance, modulo alpha renaming; with the constraints being contrary.

That's demonstrated by the inferred/improved type for g:

*Whither> :t g
===> g :: Bool -> Thither -> Thither             -- and yet

*Whither> g True Yon
===> Yon

What do I expect here?

• At least the Thither and Yon instances to be rejected as inconsistent under the FunDep.
• (The Hither instance is also inconsistent, going by the strict interpretation in published work. But GHC's rule here is bogus, as documented in Trac #10675.)

Exploiting Overlapping instances is essential to making this go wrong. The published work shies away from considering FunDeps + Overlap; and yet specifying the semantics as if the instances used bare unification variables is almost inevitably going give overlaps -- especially if there are multiple FDs.

Trac metadata

Trac field	Value
Version	8.6.1-beta1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related	#10675
Blocking
CC
Operating system
Architecture