| The important question is whether this will retain *complete* type | inference? For example, in case of type annotations we need to | test for equivalence among constraints.
An excellent question. Here's an example, adapted from Ross: class C a where type Result a method :: a -> Result a instance C (Maybe a) where type Result (Maybe a) = Bool g :: (a->a) -> Int g f = 3 w ::Int w = g (\b x -> if b then Just (method x) else x) Now, as Ross pointed out, the (\b x->...) expression has inferred type (a = Maybe (Result a), C a) => Bool -> a -> a Alas, g simply discards its argument, so there are no further constraints on 'a'. I think Martin would argue that type inference should succeed with a=Bool, since there is exactly one solution. Is this an example of what you mean? However, as a programmer I would not be in the least upset if inference failed, and I was required to add a type signature. I don't expect type inference algorithms to "guess", or to solve recursive equations, and that's what is happening here. (Notice that it's quite hard to set up this problem. First you need a program whose equality constraints become recursive. Then you need to arrange that the type variables in the recursion are not mentioned elsewhere -- if they were, they'd be instantiated there, and everything would be ok.) What I am less sure of is how to *specify* the type system so that it describes these hard-to-infer programs as illegal. Presumably it's a question of setting up the entailment system so that it has limited rules of deduction -- more limited than first order logic. Simon _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime