未评估 Haskell 类型系列应用程序答案

【问题标题】：Haskell type family applications are not evaluated未评估 Haskell 类型系列应用程序
【发布时间】：2014-09-16 16:32:57
【问题描述】：

我发现了一个有趣的情况，当使用类型族的数据类型时。

编译器的错误信息是No instance for (C (ID ())) arising from a use of W。这表明类型族应用程序没有得到充分评估，即使它已经饱和。 :kind! ID () 计算结果为 ()，因此应使用 C () 实例。

{-# LANGUAGE GADTs, TypeFamilies, UndecidableInstances, FlexibleContexts #-}

type family ID t where
  ID t = t

class C t where
instance C () where

data W where
  W :: C (AppID t) => P t -> W

type family AppID t where
  AppID t = (ConstID t) ()

type family ConstID t where
  ConstID t = ID

data P t where
  P :: P t

data A

w :: W
w = W (P :: P A)

我可以以某种方式强制评估ID ()吗？是编译器的bug吗？

我正在使用 GHC 7.8.3

【问题讨论】：

(ID ()) 如何评估任何东西？ ID 系列没有实例。
我把它写成一个封闭的类型族（haskell.org/haskellwiki/GHC/…）
写成普通类型族不会改变错误。
对不起，我没有仔细阅读您的代码。是的，它看起来应该可以工作。
Eta 扩展 ConstID t 似乎有效。可能在处理部分应用的类型族时存在一些错误，如ID。（老实说，我认为这些是不允许的。我们最近是否有效地获得了类型级别的 lambda？）

标签： haskell gadt type-families data-kinds

【解决方案1】：

问题是ConstID的那种。

type family ConstID t a where
  ConstID t a = ID a

【讨论】：