Desugar RecordUpd in `tcExpr`wip/T18802

This patch typechecks record updates by desugaring them inside
the typechecker using the HsExpansion mechanism, and then typechecking
this desugared result.

Example:

    data T p q = T1 { x :: Int, y :: Bool, z :: Char }
               | T2 { v :: Char }
               | T3 { x :: Int }
               | T4 { p :: Float, y :: Bool, x :: Int }
               | T5

The record update `e { x=e1, y=e2 }` desugars as follows

  e { x=e1, y=e2 }
    ===>
  let { x' = e1; y' = e2 } in
  case e of
     T1 _ _ z -> T1 x' y' z
     T4 p _ _ -> T4 p y' x'

The desugared expression is put into an HsExpansion, and we typecheck
that.

The full details are given in Note [Record Updates] in GHC.Tc.Gen.Expr.

Fixes #2595 #3632 #10808 #10856 #16501 #18311 #18802 #21158 #21289

Updates haddock submodule

17 files changed, 251 insertions, 7 deletions

diff --git a/testsuite/tests/typecheck/should_compile/HardRecordUpdate.hs b/testsuite/tests/typecheck/should_compile/HardRecordUpdate.hs
new file mode 100644
index 0000000000..fc32f79bb3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/HardRecordUpdate.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs, TypeFamilies #-}
+
+module HardRecordUpdate where
+
+import Data.Kind
+
+type F :: Type -> Type
+type family F a where {}
+
+type G :: Type -> Type -> Type -> Type
+data family G a b c
+data instance G a b Char where
+  MkG :: { bar :: F a } -> G a Bool Char
+
+g :: F Int -> G Float b Char -> G Int b Char
+g i r = r { bar = i }
diff --git a/testsuite/tests/typecheck/should_compile/T10808.hs b/testsuite/tests/typecheck/should_compile/T10808.hs
new file mode 100644
index 0000000000..4f6822d366
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10808.hs
@@ -0,0 +1,24 @@
+{-# LANGUAGE TypeFamilies #-}
+module T10808 where
+
+type family F a
+type family G a
+
+data T1
+type instance F T1 = Char
+type instance G T1 = Int
+
+data T2
+type instance F T2 = Bool
+type instance G T2 = Int
+
+data R a = R { x :: F a, y :: G a }
+
+r1 :: R T1
+r1 = R { x = 'a', y = 2 }
+
+r2 :: R T2
+r2 = r1 { x = True }  -- error: Cannot match T1 with T2
+
+r3 :: R T2
+r3 = r1 { x = True, y = y r1 } -- OK
diff --git a/testsuite/tests/typecheck/should_compile/T10856.hs b/testsuite/tests/typecheck/should_compile/T10856.hs
new file mode 100644
index 0000000000..6d5ff9d34b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T10856.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE ExistentialQuantification #-}
+module T10856 where
+
+data Rec a b = Show a => Mk { a :: a, b :: b }
+
+update :: Show c => c -> Rec a b -> Rec c b
+update c r = r { a = c }
diff --git a/testsuite/tests/typecheck/should_compile/T16501.hs b/testsuite/tests/typecheck/should_compile/T16501.hs
new file mode 100644
index 0000000000..7da53fabfe
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16501.hs
@@ -0,0 +1,22 @@
+{-# Language GADTs #-} -- Only uses Existentials
+module T16501 where
+
+data T where
+  Str :: Show s => { field :: s } -> T
+
+val1 :: T
+val1 = Str { field = True }
+
+{-
+val2 :: T
+val2 = val1 { field = 'a' }
+  • Record update for insufficiently polymorphic field: field :: s
+    • In the expression: val1 {field = 'a'}
+      In an equation for ‘val2’: val2 = val1 {field = 'a'}
+-}
+
+manualUpdate :: Show s => T -> s -> T
+manualUpdate (Str _) s = Str s
+
+val3 :: T
+val3 = manualUpdate val1 'a'
diff --git a/testsuite/tests/typecheck/should_compile/T18311.hs b/testsuite/tests/typecheck/should_compile/T18311.hs
new file mode 100644
index 0000000000..034e48bf81
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18311.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE TypeFamilies, RecordWildCards #-}
+
+module T18311 where
+
+type family F a
+
+type instance F Int = Int
+type instance F Bool = Int
+
+data T a = MkT {x :: F a, y :: a}
+
+
+foo1 :: T Int -> T Bool
+foo1 (MkT { x = x }) = MkT { x = x , y = True }
+
+foo2 :: T Int -> T Bool
+foo2 t = t {y = False }
+
diff --git a/testsuite/tests/typecheck/should_compile/T18802.hs b/testsuite/tests/typecheck/should_compile/T18802.hs
new file mode 100644
index 0000000000..df306c6c25
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18802.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE MonoLocalBinds, ScopedTypeVariables, RankNTypes #-}
+
+module T18802 where
+
+-- Check that we handle higher-rank types properly.
+data R b = MkR { f :: (forall a. a -> a) -> (Int,b), c :: Int }
+
+foo r = r { f = \ k -> (k 3, k 'x') }
+
+
+-- Check that we handle existentials properly.
+class C a where
+
+data D
+  = forall ty. C ty
+  => MkD { fld1 :: !ty
+         , fld2 :: Bool
+         }
+
+g :: D -> D
+g d = d { fld2 = False }
diff --git a/testsuite/tests/typecheck/should_compile/T18802b.hs b/testsuite/tests/typecheck/should_compile/T18802b.hs
new file mode 100644
index 0000000000..fe1c87d608
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T18802b.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs, DataKinds #-}
+
+module T18802b where
+
+data G a where
+  MkG :: { fld :: Char } -> G Float
+
+recUpd :: ( Char -> Char ) -> G a -> G a
+recUpd f g@(MkG { fld = c }) = g { fld = f c }
diff --git a/testsuite/tests/typecheck/should_compile/T21289.hs b/testsuite/tests/typecheck/should_compile/T21289.hs
new file mode 100644
index 0000000000..e7536eaaaa
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21289.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies #-}
+module T21289 where
+
+type family F (a :: Bool)
+type instance F True = Int
+type instance F False = Int
+
+type family G (a :: Bool)
+type instance G True = Int
+type instance G False = Bool
+
+data Rec a = MkR { konst :: F a
+                 , change :: G a }
+
+ch :: Rec True -> Rec False
+ch r = r { change = False }
diff --git a/testsuite/tests/typecheck/should_compile/T2595.hs b/testsuite/tests/typecheck/should_compile/T2595.hs
new file mode 100644
index 0000000000..0bf62b23b3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T2595.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE Rank2Types #-}
+module Foo where
+
+data Foo = forall a . Foo { foo :: a -> a, bar :: Int }
+
+x :: Foo
+x = Foo { foo = id, bar = 3 }
+
+f :: Foo -> Foo
+f rec = rec { foo = id }
+
+g :: Foo -> Foo
+g rec = rec { bar = 3 }
diff --git a/testsuite/tests/typecheck/should_compile/T3632.hs b/testsuite/tests/typecheck/should_compile/T3632.hs
new file mode 100644
index 0000000000..36e7fe6eac
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T3632.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE GADTs #-}
+module T3632 where
+
+import Data.Char ( ord )
+
+data T where
+  MkT :: { f :: a -> Int, x :: a, wombat :: String } -> T
+
+foo :: T -> T
+foo t = t { f = ord, x = '3' }
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index fb9eba2c8d..00d36bd3a4 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -830,3 +830,13 @@ test('T21315', normal, compile, ['-Wredundant-constraints'])
 test('T21516', normal, compile, [''])
 test('T21519', normal, compile, [''])
 test('T21519a', normal, compile, [''])
+test('T2595', normal, compile, [''])
+test('T3632', normal, compile, [''])
+test('T10808', normal, compile, [''])
+test('T10856', normal, compile, [''])
+test('T16501', normal, compile, [''])
+test('T18311', normal, compile, [''])
+test('T18802', normal, compile, [''])
+test('T18802b', normal, compile, [''])
+test('T21289', normal, compile, [''])
+test('HardRecordUpdate', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T21158.hs b/testsuite/tests/typecheck/should_fail/T21158.hs
new file mode 100644
index 0000000000..282989f5b8
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T21158.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+module T21158 where
+
+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
diff --git a/testsuite/tests/typecheck/should_fail/T21158.stderr b/testsuite/tests/typecheck/should_fail/T21158.stderr
new file mode 100644
index 0000000000..88394ad2e9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T21158.stderr
@@ -0,0 +1,29 @@
+
+T21158.hs:12:14: 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 a record update at field ‘x’,
+      with type constructor ‘T’
+      and data constructor ‘MkT’.
+      In the expression: emptyT {x = newx}
+      In an equation for ‘foo1’: foo1 newx = emptyT {x = newx}
+    • Relevant bindings include
+        foo1 :: [Int] -> T b (bound at T21158.hs:12:1)
+
+T21158.hs:15:49: error:
+    • Couldn't match type: F b1
+                     with: F b
+      Expected: [F b]
+        Actual: [F b1]
+      NB: ‘F’ is a non-injective type family
+      The type variable ‘b1’ 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 b1] (bound at T21158.hs:15:35)
+        foo2 :: [Int] -> T b (bound at T21158.hs:15:1)
diff --git a/testsuite/tests/typecheck/should_fail/T3323.stderr b/testsuite/tests/typecheck/should_fail/T3323.stderr
index 2f8344bb4e..1e77e05318 100644
--- a/testsuite/tests/typecheck/should_fail/T3323.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3323.stderr
@@ -1,5 +1,34 @@
 
-T3323.hs:18:7:
-    Record update for insufficiently polymorphic field: haDevice :: dev
-    In the expression: h {haDevice = undefined}
-    In an equation for ‘f’: f h = h {haDevice = undefined}
+T3323.hs:18:7: error:
+    • Could not deduce (GHC.IO.Device.RawIO dev0)
+      from the context: (GHC.IO.Device.RawIO dev,
+                         GHC.IO.Device.IODevice dev, GHC.IO.BufferedIO.BufferedIO dev,
+                         base-4.16.0.0:Data.Typeable.Internal.Typeable dev)
+        bound by a pattern with constructor:
+                   Handle__ :: forall dev enc_state dec_state.
+                               (GHC.IO.Device.RawIO dev, GHC.IO.Device.IODevice dev,
+                                GHC.IO.BufferedIO.BufferedIO dev,
+                                base-4.16.0.0:Data.Typeable.Internal.Typeable dev) =>
+                               dev
+                               -> HandleType
+                               -> GHC.IORef.IORef (GHC.IO.Buffer.Buffer GHC.Word.Word8)
+                               -> BufferMode
+                               -> GHC.IORef.IORef (dec_state, GHC.IO.Buffer.Buffer GHC.Word.Word8)
+                               -> GHC.IORef.IORef (GHC.IO.Buffer.Buffer GHC.IO.Buffer.CharBufElem)
+                               -> GHC.IORef.IORef (BufferList GHC.IO.Buffer.CharBufElem)
+                               -> Maybe (GHC.IO.Encoding.Types.TextEncoder enc_state)
+                               -> Maybe (GHC.IO.Encoding.Types.TextDecoder dec_state)
+                               -> Maybe GHC.IO.Encoding.Types.TextEncoding
+                               -> Newline
+                               -> Newline
+                               -> Maybe (GHC.MVar.MVar Handle__)
+                               -> Handle__,
+                 in a case alternative
+        at T3323.hs:18:7-28
+      The type variable ‘dev0’ is ambiguous
+    • In a record update at field ‘haDevice’,
+      with type constructor ‘Handle__’,
+      data constructor ‘Handle__’
+      and existential variables ‘dev’, ‘enc_state’, ‘dec_state’.
+      In the expression: h {haDevice = undefined}
+      In an equation for ‘f’: f h = h {haDevice = undefined}
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index aceaf051c9..83ba2c4414 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -655,3 +655,4 @@ test('T20768_fail', normal, compile_fail, [''])
 test('T21327', normal, compile_fail, [''])
 test('T21328', normal, compile_fail, [''])
 test('T21338', normal, compile_fail, [''])
+test('T21158', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail102.stderr b/testsuite/tests/typecheck/should_fail/tcfail102.stderr
index fdfedf7ebb..88b01eea0c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail102.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail102.stderr
@@ -4,10 +4,12 @@ tcfail102.hs:1:14: warning: [-Wdeprecated-flags (in -Wdefault)]
 
 tcfail102.hs:9:7: error:
     • Could not deduce (Integral (Ratio a))
-        arising from a record update
       from the context: Integral a
         bound by the type signature for:
                    f :: forall a. Integral a => P (Ratio a) -> P (Ratio a)
         at tcfail102.hs:8:1-45
-    • In the expression: x {p = p x}
+    • In a record update at field ‘p’,
+      with type constructor ‘P’
+      and data constructor ‘P’.
+      In the expression: x {p = p x}
       In an equation for ‘f’: f x = x {p = p x}
diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
index 887c65f574..fdb16ea140 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
@@ -13,5 +13,7 @@ tcfail181.hs:17:9: error:
         ...plus one instance involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the expression: foo
+      In a record update at field ‘bar’,
+      with type constructor ‘Something’
+      and data constructor ‘Something’.
       In the expression: foo {bar = return True}
-      In an equation for ‘wog’: wog x = foo {bar = return True}