Me encantaría obtener el siguiente ejemplo de verificación de tipo:

{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE RankNTypes             #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}

module Foo where

f :: Int -> (forall f. Functor f => Secret f) -> Int
f x _ = x

g :: (forall f. Functor f => Secret f) -> Int
g = f 4

type family Secret (f :: * -> *) :: * where
  Secret f = Int

Entiendo que probablemente no sea posible inferir y marcargs type (aunque en este caso específico es obvio porque es solo una aplicación parcial):Secret no es inyectivo y no hay forma de decirle al compilador quéFunctor instancia debería esperar. En consecuencia, falla con el siguiente mensaje de error:

    • Could not deduce (Functor f0)
      from the context: Functor f
        bound by a type expected by the context:
                  forall (f :: * -> *). Functor f => Secret f
        at src/Datafix/Description.hs:233:5-7
      The type variable ‘f0’ is ambiguous
      These potential instances exist:
        instance Functor IO -- Defined in ‘GHC.Base’
        instance Functor Maybe -- Defined in ‘GHC.Base’
        instance Functor ((,) a) -- Defined in ‘GHC.Base’
        ...plus one other
        ...plus 9 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: f 4
      In an equation for ‘g’: g = f 4
    |
233 | g = f 4
    |     ^^^

Así que se necesita alguna orientación del programador y sería fácilmente aceptado si pudiera escribirg Me gusta esto

g :: (forall f. Functor f => Secret f) -> Int
g h = f 4 (\\f -> h @f)

Dónde\\ es una sintaxis hipotética para la gran lambda de System Fw, p. abstracción tipo. Puedo emular esto con feoProxys, pero ¿hay alguna otra característica de GHC Haskell que me permita escribir algo como esto?