2

我正在尝试使用 DataKinds 进行类型级编程，但是当我将其中一个结构嵌套在另一个结构中时遇到了困难。

{-# LANGUAGE DataKinds, TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-}

module Temp where

data Prop1 = D | E 

data Lower :: Prop1 -> * where
  SubThing1 :: Lower D
  SubThing2 :: Lower E

class ClassLower a where
  somefunc2 :: a -> String

instance ClassLower (Lower D) where
  somefunc2 a = "string3"

instance ClassLower (Lower E) where
  somefunc2 a = "string4"

data Prop2 = A | B | C

data Upper :: Prop2 -> * where
  Thing1 :: Upper A
  Thing2 :: Upper B
  Thing3 :: Lower a -> Upper C

class ClassUpper a where
  somefunc :: a -> String

instance ClassUpper (Upper A) where
  somefunc a = "string1"

instance ClassUpper (Upper B) where
  somefunc a = "string2"

instance ClassUpper (Upper C) where
  somefunc (Thing3 x) = somefunc2 x

一旦我添加了 ClassUpper 的最后一个实例，我就会得到一个错误。

Temp.hs:37:25: error:
    • Could not deduce (ClassLower (Lower a))
        arising from a use of ‘somefunc2’
      from the context: 'C ~ 'C
        bound by a pattern with constructor:
                   Thing3 :: forall (a :: Prop1). Lower a -> Upper 'C,
                 in an equation for ‘somefunc’
        at /Users/jdouglas/jeff/emulator/src/Temp.hs:37:13-20
    • In the expression: somefunc2 x
      In an equation for ‘somefunc’: somefunc (Thing3 x) = somefunc2 x
      In the instance declaration for ‘ClassUpper (Upper 'C)’

我知道这'C ~ 'C表明类型相等，但我不明白根本问题是什么，更不用说解决方案或解决方法了。

我不明白什么，解决这个问题的最佳方法是什么？

4

2 回答 2

6

这里的问题有点微妙。人们可能期望 GHC 接受这一点的原因是你有所有可能的实例，Lower a因为你只提供了制作Lower D和Lower E. Lower但是，可以为类似构建一个病态定义

import GHC.Exts (Any)

data Lower :: Prop1 -> * where
  SubThing1 :: Lower D
  SubThing2 :: Lower E
  SubThing3 :: Lower Any

重点是，不仅D和E有善Prop1。我们不仅Any可以玩这样的恶作剧 - 甚至允许以下构造函数（也是F Int :: Prop1如此）！

  SubThing4 :: Lower (F Int)

type family F x :: Prop1 where {}

因此，总而言之，根本问题是 GHC 确实无法确定ClassLower (Lower a)约束（由于使用 而需要somefunc2）是否会得到满足。为此，它必须做大量工作来检查 GADT 构造函数，并确保每个可能的情况都被某个实例覆盖。

ClassLower (Lower a)在这种情况下，您可以通过将约束添加到 GADT 构造函数（启用FlexibleContexts）来解决您的问题。

data Upper :: Prop2 -> * where
  Thing1 :: Upper A
  Thing2 :: Upper B
  Thing3 :: ClassLower (Lower a) => Lower a -> Upper C
于 2016-12-25T07:40:31.627 回答
3

或者您可以像这样写出您的ClassLower实例，使用模式匹配（而不是类型变量）来区分 GADT 的情况：

instance ClassLower (Lower a) where
    somefunc2 SubThing1 = "string3"
    somefunc2 SubThing2 = "string4"
于 2016-12-26T08:29:44.513 回答