#714: Inconsistency between handling functional dependencies in class and
signature constraints
-------------------------------------+--------------------------------------
Reporter: [EMAIL PROTECTED] | Owner: simonpj
Type: bug | Status: new
Priority: low | Milestone: 6.10 branch
Component: Compiler (Type checker) | Version: 6.5
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown/Multiple
Os: Unknown/Multiple |
-------------------------------------+--------------------------------------
Comment (by claus):
Replying to [comment:16 chak]:
We're getting slightly off-topic for this ticket, but this is interesting.
> Type families are neither strict nor lazy (or rather, I guess, you mean
non-strict). In fact, given that the type language is supposed to be
strongly normalising, the outcome of normalisation is independent of the
evaluation order.
>
> There is absolutely no requirement that a family instance needs to be in
scope in that example. Given the absence of instances for `TF`, `(TF a)`
is simply a type that is only equal to itself and which is not inhabited,
except for bottom. `(TF a)` is already fully normalised.
I see. So you are interpreting TF as a term rewrite system, and a TF
application that can't be reduced further is still a type (or whatever its
kind says it is). Whereas I was interpreting TF as type-level functions,
strict in the sense that they have to be evaluated until they give a (TF-
application-free) type (or type constructor).
So a TF application behaves as an existential type, but can be unwrapped
by providing a matching TF instance, right?
> So, I maintain, GHC is doing the right thing.
I'll have to think about this interpretation of TF as mere rewrite systems
a bit before I can agree or disagree, but this interpretation should
probably be stressed in the TF documentation, to avoid similar
misunderstandings.
> But that name does not occur anywhere else. Hence, it will have no
effect whatsoever on the typing of the rest of the program.
All these examples were reduced to minimum, of course. Iirc, the idea was
to use the variables introduced in the superclass context, and determined
by FD, in the class declaration. Instance method types would then be
determined by the combination of class declaration, instance head, and
superclass instances, giving a net result similar to associated types.
> Judging from your previous comment, I believe I know what you were
trying to do. Given
> {{{
> class TF a ~ b => CTF a
> }}}
> your intention was that whenever somebody declares an instance
> {{{
> instance CTF t
> }}}
> the superclass rules would require that there is also an instance for
`TF t`. Is that right?
In particular, if `CTF` had a method `m :: a -> b`, then the instance
would have a method type `m :: TF t ~ b => t -> b`.
I'd like to repeat, though, that the ticket is about consistency and being
able to bring into scope variables determined by FD or TF uniformly in all
kinds of contexts (function, instance, class, data). Using this with TF
instead of FD apparently isn't meant to work the way I thought it would
(though it would still work for the non-reduced case, where the `b`
actually occurs in the class declaration, right?), but at least it should
be uniform for all contexts.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/714#comment:17>
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
