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: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
Behalf Of Ashley Yakeley
| Sent: 05 September 2003 01:24
| To: [EMAIL PROTECTED]
| 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
| [EMAIL PROTECTED]
| http://www.haskell.org/mailman/listinfo/haskell
_______________________________________________
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
