Instance decidability + Quantified Constraints

Motivation

Consider the following program:

{-# LANGUAGE RankNTypes, KindSignatures, QuantifiedConstraints #-}

module Main where

class C a 

data D (f :: * -> *) 

instance (forall b . C (f b)) => C (D f)

main = return ()

Compilation fails with

[1 of 1] Compiling Main             ( test.hs, test.o )

test.hs:9:10: error:
    • The constraint ‘C (f b)’
        is no smaller than the instance head ‘C (D f)’
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘C (D f)’
  |
9 | instance (forall b . C (f b)) => C (D f)

Proposal

Could we slightly modify the constraint-size rule to not count type variables that are bound within the constraint towards the size of the constraint? I.e. only free type variables "escaping" the constraint would count towards its size.

As a disclaimer, I am not entirely sure this is would be correct, but intuitively it seems fine. I would appreciate input from anyone with a rigorous understanding of these mechanisms.