I don't know an algorithm that can always infer the most general types in situations like this. In your example, if you give a signature for the simple function (f :: Y Maybe -> Int), and use RelaxedPolyRec, then GHC will happily infer the type you want for g. For RelaxedPolyRec to work its magic, you just need to cut the strongly connected component with a type signature - but you can cut it anywhere you please. Interesting example, though. I've added a test to GHC's regression suite to make sure we do infer the right type for g, given the monomoprhic type for f. Simon From: haskell-cafe-bounces@haskell.org [mailto:haskell-cafe-bounces@haskell.org] On Behalf Of Job Vranish Sent: 22 June 2010 16:06 To: Haskell Cafe mailing list Subject: [Haskell-cafe] Inferring the most general type Esteemed fellow haskellers, I recently ran into a very simple real life case where Haskell's rules for inferring the types for mutually recursive definitions resulted in a type that was less general than it could be. It took me a while to realize that the type error I was getting wasn't actually a problem with my code. I understand why Haskell does this (it infers the strongly connected mutually recursive definitions monomorphically), but I think it _could_ infer the more general type even with recursive definitions like this. Here is a simplified example that illustrates the problem:
import Data.Maybe
-- The fixed point datatype data Y f = Y (f (Y f))
-- silly dummy function maybeToInt :: Maybe a -> Int maybeToInt = length . maybeToList
-- f :: Y Maybe -> Int f (Y x) = g maybeToInt x
g h x = h $ fmap f x
This is the type it wants to infer for g g :: (Maybe Int -> Int) -> Maybe (Y Maybe) -> Int This is the type I think it should have, note you can't force the type with a typesig without -XRelaxedPolyRec g :: (Functor f) => (f Int -> b) -> f (Y Maybe) -> b If I use -XRelaxedPolyRec I can manually specify the more general type, but then I have to convince myself that there isn't a more general type that I'm missing. Are there other known algorithms that yield a more general type? and if so, what was the rational for Haskell keeping the current method? I worked out an alternative algorithm that would give a more general type (perhaps the most general type) but it has factorial complexity and probably wouldn't be good for strongly connected groups with 7 or more members. Even so, I would much rather have the inferred types always be the most general ones and be required to add type signatures for mutually recursive groups with 7 or more members (which probably need to be redesigned anyway) than be always required to manually figure out the more general signatures. What do you think? - Job