Unable to infer type when using DuplicateRecordFields

[mpickering]

It seems to me that GHC should be able to easily infer the types for the record updates in this simple example. Is there a reason that it is unable to infer the type currently?

{-# LANGUAGE OverloadedLabels, DuplicateRecordFields #-}
module C where

main = do
  print aThing
  print bThing
  print (aThing { a = 5 } )
  print (bThing { a = 5 } )

data B = B { a :: Int} deriving Show

bThing = B 10

data A = A { a :: Int } deriving Show

aThing = A 10

{-

[1 of 1] Compiling C                ( C.hs, C.o )

C.hs:7:10: error:
    • Record update is ambiguous, and requires a type signature
    • In the first argument of ‘print’, namely ‘(aThing {a = 5})’
      In a stmt of a 'do' block: print (aThing {a = 5})
      In the expression:
        do { print aThing;
             print bThing;
             print (aThing {a = 5});
             print (bThing {a = 5}) }
-}

[adamgundry]

By design, we don't do any inference to determine which record type is meant in this kind of situation. Instead, the type must be pushed in to the update, or the record expression being updated must have a type signature. Thus either of these should work:

  print (aThing { a = 5 } :: A)
  print ((bThing :: B) { a = 5 } )

I suppose we could add a special case for when the record expression is a variable whose type is known, which would cover this example. I'm not sure if it's a good idea to accumulate too many special cases, but perhaps this case is common enough that it's worthwhile?

[mpickering]

I definitely think that a special case should be added then. It is extremely unexpected to have to add a type signature for something like (A 10) { a = 5 }!

[simonpj]

The trouble is that it's hard to say precisely when inference should succeed. How would you suggest writing the specification of what is and is not accepted?

[adamgundry]

At the moment we permit (aThing :: A) { a = 5 } because there is a special rule that looks for a type signature on the record expression. We could have a similar rule that looks for a variable of known type, which would permit aThing { a = 5 }. We'd yet need another rule for (A 10) { a = 5 }; that one looks less useful to me. None of this is doing true inference, though.

[simonpj]

It's far from clear what a "known type" is in "a variable of known type".

Simon

[adamgundry]

When I said "known type" I meant the type of the variable

• given by a signature (or determined by bidirectional type inference) at the binding site, if it is in the same group of mutually-recursive declarations; or

• determined after type-checking, if it is in a previous group of declarations.

Under this approach, the following would work:

f (x :: A) = x { a = 5 }

g :: A -> A
g x = x { a = 5 }

h = aThing { a = 5 }

whereas these would not:

k x = (x :: A, x { a = 5 })

l (x :: Bool -> A) = (x True) { a = 5 }

This is a similar distinction to that made in bidirectional type inference for higher-rank types, where variables can be given a polymorphic type scheme by a signature or a pushed-in scheme, but inferred types must be monomorphic. I think it's easy to implement (and I've done so): given an update of a variable, look up the Id and check if its (un-zonked) type is a TyCon.

One downside is that it invalidates certain syntactic transformations, such as inlining or lambda-lifting. But so do lots of other things!

I've also experimented with an alternative approach: use the inferred type of the expression being updated. This is extremely easy to implement, as it simply requires deleting one guard. Moreover, it covers all the above cases and lots more. However, it doesn't have a nice declarative specification; it is rather dependent on the typechecker implementation. For example,

k x = (x :: A, x { a = 5 })

is accepted but

k' x = (x { a = 5 }, x :: A)

is not.

[adamgundry]

I'm inclined to think we should close this and recommend use of the forthcoming OverloadedRecordFields in cases like this. But if anyone wants to argue for a well-specified but more permissive DuplicateRecordFields, I'm not strongly opposed.