Can I get this ambiguoulsly typed function to compile?

Question

First of all: I know I wouldn't be able to use this function, unless I had TypeApplications enabled. But I thought AllowAmbiguousTypes was meant to work around that.

I currently have the following code:

{-# LANGUAGE ExplicitForAll, AllowAmbiguousTypes #-}

module A where

class B c where
    d :: forall e. e -> c e

class F g where
    h :: forall i. g i -> i

data J k = J {l :: k}

instance B J where
    d = J

instance F J where
    h = l

m :: forall n o. (B n, F n) => o -> o
m = h . d

Interpreting this with GHCi 8.10.1 or compiling it with GHC 8.10.1 leads to this error:

j.hs:20:5: error:
    • Could not deduce (F g0) arising from a use of ‘h’
      from the context: (B n, F n)
        bound by the type signature for:
                   m :: forall (n :: * -> *) o. (B n, F n) => o -> o
        at j.hs:19:1-37
      The type variable ‘g0’ is ambiguous
      These potential instance exist:
        instance F J -- Defined at j.hs:16:10
    • In the first argument of ‘(.)’, namely ‘h’
      In the expression: h . d
      In an equation for ‘m’: m = h . d
   |
20 | m = h . d
   |     ^

j.hs:20:9: error:
    • Could not deduce (B g0) arising from a use of ‘d’
      from the context: (B n, F n)
        bound by the type signature for:
                   m :: forall (n :: * -> *) o. (B n, F n) => o -> o
        at j.hs:19:1-37
      The type variable ‘g0’ is ambiguous
      These potential instance exist:
        instance B J -- Defined at j.hs:13:10
    • In the second argument of ‘(.)’, namely ‘d’
      In the expression: h . d
      In an equation for ‘m’: m = h . d
   |
20 | m = h . d
   |         ^

I understand that, perhaps, the compiler can't draw the connection between the B and F instances and the uses of d and h. I think something like this would solve that:

m @p = h @p . d @p

But, even using TypeApplications, this is refused.

Is there some language option I can choose that either makes something like that workaround possible or outright enables the compiler to infer the connection?

Answer 1

You've got the right idea, but there's no existing method to bind a type argument on the left-hand side of an equation. (There is work in progress to add this as an extension, but it has run into some edge cases that need to be worked out.) But since it's a top-level definition with an attached type signature, you can just make use of the type there:

{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}

m :: forall n o. (B n, F n) => o -> o
m = h @n . d @n

using the ScopedTypeVariables extension to refer to the type n specified in the type signature.