无需依赖类型，如何确保GADT的两个类型变量一致？

Problem Context #

你正在开发编译器，用GADT作为中间表示（IR），在从旧的非GADT数据类型转换到GADT时，遇到了NewLVal a和Pure b的类型参数无法统一的问题。你已经有了能获取值类型的Typed类，但不想依赖singletons这类依赖类型工具，希望找到纯运行时检查+类型安全转换的方案。

Solution 1: Runtime Type Check + Safe unsafeCoerce #

核心思路是利用你已有的Typed类获取运行时类型信息，先验证NewLVal和Pure的类型是否匹配，再用unsafeCoerce完成类型转换（这里的unsafeCoerce是安全的，因为我们已经通过运行时检查确保了类型一致性）。

Step 1: Implement Type Equality Check

首先给值级的Type实现相等性判断函数：

eqType :: Type -> Type -> Bool
eqType IntT IntT = True
eqType (PtrT t1) (PtrT t2) = eqType t1 t2
eqType _ _ = False

Step 2: Modify Conversion Functions to Return Type Info

调整convertLVal和convertPure，让它们同时返回转换后的GADT值和对应的运行时Type：

convertLVal :: OldLVal -> Either String (NewLVal a, Type)
convertLVal oldLval = do
  let t = typeOf oldLval
  newLval <- case oldLval of
    VarOL n -> Right $ VarNL (Temp n)
    LDeref ol -> do
      (nl, olType) <- convertLVal ol
      -- 额外检查：LDeref的操作数必须是指针类型
      case olType of
        PtrT _ -> Right $ DerefNL nl
        _ -> Left $ "Cannot dereference non-pointer type: " ++ show olType
  Right (newLval, t)

convertPure :: Exp -> Either String (Pure a, Type)
convertPure exp = do
  let t = typeOf exp
  pureExp <- case exp of
    Var n -> Right $ VarP (Temp n)
    IntT i -> Right $ ConstP i
    Deref e -> do
      (pe, eType) <- convertPure e
      -- 额外检查：Deref的表达式必须是指针类型
      case eType of
        PtrT _ -> Right $ unsafeCoerce pe -- 对应Pure的指针解引用结果类型
        _ -> Left $ "Cannot dereference non-pointer expression: " ++ show eType
  Right (pureExp, t)

Step 3: Implement matchType

现在可以实现matchType，先检查类型是否相等，再转换：

matchType :: (NewLVal a, Type) -> (Pure b, Type) -> Either String (Pure a)
matchType (_, t1) (p, t2)
  | eqType t1 t2 = Right $ unsafeCoerce p
  | otherwise = Left $ "Type mismatch: expected " ++ show t1 ++ ", got " ++ show t2

这里的unsafeCoerce是安全的：我们已经通过eqType确认了运行时类型一致，而GADT的类型参数和值级Type一一对应，所以类型级的a和b必然相等，只是编译器无法自动推导。

Solution 2: Pre-Check Types Before Conversion #

另一种更直接的方式是在转换AssignStmt时，先检查旧类型的类型是否匹配，再进行转换：

convert :: Statement -> Either String Command
convert (AssignStmt oldLval exp) = do
  let tLval = typeOf oldLval
      tExp = typeOf exp
  if not (eqType tLval tExp)
    then Left $ "Assignment type mismatch: left-hand side is " ++ show tLval ++ ", right-hand side is " ++ show tExp
    else do
      newLval <- fst <$> convertLVal oldLval
      pureExp <- fst <$> convertPure exp
      Right $ Assign newLval (unsafeCoerce pureExp)

这种方案省去了单独的matchType函数，提前在转换入口做类型检查，逻辑更简洁。

Key Notes for Safety #

• Ensure eqType is Correct: 必须保证eqType的实现和类型级Type的结构完全一致，任何遗漏或错误都会导致unsafeCoerce的不安全使用。
• Validate Typed Implementations: typeOf方法必须准确返回每个值对应的运行时Type，否则运行时检查会失效。
• Extend with Care: 如果后续扩展Type的构造器，必须同步更新eqType、typeOf以及转换函数的逻辑。

内容的提问来源于stack exchange，提问作者Mezuzza