我可以让这个模棱两可的类型的函数进行编译

Question

首先：除非启用了TypeApplications，否则我将无法使用此功能。但是我认为AllowAmbiguousTypes应该可以解决此问题。

我目前有以下代码：

{-# 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

用GHCi 8.10.1解释或用GHC 8.10.1编译会导致此错误：

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
   |         ^

[我了解，也许编译器无法绘制B和F实例之间以及d和h用法之间的联系。我认为这样可以解决问题：

m @p = h @p . d @p

但是，即使使用TypeApplications，也会被拒绝。

我是否可以选择某种语言选项，从而使类似的解决方法成为可能，或者完全允许编译器推断连接？

Answer 1

您有一个正确的想法，但是没有现有的方法可以在方程式的左侧绑定类型参数。 （正在将其添加为扩展，但仍在进行中，但是已经遇到了一些需要解决的极端情况。）但是，由于它是带有附加类型签名的顶级定义，因此您可以使用在此处输入：

{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}

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

使用the ScopedTypeVariables extension来引用类型签名中指定的类型ScopedTypeVariables。

Answer 2

为了补充实际的答案，您的尝试（n）未编译，因为它使用的是实际上完全不相关的符号。

m @p = h @p . d @p未使用类型参数m @p = ...定义多态函数m；此类语法没有语法（使用p的解决方案是最接近的近似值）。 ScopedTypeVariables是一种模式，将两个变量m@p和m绑定到相同的值。当p的正确成分为非平凡模式时，更常用：

@