如何使用GADT限制约束？

Question

我有以下代码,我希望这样的类型检查失败:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

import Control.Lens

data GADT e a where
  One :: Greet e => String -> GADT e String
  Two :: Increment e => Int -> GADT e Int

class Greet a where
  _Greet :: Prism' a String

class Increment a where
  _Increment :: Prism' a Int

instance Greet (Either String Int) where
  _Greet = _Left

instance Increment (Either String Int) where
  _Increment = _Right

run :: GADT e a -> Either String Int
run = go
  where
  go (One x) = review _Greet x
  go (Two x) = review _Greet "Hello"

这个想法是GADT中的每个条目都有一个相关的错误,我正在用一个Prism更大的结构建模.当我"解释"这个GADT时,我提供了一个具体的类型,e它具有所有这些Prism的实例.但是,对于每个个案,我不希望能够使用未在构造函数的关联上下文中声明的实例.

上面的代码应该是一个错误,因为当我模式匹配时,Two我应该知道我只能使用Increment e,但我正在使用Greet.我可以看出为什么这样做 - Either String Int有一个实例Greet,所以一切都检查出来.

我不确定解决这个问题的最佳方法是什么.也许我可以使用蕴涵Data.Constraint,或者可能有更高等级类型的技巧.

有任何想法吗？

Answer 1

问题是您正在修复最终结果类型,因此实例存在且类型检查器可以找到它.

尝试类似的东西:

run :: GADT e a -> e

现在结果类型无法选择实例review,参数化强制执行不变量.