(#14860) QuantifiedConstraints: Can't quantify constraint involving type family

TF_QC.md

For the Trac ticket #14860.

All these types are valid for h, but its principal type involves -XQuantifiedConstraints

{-# Language FlexibleInstances, MultiParamTypeClasses, GADTs, QuantifiedConstraints #-}

import Data.Kind

type family FB (a::Type) (b::Type) :: Type where
  FB Int _ = Bool
  FB [a] b = FB a b

data Bar a where
  K :: a -> xx -> Bar a

h :: Bar     Int     -> Bool
h :: Bar    [Int]    -> Bool
h :: Bar   [[Int]]   -> Bool
h :: Bar  [[[Int]]]  -> Bool
h :: Bar [[[[Int]]]] -> Bool
h (K a xx) = not (fb a xx)

fb :: a -> b -> FB a b
fb = undefined 

We really want: h :: forall a. (forall b. FB a b ~ Bool) => Bar a -> Bool.

This is possible with the following steps:

1. Class alias for FB a b ~ Bool

   class    FB a b ~ Bool => FB_Bool a b
   instance FB a b ~ Bool => FB_Bool a b

2. Quantify over alias

   h :: forall a. (forall xx. FB_Bool a xx) => Bar a -> Bool

3. Helper function that converts (a -> xx -> FB a xx) into (a -> xx -> Bool) given a witness of FB_Bool a xx

   h :: forall a. (forall xx. FB_Bool a xx) => Bar a -> Bool
   h (K a xx) = go Dict fb a xx where
   
     go :: Dict (FB_Bool a xx) -> (a -> xx -> FB a xx) -> (a -> xx -> Bool)
     go Dict k = k

where we can instantiate h

h :: Bar     Int     -> Bool
h :: Bar    [Int]    -> Bool
h :: Bar   [[Int]]   -> Bool
h :: Bar  [[[Int]]]  -> Bool
h :: Bar [[[[Int]]]] -> Bool