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.