Trivial Functional Dependencies (and downright nonsense) accepted

Summary

GHC accepts Functional Dependencies that are pointless and/or nonsensical.

(This ticket was originally posted as a possible 'feature'. But the allowed syntax is misleading: there's no useful behaviour. Commentary from SPJ & RAE retained below for ref.)

Steps to reproduce

These FunDeps are accepted

class C a  | a -> a  where            -- not even MultiParam
  cMeth :: a -> String

class D a b  | a b -> b  where
  dMeth :: a -> b -> String

class D2 a b | a b a b -> b a b a

Expected behavior

I expect these to be rejected, because they're pointless. The class behaves just as if there were no FunDep at all.

Environment

• GHC version used: 8.6.4

Optional:

• Operating System: Windows

• For comparison, the validation on FunDeps in Hugs static validation, search for "trivial" is, for each FunDep in the class decl:

  • the tyvars to the right of each -> must be non-empty;
  • no tyvar can appear both left and right of the same ->;
  • no tyvar repeated left of each ->;
  • no tyvar repeated right of each ->.

• In general, in database theory for functional dependencies, these are known as 'trivial'. (Neither the Jones 2000 paper introducing FunDeps; nor the JFP 2006 Sulzmann et al 'via CHRs paper' explicitly give these rules.)

/label ~bug

-- as originally posted, for ref

Motivation

This isn't so much a feature request as: does anybody know GHC can do this?/Is there some reasoning behind it?/I can think of a possible use.

There's a long-standing ticket #8634 which got dubbed 'Dysfunctional Dependencies'. It seems GHC already supports something like it.

Proposal

Consider these FunDeps

class C a  | a -> a  where            -- not even MultiParam
  cMeth :: a -> String

class D a b  | a b -> b  where
  dMeth :: a -> b -> String

This is accepted by GHC (8.6.4), and I can write and use instances for those classes. Those dependencies are what's called "trivial" -- that is, the FunDep target also appears on LHS of the ->. FunDep theory (such as the 'via CHRs' paper) says they shouldn't be allowed, and indeed Hugs rejects those class decls.

But wait! Here's some useful instances

instance D Int Bool  where
  dMeth x p = show $ if p then x else -x

instance D Int Char  where            -- rejected if FunDep is bare a -> b
  dMeth x y = y : show x              -- because FunDep conflict between instances

instance (b1 ~ Int) => D Int (b1 -> b1)  where
  dMeth x f = show $ f x

fi = dMeth (5 :: Int) ((\x -> x + x) :: Num b2 => b2 -> b2)

instance {-# OVERLAPPABLE #-} (b ~ String) => D Int b  where
  dMeth x _ = "String" ++ show x

(That last instance and the (b1 -> b1) would need UndecidableInstances if just FunDep a -> b.)

OTOH I don't seem to be getting behaviour any different from just D without a FunDep at all. For example

f :: D a b => a -> a
f x = x

is rejected as ambiguous, as would be with no FunDep on D.

From what I recall of 'Dysfunctional Dependencies' (by now the ticket is long and turgid), a FunDep a b -> b does represent what's happening: for some instances you can get from a to b by the coverage conditions; for some you can get from a to b via Constraints (and UndecidableInstances); for some you need to also look at the combo of a, b -- in that case, the Wanted from the use site will give sufficient typing to select the instance and then fix b. Just trust me that when the FunDep says ... -> b you'll be able to infer b.