如何在Haskell中使用引用来指示类型检查器？

Question

在以下程序中填补空缺是否一定需要非建设性的手段？如果可以，是否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 = _