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: