I'd love to get the following example to type-check:
{-# 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
I get it that it's probably not possible to infer and check gs type (even though in this specific case it's obvious because it's just a partial application): Secret is not injective and there's no way to tell the compiler which Functor instance it should expect. Consequently, it fails with the following error message:
• 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
| ^^^
So some guidance by the programmer is needed and it would readily be accepted if I could write g like this:
g :: (forall f. Functor f => Secret f) -> Int
g h = f 4 (\\f -> h @f)
Where \\ is hypothetical syntax for System Fw's big lambda, i.e. type abstraction. I can emulate this with ugly Proxys, but is there some other GHC Haskell feature that let's me write something like this?
This is by design. It seems there is no way around using Proxys for now: https://ghc.haskell.org/trac/ghc/ticket/15119.
Edit Jul 2019: There's now a GHC proposal for this!