制定一个可能的约束方程式

Question

我怎样才能约束到Eq a？它需要是善良的 - >>约束

我尝试了什么:

class (a ~ Maybe b, Eq b) => K a where
instance (a ~ Maybe b, Eq b) => K a where

错误:

Not in scope: type variable ‘b’

用法示例:

data Test c = forall a. (c a) => Test a
r :: Test K -> Maybe Bool
r (Test o) = (==) <$> o <*> o -- I need GHC to infer that o is Maybe Eq

有效的案例:

pp :: Test ((~) String) -> String
pp (Test o) = o ++ "X" -- GHC infers that o is a string

hh :: Test Eq -> Bool
hh (Test o) = o == o -- GHC infers that o is Eq

这里的通用答案:是否有一种将约束应用于类型应用程序的一般方法？

Answer 1

以下编译在我的机器上.不知道它是多么明智.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ConstraintKinds #-}
class (Eq (UnMaybe a), a ~ Maybe (UnMaybe a)) => EqMaybe a where
    type UnMaybe a

instance Eq a => EqMaybe (Maybe a) where
    type UnMaybe (Maybe a) = a

data Test c = forall a. c a => Test a
r :: Test EqMaybe -> Maybe Bool
r (Test o) = (==) <$> o <*> o
f :: Test Eq -> Test EqMaybe
f (Test o) = Test (Just o)

Answer 2

这是一个已知问题.GHC正在窒息,因为你已经引入了一个b在实例头中没有提到的新类型变量.一种解决方法是使用类型族和约束种类.

{-# LANGUAGE ConstraintKinds, TypeFamilies, UndecideableInstances, 
             UndecideableSuperclasses, FlexibleInstances
  #-}

import GHC.Exts (Constraint)
import GHC.Prim (Any)

type family MaybeEq x :: Constraint where
  MaybeEq (Maybe a) = Eq a
  MaybeEq _         = Any    -- A good "unsatisfiable" constraint

class MaybeEq a => K a where
instance MaybeEq a => K a where