OK, this is an issue I have raised before I think, but I don't remember what the opinion on it was. The following doesn't compile with ghc -fglasgow-exts (or Hugs -98):
-- ghc -fglasgow-exts -c TypeLambda.hs module TypeLambda where { class Fc a b | a -> b; instance Fc Bool Int; data F1 a = forall b. (Fc a b) => MkF1 b; makeF1 :: Int -> F1 Bool; makeF1 = MkF1; getF1 :: F1 Bool -> Int; getF1 (MkF1 i) = i; data F2 a = MkF2 (forall b. (Fc a b) => b); makeF2 :: Int -> F2 Bool; makeF2 i = MkF2 i; getF2 :: F2 Bool -> Int; getF2 (MkF2 i) = i; } Clearly makeF1 and getF2 are OK. But I claim getF1 and makeF2 should compile, since the type inside either an "F1 Bool" or an "F2 Bool" must always be an Int. Instead I get this: TypeLambda.hs:14: Inferred type is less polymorphic than expected Quantified type variable `b' is unified with `Int' When checking an existential match that binds i :: b and whose type is F1 Bool -> Int In the definition of `getF1': getF1 (MkF1 i) = i TypeLambda.hs:19: Cannot unify the type-signature variable `b' with the type `Int' Expected type: b Inferred type: Int In the first argument of `MkF2', namely `i' In the definition of `makeF2': makeF2 i = MkF2 i So why is this useful? Because you can do some form of type-lambda with it. For instance, you might have some system of collection types: Word8 -->> UArray Int Word8 Word16 -->> UArray Int Word16 (a -> b) -->> Array Int (a -> b) It would be nice to hide the implementation and just expose some type-constructor: MyCollection Word8 MyCollection Word16 MyCollection (a -> b) I believe this can't be done currently. -- Ashley Yakeley, Seattle WA _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell