Apply the patch from idris2-boot.

CHANGELOG.md

@@ -21,6 +21,9 @@ Language changes:
 * A %spec flag on functions which allows arguments to be marked for partial
   evaluation, following the rules from "Scrapping Your Inefficient Engine"
   (ICFP 2010, Brady & Hammond)
+* To improve error messages, one can use `with NS.name <term>`
+  or `with [NS.name1, NS.name2, ...] <term>` to disable disambiguation
+  for the given names in `<term>`. Example: `with MyNS.(>>=) do ...`.
 
 Library additions:
 

docs/source/tutorial/modules.rst

@@ -64,7 +64,15 @@ the name of the module. The names defined in the ``BTree`` module are, in full:
 
 If names are otherwise unambiguous, there is no need to give the fully
 qualified name. Names can be disambiguated either by giving an explicit
-qualification, or according to their type.
+qualification, using the ``with`` keyword, or according to their type.
+
+The ``with`` keyword in expressions comes in two variants:
+
+* ``with BTree.insert (insert x empty)`` for one name
+* ``with [BTree.insert, BTree.empty] (insert x empty)`` for multiple names
+
+This is particularly useful with ``do`` notation, where it can often improve
+error messages: ``with MyModule.(>>=) do ...``
 
 There is no formal link between the module name and its filename,
 although it is generally advisable to use the same name for each. An

src/Idris/Desugar.idr

@@ -353,6 +353,8 @@ mutual
       = desugarB side ps $
           PLam fc top Explicit (PRef fc (MN "rec" 0)) (PImplicit fc) $
             foldl (\r, f => PApp fc (PRef fc f) r) (PRef fc (MN "rec" 0)) fields
+  desugarB side ps (PWithUnambigNames fc ns rhs)
+      = IWithUnambigNames fc ns <$> desugarB side ps rhs
 
   desugarUpdate : {auto s : Ref Syn SyntaxInfo} ->
                   {auto b : Ref Bang BangData} ->

src/Idris/Parser.idr

@@ -128,6 +128,7 @@ mutual
     <|> lambdaCase fname indents
     <|> lazy fname indents
     <|> if_ fname indents
+    <|> with_ fname indents
     <|> doBlock fname indents
     <|> do start <- location
            f <- simpleExpr fname indents
@@ -188,6 +189,29 @@ mutual
            symbol "}"
            pure (Nothing, tm)
 
+  with_ : FileName -> IndentInfo -> Rule PTerm
+  with_ fname indents
+      = do start <- location
+           keyword "with"
+           commit
+           ns <- singleName <|> nameList
+           end <- location
+           rhs <- expr pdef fname indents
+           pure (PWithUnambigNames (MkFC fname start end) ns rhs)
+    where
+      singleName : Rule (List Name)
+      singleName = do
+        n <- name
+        pure [n]
+
+      nameList : Rule (List Name)
+      nameList = do
+        symbol "["
+        commit
+        ns <- sepBy1 (symbol ",") name
+        symbol "]"
+        pure ns
+
   opExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
   opExpr q fname indents
       = do start <- location

src/Idris/Resugar.idr

@@ -252,6 +252,9 @@ mutual
   toPTerm p (Implicit fc True) = pure (PImplicit fc)
   toPTerm p (Implicit fc False) = pure (PInfer fc)
 
+  toPTerm p (IWithUnambigNames fc ns rhs) =
+    PWithUnambigNames fc ns <$> toPTerm startPrec rhs
+
   mkApp : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           PTerm -> List (FC, Maybe (Maybe Name), PTerm) -> Core PTerm

src/Idris/Syntax.idr

@@ -96,7 +96,8 @@ mutual
        -- Debugging
        PUnifyLog : FC -> Nat -> PTerm -> PTerm
 
-       -- TODO: 'with' disambiguation
+       -- with-disambiguation
+       PWithUnambigNames : FC -> List Name -> PTerm -> PTerm
 
   public export
   data PFieldUpdate : Type where
@@ -493,6 +494,8 @@ mutual
         = showPrec d rec ++ concatMap show fields
     showPrec d (PRecordProjection fc fields)
         = concatMap show fields
+    showPrec d (PWithUnambigNames fc ns rhs)
+        = "with " ++ show ns ++ " " ++ showPrec d rhs
 
 public export
 record IFaceInfo where
@@ -776,6 +779,9 @@ mapPTermM f = goPTerm where
       >>= f
     goPTerm (PRecordProjection fc fields) =
       f (PRecordProjection fc fields)
+    goPTerm (PWithUnambigNames fc ns rhs) =
+      PWithUnambigNames fc ns <$> goPTerm rhs
+      >>= f
 
     goPFieldUpdate : PFieldUpdate -> Core PFieldUpdate
     goPFieldUpdate (PSetField p t)    = PSetField p <$> goPTerm t

src/TTImp/Elab/Ambiguity.idr

@@ -15,6 +15,7 @@ import TTImp.TTImp
 
 import Data.Bool.Extra
 import Data.List
+import Data.StringMap
 
 %default covering
 
@@ -49,6 +50,11 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
                         ci <- fromCharName
                         let prims = mapMaybe id [fi, si, ci]
                         let primApp = isPrimName prims x
+                        case lookupUN (userNameRoot x) (unambiguousNames est) of
+                          Just xr => do
+                            log 10 $ "unambiguous: " ++ show (fst xr)
+                            pure $ mkAlt primApp est xr
+                          Nothing => do
                             ns <- lookupCtxtName x (gamma defs)
                             ns' <- filterM visible ns
                             case ns' of
@@ -60,6 +66,10 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
                                nalts => pure $ IAlternative fc (uniqType fi si ci x args)
                                                       (map (mkAlt primApp est) nalts)
   where
+    lookupUN : Maybe String -> StringMap a -> Maybe a
+    lookupUN Nothing _ = Nothing
+    lookupUN (Just n) sm = lookup n sm
+
     visible : (Name, Int, GlobalDef) -> Core Bool
     visible (n, i, def)
         = do let NS ns x = fullname def

src/TTImp/Elab/Check.idr

@@ -131,13 +131,18 @@ record EState (vars : List Name) where
   linearUsed : List (Var vars)
   saveHoles : NameMap () -- things we'll need to save to TTC, even if solved
 
+  unambiguousNames : StringMap (Name, Int, GlobalDef)
+                  -- Mapping from userNameRoot to fully resolved names.
+                  -- For names in this mapping, we don't run disambiguation.
+                  -- Used in with-expressions.
+
 export
 data EST : Type where
 
 export
 initEStateSub : {outer : _} ->
                 Int -> Env Term outer -> SubVars outer vars -> EState vars
-initEStateSub n env sub = MkEState n env sub [] [] [] [] [] Z [] empty
+initEStateSub n env sub = MkEState n env sub [] [] [] [] [] Z [] empty empty
 
 export
 initEState : {vars : _} ->
@@ -167,7 +172,8 @@ weakenedEState {e}
                               (allPatVars est)
                               (delayDepth est)
                               (map weaken (linearUsed est))
-                              (saveHoles est))
+                              (saveHoles est)
+                              (unambiguousNames est))
          pure eref
   where
     wknTms : (Name, ImplBinding vs) ->
@@ -199,7 +205,8 @@ strengthenedEState {n} {vars} c e fc env
                         (allPatVars est)
                         (delayDepth est)
                         (mapMaybe dropTop (linearUsed est))
-                        (saveHoles est))
+                        (saveHoles est)
+                        (unambiguousNames est))
   where
     dropSub : SubVars xs (y :: ys) -> Core (SubVars xs ys)
     dropSub (DropCons sub) = pure sub
@@ -293,6 +300,7 @@ updateEnv env sub bif st
                (delayDepth st)
                (linearUsed st)
                (saveHoles st)
+               (unambiguousNames st)
 
 export
 addBindIfUnsolved : {vars : _} ->
@@ -309,6 +317,7 @@ addBindIfUnsolved hn r p env tm ty st
                (delayDepth st)
                (linearUsed st)
                (saveHoles st)
+               (unambiguousNames st)
 
 clearBindIfUnsolved : EState vars -> EState vars
 clearBindIfUnsolved st
@@ -320,6 +329,7 @@ clearBindIfUnsolved st
                (delayDepth st)
                (linearUsed st)
                (saveHoles st)
+               (unambiguousNames st)
 
 -- Clear the 'toBind' list, except for the names given
 export

src/TTImp/Elab/Term.idr

@@ -1,5 +1,7 @@
 module TTImp.Elab.Term
 
+import Data.StringMap
+
 import Core.Context
 import Core.Core
 import Core.Env
@@ -215,6 +217,37 @@ checkTerm rig elabinfo nest env (Implicit fc b) Nothing
             do est <- get EST
                put EST (addBindIfUnsolved nm rig Explicit env metaval ty est)
          pure (metaval, gnf env ty)
+checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
+    = with Core do
+         -- enter the scope -> add unambiguous names
+         est <- get EST
+         rns <- resolveNames fc ns
+         put EST $ record { unambiguousNames = mergeLeft rns (unambiguousNames est) } est
+
+         -- inside the scope -> check the RHS
+         result <- check rig elabinfo nest env rhs exp
+
+         -- exit the scope -> restore unambiguous names
+         newEST <- get EST
+         put EST $ record { unambiguousNames = unambiguousNames est } newEST
+
+         pure result
+  where
+    resolveNames : FC -> List Name -> Core (StringMap (Name, Int, GlobalDef))
+    resolveNames fc [] = pure empty
+    resolveNames fc (n :: ns) =
+      case userNameRoot n of
+        -- should never happen
+        Nothing => throw $ InternalError $ "non-UN in \"with\" LHS: " ++ show n
+        Just nRoot => do
+          -- this will always be a global name
+          -- so we lookup only among the globals
+          ctxt <- get Ctxt
+          rns <- lookupCtxtName n (gamma ctxt)
+          case rns of
+            []   => throw $ UndefinedName fc n
+            [rn] => insert nRoot rn <$> resolveNames fc ns
+            _    => throw $ AmbiguousName fc (map fst rns)
 
 -- Declared in TTImp.Elab.Check
 -- check : {vars : _} ->

