[ fix #835 ] Keep names of implicit variables in with clauses (#1017)

Makefile

@@ -82,7 +82,7 @@ libs : prelude base contrib network
 testbin:
 	@${MAKE} -C tests testbin
 
-test:
+test: testbin
 	@echo
 	@echo "NOTE: \`${MAKE} test\` does not rebuild idris; to do that run \`${MAKE}\`"
 	@echo

src/Core/Name.idr

@@ -69,6 +69,11 @@ isUserName (NS _ n) = isUserName n
 isUserName (DN _ n) = isUserName n
 isUserName _ = True
 
+export
+isUN : Name -> Maybe String
+isUN (UN str) = Just str
+isUN _ = Nothing
+
 export
 nameRoot : Name -> String
 nameRoot (NS _ n) = nameRoot n

src/Idris/IDEMode/Holes.idr

@@ -1,6 +1,7 @@
 module Idris.IDEMode.Holes
 
 import Core.Env
+import Core.Context.Log
 
 import Idris.Resugar
 import Idris.Syntax
@@ -78,7 +79,8 @@ extractHoleData defs env fn (S args) (Bind fc x (Let _ c val ty) sc)
 extractHoleData defs env fn (S args) (Bind fc x b sc)
   = do rest <- extractHoleData defs (b :: env) fn args sc
        let True = showName x
-         | False => pure rest
+         | False => do log "idemode.hole" 10 $ "Not showing name: " ++ show x
+                       pure rest
        ity <- resugar env !(normalise defs env (binderType b))
        let premise = MkHolePremise x ity (multiplicity b) (isImplicit b)
        pure $ record { context $= (premise ::)  } rest

src/TTImp/Elab/Check.idr

@@ -27,6 +27,11 @@ import Libraries.Data.StringMap
 public export
 data ElabMode = InType | InLHS RigCount | InExpr | InTransform
 
+export
+isLHS : ElabMode -> Maybe RigCount
+isLHS (InLHS w) = Just w
+isLHS _ = Nothing
+
 Show ElabMode where
   show InType = "InType"
   show (InLHS c) = "InLHS " ++ show c

src/TTImp/Elab/Term.idr

@@ -279,11 +279,11 @@ checkTerm rig elabinfo nest env (IWithUnambigNames fc ns rhs) exp
 TTImp.Elab.Check.check rigc elabinfo nest env (ICoerced fc tm) exp
     = checkImp rigc elabinfo nest env tm exp
 -- Don't add implicits/coercions on local blocks or record updates
-TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILet fc c n nty nval sc) exp
+TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILet _ _ _ _ _ _) exp
     = checkImp rigc elabinfo nest env tm exp
-TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILocal fc ds sc) exp
+TTImp.Elab.Check.check rigc elabinfo nest env tm@(ILocal _ _ _) exp
     = checkImp rigc elabinfo nest env tm exp
-TTImp.Elab.Check.check rigc elabinfo nest env tm@(IUpdate fc fs rec) exp
+TTImp.Elab.Check.check rigc elabinfo nest env tm@(IUpdate _ _ _) exp
     = checkImp rigc elabinfo nest env tm exp
 TTImp.Elab.Check.check rigc elabinfo nest env tm_in exp
     = do defs <- get Ctxt

src/TTImp/ProcessDef.idr

@@ -395,8 +395,8 @@ checkClause mult vis totreq hashit n opts nest env (ImpossibleClause fc lhs)
                (_, lhs) <- bindNames False lhs_raw
                setUnboundImplicits autoimp
 
-               log "declare.def.clause" 5 $ "Checking " ++ show lhs
-               logEnv "declare.def.clause" 5 "In env" env
+               log "declare.def.clause.impossible" 5 $ "Checking " ++ show lhs
+               logEnv "declare.def.clause.impossible" 5 "In env" env
                (lhstm, lhstyg) <-
                            elabTerm n (InLHS mult) opts nest env
                                       (IBindHere fc PATTERN lhs) Nothing
@@ -447,16 +447,16 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
                 elabTermSub n wmode opts nest' env' env sub' wval_raw Nothing
          clearHoleLHS
 
-         logTerm "declare.def.clause" 5 "With value" wval
-         logTerm "declare.def.clause" 3 "Required type" reqty
+         logTerm "declare.def.clause.with" 5 "With value" wval
+         logTerm "declare.def.clause.with" 3 "Required type" reqty
          wvalTy <- getTerm gwvalTy
          defs <- get Ctxt
          wval <- normaliseHoles defs env' wval
          wvalTy <- normaliseHoles defs env' wvalTy
 
          let (wevars ** withSub) = keepOldEnv sub' (snd (findSubEnv env' wval))
