#5248: Infer type context in a type signature
----------------------------------------+-----------------------------------
Reporter: gidyn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 7.0.3
Keywords: | Testcase:
Blockedby: | Difficulty:
Os: Unknown/Multiple | Blocking:
Architecture: Unknown/Multiple | Failure: GHC rejects valid
program
----------------------------------------+-----------------------------------
Comment(by gidyn):
Replying to [comment:3 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.
> 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.
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.
> 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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5248#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
