Can I get this ambiguoulsly typed function to compile?

user_8025936 0
Viewed 53

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?

ambiguous haskell types
2 Answers

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.

user_3832000

To complement the actual answer, your attempt (m @p = h @p . d @p) did not compile because it uses notation that actually has a totally unrelated meaning.

m @p = ... is not defining a polymorphic function m with a type parameter p; there is no syntax for such a thing (and the solution using ScopedTypeVariables is the closest approximation). m@p is an as-pattern, binding two variables m and p to the same value. @ is more commonly used when its right component is a nontrivial pattern:

t@(x, y) = somepair

-- equivalent to --

t = somepair
(x, y) = t
user_68637490
Related