Skip to content

InstanceSig incorrectly rejected

Summary

An InstanceSig that's exactly the type inferred by GHC is rejected * Could not deduce (Eq a) from the context: ..., where (Eq a) is exactly what ghci shows for the :type inferred. And indeed is needed for the method implementation.

Ref this discussion.

Steps to reproduce

{-# LANGUAGE  InstanceSigs, FlexibleContexts   #-}

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

instance Functor Set  where
  fmap f  NilSet        = NilSet
  fmap f (ConsSet x xs) = ConsSet (f x) (fmap f xs)

class WFT c_a  where                                      -- Well-Formed Type
  isWF :: c_a -> Bool                                     -- is c_a well-formed?
  mkWF :: c_a -> c_a                                      -- edit c_a to make it well-formed
  mergeWF :: c_a -> c_a -> c_a                            -- merge two c_a giving a well-formed result
instance Eq a => WFT (Set a)  where
  isWF NilSet = True
  isWF (ConsSet x xs) = not (sElem x xs) && isWF xs
  mkWF = fmapSet id
  mergeWF NilSet yss = yss
  mergeWF (ConsSet x xs) yss | sElem x yss = mergeWF xs yss
                             | otherwise   = ConsSet x $ mergeWF xs yss

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
instance WFTFunctor Set  where      
  -- wftfmap :: (Eq aa, Eq bb) => (aa -> bb) -> Set aa -> Set bb                       -- ** rejected **
  -- wftfmap :: (WFT (Set aa), Eq aa, WFT (Set bb), Eq bb) => (aa -> bb) -> Set aa -> Set bb   -- **
  wftfmap :: (WFT (Set aa), WFT (Set bb)) => (aa -> bb) -> Set aa -> Set bb            -- accepted
  wftfmap f xss = mkWF $ fmap f xss

sElem fx NilSet = False
sElem fx (ConsSet fy fys) = fx == fy ||  sElem fx fys

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

Rejection is

* Could not deduce (Eq a)
  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

But Eq a must hold, otherwise the call to mkWF would be ill-typed. The InstanceSig accepted is strictly more polymorphic than what's inferred. ghci's :type:

wftfmap @Set :: (Eq a, Eq b) => (a -> b) -> Set a -> Set b

Expected behavior

Accept the InstanceSig that includes an Eq a.

Environment

  • GHC version used: 8.10.2

Optional:

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