-         logTerm "declare.def.clause" 5 "With value type" wvalTy
-         log "declare.def.clause" 5 $ "Using vars " ++ show wevars
+         logTerm "declare.def.clause.with" 5 "With value type" wvalTy
+         log "declare.def.clause.with" 5 $ "Using vars " ++ show wevars
 
          let Just wval = shrinkTerm wval withSub
              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #1")
@@ -495,8 +495,8 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
                  = map Just reqns ++
                    Nothing :: map Just notreqns
 
-         logTerm "declare.def.clause" 3 "With function type" wtype
-         log "declare.def.clause" 5 $ "Argument names " ++ show wargNames
+         logTerm "declare.def.clause.with" 3 "With function type" wtype
+         log "declare.def.clause.with" 5 $ "Argument names " ++ show wargNames
 
          wname <- genWithName !(prettyName !(toFullNames (Resolved n)))
          widx <- addDef wname (record {flags $= (SetTotal totreq ::)}
@@ -513,7 +513,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
 
          -- Generate new clauses by rewriting the matched arguments
          cs' <- traverse (mkClauseWith 1 wname wargNames lhs) cs
-         log "declare.def.clause" 3 $ "With clauses: " ++ show cs'
+         log "declare.def.clause.with" 3 $ "With clauses: " ++ show cs'
 
          -- Elaborate the new definition here
          nestname <- applyEnv env wname
@@ -552,16 +552,19 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
                    RawImp -> ImpClause ->
                    Core ImpClause
     mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)
-        = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
+        = do log "declare.def.clause.with" 20 "PatClause"
+             newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              newrhs <- withRHS ploc drop wname wargnames rhs lhs
              pure (PatClause ploc newlhs newrhs)
     mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs flags ws)
-        = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
+        = do log "declare.def.clause.with" 20 "WithClause"
+             newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              newrhs <- withRHS ploc drop wname wargnames rhs lhs
              ws' <- traverse (mkClauseWith (S drop) wname wargnames lhs) ws
              pure (WithClause ploc newlhs newrhs flags ws')
     mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs)
-        = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
+        = do log "declare.def.clause.with" 20 "ImpossibleClause"
+             newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs
              pure (ImpossibleClause ploc newlhs)
 
 nameListEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)

src/TTImp/WithClause.idr

@@ -5,8 +5,10 @@ import Core.Context.Log
 import Core.TT
 import TTImp.BindImplicits
 import TTImp.TTImp
+import TTImp.Elab.Check
 
 import Data.List
+import Data.Maybe
 
 %default covering
 
@@ -113,20 +115,26 @@ mutual
 
 -- Get the arguments for the rewritten pattern clause of a with by looking
 -- up how the argument names matched
-getArgMatch : FC -> Bool -> RawImp -> List (String, RawImp) ->
-              Maybe (PiInfo RawImp, Name) -> RawImp
-getArgMatch ploc search warg ms Nothing = warg
-getArgMatch ploc True warg ms (Just (AutoImplicit, UN n))
-    = case lookup n ms of
-           Nothing => ISearch ploc 500
-           Just tm => tm
-getArgMatch ploc True warg ms (Just (AutoImplicit, _))
-    = ISearch ploc 500
-getArgMatch ploc search warg ms (Just (_, UN n))
-    = case lookup n ms of
-           Nothing => Implicit ploc True
-           Just tm => tm
-getArgMatch ploc search warg ms _ = Implicit ploc True
+getArgMatch : FC -> (side : ElabMode) -> (search : Bool) ->
+              (warg : RawImp) -> (matches : List (String, RawImp)) ->
+              (arg : Maybe (PiInfo RawImp, Name)) -> RawImp
+getArgMatch ploc mode search warg ms Nothing = warg
+getArgMatch ploc mode True warg ms (Just (AutoImplicit, nm))
+    = case (isUN nm >>= \ n => lookup n ms) of
+        Just tm => tm
+        Nothing =>
+          let arg = ISearch ploc 500 in
+          if isJust (isLHS mode)
+            then IAs ploc UseLeft nm arg
+             else arg
+getArgMatch ploc mode search warg ms (Just (_, nm))
+    = case (isUN nm >>= \ n => lookup n ms) of
+        Just tm => tm
+        Nothing =>
+          let arg = Implicit ploc True in
+           if isJust (isLHS mode)
+             then IAs ploc UseLeft nm arg
+             else arg
 
 export
 getNewLHS : {auto c : Ref Ctxt Defs} ->
@@ -135,21 +143,27 @@ getNewLHS : {auto c : Ref Ctxt Defs} ->
             RawImp -> RawImp -> Core RawImp
 getNewLHS ploc drop nest wname wargnames lhs_raw patlhs
     = do (mlhs_raw, wrest) <- dropWithArgs drop patlhs
