2

考虑以下代码

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
module Test () where

type C x = x ~ 1
type family F x = r where
  F 0 = 0
  F 1 = 2
  F 2 = 4

我试图说服 gchi:kind! forall x . C x => F x 解决2. 但看起来我只能在=>. 有没有办法解决这个问题？特别是我得到

<interactive>:1:20: error:
    • Expected a type, but ‘F x’ has kind ‘GHC.Types.Nat’
    • In the type ‘forall x. C x => F x’

编辑：将其包装在代理中似乎不起作用：

:kind! (forall x . C x => Proxy (F x))
(forall x . C x => Proxy (F x)) :: *
= C x => Proxy (F x)
4

0 回答 0