"import qualified" is desired

[luochen1990]

I'm using Idris 1.2.0, and find that import ... as ... is not qualified, and still cause name confliction.

Here is my test code:

module TestNamespace

import Data.Vect as V

data Ty = UNIT | ARR Ty Ty

data Elem : V.Vect n Ty -> Ty -> Type where
  Here : {ts : V.Vect n Ty} -> Elem (t::ts) t
  There : {ts : V.Vect n Ty} -> Elem ts t -> Elem (t'::ts) t

-- Type checking .\namespace-issue.idr
-- namespace-issue.idr:9:11-60:
--   |
-- 9 |   There : {ts : V.Vect n Ty} -> Elem ts t -> Elem (t'::ts) t
--   |           ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- When checking type of There:
-- Can't disambiguate name: TestNamespace.Elem, Data.Vect.Elem

I think we have to provide qualified importing. Consider the following situation: We have written down thousands of code and using some Identifier A, and one day, we need to import a new package P, and P also defined A. If there is no qualified importing, we have to change thousands of code to replace A into Main.A, just because we want to import another package.

[ahmadsalim]

Thanks for the feature request. Contributions are more than welcome!