Another tricky one. There are at least two difficulties. 1. Consider the simpler function foo :: Fc Bool b => [b] -> Int foo (x:xs) = x Since b must be Int, you might argue that this function is OK, but GHC rejects it because it unifies the signature type variable b. This is a "legitimate" constraint on 'b'. The question is how to distinguish the legitimate constraints on b from the illegitimate ones. In principle, not too hard -- just "improve" the type signature, but GHC translates the whole thing to System F, so it really will pass a type parameter for 'b'... Maybe it can be done, but I feel queasy about it. 2. Suppose we have makeF3 i = [MkF2 i, ...., (undefined :: F2 Bool)] When type-checking MkF2 it's less obvious that the result will be an (F2 Bool) than it was in your example. So perhaps type-correctness depends on the "pushing-types-inwards" idea. Well, ok, that's what I do for higher-rank types, but we'd need to precisely say what programs are accepted and what programs are not. At the moment I'm somewhat resisting making further ad-hoc "improvements" to GHC's type-inference algorithm, even though it falls short in various ways, because I keep hoping someone is going to come up with a simple non-ad-hoc story that will address these various issues in a more systematic way. Simon | -----Original Message----- | From: haskell-admin@haskell.org [mailto:haskell-admin@haskell.org] On Behalf Of Ashley Yakeley | Sent: 05 September 2003 01:24 | To: haskell@haskell.org | Subject: Fundep & Datatype Request | | 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 | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell