[octatoan]

If I remember correctly, isn't this one of the problems Idris and Agda are good at solving?

[andolanra]

We could in fact write mkMap in Idris with very little change, and give it a proper type:

    -- This might not be the best/cleanest way of writing it, as my
    -- Idris is a little rusty, but this will work:
    mkMap : (size: Int) -> (if size > threshold then HashMap else TreeMap)
    mkMap size with (size > threshold)
      | True  = newHashMap
      | False = newTreeMap

So yes, although again, other tradeoffs are made to allow this kind of radical expressiveness.