#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 )
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
Description: | modified (diff) |
---|---|
Summary: | Infer type context from type or data constructor → Infer type context in a type signature |
comment:2 follow-up: 3 Changed 8 years ago by
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 follow-up: 4 Changed 8 years ago by
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 follow-up: 5 Changed 8 years ago by
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 constructorBar
, 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.
comment:5 Changed 8 years ago by
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 follow-up: 7 Changed 8 years ago by
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.
comment:8 Changed 8 years ago by
Milestone: | → 7.4.1 |
---|
comment:9 Changed 8 years ago by
Milestone: | 7.4.1 → 7.6.1 |
---|---|
Priority: | normal → low |
comment:10 Changed 7 years ago by
Milestone: | 7.6.1 → 7.6.2 |
---|
comment:11 Changed 6 years ago by
Cc: | gideon@… removed |
---|
comment:13 Changed 5 years ago by
difficulty: | → Unknown |
---|---|
Resolution: | → duplicate |
Status: | new → closed |
This is now covered by Partial Type Signatures for general type inference, and #8026 for the specific case of data types.
I'm sorry but that's the way Haskell is. You could imagine some form like
meaning "please infer the context for me". This would be useful for type signatures more generally. For example:
Here the full type signature would be
This has come up before but I can't find a ticket for it, so I'll treat this as it.
Simon