Wrongfully assumes user-defined Typeable instance when using QuantifiedConstraints

Summary

If Typeable is used on the rhs of a QuantifiedConstraint ghc assumes that the instance is user-defined.

Steps to reproduce

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ConstraintKinds #-}
module Some where

import Data.Typeable
import Data.Kind


data Some c where
    Some :: c a => a -> Some c

extractSome :: (Typeable a, forall x. c x => Typeable x) => Some c -> Maybe a
extractSome (Some a) = cast a

Some.hs:17:16: error:
    • Class ‘Typeable’ does not support user-specified instances
    • In the quantified constraint ‘forall x. c x => Typeable x’
      In the type signature:
        extractSome :: (Typeable a, forall x. c x => Typeable x) =>
                       Some c -> Maybe a
   |
17 | extractSome :: (Typeable a, forall x. c x => Typeable x) => Some c -> Maybe a
   |

Expected behavior

This should compile without issue. forall x. c x => Typeable x does not imply any user-defined instances.

Environment

• GHC versions used:
• • 8.10.4
• • 9.0.1
• Operating System: Linux
• System Architecture: x86 64bit

Note

Via IRC:

boxscape: FWIW unless there really is a reason to not allow this it looks like not quantified_constraint is missing in this guard https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Tc/Validity.hs#L1539-1542