Regression of deriving for quantified constraints
## Summary
GHC HEAD does not type check a program, accepted by GHC 9.12.2.
## Steps to reproduce
```haskell
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Data.Kind
import Data.Type.Equality
import GHC.TypeNats
newtype Vector (el :: Type) (len :: Natural) = Vector [el]
deriving (Eq)
data Sized (f :: Natural -> Type) where
Sized :: KnownNat len => f len -> Sized f
instance (forall (len :: Natural). Eq (f len)) => Eq (Sized f) where
Sized xs == Sized ys = case sameNat xs ys of
Nothing -> False
Just Refl -> xs == ys
newtype Foo (el :: Type) = Foo (Sized (Vector el))
deriving (Eq)
```
```shellsession
$ ghc Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
$ ghc-9.14 Foo.hs
[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
Foo.hs:24:13: error: [GHC-05617]
• Could not solve: ‘forall (len :: Natural). Eq (Vector el len)’
arising from the 'deriving' clause of a data type declaration
• When deriving the instance for (Eq (Foo el))
|
24 | deriving (Eq)
| ^^
```
## Expected behavior
GHC should accept the program as GHC 9.12.2 does.
The issue looks similar to #26315, so let me tag @simonpj and @sheaf.
## Environment
* GHC: 9.14-alpha1, HEAD.
* Operating System: macOS, Ubuntu
* System Architecture: aarch64, amd64
issue