Fundep & Datatype Request

5 Sep 2003

      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