伊德里斯没有减少地图查找

Question

为什么不减少函数调用？如何在编译时验证映射是否包含键值对？

import Data.SortedMap

N : SortedMap String Type
N = fromList
    [ ("a", Nat)
    , ("b", String)
    ]

t : lookup "a" N = Just Nat
t = Refl

Type mismatch between
        Just Nat = Just Nat (Type of Refl)
and
        lookup "a" (fromList [("a", Nat), ("b", String)]) = Just Nat (Expected type)

Specifically:
        Type mismatch between
                Just Nat
        and
                lookup "a" (fromList [("a", Nat), ("b", String)])

Answer 1

它必须与SortedMap 的实现有关，因为使用普通List 的版本按预期工作：

N : List (String, Type)
N =
    [ ("a", Nat)
    , ("b", String)
    ]

t : lookup "a" N = Just Nat
t = Refl

根据文档Data.SortedMap.lookup 也是总数，因此应该减少。可能原因是SortedMap 中的函数和数据类型似乎有导出限定符，而Data.List 中的那些使用public export。