Instance signatures: constraints on methods

Question

With InstanceSignatures, I can give a signature for a method within an instance decl.

The type signature in the instance declaration must be more polymorphic than (or the same as) the one in the class declaration, instantiated with the instance type.

I can see from this answer that the type part of the sig can't be more specific; but why couldn't you add extra constraints? After all you can put constraints on the instance decl that will make the instance more specific than "the class declaration, instantiated with the instance type".

Addit: (In response to the first couple of comments.) To explain "you can put constraints on the instance decl ... instance more specific": the OVERLAPPABLE instance head here alleges it provides addNat for all types a, b, c. But it doesn't: it only provides if a is of the form SNat a', c is of the form SNat c', etc. I'm asking why I can't similarly restrict the types at the method level?

For example [adapted from Hughes 1999] (more realistically this could be a BST/Rose tree, etc):

data AscList a = AscList [a]                          -- ascending list

instance Functor AscList  where                       -- constructor class
  fmap f (AscList xs) = AscList $ sort $ fmap f xs
  -- :: Ord b => (a -> b) -> AscList a -> AscList b   -- inferred

Without an instance signature GHC complains no instance for (Ord b). With the signature GHC complains the instantiated sig from the class is more polymorphic than the one given.

This (excellent) answer explains the machinery in the instance dictionary. I can see the entry in the dictionary for the method has a type set from the number of constraints for the method (if any) in the class decl. There's no room to put an extra dictionary/parameter for the method.

That seems merely that the implementation didn't foresee a need. Is there a deeper/more theory-based reason against?

(BTW I'm not ever-so convinced by Hughes' approach: that would want both Ord a => WFT(AscList a) and Ord b => WFT(AscList b). But there's no need to require the incoming (AscList a) is ascending. Other constructor classes for AscList perhaps don't need an Ord constraint anywhere.)

ghc's error message is quite clear here: you cannot fmap an arbitrary function and receive a sorted list. As it's currently written in your question, you don't even require AscList's argument be Ord. — bipll
The functor class definition states that a type constructor F is a functor iff it provides fmap for all types a and b. So it's all-or-nothing, either F is a functor or it is not (fmap does not work in at least one case). This would be different if we had a functor class like class Functor' f a b where fmap' :: (a->b)->f a->f b where a,b are indices of the class, hence can be constrained in instances. In the libraries there are some variants like this but they are not frequently used in practice. — chi
Your Functor instance violates the law fmap id == id. (id (AscList [3,2,1]) == AscList [3,2,1], but fmap id (AscList [3,2,1]) == AscList [1,2,3].) (Though you can get away with it if you ensure that an AscList value can only be created with a smart constructor prevents an unsorted list from being created in the first place.) — chepner
@chepner, ah ok, so I do need WFT (AscList a) as proxy saying the incoming list is sorted. Then the law still holds. — AntC
Actually, I'm don't think you can preserve the other law, fmap (f.g) == fmap f . fmap g. If fmap g reorders the list, f is applied to different elements than if f.g were used directly. — chepner

Li-yao Xia Li-yao Xia · Accepted Answer · 2021-02-10T13:51:44

If you allow adding constraints to instance methods that aren't already in the class method, a polymorphic function using type classes might no longer typecheck when you specialize it.

For example, consider your AscList instance above, and the following usage of Functor:

data T f = T (f (IO ()))  -- f applied to a non-Ord

example :: Functor f => T f -> T f
example (T t) = T (fmap (\x -> x >> print 33) t)

The type of example says you can instantiate f with any functor, such as f = AscList.
But that makes no sense because it would try to sort an AscList (IO ()).

The only way to tell that something goes wrong when we specialize example here is to read its definition, to find whether uses of fmap are still valid, and that goes against modularity. The type class constraints in a type signature do not and should not record how their methods are used. Conversely, that means that instances do not get to add constraints to their method implementations.

Instance signatures: constraints on methods

1 Answers