Why can't GHC typecheck this function involving polymorphism and existential types?

Question

I have some Haskell code that won't compile (with GHC 8.0.2). I think I understand the basic problem, but I would like to understand it better so I can avoid this in the future.

My library looks similar to this:

{-# language TypeFamilyDependencies #-}
{-# language GADTs #-}
{-# language RankNTypes #-}

module Lib where

type Key = Int

class Handle m where
    type Connection m = c | c -> m
    withConnection :: Connection m -> m a -> IO a

class (Handle m) => Data m where
    getKeyVal :: Key -> m String

data SomeConn where
    SomeConn :: (Data m) => Connection m -> SomeConn

useConnection :: SomeConn -> (forall m. Data m => m String) -> IO String
useConnection (SomeConn c) action = withConnection c action

The idea is that Data m represents a class of monads similar to ReaderT (Connection m) IO. I am hoping to write generic functions with the methods of this typeclass, and have the exact method instance be determined by the connection type wrapped with SomeConn (which is chosen at run-time).

Now the following code

getKeyValWith :: SomeConn -> Key -> IO String
getKeyValWith c = (useConnection c). getKeyVal

gives me the following error from GHC 8.0.2:

• Couldn't match type ‘m0 String’
                 with ‘forall (m :: * -> *). Data m => m String’
  Expected type: m0 String -> IO String
    Actual type: (forall (m :: * -> *). Data m => m String)
                 -> IO String
• In the first argument of ‘(.)’, namely ‘useConnection c’
  In the expression: useConnection c . getKeyVal
  In an equation for ‘getKeyValWith’:
      getKeyValWith c = useConnection c . getKeyVal

Strangely enough, the following works just fine:

getKeyValWith c k = useConnection c (getKeyVal k)

Less surprisingly, so does this:

getKeyValWith (SomeConn c) = withConnection c . getKeyVal

Is there a simple rule to understand why GHC doesn't like the first example, but the other examples are okay? Is there a way I can ask GHC for more information about what it's doing when it tries to compile the first definition? I understand this is probably not idiomatic Haskell (what some call the "Existential/typeclass anti-pattern").

Edit:

I should add that I run into the same problem even if I explicitly add the type getKeyVal :: Key -> (Data m => m String) in the first example. I can even give this function its own name with my chosen type signature (which typechecks), but I get the same error. But I see now that even when I explicitly add the type, running :t in GHCI (with -XRankNTypes) on it gives me back the original type with Data m => floated to the left. So I think I understand why GHC is balking at me. Can I force GHC to use my chosen type?

I have read this and this but the content seems obscured by the discussion of ($). I am trying to understand what the problem is in general, and how I can either help GHC understand my code, or ask GHC to help me understand the problem. — dunnl
The type of (. getKeyVal) is Data m => (m String -> c) -> Key -> c; the type of useConnection c is (forall m. Data m => m String) -> IO String. Do you see why the types m String -> IO String and (forall m . Data m => m String) -> IO String cannot unify? Neither of the latter two definitions require performing this unification. — user2407038
This might be a near-duplicate of stackoverflow.com/questions/45964162/… — chi
@user2407038, I do see that, and I edited my question to ask a new one: Can I force GHC to accept a different type signature on getKeyVal? — dunnl

leftaroundabout leftaroundabout · Accepted Answer · 2017-08-31T13:19:51

This is all about .. It's unable to pass a polymorphic argument between the functions, hence f . g doesn't work if f is rank-2 polymorphic. Notice the following works:

(~.) :: ((∀ m. Data m => m String) -> z) -> (x -> (∀ m. Data m => m String))
          -> x -> z
(~.) f g x = f (g x)

getKeyValWith :: SomeConn -> Key -> IO String
getKeyValWith c = useConnection c ~. getKeyVal

Ideally, . would have a type like

(.) :: ∀ c . ((∀ y . c y => y) -> z) -> x -> ((∀ y . c y => y) -> x)
               -> x -> z

and thus cover all special cases like ~. above. But this is not possible – it would require inferring the weakest possible constraint c to pick in any given situation – in the traditional case, c y = y~y₀ – and I'm pretty sure that is uncomputable in general.

(An interesting question is how far we could get if the compiler just inlined . as much as possible before type-checking, as it right now already does with $. If it did automatic eta-expansion, it could certainly get useConnection c . getKeyVal to work, but automatic eta-expansion is in general not a good idea...)

Hiding the Rank-2 polymorphism by wrapping the polymorphic argument in a GADT, as you did with SomeConn, is the usual workaround.

Why can't GHC typecheck this function involving polymorphism and existential types?

1 Answers