Allow HasField in quantified constraints

We perform validity checking on user-written HasField instances,
for example to disallow:

  data Foo a = Foo { fld :: Int }
  instance HasField "fld" (Foo a) Bool

However, these checks were also being made on quantified constraints,
e.g.

  data Bar where
    Bar :: (forall a. HasField s (Foo a) Int) => Proxy s -> Bar

This patch simply skips validity checking for quantified constraints,
in line with what we already do for equality constraints such as
Coercible.

Fixes #20989

3 files changed, 43 insertions, 1 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 9d6a05c7aa..cad2ea1796 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1417,6 +1417,10 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args
         ; when (safeInferOn dflags) (recordUnsafeInfer emptyMessages) }
 
   | clas_nm == hasFieldClassName
+  , not quantified_constraint
+  -- Don't do any validity checking for HasField contexts
+  -- inside quantified constraints (#20989): the validity checks
+  -- only apply to user-written instances.
   = checkHasFieldInst clas cls_args
 
   | isCTupleClass clas
diff --git a/testsuite/tests/overloadedrecflds/should_compile/T20989.hs b/testsuite/tests/overloadedrecflds/should_compile/T20989.hs
new file mode 100644
index 0000000000..bf22f170c9
--- /dev/null
+++ b/testsuite/tests/overloadedrecflds/should_compile/T20989.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Haskell2010 #-}
+
+module T20989 where
+
+import Data.Proxy
+  ( Proxy )
+import GHC.Records
+  ( HasField )
+
+data Bar0 where
+  Bar0 :: HasField s r a => Proxy s -> Proxy r -> Proxy a -> Bar0
+
+-- See Note [Validity checking of HasField instances] in GHC.Tc.Validity
+
+-- 1. `HasField _ r _` where r is a variable
+data Bar1 where
+  Bar1 :: (forall r. HasField s r Int) => Proxy s -> Bar1
+
+-- 2. `HasField _ (T ...) _` if T is a data family
+data family Foo2 a
+data Bar2 where
+  Bar2 :: (forall a. HasField s (Foo2 a) Int) => Proxy s -> Bar2
+
+-- 3. `HasField x (T ...) _` where x is a variable,
+--    if T has any fields at all
+data Foo3 a = Foo3 { fld1 :: Int, fld2 :: Bool }
+data Bar3 where
+  Bar3 :: (forall a. HasField s (Foo3 a) Int) => Proxy s -> Bar3
+
+-- 4. `HasField "foo" (T ...) _` if T has a "foo" field.
+data Foo4 a = Foo4 { foo4 :: Int }
+data Bar4 where
+  Bar4 :: (forall a. HasField "foo4" (Foo4 a) Int) => Bar4
diff --git a/testsuite/tests/overloadedrecflds/should_compile/all.T b/testsuite/tests/overloadedrecflds/should_compile/all.T
index 863fbacca8..dd5660b445 100644
--- a/testsuite/tests/overloadedrecflds/should_compile/all.T
+++ b/testsuite/tests/overloadedrecflds/should_compile/all.T
@@ -10,4 +10,4 @@ test('T18999_NoFieldSelectors', normal, compile, [''])
 test('T18999_FieldSelectors', normal, compile, [''])
 test('T19154', normal, compile, [''])
 test('T20723', normal, compile, [''])
-
+test('T20989', normal, compile, [''])