Infer type context in a type signature

If I have code such as

class Foo f where
    foo :: a -> f a

data Bar f a = Foo f => Bar {bar :: f a}

instance Foo (Bar f) where
    foo a = Bar (foo a)

GHC will demand Foo f => on the instance declaration, even though this can be inferred from the definition of Bar.

I understand why this is happening, but it should not be necessary to repeat information already given. Some code violates DRY dozens of times because of this limitation.

changed weight to 5

added Tfeature request Trac import typechecker labels

changed title from Infer type context from type or data constructor to Infer type context in a type signature

changed the description

I'm sorry but that's the way Haskell is. You could imagine some form like

instance (...) => Foo (Bar f) where
  foo a = ...

meaning "please infer the context for me". This would be useful for type signatures more generally. For example:

f :: (...) => [a] -> String
f xs = show (sum xs)

Here the full type signature would be

f :: (Num a, Show a) => [a] -> String

This has come up before but I can't find a ticket for it, so I'll treat this as it.

Simon

I'm not sure what you mean by "that's the way Haskell is"; many GHC features go beyond the Haskell standard.

Perhaps I misworded the ticket, as I wasn't referring to inferring type contexts from a method's implementation. The type context given in a data-type's definition should be available wherever the data type is used, so the (...) => syntax shouldn't be necessary for this case.

To put the issue differently: A type variable in a data/type constructor is restricted to a given type class. Currently, this restriction has to be repeated in the signature of every function that uses the restriction. This repetition is superfluous noise, which is required by the compiler, but adds no information.

Replying to [ticket:5248#comment:51954 gidyn]:

I'm not sure what my first sentence means either!

To put the issue differently: A type variable in a data/type constructor is restricted to a given type class.

That is no more true of a data constructor than it is of any ordinary function. Consider

bar :: Foo f => f a -> Bar f a
bar = ...lots of code...

Now function bar has the same signature as your data constructor Bar, and gives rise to exactly the same type constraints.

Nor would a function or instance decl necessarily have the same context of the bar or Bar functions. To take a slightly simpler example, consider

class C a where
  op :: a -> a

data Bar a = C a => Bar a a
 -- So Bar :: C a => a -> a -> Bar a

instance (...) => C (Bar a) where
  op (Bar a b) = Bar b a

Here the (...) is empty (not C a) because the constraint arising from the use of Bar is satisfied by the pattern match. }}} Now suppose the instance declaration whose context you want to infer is this:

{{{ instance (...) => Foo (Bar f) where

In short, it's not specifically to do with data constructors, and it's not specifically to do with instance declarations. It would certainly be a useful feature to be allowed to ask GHC to infer the context; but it should certainly be explicit when you are doing so.

Replying to [ticket:5248#comment:51955 simonpj]:

That is no more true of a data constructor than it is of any ordinary function. Consider

bar :: Foo f => f a -> Bar f a
bar = ...lots of code...

Now function bar has the same signature as your data constructor Bar, and gives rise to exactly the same type constraints.

The uniqueness of data constructors in this context is that they are (under normal circumstances) the only way to construct a data type; whenever you see a data type, you know that the type constraint of its constructor has been satisfied.

It would certainly be a useful feature to be allowed to ask GHC to infer the context; but it should certainly be explicit when you are doing so.

This would be different to normal type inference. Instead of inferring the type context required by an equation, the data type (or constructor) itself carries a type context, which is there whether or not it's needed.

For example, your instance C (Bar a) would have a C a => type context. Not because the instance declaration requires it (it doesn't), but because Bar implies it.

That Bar a implies C a => is something that we know to be true in any case, but the compiler currently discards this information.

Replying to [ticket:5248#comment:51960 gidyn]:

This example doesn't require the C a => constraint, but it's certainly there for practical purposes; you can't get a Bar without it.

I don't know what you mean by "for practical purposes". Yes you need (Bar a), but it's supplied by the pattern match on Bar. So it's not needed on the instance, and absolutely should not be. Try it!

This would be different to normal type inference. Instead of inferring the type context required by an equation, the data type (or constructor) itself carries a type context, which is there whether or not it's needed. For example, your instance C (Bar a) would have a C a => type context. Not because the instance declaration requires it (it doesn't), but because Bar implies it.

No. What constraint is required depends on what type Bar (or bar) are applied at. If you apply them at Int you'll need C Int; if you apply them at [a] you'll need C [a], and so on.

That Bar a implies C a => is something that we know to be true in any case, but the compiler currently discards this information.

I don't know what you mean by "know to be true". If you add an unnecessary context to an instance declaration, you'll make some programs fail that previously would type check.

To use a simpler example,

data Eq a => Pair a = Pair {x::a, y::a}

equal :: Eq a => Pair a -> a -> Bool
equal pair z = (x pair) == (y pair) && (x pair) == z

Whenever we see Pair a, we know that Eq a. Nevertheless, the type signature for equal must be augmented with a redundant Eq a =>. If I have two dozen functions relying on the Eq-ness of Pair a, that's two dozen redundant type contexts.

Eq a => should not need to be inferred from the definition of equal, as it is stated explicitly in the definition of Pair.

changed milestone to %7.4.1

changed milestone to %7.6.1

changed weight to 3

Trac metadata

Trac field	Value
Priority	normal → low

changed milestone to %7.6.2

Trac metadata

Trac field	Value
CC	gideon@accursoft.com →

changed milestone to %7.10.1

Moving to 7.10.1.

closed

This is now covered by Partial Type Signatures for general type inference, and #8026 (closed) for the specific case of data types.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedDuplicate

added Plow label