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
andYon
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 |