Record update typing is wrong
Consider this
type family F a
data T b = MkT { x :: [Int], y :: [F b] }
emptyT :: T b
emptyT = MkT [] []
foo1 :: [Int] -> T b
foo1 newx = emptyT { x = newx }
foo2 :: [Int] -> T b
foo2 newx = case emptyT of MkT x y -> MkT newx y
According to the Haskell report, foo1
and foo2
should behave the same. But they don't: foo2
is rejected with
Foo.hs:29:49: error:
• Couldn't match type: F b0
with: F b
Expected: [F b]
Actual: [F b0]
NB: ‘F’ is a non-injective type family
The type variable ‘b0’ is ambiguous
• In the second argument of ‘MkT’, namely ‘y’
In the expression: MkT newx y
In a case alternative: MkT x y -> MkT newx y
• Relevant bindings include
y :: [F b0] (bound at Foo.hs:29:35)
foo2 :: [Int] -> T b (bound at Foo.hs:29:1)
|
29 | foo2 newx = case emptyT of MkT x y -> MkT newx y
| ^
And indeed that makes sense: becuase F
is a type family, we have no way to know at what type to instantiate emptyT
.
So why does foo1
work? It's because of this code in GHC.Tc.Gen.Expr, in the RecordUpd
case of tcExpr
:
-- STEP 4 Note [Type of a record update]
-- Figure out types for the scrutinee and result
-- Both are of form (T a b c), with fresh type variables, but with
-- common variables where the scrutinee and result must have the same type
-- These are variables that appear in *any* arg of *any* of the
-- relevant constructors *except* in the updated fields
--
; let fixed_tvs = getFixedTyVars upd_fld_occs con1_tvs relevant_cons
is_fixed_tv tv = tv `elemVarSet` fixed_tvs
Those "fixed" tyvars are the ones that GHC thinks are going to be the same in "before" and "after" -- and it used all the free vars of unaffected fields (in this case the field y
).
So b
is treated as "fixed".
But that is not what the report says; and it would be reasonably complicated to specify. The simplest thing is to regard this a bug, which leads GHC to accept too many programs. It is not hard to fix foo2
:
foo2 :: forall b. [Int] -> T b
foo2 newx = case (emptyT :: T b) of MkT x y -> MkT newx y
This came up during @CarrieMY's work on !7320 (closed)/#18802 (closed). It turns out that GHC itself uses this idiom in GHC.Hs.Utils:
mkRecStmt anns stmts = (emptyRecStmt' anns) { recS_stmts = stmts }
When we desugar record update in the renamer, this rejected for the reasons above.