Hello,
please consider the following code: > {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} > > data GADT a where > > GADT :: GADT () > > class Class a b | a -> b > > instance Class () () > > fun :: (Class a b) => GADT a -> b > fun GADT = () I’d expect this to work but unfortunately, using GHC 6.8.2, it fails with the following message: > FDGADT.hs:12:11: > Couldn't match expected type `b' against inferred type `()' > `b' is a rigid type variable bound by > the type signature for `fun' at FDGADT.hs:11:16 > In the expression: () > In the definition of `fun': fun GADT = () What’s the reason for this? Is there a workaround? Does this work in 6.8.3 or 6.10.1? Thank you in advance. Best wishes, Wolfgang _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch
<[hidden email]> wrote: > Hello, > > please consider the following code: > >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} >> >> data GADT a where >> >> GADT :: GADT () >> >> class Class a b | a -> b >> >> instance Class () () >> >> fun :: (Class a b) => GADT a -> b >> fun GADT = () > > I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the > following message: bear in mind that the only instance you defined is instance Class () () which doesn't involve your GADT at all. Maybe you meant something like: instance Class (GADT a) () Moreover, your fun cannot typecheck, regardless of using MPTC or GADTs. The unit constructor, (), has type () and not b. _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Am Dienstag, 23. September 2008 18:19 schrieben Sie:
> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch > > <[hidden email]> wrote: > > Hello, > > > > please consider the following code: > >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} > >> > >> data GADT a where > >> > >> GADT :: GADT () > >> > >> class Class a b | a -> b > >> > >> instance Class () () > >> > >> fun :: (Class a b) => GADT a -> b > >> fun GADT = () > > > > I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with > > the following message: > > bear in mind that the only instance you defined is > > instance Class () () > > which doesn't involve your GADT at all. This is correct. (It’s only a trimmed-down example, after all.) > Maybe you meant something like: > > instance Class (GADT a) () No, I didn’t. > Moreover, your fun cannot typecheck, regardless of using MPTC or > GADTs. The unit constructor, (), has type () and not b. Pattern matching against the data constructor GADT specializes a to (). Since Class uses a functional dependency, it is clear that b has to be (). So it should typecheck. At least, I want it to. ;-) Best wishes, Wolfgang _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
On Tue, Sep 23, 2008 at 6:36 PM, Wolfgang Jeltsch
<[hidden email]> wrote: > Pattern matching against the data constructor GADT specializes a to (). Since > Class uses a functional dependency, it is clear that b has to be (). True, but it wont work if you provide () as the result and b in the explicit signature. GHC is ranting with reason, the provided type, b, does not match (). On the other hand, this works: fun :: (Class a b) => GADT a -> b fun GADT = undefined And as you stated, b can only be () _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Wolfgang Jeltsch-2
On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch
<[hidden email]> wrote: > Am Dienstag, 23. September 2008 18:19 schrieben Sie: >> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch >> >> <[hidden email]> wrote: >> > Hello, >> > >> > please consider the following code: >> >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} >> >> >> >> data GADT a where >> >> >> >> GADT :: GADT () >> >> >> >> class Class a b | a -> b >> >> >> >> instance Class () () >> >> >> >> fun :: (Class a b) => GADT a -> b >> >> fun GADT = () >> > >> > I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with >> > the following message: >> >> bear in mind that the only instance you defined is >> >> instance Class () () >> >> which doesn't involve your GADT at all. > > This is correct. (It's only a trimmed-down example, after all.) > >> Maybe you meant something like: >> >> instance Class (GADT a) () > > No, I didn't. > >> Moreover, your fun cannot typecheck, regardless of using MPTC or >> GADTs. The unit constructor, (), has type () and not b. > > Pattern matching against the data constructor GADT specializes a to (). Since > Class uses a functional dependency, it is clear that b has to be (). So it > should typecheck. At least, I want it to. ;-) In the signature: fun :: (Class a b) => GADT a -> b What is there to determine the type a? It's a phantom in the definition of GADT, so it can unify arbitrarily for us, but there is nothing in your program to cause it to unify a certain way. Based on what you're hoping for, I think you would need: class Class a b | b -> a But, then think about how the type checker looks at fun, which returns (). Now we see that b should be (), but () is not the same as b. That is, () does not generalize to b, even though an arbitrary b could specialize to (). Did some other version of ghc accept this code? Jason _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Wolfgang Jeltsch-2
On Tue, Sep 23, 2008 at 9:36 AM, Wolfgang Jeltsch
<[hidden email]> wrote: > Am Dienstag, 23. September 2008 18:19 schrieben Sie: >> On Tue, Sep 23, 2008 at 6:07 PM, Wolfgang Jeltsch >> >> <[hidden email]> wrote: >> > Hello, >> > >> > please consider the following code: >> >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} >> >> >> >> data GADT a where >> >> >> >> GADT :: GADT () >> >> >> >> class Class a b | a -> b >> >> >> >> instance Class () () >> >> >> >> fun :: (Class a b) => GADT a -> b >> >> fun GADT = () >> > >> > I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with >> > the following message: >> >> bear in mind that the only instance you defined is >> >> instance Class () () >> >> which doesn't involve your GADT at all. > > This is correct. (It's only a trimmed-down example, after all.) > >> Maybe you meant something like: >> >> instance Class (GADT a) () > > No, I didn't. > >> Moreover, your fun cannot typecheck, regardless of using MPTC or >> GADTs. The unit constructor, (), has type () and not b. > > Pattern matching against the data constructor GADT specializes a to (). Since > Class uses a functional dependency, it is clear that b has to be (). So it > should typecheck. At least, I want it to. ;-) I'm re-reading what you said after my first reply. I'm inserting types in places that may not be valid in Haskell... You're saying that the types should be like this: fun :: (Class a b) => GADT a -> b fun (GADT :: GADT ()) = () So, now I'm more inclined to agree with you than before. And suppose we added this: data GADT a where GADT :: GADT () GADT2 :: GADT String Now I would expect this: fun :: (Class a b) => GADT a -> b fun (GADT :: GADT ()) = () fun (GADT2 :: GADT String) = -- I can't put anything here till I add more instances of Class Now, I'm too confused about how this should work. Jason _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Wolfgang Jeltsch-2
On Tue, Sep 23, 2008 at 9:07 AM, Wolfgang Jeltsch
<[hidden email]> wrote: > Hello, > > please consider the following code: > >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} >> >> data GADT a where >> >> GADT :: GADT () >> >> class Class a b | a -> b >> >> instance Class () () >> >> fun :: (Class a b) => GADT a -> b >> fun GADT = () > > I'd expect this to work but unfortunately, using GHC 6.8.2, it fails with the > following message: > >> FDGADT.hs:12:11: >> Couldn't match expected type `b' against inferred type `()' >> `b' is a rigid type variable bound by >> the type signature for `fun' at FDGADT.hs:11:16 >> In the expression: () >> In the definition of `fun': fun GADT = () > > What's the reason for this? Is there a workaround? Does this work in 6.8.3 > or 6.10.1? There is one workaround that I can think of. Use a data type to get the level of polymorphism you need. You could create a data type to hold b and return that instead of the naked b. data Any where Any :: a -> Any Now you could say, fun :: GADT a -> Any If you go with this existential solution you'll probably want to add type class constraints to the 'a' in Any so that you can recover enough about the type to use the value later. Jason _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Jason Dagit-2
You cannot create a normal function "fun". You can make a type class function
fun :: Class a b => GADT a -> b > data GADT a where > GADT :: GADT () > GADT2 :: GADT String > > -- fun1 :: GADT () -> () -- infers type > fun1 g = case g of > (GADT :: GADT ()) -> () > > -- fun2 :: GADT String -> Bool -- infers type > fun2 g = case g of > (GADT2 :: GADT String) -> True > > -- "fun" cannot type check. The type of 'g' cannot be both "GADT ()" and "GADT String" > -- This is because "fun" is not a member of type class. > {- > fun g = case g of > (GADT :: GADT ()) -> () > (GADT2 :: GADT String) -> True > -} > > class Class a b | a -> b where > fun :: GADT a -> b > > instance Class () () where > fun GADT = () > > instance Class String Bool where > fun GADT2 = True > > main = print $ (fun GADT, fun GADT2) == ( (), True ) > _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
On Tue, Sep 23, 2008 at 1:44 PM, Chris Kuklewicz
<[hidden email]> wrote: > You cannot create a normal function "fun". You can make a type class > function > > fun :: Class a b => GADT a -> b > >> data GADT a where >> GADT :: GADT () >> GADT2 :: GADT String >> >> -- fun1 :: GADT () -> () -- infers type >> fun1 g = case g of >> (GADT :: GADT ()) -> () >> >> -- fun2 :: GADT String -> Bool -- infers type >> fun2 g = case g of >> (GADT2 :: GADT String) -> True >> >> -- "fun" cannot type check. The type of 'g' cannot be both "GADT ()" and >> "GADT String" >> -- This is because "fun" is not a member of type class. >> {- fun g = case g of >> (GADT :: GADT ()) -> () >> (GADT2 :: GADT String) -> True >> -} It may be that fun cannot type check, but surely it isn't for the reason you've given. data Rep a where Unit :: Rep () Int :: Rep Int zero :: Rep a -> a zero r = case r of Unit -> () Int -> 0 The type of r is "both" Rep () and Rep Int. No type class needed. If I had to guess, I'd say the original problem is that any specialization triggered by the functional dependency happens before the specialization triggered by pattern matching on the GADT. If I recall correctly, it is known that GADTs and fundeps don't always work nicely together. The example does seem to work if translated to use type families. type family Fam t :: * type instance Fam () = () data GADT a where GADT :: GADT () fun :: GADT a -> Fam a fun GADT = () -- Dave Menendez <[hidden email]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Wolfgang Jeltsch-2
Am Dienstag, 23. September 2008 19:07 schrieben Sie:
> >> {-# LANGUAGE GADTs, MultiParamTypeClasses, FunctionalDependencies #-} > >> > >> data GADT a where > >> > >> GADT :: GADT () > >> > >> class Class a b | a -> b > >> > >> instance Class () () > >> > >> fun :: (Class a b) => GADT a -> b > >> fun GADT = () > > > > I’d expect this to work but unfortunately, using GHC 6.8.2, it fails with > > the > > > > following message: > >> FDGADT.hs:12:11: > >> Couldn't match expected type `b' against inferred type `()' > >> `b' is a rigid type variable bound by > >> the type signature for `fun' at FDGADT.hs:11:16 > >> In the expression: () > >> In the definition of `fun': fun GADT = () > > > > What’s the reason for this? Is there a workaround? Does this work in > > 6.8.3 or 6.10.1? > > This similar code using type families compiles in 6.8.3 and 6.9: > > data GADT a where > GADT :: GADT () > > type family F a > type instance F () = () > > fun :: GADT a -> F a > fun GADT = () Exactly. But this makes my code incompatible with GHC 6.6. :-( I thought, someone said that with the new typing machinery in GHC 6.10, more functional dependency programs are accepted because functional dependencies are handled similarly to type families (or something like that). Is this true? Since the type family version is okay, why shouldn’t the functional dependency version be okay? Best wishes, Wolfgang _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
On Wed, Sep 24, 2008 at 12:55:29PM +0200, Wolfgang Jeltsch wrote:
> > I thought, someone said that with the new typing machinery in GHC 6.10, more > functional dependency programs are accepted because functional dependencies > are handled similarly to type families (or something like that). Is this > true? Since the type family version is okay, why shouldn’t the functional > dependency version be okay? In http://hackage.haskell.org/trac/ghc/ticket/345 Simon says: Ultimately, I think we can implement fundeps using type families, and then the fundep version will work too. Until then, it'll only work in type-family form. Thanks Ian _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Am Mittwoch, 24. September 2008 15:11 schrieb Ian Lynagh:
> On Wed, Sep 24, 2008 at 12:55:29PM +0200, Wolfgang Jeltsch wrote: > > I thought, someone said that with the new typing machinery in GHC 6.10, > > more functional dependency programs are accepted because functional > > dependencies are handled similarly to type families (or something like > > that). Is this true? Since the type family version is okay, why > > shouldn’t the functional dependency version be okay? > > In > http://hackage.haskell.org/trac/ghc/ticket/345 > Simon says: > Ultimately, I think we can implement fundeps using type families, > and then the fundep version will work too. Until then, it'll only > work in type-family form. > > > Thanks > Ian And further: > So, since we now have a good workaround (well, actually, a better way to > write the program rather than a workaround), I'll leave it open, but at low > priority and with milestone bottom. So for now the answer is: Use type families and thereby drop 6.6 compatibility? Best wishes, Wolfgang _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Wolfgang Jeltsch-2
Wolfgang writes
| > data GADT a where | > | > GADT :: GADT () | > | > class Class a b | a -> b | > | > instance Class () () | > | > fun :: (Class a b) => GADT a -> b | > fun GADT = () You're right that this program should typecheck. In the case branch we discover (locally) that a~(), and hence by the fundep, b~(), and away you go. This has never worked with fundeps, because it involves a *local* type equality (one that holds in some places and not others) and my implementation of fundeps is fundamentally based on *global* equality. Prior to GADTs that was fine! By adding local type equalities, GADTs change the game, and associated types/type families change it even more. (One reason that the game is different is that GHC has a typed intermediate language, so we need to maintain evidence of type equality throughout. In contrast, global equalities can be handled by straightforward unification, that makes the two types *identical*.) Our new implementation of type functions does, for the first time, a thorough principled job of handling arbitrary local type equalities. But that still leaves fundeps. Rather than try to fix fudeps directly (which would be a big job -- as I say, the current impl is fundamentally global) the best thing to do is to translate them into type equalities, thus: class (F a ~ b) => C a b type family F a (Note for 6.10 users: type equalities in superclasses is the piece we still have not implemented.) When you write an instance decl you add a type instance decl: instance C () () type F () = () Now everything should be good. Almost all fundep programs can be translated in this way. (Maybe all, I'm not 100% certain.) If you are doing this yourself, you can usually remove C's second parameter; but only if the fundep is unidirectional. So, as of now (6.10), the fundep stuff is still handled exactly as before, using global unification, so your program isn't going to work in 6.10 either. I'm frankly dubious about whether it's worth the effort of automatically performing the above translation from fundeps to type equalities; if you want this level of sophistication, you could just use type functions directly. It's not really a lack of backward compat. I think 6.10 will do all that 6.8 does; but if you want *more* you'll have to switch notation. Does that help clear things up, and explain why things are the way they are? Simon _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
> This has never worked with fundeps, because it involves a *local* type equality (one that holds in
> some places and not others) and my implementation of fundeps is fundamentally based on *global* > equality. Prior to GADTs that was fine! Thanks for the explanation, Simon - it clears up some outstanding FD issues. > Now everything should be good. Almost all fundep programs can be translated in this way. (Maybe > all, I'm not 100% certain.) If you are doing this yourself, you can usually remove C's second > parameter; but only if the fundep is unidirectional. You can be 100% certain that not all FD programs can be translated to TF, if only because of interaction with overlapping instances. This is an area where Ghc differs from Hugs, doing different things for the "same" LANGUAGE extension, and it is difficult territory: Hugs' interpretation is safe, but too restricted in practice, Ghc's is a lot more flexible in practice, at the expense of not knowing whether it is safe in general, leaving those concerns to type class library implementers. I had hoped that Haskell' or Ghc would single out the actual use cases, and work towards principled solutions for these, whether for FD or for TF (eg, guards and closed instances might help). > So, as of now (6.10), the fundep stuff is still handled exactly as before, using global > unification, so your program isn't going to work in 6.10 either. I'm frankly dubious about > whether it's worth the effort of automatically performing the above translation from fundeps to > type equalities; if you want this level of sophistication, you could just use type functions > directly. > > It's not really a lack of backward compat. I think 6.10 will do all that 6.8 does; but if you > want *more* you'll have to switch notation. Does that help clear things up, and explain why > things are the way they are? Many of the issues that are going to be fixed for TF have been raised as bugs in the old implementation of FD. If FD are not going to see the same fixes, programs need to switch to TF, which isn't backwards or otherwise compatible (and may well deliver the final blow to the idea of more than one Haskell implementation?). Claus _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Simon Peyton Jones
Hello Simon,
thank you for your extensive answer! I think, I’ll try to work around the fundep deficiencies and if that doesn’t work, switch to type families. But your answer raised further questions/comments: > class (F a ~ b) => C a b > type family F a > > (Note for 6.10 users: type equalities in superclasses is the piece we still > have not implemented.) Do you mean type equalities like the one in the example above? Didn’t this already work in 6.8.2? > Almost all fundep programs can be translated in this way. (Maybe all, I'm > not 100% certain.) Not all, I’m afraid. There was a mailing list discussion between us several months ago where we talked about this. The translation from fundeps to type families doesn’t work as soon as overlapping instances are involved. The type equality check from HList is an example for this. You told me that such a check can be implemented with type families as soon as we have closed TFs: type family TypeEq t1 t2 :: * where TypeEq t t = True TypeEq t1 t2 = False Greetings to Victoria! (from Cottbus) Wolfgang _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Claus Reinke
>> This has never worked with fundeps, because it involves a *local* type equality (one that holds
>> in some places and not others) and my implementation of fundeps is fundamentally based on >> *global* equality. Prior to GADTs that was fine! Actually, how does that relate to reasoning under assumptions? class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => .. f = .. There is no instance of 'FD', so no equalities can be derived from there outside of 'f', and no equalities should be derived globally from instances that are only local hypotheses in 'f' . But inside 'f', we assume that those two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of the implication. Isn't that decidedly local? Claus _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
By "global" I really meant "throughout the scope of the type variable concerned.
Nevertheless, the program you give is rejected, even though the scope is global: class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y Both GHC and Hugs erroneously reject the program, just as they do this one instance FD Int Bool g :: FD Int b => ... The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) isn't up to the job. That is what we are fixing with type functions. I do not know how to fix it for FDs (except by way of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to. Simon | -----Original Message----- | From: Claus Reinke [mailto:[hidden email]] | Sent: 24 September 2008 19:27 | To: Simon Peyton-Jones; [hidden email] | Subject: Re: GADTs and functional dependencies | | >> This has never worked with fundeps, because it involves a *local* type | equality (one that holds | >> in some places and not others) and my implementation of fundeps is | fundamentally based on | >> *global* equality. Prior to GADTs that was fine! | | Actually, how does that relate to reasoning under assumptions? | | class FD a b | a -> b | | f :: (FD t1 t2, FD t1 t3) => .. | f = .. | | There is no instance of 'FD', so no equalities can be derived from there | outside of 'f', and no equalities should be derived globally from instances | that are only local hypotheses in 'f' . But inside 'f', we assume that those | two 'FD' instances exist, so we should assume 't2 ~ t3' to the right of | the implication. | | Isn't that decidedly local? | Claus | | _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
> By "global" I really meant "throughout the scope of the type variable concerned.
> > Nevertheless, the program you give is rejected, even though the scope is global: > > class FD a b | a -> b > > f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 > f x y = y > > Both GHC and Hugs erroneously reject the program, while both GHC and Hugs accept this variation: class FD a b | a -> b f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = undefined and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'. So they use the FD globally (when checking use of 'f'), but not locally (when checking the definition of 'f'). Is that interpretation correct, or is there another bug involved? > The problem is that the implementation technique for FDs used by GHC and Hugs (global unification) > isn't up to the job. Interesting. When the FD-via-CHR discussion started, I toyed with the idea of writing an instance inference engine based on CHR (since CHR happen to be a variant of CPN - Coloured Petri Nets -, I happened to have an implementation at hand;-). But once I noticed the difficulties of managing local constraint stores (and exchanging some, but not all inferred information with the global constraint store), I abandoned the idea. Ever since then I've been wondering how GHC handles that!-) >That is what we are fixing with type functions. I do not know how to fix it for FDs (except by way >of translation to TFs) -- at least, not while maintaining a strongly typed intermediate language. >This latter constraint is a condition imposed by GHC, but it's one I am strongly committed to. Since FDs constrain the set of valid instances, I had been wondering whether one could apply the FD-based refinements/substitutions to the code obtained (just as they are applied to the class constraints) while keeping a typed intermediate language. Claus _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
| while both GHC and Hugs accept this variation:
| | class FD a b | a -> b | f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 | f x y = undefined | | and infer the type of 'f' to be 'f :: (FD t1 t3) => t1 -> t3 -> t3'. | | So they use the FD globally (when checking use of 'f'), but not locally | (when checking the definition of 'f'). Is that interpretation correct, or is | there another bug involved? No, by "globally" I meant "throughout the scope of a type variable". I'm surprised GHC accepts the program you give, because it should unify two skolems. With a minor change it fails f :: (FD t1 t2, FD t1 t3) => t1 -> t2 -> t3 f x y = y As I say, GHC's implementation of FDs is flaky and inconsistent; and that is not just because I'm lazy but because it is hard to know just what to do, most especially in situations like this when there is no System F translation. That is why I've been working so hard on FC. Simon _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Free forum by Nabble | Edit this page |