instance constraints compare type-family constraints

Question

Usually I reckon type-families are similarly expressive as compared with typeclasses/instances -- the difference is awkwardness/ergonomics of the code. In this case I have code working with type-families to raise a constraint, but the equivalent typeclass code won't compile. (* Could not deduce (Eq a) ... when (Eq a) is exactly the constraint I'm supplying.) Is this a case typeclasses just can't express, or am I doing something wrong?

data Set a = NilSet | ConsSet a (Set a)    deriving (Eq, Show, Read)

-- fmap over a Set, squishing out duplicates
fmapSet :: (Eq a, Eq b ) => (a -> b) -> Set a -> Set b 
fmapSet f NilSet = NilSet
fmapSet f (ConsSet x xs) = uqCons (f x) (fmapSet f xs)

uqCons fx fxs | sElem fx fxs = fxs
              | otherwise = ConsSet fx fxs
sElem fx NilSet = False
sElem fx (ConsSet fy fys) = fx == fy ||  sElem fx fys 

I want to call that fmap via a Functor-like class, with a constraint that the data-structure is well-formed. Either of these approaches with type-families work (based on this answer, but preferring a standalone family).

{-# LANGUAGE ConstraintKinds, TypeFamilies #-}

import Data.Kind (Type, Constraint)

type family   WFTF (f :: * -> *) a :: Constraint
type instance WFTF Set a           =  Eq a

class WFTFFunctor f  where
  wftFfmap :: (WFTF f a, WFTF f b) => (a -> b) -> f a -> f b
instance WFTFFunctor Set  where
  wftFfmap = fmapSet

type family   WFTF2 c_a     :: Constraint 
type instance WFTF2 (Set a) =  Eq a

class WFTF2Functor f  where
  wftF2fmap :: (WFTF2 (f a), WFTF2 (f b)) => (a -> b) -> f a -> f b
instance WFTF2Functor Set  where
  wftF2fmap = fmapSet

The equivalent (I think) typeclass at least compiles providing I don't give an implementation for the method:

class WFT c_a  where  
instance Eq a => WFT (Set a)

class WFTFunctor f  where
  wftfmap :: (WFT (f a), WFT (f b)) => (a -> b) -> f a -> f b 
instance WFTFunctor Set  where wftfmap f xss   =  undefined     -- s/b fmapSet f xss

Inferred :t (\ f (xss :: Set a) -> wftfmap f xss) :: (Eq a, Eq b) => (a -> b) -> Set a -> Set b -- which is exactly the type of fmapSet. But if I put that call to fmapSet f xss in place of undefined, rejected:

* Could not deduce (Eq a) arising from a use of `fmapSet'
  from the context: (WFT (Set a), WFT (Set b))
    bound by the type signature for:
               wftfmap :: forall a b.
                          (WFT (Set a), WFT (Set b)) =>
                          (a -> b) -> Set a -> Set b
    at ...
  Possible fix:
    add (Eq a) to the context of
      the type signature for:
        wftfmap :: forall a b.
                   (WFT (Set a), WFT (Set b)) =>
                   (a -> b) -> Set a -> Set b

WFT (Set a) implies raises Wanted (Eq a), so I shouldn't need to add it. (And if I do via InstanceSignatures, rejected because it's not as general as the inferred constraint.) [In response to @dfeuer's answer/my comment] True that there's nothing in the instance decl to Satisfy (Eq a), but fmapSet's sig also Wants (Eq a) so (why) doesn't that ensure the constraint gets satisfied at the call site?

I've tried decorating everything with ScopedTypeVariables/PatternSignatures to make the constraints more explicit. I've tried switching on ImpredicativeTypes (GHC 8.10.2). I sometimes get different rejection messages, but nothing that compiles.

If I take away the WFT (Set a) and (Eq a) from fmapSet's signature, I get a similar rejection * Could not deduce (Eq b) .... Yes I know that rejection message is a FAQ. In the q's I've looked through, the constraint is indeed unsatisfiable. But then in this case

a) why does the version with implementation undefined typecheck;
b) isn't the constraint wanted from WFT (Set a) getting satisfied by fmapSet having the (Eq a)?)

Addit: To explain a bit more about what I'm expecting in terms of Wanted/Satisfied constraints:

There's no signature given for uqCons, nor for sElem, which it calls. In sElem there's a call to (==), that raises Wanted (Eq b) in sElem's sig, which gets passed as a Wanted in the sig for uqCons, which gets passed as a Wanted in the sig for fmapSet, which does have a sig given including (Eq b).

Similarly the Set instance for method wftfmap raises Wanted (Eq a, Eq b); I expect it can use that to Satisfy the Wanted arising from the call to fmapSet.

Answer 1

There's a huge difference between superclass constraints and instance constraints. A superclass constraint is something required to form any instance of the class, and is available whenever the subclass constraint is in force. An instance constraint is required to form a specific instance, and is not automatically available when the class constraint is in force. This difference is pretty deeply wired into the system, and is reflected in the Core representations. In Core:

1. A class is a type of records of class methods and superclasses.
2. An instance is a value of a class type or a function from its instance constraints to such a value.

Once a "dictionary function" is called to produce an instance dictionary, you only have the dictionary, not the arguments that were used to create it.

Answer 2

[re @Ben's comment to @dfeuer's answer] not something you have on the inside to implement wftfmap.

OK I can have the right sig on the inside:

-- class/instance WFT, funcs fmapSet, uqCons, sElem as before

{-# LANGUAGE  InstanceSigs,  QuantifiedConstraints #-}

class WFTQFunctor f  where
  wftQfmap :: (WFT (f a), WFT (f b)) => (a -> b) -> f a -> f b       

instance (forall b. (WFT (Set b) => Eq b)) => WFTQFunctor Set  where 
  wftQfmap :: (Eq a, Eq b) => (a -> b) -> (Set a) -> (Set b)        -- yay
  wftQfmap f xss = fmapSet f xss

Compiles with a warning that I can suppress with -XMonoLocalBinds:

* The constraint `WFT (Set b)' matches
    instance Eq a => WFT (Set a)
  This makes type inference for inner bindings fragile;
    either use MonoLocalBinds, or simplify it using the instance
* In the instance declaration for `WFTQFunctor Set'

I appreciate that QuantifiedConstraint is a fib. I might have instance {-# OVERLAPPING #-} WFT (Set (b -> c)) for which Eq does not hold; but I don't; and/or at least if I use a Set element for which Eq holds, I'll get away with it(?)

But no:

*> wftQfmap toUpper mySet                -- mySet :: Set Char

<interactive>:2:1: error:
* Could not deduce (Eq b) arising from a use of `wftQfmap'
  from the context: WFT (Set b)
    bound by a quantified context at <interactive>:2:1-22
  Possible fix: add (Eq b) to the context of a quantified context
* In the expression: wftQfmap toUpper mySet
  In an equation for `it': it = wftQfmap toUpper mySet

So why does that instance WFTQFunctor Set compile? And can it ever do anything useful?

Answer 3

OK I have something working. It's ugly and clunky, and not scalable, but answers the q as put:

class WFT c_a  where  
  isWF :: c_a -> Bool                                -- is c_a well-formed?
  mkWF :: c_a -> c_a                                 -- edit c_a to make it well-formed
  mkWF = id
instance Eq a => WFT (Set a)                         -- instance types same as q
  isWF NilSet         = True
  isWF (ConsSet x xs) = not (sElem x xs) && isWF xs  -- sElem decl'd in the q
  mkWF = fmapSet id                                  -- fmapSet also

class WFTFunctor f  where                            -- class as decl'd in the q
  wftfmap :: (WFT (f a), WFT (f b)) => (a -> b) -> f a -> f b 
instance WFTFunctor Set  where wftfmap f xss   = mkWF $ fmap f xss 


instance Functor Set  where                          -- conventional/unconstrained fmap
  fmap f  NilSet        = NilSet
  fmap f (ConsSet x xs) = ConsSet (f x) (fmap f xs)

If I'm using fmap, generalise:

class Functor f => WFTFunctor f  where
  wftfmap :: (WFT (f a), WFT (f b)) => (a -> b) -> f a -> f b   
  wftfmap f xss = mkWF $ fmap f xss

This is not far off H2010 compliant. (Needs FlexibleConstraints.) So I can get the Eq constraint effective 'inside' the WFTFunctor instance; it needs a method call from WFT to pull it through.

I could have heaps of other methods in class WFT, but I say "not scalable" because you couldn't in general 'edit' an ill-formed structure to well-formed. Hmm since it's a Functor: could unload to a List then load back to the structure.