GHC insists that every type class constraint mentions a type variable that is quantified just outside the constraint. E.g. forall a b c. (C a c, D b) => ... The constraints (C a c), (D b) must each mention at least one of a,b,c. Why? Because it makes it much easier to know when a constraint must be solved. Consider f :: K a => ... g :: E b => b -> b g x = let h :: D b => ... h x = ....(f e).... in ... Notice that there is no 'forall' on the type sig for h, so it disobeys GHC's rule. Suppose the call to f is at type (Tree [b]). That gives rise to the constraint (K (Tree [b])). Now, can the constraint (K (Tree [b])) be satisfied by the (D b)? Or by the enclosing constraint (E b)? Or by a combination of the two? At the moment GHC's rule means it can use the rule "a constraint C floats outwards until it hit a 'forall' that binds one of the type variables mentioned in C. Then C must be solved using the constraints bound at that forall". All this makes solving easier. Everything would work fine without the restriction, but inference would be a bit harder. So far, solving that harder inference problem hasn't seemed important enough, but it's certainly soluble. (Martin Sulzmann's implication constraints suggest how.) Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Paul Govereau | Sent: 22 November 2005 07:56 | To: haskell@haskell.org | Subject: Re: [Haskell] Type Class Question | | | Ah yes, but this forces me to write my instance of Show right away. I | cannot write: | | module A where data X = X | module B where | import A | bar x = show x -- here is the problem | moduel C where | import A | instance Show X where show x = "X" | module Main where | import A | import B -- Show instance used | import C -- Show instance defined | | I am not saying that this is terribly useful, I am just wondering why | it is a problem to allow it? | | Paul | | BTW, The above program is a translation of an idiomatic use of | functors in ML (pardon my syntax): | | module A : sig type t = ... end | module B : funsig(X:SHOW where t = A.t) sig bar : A.t -> string end | module C : SHOW where t = A.t | open A | open B(C) | | | On Nov 21, Cale Gibbard wrote: | > data X = X deriving Show | > | > bar :: X -> String | > bar x = show x | > | > There's no need for the class constraint at all. If it's an instance | > of Show, then you're okay with just applying show to it. There's no | > need to actually assert that it's actually an instance of Show again. | > | > The only purpose of class constraints is to restrict polymorphism. If | > a function isn't polymorphic to begin with, you should never need | > them. | > | > - Cale | > | > On 21/11/05, Paul Govereau <govereau@eecs.harvard.edu> wrote: | > > Hello, | > > | > > I was hoping that someone could answer a question I have about the | > > type class system. In Haskell, I cannot write a term with an exact | > > constraint: | > > | > > > data X = X | > > > bar :: Show X => X -> String | > > > bar x = show x | > > | > > According to the Haskell 98 report, a qualifier can only be applied to | > > type variables, but I don't see where the trouble is. The term seems | > > to have reasonable type, and I don't see any reason why the | > > dictionary-passing translation shouldn't work out; I am wondering what | > > problems you run into if this restriction is lifted? | > > | > > Note, with GHC and Glasgow extensions you can write this program: | > > | > > > data Y a = Y | > > > foo :: Show (Y a) => Y a -> String | > > > foo x = show x | > > | > > However, the first program is still ruled out. Are there any | > > type-class experts out there that can offer an explanation? | > > | > > Thanks, | > > Paul | > > _______________________________________________ | > > Haskell mailing list | > > Haskell@haskell.org | > > http://www.haskell.org/mailman/listinfo/haskell | > > | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell