Dubious FunDep behaviour, even for a 'textbook' example with non dodgy extensions
Summary
GHC's behaviour for a 'textbook' FunDep instance (without the known-to-be-dodgy extensions) is not as per the theory in the 'FunDeps via CHRs' 2006 paper.
In itself this is not problematic; there's an easy workaround; indeed FunDepers probably take it 'this is how GHC works'. But the workaround needs UndecidableInstances
, which removes any confidence about confluence and termination across all instances in the module.
(I'm documenting this in context of a whirl of recent issues #18759, #18851 and ref this comment on a github proposal.)
Steps to reproduce
Consider this classic textbook FunDep, from the Jones 2000 paper
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
class Collects e ce | ce -> e where
member :: e -> ce -> Bool
-- etc
instance Eq e => Collects e [e] where
member = elem
x1 = member True [False, False, True] -- ===> True
x2 = member undefined ([] :: [Bool]) -- ===> False
The FunDeps via CHRs paper [Section 4.2/Fig 2 translation rules] says that instance should be equivalent to this:
{-# LANGUAGE UndecidableInstances, GADTs #-}
class CollectF2 e ce | ce -> e where
memberF2 :: e -> ce -> Bool
instance (a ~ e, Eq e) => CollectF2 a [e] where
memberF2 = elem
Using ~
constraint to explicitly apply the type improvement (needs GADTs
), and bare tyvar a
in the instance head as target for the improvement (needs UndecidableInstances
).
Expected behavior
This instance and its non-confluent consequence should be rejected:
instance {-# OVERLAPPABLE #-} (a ~ ()) => Collects a [e] where
member _ _ = False
x3 = member () [False, False, True] -- ===> False
Compare:
instance {-# OVERLAPPABLE #-} (a ~ ()) => CollectF2 a [e] where
memberF2 _ _ = False
-- error: Duplicate instance declarations:
Best practice for using FunDeps (see examples cited in the github comments) is to use instance heads in a style per CollectF2
with a bare fresh tyvar as the target. This needs UndecidableInstances
even though the type improvement via ~
is perfectly decidable. That extension is module-wide, and allows exactly the non-confluence with that instance (a ~ ()) => Collects a [e]
it was seeking to avoid. FunDepers must be disciplined in how they write instances.
Environment
- GHC version used: 8.10.2
Optional:
- Operating System: Windows 8
- System Architecture: