小编mad*_*gen的帖子

如果启用MagicHash，则将具有未填充的值，如42#type Int#。

现在，如果Type是值的那种类型，那么样的Int#应该是Type，但它不是，因为Type是一个代名词TYPE 'LiftedRep，而那种Int#是TYPE 'IntRep。我们可以很容易地确认这ghci，

Prelude> :set -XMagicHash -XKindSignatures
Prelude> :m +Data.Kind GHC.Prim
Prelude Data.Kind GHC.Prim> :k (Int# :: Type)

<interactive>:1:2: error:
    • Expecting a lifted type, but ‘Int#’ is unlifted
    • In the type ‘(Int# :: Type)’

难道我们不考虑诸如42#值之类的魔术文字吗？

在以下程序中填补空缺是否一定需要非建设性的手段？如果可以，是否x :~: y可以决定？

更一般而言，如何使用引用来指导类型检查器？

（我知道我可以通过定义Choose为GADT 来解决此问题，我专门针对类型系列）

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module PropositionalDisequality where

import Data.Type.Equality
import Data.Void

type family Choose x y where
  Choose x x = 1
  Choose x _ = 2

lem :: (x :~: y -> Void) -> Choose x y :~: 2
lem refutation = _