+
          autoimp <- isUnboundImplicits
          setUnboundImplicits True
          (_, lhs) <- bindNames False lhs_raw
          (_, mlhs) <- bindNames False mlhs_raw
          setUnboundImplicits autoimp
 
+         log "declare.def.clause.with" 20 $ "Parent LHS (with implicits): " ++ show lhs
+         log "declare.def.clause.with" 20 $ "Modified LHS (with implicits): " ++ show mlhs
+
          let (warg :: rest) = reverse wrest
              | _ => throw (GenericMsg ploc "Badly formed 'with' clause")
-         log "with" 5 $ show lhs ++ " against " ++ show mlhs ++
+         log "declare.def.clause.with" 5 $ show lhs ++ " against " ++ show mlhs ++
                  " dropping " ++ show (warg :: rest)
          ms <- getMatch True lhs mlhs
-         log "with" 5 $ "Matches: " ++ show ms
-         let newlhs = apply (IVar ploc wname)
-                            (map (getArgMatch ploc False warg ms) wargnames ++ rest)
-         log "with" 5 $ "New LHS: " ++ show newlhs
+         log "declare.def.clause.with" 5 $ "Matches: " ++ show ms
+         let params = map (getArgMatch ploc (InLHS top) False warg ms) wargnames
+         log "declare.def.clause.with" 5 $ "Parameters: " ++ show params
+
+         let newlhs = apply (IVar ploc wname) (params ++ rest)
+         log "declare.def.clause.with" 5 $ "New LHS: " ++ show newlhs
          pure newlhs
   where
     dropWithArgs : Nat -> RawImp ->
@@ -180,13 +194,13 @@ withRHS fc drop wname wargnames tm toplhs
     updateWith fc tm []
         = throw (GenericMsg fc "Badly formed 'with' application")
     updateWith fc tm (arg :: args)
-        = do log "with" 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm
+        = do log "declare.def.clause.with" 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm
              ms <- getMatch False toplhs tm
-             log "with" 10 $ "Result: " ++ show ms
+             log "declare.def.clause.with" 10 $ "Result: " ++ show ms
              let newrhs = apply (IVar fc wname)
-                                (map (getArgMatch fc True arg ms) wargnames)
-             log "with" 10 $ "With args for RHS: " ++ show wargnames
-             log "with" 10 $ "New RHS: " ++ show newrhs
+                                (map (getArgMatch fc InExpr True arg ms) wargnames)
+             log "declare.def.clause.with" 10 $ "With args for RHS: " ++ show wargnames
+             log "declare.def.clause.with" 10 $ "New RHS: " ++ show newrhs
              pure (withApply fc newrhs args)
 
     mutual

tests/Main.idr

@@ -71,7 +71,7 @@ idrisTestsInteractive = MkTestPool []
        "interactive005", "interactive006", "interactive007", "interactive008",
        "interactive009", "interactive010", "interactive011", "interactive012",
        "interactive013", "interactive014", "interactive015", "interactive016",
-       "interactive017", "interactive018", "interactive019"]
+       "interactive017", "interactive018", "interactive019", "interactive020"]
 
 idrisTestsInterface : TestPool
 idrisTestsInterface = MkTestPool []

tests/idris2/interactive020/Issue835.idr

@@ -0,0 +1,14 @@
+module Issue835
+
+baz : (x : Nat) -> {P2 : Nat -> Type} -> P2 x
+baz x = ?rhs3
+
+foo : {P : Nat -> Type}  -> Dec (P 0)
+foo = ?rhs1 where
+
+
+  bar : {P2 : Nat -> Type} ->
+          (x : Nat)
+          -> P2 x
+  bar x with (S x)
+     bar x | x1 =  ?rhs2

tests/idris2/interactive020/expected

@@ -0,0 +1,14 @@
+1/1: Building Issue835 (Issue835.idr)
+Issue835>    P : Nat -> Type
+------------------------------
+rhs1 : Dec (P 0)
+Issue835>    P : Nat -> Type
+   x1 : Nat
+   x : Nat
+------------------------------
+rhs2 : P2 x
+Issue835>    P2 : Nat -> Type
+   x : Nat
+------------------------------
+rhs3 : P2 x
+Issue835> Bye for now!

tests/idris2/interactive020/input

@@ -0,0 +1,4 @@
+:t rhs1
+:t rhs2
+:t rhs3
+:q

tests/idris2/interactive020/run

@@ -0,0 +1,3 @@
+$1 --no-banner --no-color --console-width 0 Issue835.idr < input
+
+rm -rf build