functions on records with overloaded names can be given a too-specific type

[dmwit]

Here's a reduced test-case showing a discrepancy between the symmetric functions foo and bar; the inferred type for foo is too specific.

data T a = A{ m1 :: a } | B{ m1, m2 :: a } | C{ m2 :: a }

-- bar :: (t -> a) -> T t -> T a
bar f x@(A m) = x{m1 = f m}

-- foo :: (a -> a) -> T a -> T a
foo f x@(C m) = x{m2 = f m}

[simonpj]

What you say is true but depends, in a way that's invisible to the type system, on the pattern match on C. If you had

-- foo1 :: (a -> a) -> T a -> T a
foo1 f x = x{m2 = f m}

then indeed the inferred type would be right.

For better or worse, the type system takes no account of which data constructors are matched in an enclosing context except for GADTs, and that is a different story.

In short, this is more of a feature request than a bug, so I'll close it as invalid. If you want to make a feature request, by all means do, but personally I doubt that there'd be a big market for it.

Simon

[dmwit]

Okay, in that case, I'd like to change the bug description. =)

It doesn't bother me so much that the type is too specific; what bothers me is the discrepancy between foo and bar. Why wouldn't your argument apply equally well to bar, leading us to expect an inferred type of bar :: (a -> a) -> T a -> T a? In other words, either both types should be general, or both types should be specific.

I'm re-opening, but I've had my say; if you still consider it invalid, I'll quiesce.

[simonpj]

Aha! I was looking only at bar, for which my claims are correct. I ignored foo, and you are quite right: foo's inferred type is utterly wrong. And indeed, compiling your code with -dcore-lint barfs in GHC 6.10.

Fixed by this patch, with a test case added to the regression suite:

Wed May 13 16:09:22 BST 2009  simonpj@microsoft.com
  * Fix Trac #3219: type of a record update
  
  Record updates are amazingly hard to typecheck right.  This is one place
  where GHC's policy of typechecking the original source is much harder than
  desugaring and typechecking that!
  
  Anyway, the bug here is that to compute the 'fixed' type variables I was
  only looking at one constructor rather than all the relevant_cons

Thank you for being persistent.

Simon