Type abstraction in GHC Haskell

Question

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?

Phallicism

I get an ambiguity error in f's declaration. Do you have AllowAmbiguousTypes turned on? – Chunk

Yes, I do. Give me a moment to edit the question with all necessary extensions. – Phallicism

Answer 1

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!

Phallicism

I can't understand why this is not considered to be a bug. If ambiguous types were not allowed, I would not. But since ambiguous types now can be turned on, I can't see anything wrong with the code. I'd consider this a very weird technical limitation of GHC, at best. I wonder if there is some deep reason in the inference algorithm for this to fail type checking, or if it is only an incident. Oh, well. – Og

I guess you just can't make it work in the general case, and not trying to for some concrete and obvious cases keeps inference simple and reasonable. If this would work, we'd have the same discussion for some other example that would be even trickier to infer. The question is, where do we stop with such ad-hoc hacks in type inference? – Phallicism

That might be the case, but the trac discussion does not support that view. It only says "it is ambiguous, therefore GHC can't handle it", when this reason alone is not at all sufficient, since GHC accepts f just fine, even if it has an ambiguous type. Indeed, the trac discussion seems to point out, wrongly, that you can not write f. Whatever type checking algorithm accepts x :: T ; x = expr (for some T,expr) but rejects x :: T ; x = expr ; y :: T ; y = x is very, very weird in my eye. – Og

Answer 2

This might be a GHC bug. I can not see how this GHC behavior makes any sense.

This issue has nothing to do with type families, but it seems to arise from ambiguous types and typeclass constraints.

Here is a MCVE for the same issue.

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

class C a where
   getInt :: Int

instance C Char where
   getInt = 42

f :: (forall a. C a => Int) -> Bool
f x = even (x @ Char)

g :: (forall a. C a => Int) -> Bool
-- g = f               -- fails
-- g h = f h           -- fails
-- g h = f getInt      -- fails
g _ = f 42             -- OK

It seems that f can not be called with any argument that actually exploits the constraint.

Og