使用依赖对时类型检查失败

Question

我写下这个：

data IsTag : String -> Type where
    NumIsTag : IsTag "num"
    StrIsTag : IsTag "str"

arr1 : List (tag : String ** (IsTag tag, (case tag of "num" => Int; "str" => String)))
arr1 = [("num" ** (NumIsTag, 1)), ("str" ** (StrIsTag, "hello"))]

并得到以下使用错误消息：

When checking right hand side of arr1 with expected type
        List (tag : String **
              (IsTag tag, case tag of   "num" => Int "str" => String))

When checking argument b to constructor Builtins.MkPair:
        case "num" of
          "num" => Int
          "str" => String is not a numeric type

但我不明白，为什么case "num" of "num" => Int; "str" => String 不是数字类型？不是等于Int吗？

Answer 1

不是，因为 Idris 在类型检查期间不会减少部分（非全部）函数。

如果您的字符串不等于 "num" / "str" 的情况下您有一个很好的默认类型，那么您可以有这样的事情：

total
tagToType : String -> Type
tagToType "num" = Int
tagToType "str" = String
tagToType _ = ?defaultType

arr1 : List (tag : String ** (IsTag tag, tagToType tag))
arr1 = [("num" ** (NumIsTag, 1)), ("str" ** (StrIsTag, "hello"))]

---

另一种选择是这样定义它：

total
tagToType : IsTag s -> Type
tagToType NumIsTag = Int
tagToType StrIsTag = String

arr1 : List (tag : String ** istag : IsTag tag ** tagToType istag)
arr1 = [("num" ** NumIsTag ** 1), ("str" ** StrIsTag ** "hello")]