2

我有以下片段：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

import Data.Proxy

data Foo where
  FooInt :: Foo
  FooProxy :: IsEnum e ~ True => Proxy e -> Foo

type family IsEnum e :: Bool

type family FromFoo (foo :: Foo) where
  FromFoo FooInt = Int
  FromFoo (FooProxy ('Proxy :: Proxy e)) = e

一般的想法是，我正在尝试将其Foo用作我可以做的数据类型

type MyFoo1 = FooInt :: Foo
type instance IsEnum Bool = True
type MyFoo2 = FooProxy ('Proxy :: Proxy Bool) :: Foo

并确保传递给的代理类型是类型族FooProxy的一部分IsEnum（我不能这样做FooProxy :: Enum e => Proxy e -> Foo，因为目前只支持等式约束）。

但是当我尝试编译它时，我得到了错误：

<interactive>:30:12: error:
    • Couldn't match expected kind ‘'True’ with actual kind ‘IsEnum e’
    • In the first argument of ‘FromFoo’, namely
        ‘(FooProxy ( 'Proxy :: Proxy e))’
      In the type family declaration for ‘FromFoo’

问题是当我想从我Foo的类型转换为具体类型时FromFoo，我想FooProxy评估为代理类型。所以我试图模式匹配Proxy以返回代理类型e，但它似乎IsEnum e ~ True再次检查约束。我认为只有在创建值时才会检查约束，但在模式匹配FooProxy时似乎会再次检查。

4

0 回答 0