1

我想为具有指向可以解除超类约束的字典的静态指针的类型编写一个类型类。在这个人为的例子中,超级约束是Typeable,因为现代 GHC 版本会自动为所有类型提供实例。

实际上,超级约束是非平凡的,并且Static a允许这些约束的字典被序列化的实例,因为forall a. StaticPtr a可以被序列化。

首先,以下代码编译没有问题,

{-# LANGUAGE StaticPointers #-}
{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE UndecideableInstances, MultiParamTypeClasses #-}

import GHC.StaticPtr
import Data.Constraint
import Data.Constraint.Lifting
import Data.Typeable (Typeable)

class Typeable a => Static a where
    sdict :: Dict (Static a)

-- The 'Typeable f' constraint should be trivial, but typechecking 
-- fails without it. Is it possible to get rid of it, if not then why?
instance (Typeable f, Lifting Static f, Static a) => Static (f a) where
    sdict = Dict \\ lifting @Static @f @a

但是当我使用静态指针以所需的方式编写类时,

class Typeable a => Static a where
    sdict :: StaticPtr (Dict (Static a))

instance (Typeable f, Lifting Static f, Static a) => Static (f a) where
    sdict = static (Dict \\ lifting @Static @f @a)

GHC 抱怨静态表单主体中的类型应用程序:

Only identifiers of top-level bindings can appear in the body of the static form:
  static (Dict \\ lifting @Static @f @a)
but the following identifiers were found instead: f a

然后我尝试让 GHC 完全自行解析实例,而不使用Lifting引导类型检查器

instance (Typeable f, Static a) => Static (f a) where sdict = static Dict

但这也失败了,

• No instance for (Static a) arising from a use of ‘Dict’                                    
• In the body of a static form: Dict                                                                 
  In the expression: static Dict
  In an equation for ‘sdict’: sdict = static Dict                                                    

一个更单态的实例也会失败,并出现非常相似的错误No instance for (Static a)

instance Static a => Static [a] where sdict = static Dict

这让我更多地了解了 GHC 的类型类实例解析是如何工作的:类的超级约束直到实例被实际解析后才会应用。但是 GHC 能够满足Dict :: Static a => Dict (Static a)第一个示例,这显然需要一个Static a实例在范围内。

如果可能的话,有什么建议如何写这个吗?希望对约束包有更多经验的人可以提供正确的扭曲来满足类型检查器。

4

0 回答 0