在依赖型CASE表达式工作不正常的伊德里斯

Question

我玩耍的PureScript码小块移植到伊德里斯在那里依赖类型可以应用和整个的情况跌跌撞撞，其中使用case一个依赖型内不工作。

由于这是有效的（简化的）：

data ValidInvoice3 : (ft : FeeType) -> Type where
  MkVI3 : ValidInvoice3 ft

为什么下面不是类型检查？

-- BROKEN
data ValidInvoice4 : (ft : FeeType) -> Type where
  MkVI4 : case ft of
            FeeMarkupHidden => ValidInvoice4 ft -- simplified;
            FeeExplicit     => ValidInvoice4 ft -- more elaborate example below

如果你有兴趣，为什么我要寻找到这样的：这里有点更复杂的代码示例：

module DependentWithCase

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
  MkFee : Fee ft -- simplified

data ValidArticle : (ft : FeeType) -> Type where
  MkVA : ValidArticle ft -- simplified

这里现在是如何的依赖型的“发票”，可以成功地使用case表达式来决定是否收取费用将作为显式参数添加（在实际的代码，在这种情况下写的，收录在FeeType，该“物品”型然后有一个“标记”的一部分，这是我离开这里了，这样，我可以肯定的是“标记”只是一次发票）：

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft ->
         case ft of FeeMarkupHidden => Unit; FeeExplicit => Fee ft;
         ->
         ValidInvoice ft

所以你看发票数据类型（而在实际的代码中，文章类型而言）取决于费用的类型。

但是，而不是使用埋在构造函数中的情况下表达，我宁愿有它看起来像这种类型的同义词（这当然没有一个构造函数，但是这基本上是它在PureScript代码如何读取，而是使用总和类型有独立构造，而不是依赖型这里，索引超过FeeType）。这是更可读，我（尤其是在实际的代码）。

ValidInvoice2 : (ft : FeeType) -> Type
ValidInvoice2 FeeMarkupHidden = ValidArticle FeeMarkupHidden -> Unit            -> ValidInvoice2 FeeMarkupHidden
ValidInvoice2 FeeExplicit     = ValidArticle FeeExplicit     -> Fee FeeExplicit -> ValidInvoice2 FeeExplicit

那么，为什么ValidInvoice4不是类型检查？我写这错了吗？或者期待着什么工作，只是不能工作？

Answer 1

看来，伊德里斯没有注意到你的case语句的结果，要么分支在ValidInvoice4。它也不会在相似的位置评估功能。你几乎总是可以做一些稍微不同，虽然得到相同的结果。

纵观你想实现什么，我建议你做一个Fee FeeType索引Maybe - 简化了整个事情：

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
    HidFee : Fee FeeMarkupHidden
    ExFee : Nat {- or w/e -} -> Fee FeeExplicit

data ValidArticle : (ft : FeeType) -> Type where
    MkVA : ValidArticle ft

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft -> Fee ft -> ValidInvoice ft