src/TTImp/TTImp.idr

@@ -105,6 +105,9 @@ mutual
        -- at the end of elaborator
        Implicit : FC -> (bindIfUnsolved : Bool) -> RawImp
 
+       -- with-disambiguation
+       IWithUnambigNames : FC -> List Name -> RawImp -> RawImp
+
   public export
   data IFieldUpdate : Type where
        ISetField : (path : List String) -> RawImp -> IFieldUpdate
@@ -170,6 +173,7 @@ mutual
       show (IType fc) = "%type"
       show (Implicit fc True) = "_"
       show (Implicit fc False) = "?"
+      show (IWithUnambigNames fc ns rhs) = "(%with " ++ show ns ++ " " ++ show rhs ++ ")"
 
   export
   Show IFieldUpdate where
@@ -590,6 +594,7 @@ getFC (IUnquote x _) = x
 getFC (IRunElab x _) = x
 getFC (IAs x _ _ _) = x
 getFC (Implicit x _) = x
+getFC (IWithUnambigNames x _ _) = x
 
 export
 apply : RawImp -> List RawImp -> RawImp
@@ -679,6 +684,8 @@ mutual
 
     toBuf b (Implicit fc i)
         = do tag 28; toBuf b fc; toBuf b i
+    toBuf b (IWithUnambigNames fc ns rhs)
+        = do tag 29; toBuf b ns; toBuf b rhs
 
     fromBuf b
         = case !getTag of
@@ -763,6 +770,10 @@ mutual
                28 => do fc <- fromBuf b
                         i <- fromBuf b
                         pure (Implicit fc i)
+               29 => do fc <- fromBuf b
+                        ns <- fromBuf b
+                        rhs <- fromBuf b
+                        pure (IWithUnambigNames fc ns rhs)
                _ => corrupt "RawImp"
 
   export

tests/Main.idr

@@ -90,7 +90,9 @@ idrisTests
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008",
        -- The 'with' rule
-       "with001", "with002"]
+       "with001", "with002",
+       -- with-disambiguation
+       "with003"]
 
 typeddTests : List String
 typeddTests

tests/idris2/with003/Main.idr

@@ -0,0 +1,10 @@
+module Main
+
+import Data.List
+import Data.Vect
+
+-- add some definition of (>>=) in another namespace
+namespace Other
+  public export
+  (>>=) : IO a -> IO b -> IO b
+  (>>=) f x = f *> x

tests/idris2/with003/expected

@@ -0,0 +1,53 @@
+1/1: Building Main (Main.idr)
+Main> (interactive):1:60--1:73:Sorry, I can't find any elaboration which works. All errors:
+If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors:
+If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
+Mismatch between:
+	?_ -> IO ()
+and
+	IO ?b
+
+If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b
+Mismatch between:
+	?_ -> IO ()
+and
+	IO ?b
+
+
+If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
+If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
+Mismatch between:
+	?_ -> IO ()
+and
+	IO ?b
+
+If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors:
+If Prelude.>>=: When unifying ?_ -> IO () and IO ?b
+Mismatch between:
+	?_ -> IO ()
+and
+	IO ?b
+
+If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b
+Mismatch between:
+	?_ -> IO ()
+and
+	IO ?b
+
+
+
+Main> (interactive):1:57--1:62:Can't find an implementation for Num ()
+Main> (interactive):1:4--1:6:Ambiguous elaboration. Possible correct results:
+	[]
+	[]
+	[]
+Main> [] : Vect 0 ?elem
+Main> [] : List ?a
+Main> (interactive):1:34--1:41:When unifying Vect 0 ?elem and List ?a
+Mismatch between:
+	Vect 0 ?elem
+and
+	List ?a
+Main> the (Maybe Integer) (pure 4) : Maybe Integer
+Main> Parse error: Unrecognised command (next tokens: [identifier t, with, symbol [, symbol ], literal 4, end of input])
+Main> Bye for now!

tests/idris2/with003/input

@@ -0,0 +1,9 @@
+do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo"
+with Prelude.(>>=) do printLn "foo"; printLn "boo"; map (+1) (printLn "woo"); printLn "goo"; printLn "foo"
+:t []
+:t with Vect.Nil []
+:t with Prelude.Nil []
+:t with [Vect.Nil, Prelude.(::)] [1,2,3]
+:t with pure the (Maybe _) (pure 4)
+:t with [] 4
+:q

tests/idris2/with003/run

@@ -0,0 +1,3 @@
+$1 --no-banner Main.idr < input
+
+rm -rf build