Opened 8 years ago

Closed 5 years ago

Last modified 5 years ago

#5248 closed feature request (duplicate)

Infer type context in a type signature

Reported by: gidyn Owned by:
Priority: low Milestone: 7.10.1
Component: Compiler (Type checker) Version: 7.0.3
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

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.

Change History (13)

comment:1 Changed 8 years ago by simonpj

Description: modified (diff)
Summary: Infer type context from type or data constructorInfer type context in a type signature

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

comment:2 Changed 8 years ago by gidyn

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.

comment:3 in reply to:  2 ; Changed 8 years ago by simonpj

Replying to 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. 

comment:4 in reply to:  3 ; Changed 8 years ago by gidyn

Replying to 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.

Last edited 5 years ago by gidyn (previous) (diff)

comment:5 in reply to:  4 Changed 8 years ago by simonpj

Replying to 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.

comment:6 Changed 8 years ago by gidyn

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.

Last edited 5 years ago by gidyn (previous) (diff)

comment:7 in reply to:  6 Changed 8 years ago by gidyn

Last edited 5 years ago by gidyn (previous) (diff)

comment:8 Changed 8 years ago by igloo

Milestone: 7.4.1

comment:9 Changed 8 years ago by igloo

Milestone: 7.4.17.6.1
Priority: normallow

comment:10 Changed 7 years ago by igloo

Milestone: 7.6.17.6.2

comment:11 Changed 6 years ago by gidyn

Cc: gideon@… removed

comment:12 Changed 5 years ago by thoughtpolice

Milestone: 7.6.27.10.1

Moving to 7.10.1.

comment:13 Changed 5 years ago by gidyn

difficulty: Unknown
Resolution: duplicate
Status: newclosed

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

Note: See TracTickets for help on using tickets.