<Man of Letters (Mikolaj)> unfortunately, this failed in the wild at use of higher-order functions with quantified arguments, similarly as in
[...]
ghci> let h :: (forall a_b. [T (a_b :: (Type, Type))] -> Int) -> Int; h f = f []
ghci> h lengthT2
<interactive>:38:3: error: [GHC-25897]
    • Couldn't match type ‘a_b’ with ‘'(Fst a_b, Snd a_b)’
        arising from a use of ‘lengthT2’
      ‘a_b’ is a rigid type variable bound by
        a type expected by the context:
          forall (a_b :: (*, *)). [T a_b] -> Int
        at <interactive>:38:3-10
    • In the first argument of ‘h’, namely ‘lengthT2’
      In the expression: h lengthT2
      In an equation for ‘it’: it = h lengthT2