为什么这里不需要UndecidableInstances，例如C1

Question

在其他上下文中尝试此操作需要扩展（这似乎是正确的），但在这里不是：

{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE QuantifiedConstraints #-}
import Data.Kind (Type)

class (forall a. c a => c (f a)) => C1 c f
-- Why can I do this without UndecidableInstances?:
instance (forall a. c a => c (f a)) => C1 c f
-- As opposed to requiring
--instance C1 Eq Maybe

---------- below just demonstrates using above

data AnnBoolExpFld backend leaf =
    AVAggregationPredicates Int (AggregationPredicates backend leaf)

class (C1 Eq (AggregationPredicates b)) => Backend b where
  type AggregationPredicates b :: Type -> Type

instance Backend Int where
  type AggregationPredicates Int = Maybe

deriving instance (Eq a, Backend b) =>  Eq (AnnBoolExpFld b a)

main = print $
  AVAggregationPredicates 1 (Just 1) == (AVAggregationPredicates 1 (Just 1) :: AnnBoolExpFld Int Int )

Answer 1

可能是这个问题。 对于具有不可见参数的类型类（包括多类类型类），终止检查是有缺陷的。 使用推断类型：

type C1 :: (k -> Constraint) -> (k -> k) -> Constraint

实例被接受。 如果您添加显式类型签名，例如

type C1 :: (Type -> Constraint) -> (Type -> Type) -> Constraint

，则实例将被拒绝并出现预期错误：

Foo.hs:10:10: error:
    • The constraint ‘c (f a)’
        is no smaller than the instance head ‘C1 c f’
      (Use UndecidableInstances to permit this)
    • In the instance declaration for ‘C1 c f’
   |
10 | instance (forall a. c a => c (f a)) => C1 c f
   |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^