Type Checking failed when using Dependent Pair

Question

I write down this:

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"))]

And get the following wield error message:

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

But I can't understand, Why case "num" of "num" => Int; "str" => String is not a numeric type? isn't it equals to Int ?

Answer 1

It's not, because Idris does not reduce partial (non-total) functions during type-checking.

If you have a good default type for the cases when your string is not equal to "num" / "str" then you can have something like this:

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"))]

---

Another option is to define it like so:

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")]