标签: quantified-constraints

有了量化的约束，我可以Eq (A f)很好地推导出来吗？但是，当我尝试推导 Ord (A f) 时，它失败了。当约束类具有超类时，我不明白如何使用量化约束。我如何派生Ord (A f)和其他具有超类的类？

> newtype A f = A (f Int)
> deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
> deriving instance (forall a. Ord a => Ord (f a)) => Ord (A f)
<interactive>:3:1: error:
    • Could not deduce (Ord a)
        arising from the superclasses of an instance declaration
      from the context: forall a. Ord a => Ord (f a)
        bound by …

我正在尝试使用这篇博文的方法来处理更高级的数据，而无需Identity为琐碎的情况使用悬空函子以及量化约束推导：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-}
module HKD2 where

import Control.Monad.Identity

type family HKD f a where
    HKD Identity a = a
    HKD f        a = f a

data Result f = MkResult
    { foo :: HKD f Int
    , bar :: HKD f Bool
    }

deriving instance (forall a. Show a => Show (HKD f a)) => Show (Result f)

这导致了令人气愤的自相矛盾的错误信息：

无法Show (HKD f a) 从上下文推断：forall a. Show …

为什么是下面的代码：

class TheClass (t :: * -> * -> *)
  where
  type TheFamily t :: * -> Constraint

data Dict (c :: Constraint)
  where
  Dict :: c => Dict c

foo :: forall t a b.
  ( TheClass t
  , (forall x y. (TheFamily t x, TheFamily t y) => TheFamily t (t x y))
  , TheFamily t a
  , TheFamily t b
  ) => Dict (TheFamily t (t a b))
foo = Dict

-- NB: Only using `Dict` to …

考虑以下代码，它进行类型检查：

module Scratch where

import GHC.Exts

ensure :: forall c x. c => x -> x
ensure = id

type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)

foo :: forall t a.
  ( Eq2 t
  , Eq a
  ) => ()
foo = ensure @(Eq (a `t` a)) ()

foo在这里没有做任何有用的事情，但让我们想象一下它正在做一些需要Eq (t a a)实例的重要业务。编译器能够接受(Eq2 t, Eq a)约束并详细说明Eq (t a a)字典，因此解除约束并且一切正常。

现在假设我们想要foo做一些额外的工作，这取决于以下相当复杂的类的实例：

-- …

以前，为了在类型类上使用量化约束，例如Ord，您必须在实例中包含超类，如下所示：

newtype A f = A (f Int)
deriving instance (forall a. Eq a => Eq (f a)) => Eq (A f)
deriving instance (forall a. Eq a => Eq (f a), forall a. Ord a => Ord (f a)) => Ord (A f)

（这实际上正是这个问题中给出的解决方案）。

但是，在 GHC 9 中，上述代码不起作用。它失败并出现以下错误：

   • Could not deduce (Eq (f a))
      from the context: (forall a. Eq a => Eq (f a),
                         forall a. Ord a => Ord (f a))
        bound …

编辑：我提出了一个更具体的问题。谢谢这里的回答者，我认为后续问题可以更好地解释我在这里引入的一些困惑。

TL;DR我正在努力将约束证明放入表达式中，同时在构造函数上使用具有存在约束的 GADT。（这是一个严肃的口，抱歉！）

我将问题归结为以下几点。我有一个简单的 GADT，它表示名为 的点X和名为 的函数应用程序F。点X被限制为Objects。

data GADT ix a where\n  X :: Object ix a => a -> GADT ix a\n  F :: (a -> b) -> GADT ix a -> GADT ix b\n

Constrained指的是其对象受某物约束的容器，并且Object是某物。（编辑：我真正的问题涉及Category约束类别Cartesian中的类）

-- | I can constrain the values within containers of …

我试图表达一个给定的想法

instance (MonadTrans t, MonadX m) => MonadX (t m)\n

由此可见，只要所有的都有实例，任何t1 (t2 ... (tn m))也是。但是，当我尝试写下来时，它不起作用：MonadXtxMonadTrans

{-# LANGUAGE BasicallyEverything #-}\n\ndata Dict c where\n  Dict :: c => Dict c\n\nclass (forall m . Monad m => Monad (t m)) => MonadTrans t where\n  lift :: Monad m => m a -> t m a\n\nclass    (c m, Monad m, forall t . (MonadTrans t, Monad (t m)) => c (t m)) => Foo c m\ninstance …

我正在玩一种多类型的无标签编码 Free

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
module Free where
import GHC.Types

type (a :: k) ~> (b :: k) = Morphism k a b

newtype Natural (f :: j -> k) (g :: j -> k) = 
  Natural { getNatural :: forall (x :: j). f x ~> …