#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 chak):
Replying to [comment:12 claus]:
> Replying to [comment:10 chak]:
> >What is the problem with the following answer?
{{{
*Main> :t tf
tf :: a
}}}
> > The constraint `TF a ~ b` can always be satisfied by `b := TF a` and
does not put any restriction on the application of `tf`.
>
> There should be the restriction that there '''exists''' at least one
type family instance (type function application is strict, not lazy,
right?-) at the point of use. There isn't one at all here.
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.
So, I maintain, GHC is doing the right thing.
> > The same holds for the super class constraint `TF a ~ b`. It is
meaningless; hence, I cannot see why we should support it.
>
> It brings a short name `b` into scope, bound to the result of the type
function application.
But that name does not occur anywhere else. Hence, it will have no effect
whatsoever on the typing of the rest of the program.
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?
Unfortunately, this wouldn't work anyway, for the same reason that `:t tf`
gives you `a`, not `TF a ~ b => a`. A superclass equality of the form `TF
a ~ b`, where `b` doesn't occur anywhere else is trivial to satisfy: just
instantiate `b` with `TF a`. (This again works even if there is no single
instance for `TF`.)
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/714#comment:16>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
