Skip to content

QuantifiedConstraint with InstanceSig compiles (surprise) but does nothing useful

Summary

Should this compile? (The InstanceSig is rejected without the QuantifiedConstraint at the instance constraint.) If so, can it do anything useful? (Because it doesn't achieve what it appears.)

Steps to reproduce

-- attempt at a constrained Functor-like class

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

class WFT c_a  where                                                       -- Well-Formed Type
instance Eq a => WFT (Set a)

{-# LANGUAGE  InstanceSigs,  QuantifiedConstraints, UndecidableInstances #-}

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       -- QuantifiedConstraint  
  wftQfmap :: (Eq a, Eq b) => (a -> b) -> (Set a) -> (Set b)        -- yay -- InstanceSig
  wftQfmap f xss = fmapSet f xss

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

This compiles, with a MonoLocalBinds warning about the instance (...) => WFTQFunctor Set, presumably because of the QuantifiedConstraint:

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

(BTW the InstanceSig is unnecessary. I'm merely demonstrating the QuantifiedConstraint is inferring the (Eq a, Eq b) so it can call fmapSet. Switching on MonoLocalBinds makes the warning go away, but doesn't affect the behaviour.)

Expected behavior

Since it compiles with the (Eq a, Eq b) => accepted on the InstanceSig, I expect wftQfmap to be callable on a Set for an Eq element type. But:

*> wftQfmap toUpper (mySet :: Set Char)

<interactive>:5: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>:5:1-36
      Possible fix: add (Eq b) to the context of a quantified context
    * In the expression: wftQfmap toUpper (mySet :: Set Char)
      In an equation for `it': it = wftQfmap toUpper (mySet :: Set Char)

It seems wftQfmap cannot be called for any Set type.

Environment

  • GHC version used: 8.10.2

Optional:

  • Operating System: Windows
  • System Architecture:
Edited by Anthony Clayden
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information