Constraint Inference from Instances

Question

Consider the following:

{-# LANGUAGE FlexibleContexts #-}
module Foo where

data D a = D a
class Foo b

instance (Num a) => Foo (D a)

f :: (Foo (D a)) => a -> a
f x = x+1

GHC complains that it cannot deduce Num a in f. I would like this constraint to be inferred from the (non-overlapping) instance of Foo for D a.

I know I could use a GADT for D and add the constraint Num a there, but I'm hoping to not have to pollute the constructor for D with lots of unnecessary constraints. Is there any hope of this ever happening, and is it possible now?

Answer 1

I am guessing this would break for overlapping instances, and therefore is not inferred in general. That is, you could have

{-# LANGUAGE OverlappingInstances #-}
...
instance (Num a) => Foo (D a)

instance Foo (D Bool)

and then your desired inference would certainly not be sound.

EDIT: Looking more closely at the documentation, it is possible to have

{-# LANGUAGE FlexibleContexts #-}
module Foo where

data D a = D a
class Foo b

instance (Num a) => Foo (D a)

f :: (Foo (D a)) => a -> a
f x = x+1

and then in a separate file:

{-# LANGUAGE OverlappingInstances #-}
module Bar where

import Foo

instance Foo Bool

test = f True

That is, the documentation implies only one of the modules defining the two instances needs to have the OverlappingInstances flag, so if Foo.f were definable as this, you could make another module Bar break type safety completely. Note that with GHC's separate compilation, f would be compiled completely without knowledge of the module Bar.

Answer 2

The arrow => is directional. It means that if Num a holds then Foo (D a). It does not mean that if Foo (D a) holds then Num a holds.

The knowledge that there are (and will never be) any overlapping instances for Foo (D a) should imply that the reverse implication is also true, but (a) GHC doesn't know this and (b) GHC's instance machinery is not set up to use this knowledge.

To actually compile functions that use type classes, it's not enough for GHC to merely prove that a type must be an instance of a class. It has to actually come up with a specific instance declaration that provides definitions of the member functions. We need a constructive proof, not just an existence proof.

To identify an instance of class C, it can either reuse one that will be chosen by the caller of the function being compiled, or it must know the types involved concretely enough to select a single instance from those available. The function being compiled will only be passed an instance for C if it has a constraint for C; otherwise the function must be sufficiently monomorphic that it can only use a single instance.

Considering your example specifically, we can see that f has a constraint for Foo (D a), so we can rely on the caller providing that for us. But the caller isn't going to give us an instance for Num a. Even if you presume that we know from the Num a constraint on Foo (D a) that there must be such an instance out there somewhere, we have no idea what a is, so which definition of + should we invoke? We can't even call another function that works for any Num a but is defined outside the class, because they will all have the Num a constraint and thus expect us to identify an instance for them. Knowing that there is an instance without having having the instance is just not useful.

It isn't at all obvious, but what you're actually asking GHC to do is to do a runtime switch on the type a that arrives at runtime. This is impossible, because we're supposed to be emitting code that works for any type in Num, even types that don't exist yet, or whose instances don't exist yet.

A similar idea that does work is when you have a constraint on the class rather than on the instance. For example:

class Num a => Foo a 

f :: Foo a => a -> a
f x = x + 1

But this only works because we know that all Foo instances must have a corresponding Num instance, and thus all callers of a function polymorphic in Foo a know to also select a Num instance. So even without knowing the particular a in order to select a Num instance, f knows that its caller will also provide a Num instance along with the Foo instance.

In your case, the class Foo knows nothing about Num. In other examples Num might not even be defined in code accessible to the module where the class Foo is defined. It's the class that sets the required information that has to be provided to call a function that is polymorphic in the type class, and those polymorphic functions have to be able to work without any knowledge specific to a certain instance.

So the Num a => Foo (D a) instance can't store the Num instance - indeed, the instance definition is also polymorphic in a, so it's not able to select a particular instance to store even if there was space! So even though f might be able to know that there is a Num a instance from Foo (D a) (if we presume certain knowledge that no overlapping could ever be involved), it still needs a Num a constraint in order to require its callers to select a Num instance for it to use.