Idris not reducing map lookup

Question

Why does is not reduce the function call? How can I verify at compile time that a map contains a key value pair?

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

It must have something todo with the implementation of SortedMap as the version using a plain List works as expected:

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

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

According to the docs Data.SortedMap.lookup is total as well, so it should reduce. Maybe the reason is that the functions and data types in SortedMap seem to have the export qualifier, whereas the ones in Data.List use public export.