[ fix #893 ] proof gadget for with clauses (#1222)

libs/contrib/Data/Fun/Graph.idr

@@ -5,7 +5,7 @@ public export
 record Graph {0 a : Type} {0 b : a -> Type}
              (f : (x : a) -> b x) (x : a) (y : b x) where
   constructor MkGraph
-  proof : f x === y
+  equality : f x === y
 
 ||| An alternative for 'Syntax.WithProof' that allows to keep the
 ||| proof certificate in non-reduced form after nested matching.

src/Core/Binary.idr

@@ -31,7 +31,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 46
+ttcVersion = 47
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/TT.idr

@@ -365,12 +365,12 @@ setMultiplicity (PLet fc _ val ty) c = PLet fc c val ty
 setMultiplicity (PVTy fc _ ty) c = PVTy fc c ty
 
 Show ty => Show (Binder ty) where
-	show (Lam _ c _ t) = "\\" ++ showCount c ++ show t
+  show (Lam _ c _ t) = "\\" ++ showCount c ++ show t
-	show (Pi _ c _ t) = "Pi " ++ showCount c ++ show t
+  show (Pi _ c _ t) = "Pi " ++ showCount c ++ show t
-	show (Let _ c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t
+  show (Let _ c v t) = "let " ++ showCount c ++ show v ++ " : " ++ show t
-	show (PVar _ c _ t) = "pat " ++ showCount c ++ show t
+  show (PVar _ c _ t) = "pat " ++ showCount c ++ show t
-	show (PLet _ c v t) = "plet " ++ showCount c ++ show v ++ " : " ++ show t
+  show (PLet _ c v t) = "plet " ++ showCount c ++ show v ++ " : " ++ show t
-	show (PVTy _ c t) = "pty " ++ showCount c ++ show t
+  show (PVTy _ c t) = "pty " ++ showCount c ++ show t
 
 export
 setType : Binder tm -> tm -> Binder tm

src/Core/Unify.idr

@@ -1142,23 +1142,23 @@ mutual
                        (NDCon xfc x tagx ax xs)
                        (NDCon yfc y tagy ay ys)
   unifyNoEta mode loc env (NTCon xfc x tagx ax xs) (NTCon yfc y tagy ay ys)
-      = if x == y
+   = do x <- toFullNames x
-           then do ust <- get UST
+        y <- toFullNames y
-                   -- see above
+        log "unify" 20 $ "Comparing type constructors " ++ show x ++ " and " ++ show y
-                   {-
+        if x == y
-                   when (logging ust) $
+           then do let xs = map snd xs
-                      do log "" 0 $ "Constructor " ++ show !(toFullNames x) ++ " " ++ show loc
+                   let ys = map snd ys
-                         log "" 0 "ARGUMENTS:"
+
-                         defs <- get Ctxt
+                   logC "unify" 20 $
-                         traverse_ (dumpArg env) xs
+                     pure $ "Constructor " ++ show x
-                         log "" 0 "WITH:"
+                   logC "unify" 20 $ map (const "") $ traverse_ (dumpArg env) xs
-                         traverse_ (dumpArg env) ys
+                   logC "unify" 20 $ map (const "") $ traverse_ (dumpArg env) ys
-                   -}
+                   unifyArgs mode loc env xs ys
-                   unifyArgs mode loc env (map snd xs) (map snd ys)
              -- TODO: Type constructors are not necessarily injective.
              -- If we don't know it's injective, need to postpone the
              -- constraint. But before then, we need some way to decide
              -- what's injective...
+             -- gallais: really? We don't mind being anticlassical do we?
 --                then postpone True loc mode env (quote empty env (NTCon x tagx ax xs))
 --                                           (quote empty env (NTCon y tagy ay ys))
            else convertError loc env

src/Idris/Desugar.idr

@@ -650,11 +650,11 @@ mutual
 
            pure (nm, PatClause fc lhs' rhs')
 
-  desugarClause ps arg (MkWithClause fc lhs wval flags cs)
+  desugarClause ps arg (MkWithClause fc lhs wval prf flags cs)
       = do cs' <- traverse (map snd . desugarClause ps arg) cs
            (nm, bound, lhs') <- desugarLHS ps arg lhs
            wval' <- desugar AnyExpr (bound ++ ps) wval
-           pure (nm, WithClause fc lhs' wval' flags cs')
+           pure (nm, WithClause fc lhs' wval' prf flags cs')
 
   desugarClause ps arg (MkImpossible fc lhs)
       = do (nm, _, lhs') <- desugarLHS ps arg lhs
@@ -774,8 +774,8 @@ mutual
       toIDef : Name -> ImpClause -> Core ImpDecl
       toIDef nm (PatClause fc lhs rhs)
           = pure $ IDef fc nm [PatClause fc lhs rhs]
-      toIDef nm (WithClause fc lhs rhs flags cs)
+      toIDef nm (WithClause fc lhs rhs prf flags cs)
-          = pure $ IDef fc nm [WithClause fc lhs rhs flags cs]
+          = pure $ IDef fc nm [WithClause fc lhs rhs prf flags cs]
       toIDef nm (ImpossibleClause fc lhs)
           = pure $ IDef fc nm [ImpossibleClause fc lhs]
 

src/Idris/Elab/Implementation.idr

@@ -477,10 +477,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im
     updateClause ns (PatClause fc lhs rhs)
         = do lhs' <- updateApp ns lhs
              pure (PatClause fc lhs' rhs)
-    updateClause ns (WithClause fc lhs wval flags cs)
+    updateClause ns (WithClause fc lhs wval prf flags cs)
         = do lhs' <- updateApp ns lhs
              cs' <- traverse (updateClause ns) cs
-             pure (WithClause fc lhs' wval flags cs')
+             pure (WithClause fc lhs' wval prf flags cs')
     updateClause ns (ImpossibleClause fc lhs)
         = do lhs' <- updateApp ns lhs
              pure (ImpossibleClause fc lhs')

src/Idris/Elab/Interface.idr

@@ -483,9 +483,9 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
         changeName : Name -> ImpClause -> ImpClause
         changeName dn (PatClause fc lhs rhs)
             = PatClause fc (changeNameTerm dn lhs) rhs
-        changeName dn (WithClause fc lhs wval flags cs)
+        changeName dn (WithClause fc lhs wval prf flags cs)
             = WithClause fc (changeNameTerm dn lhs) wval
-                         flags (map (changeName dn) cs)
+                         prf flags (map (changeName dn) cs)
         changeName dn (ImpossibleClause fc lhs)
             = ImpossibleClause fc (changeNameTerm dn lhs)
 

src/Idris/Parser.idr

@@ -866,14 +866,16 @@ mutual
             let fc = boundToFC fname (mergeBounds start b)
             pure (MkPatClause fc lhs rhs ws)
      <|> do b <- bounds (do keyword "with"
+                            commit
                             flags <- bounds (withFlags)
                             symbol "("
                             wval <- bracketedExpr fname flags indents
+                            prf <- optional (keyword "proof" *> name)
                             ws <- mustWork $ nonEmptyBlockAfter col (clause (S withArgs) fname)
-                            pure (flags, wval, forget ws))
+                            pure (prf, flags, wval, forget ws))
-            (flags, wval, ws) <- pure b.val
+            (prf, flags, wval, ws) <- pure b.val
             let fc = boundToFC fname (mergeBounds start b)
-            pure (MkWithClause fc lhs wval flags.val ws)
+            pure (MkWithClause fc lhs wval prf flags.val ws)
      <|> do end <- bounds (keyword "impossible")
             atEnd indents
             pure (MkImpossible (boundToFC fname (mergeBounds start end)) lhs)
@@ -888,7 +890,9 @@ mutual
            -- Can't have the dependent 'if' here since we won't be able
            -- to infer the termination status of the rule
            ifThenElse (withArgs /= length extra)
-              (fatalError "Wrong number of 'with' arguments")
+              (fatalError $ "Wrong number of 'with' arguments:"
+                         ++ " expected " ++ show withArgs
+                         ++ " but got " ++ show (length extra))
               (parseRHS withArgs fname b col indents (applyArgs lhs extra))
     where
       applyArgs : PTerm -> List (FC, PTerm) -> PTerm

src/Idris/Pretty.idr

@@ -108,7 +108,7 @@ mutual
   prettyAlt : PClause -> Doc IdrisAnn
   prettyAlt (MkPatClause _ lhs rhs _) =
     space <+> pipe <++> prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs <+> semi
-  prettyAlt (MkWithClause _ lhs wval flags cs) =
+  prettyAlt (MkWithClause _ lhs wval prf flags cs) =
     space <+> pipe <++> angles (angles (reflow "with alts not possible")) <+> semi
   prettyAlt (MkImpossible _ lhs) =
     space <+> pipe <++> prettyTerm lhs <++> impossible_ <+> semi
@@ -116,7 +116,7 @@ mutual
   prettyCase : PClause -> Doc IdrisAnn
   prettyCase (MkPatClause _ lhs rhs _) =
     prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs
-  prettyCase (MkWithClause _ lhs rhs flags _) =
+  prettyCase (MkWithClause _ lhs rhs prf flags _) =
     space <+> pipe <++> angles (angles (reflow "with alts not possible"))
   prettyCase (MkImpossible _ lhs) =
     prettyTerm lhs <++> impossible_

src/Idris/REPL.idr

@@ -217,12 +217,16 @@ printClause l i (PatClause _ lhsraw rhsraw)
     = do lhs <- pterm lhsraw
          rhs <- pterm rhsraw
          pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
-printClause l i (WithClause _ lhsraw wvraw flags csraw)
+printClause l i (WithClause _ lhsraw wvraw prf flags csraw)
     = do lhs <- pterm lhsraw
          wval <- pterm wvraw
          cs <- traverse (printClause l (i + 2)) csraw
-         pure ((relit l ((pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n")) ++
+         pure (relit l ((pack (replicate i ' ')
-                 showSep "\n" cs))
+                ++ show lhs
+                ++ " with (" ++ show wval ++ ")"
+                ++ maybe "" (\ nm => " proof " ++ show nm) prf
+                ++ "\n"))
+               ++ showSep "\n" cs)
 printClause l i (ImpossibleClause _ lhsraw)
     = do lhs <- pterm lhsraw
          pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))

src/Idris/Resugar.idr

@@ -352,9 +352,10 @@ mutual
       = pure (MkPatClause fc !(toPTerm startPrec lhs)
                              !(toPTerm startPrec rhs)
                              [])
-  toPClause (WithClause fc lhs rhs flags cs)
+  toPClause (WithClause fc lhs rhs prf flags cs)
       = pure (MkWithClause fc !(toPTerm startPrec lhs)
                               !(toPTerm startPrec rhs)
+                              prf
                               flags
                               !(traverse toPClause cs))
   toPClause (ImpossibleClause fc lhs)

src/Idris/Syntax.idr

@@ -221,14 +221,15 @@ mutual
   data PClause : Type where
        MkPatClause : FC -> (lhs : PTerm) -> (rhs : PTerm) ->
                      (whereblock : List PDecl) -> PClause
-       MkWithClause : FC -> (lhs : PTerm) -> (wval : PTerm) ->
+       MkWithClause : FC -> (lhs : PTerm) ->
+                      (wval : PTerm) -> (prf : Maybe Name) ->
                       List WithFlag -> List PClause -> PClause
        MkImpossible : FC -> (lhs : PTerm) -> PClause
 
   export
   getPClauseLoc : PClause -> FC
   getPClauseLoc (MkPatClause fc _ _ _) = fc
-  getPClauseLoc (MkWithClause fc _ _ _ _) = fc
+  getPClauseLoc (MkWithClause fc _ _ _ _ _) = fc
   getPClauseLoc (MkImpossible fc _) = fc
 
   public export
@@ -482,7 +483,7 @@ record Module where
 mutual
   showAlt : PClause -> String
   showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
-  showAlt (MkWithClause _ lhs wval flags cs) = " | <<with alts not possible>>;"
+  showAlt (MkWithClause _ lhs wval prf flags cs) = " | <<with alts not possible>>;"
   showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;"
 
   showDo : PDo -> String
@@ -540,7 +541,7 @@ mutual
       where
         showAlt : PClause -> String
         showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
-        showAlt (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
+        showAlt (MkWithClause _ lhs rhs prf flags _) = " | <<with alts not possible>>"
         showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;"
     showPrec _ (PCase _ tm cs)
         = "case " ++ show tm ++ " of { " ++
@@ -548,7 +549,7 @@ mutual
       where
         showCase : PClause -> String
         showCase (MkPatClause _ lhs rhs _) = show lhs ++ " => " ++ show rhs
-        showCase (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
+        showCase (MkWithClause _ lhs rhs _ flags _) = " | <<with alts not possible>>"
         showCase (MkImpossible _ lhs) = show lhs ++ " impossible"
     showPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form...
         = "let { << definitions >>  } in " ++ showPrec d sc
@@ -1010,9 +1011,10 @@ mapPTermM f = goPTerm where
       MkPatClause fc <$> goPTerm lhs
                      <*> goPTerm rhs
                      <*> goPDecls wh
-    goPClause (MkWithClause fc lhs wVal flags cls) =
+    goPClause (MkWithClause fc lhs wVal prf flags cls) =
       MkWithClause fc <$> goPTerm lhs
                       <*> goPTerm wVal
+                      <*> pure prf
                       <*> pure flags
                       <*> goPClauses cls
     goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs

src/Parser/Lexer/Source.idr

@@ -201,7 +201,7 @@ mkDirective str = CGDirective (trim (substr 3 (length str) str))
 keywords : List String
 keywords = ["data", "module", "where", "let", "in", "do", "record",
             "auto", "default", "implicit", "mutual", "namespace",
-            "parameters", "with", "impossible", "case", "of",
+            "parameters", "with", "proof", "impossible", "case", "of",
             "if", "then", "else", "forall", "rewrite",
             "using", "interface", "implementation", "open", "import",
             "public", "export", "private",

src/TTImp/Elab/Case.idr

@@ -336,11 +336,11 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
                         (bindCaseLocals loc' (map getNestData (names nest))
                                         ns rhs)
     -- With isn't allowed in a case block but include for completeness
-    updateClause casen splitOn nest env (WithClause loc' lhs wval flags cs)
+    updateClause casen splitOn nest env (WithClause loc' lhs wval prf flags cs)
         = let (_, args) = addEnv 0 env (usedIn lhs)
               args' = mkSplit splitOn lhs args
               lhs' = apply (IVar loc' casen) args' in
-              WithClause loc' (applyNested nest lhs') wval flags cs
+              WithClause loc' (applyNested nest lhs') wval prf flags cs
     updateClause casen splitOn nest env (ImpossibleClause loc' lhs)
         = let (_, args) = addEnv 0 env (usedIn lhs)
               args' = mkSplit splitOn lhs args

src/TTImp/Elab/Quote.idr

@@ -82,9 +82,14 @@ mutual
                      Core ImpClause
   getUnquoteClause (PatClause fc l r)
       = pure $ PatClause fc !(getUnquote l) !(getUnquote r)
-  getUnquoteClause (WithClause fc l w flags cs)
+  getUnquoteClause (WithClause fc l w prf flags cs)
-      = pure $ WithClause fc !(getUnquote l) !(getUnquote w)
+      = pure $ WithClause
-                          flags !(traverse getUnquoteClause cs)
+                 fc
+                 !(getUnquote l)
+                 !(getUnquote w)
+                 prf
+                 flags
+                 !(traverse getUnquoteClause cs)
   getUnquoteClause (ImpossibleClause fc l)
       = pure $ ImpossibleClause fc !(getUnquote l)
 

src/TTImp/Interactive/GenerateDef.idr

@@ -78,7 +78,8 @@ expandClause loc opts n c
     updateRHS : ImpClause -> RawImp -> ImpClause
     updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs
     -- 'with' won't happen, include for completeness
-    updateRHS (WithClause fc lhs wval flags cs) rhs = WithClause fc lhs wval flags cs
+    updateRHS (WithClause fc lhs wval prf flags cs) rhs
+      = WithClause fc lhs wval prf flags cs
     updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs
 
     dropLams : Nat -> RawImp -> RawImp
@@ -141,7 +142,7 @@ generateSplits : {auto m : Ref MD Metadata} ->
                  FC -> SearchOpts -> Int -> ImpClause ->
                  Core (List (Name, List ImpClause))
 generateSplits loc opts fn (ImpossibleClause fc lhs) = pure []
-generateSplits loc opts fn (WithClause fc lhs wval flags cs) = pure []
+generateSplits loc opts fn (WithClause fc lhs wval prf flags cs) = pure []
 generateSplits loc opts fn (PatClause fc lhs rhs)
     = do (lhstm, _) <-
                 elabTerm fn (InLHS linear) [] (MkNested []) []

src/TTImp/Parser.idr

@@ -510,10 +510,11 @@ mutual
            symbol "("
            wval <- expr fname indents
            symbol ")"
+           prf <- optional (keyword "proof" *> name)
            ws <- nonEmptyBlock (clause (S withArgs) fname)
            end <- location
            let fc = MkFC fname start end
-           pure (!(getFn lhs), WithClause fc lhs wval [] (forget $ map snd ws))
+           pure (!(getFn lhs), WithClause fc lhs wval prf [] (forget $ map snd ws))
 
     <|> do keyword "impossible"
            atEnd indents

src/TTImp/ProcessDef.idr

@@ -463,7 +463,8 @@ checkClause {vars} mult vis totreq hashit n opts nest env (PatClause fc lhs_in r
 
          pure (Right (MkClause env' lhstm' rhstm))
 -- TODO: (to decide) With is complicated. Move this into its own module?
-checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs)
+checkClause {vars} mult vis totreq hashit n opts nest env
+    (WithClause fc lhs_in wval_raw mprf flags cs)
     = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-
              checkLHS False mult hashit n opts nest env fc lhs_in
          let wmode
@@ -495,8 +496,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
 
          -- Abstracting over 'wval' in the scope of bNotReq in order
          -- to get the 'magic with' behaviour
-         let wargn = MN "warg" 0
+         (wargs ** (scenv, var, binder)) <- bindWithArgs wvalTy ((,wval) <$> mprf) wvalEnv
-         let scenv = Pi fc top Explicit wvalTy :: wvalEnv
 
          let bnr = bindNotReq fc 0 env' withSub [] reqty
          let notreqns = fst bnr
@@ -505,11 +505,11 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
          rdefs <- if Syntactic `elem` flags
                      then clearDefs defs
                      else pure defs
-         wtyScope <- replace rdefs scenv !(nf rdefs scenv (weaken wval))
+         wtyScope <- replace rdefs scenv !(nf rdefs scenv (weakenNs (mkSizeOf wargs) wval))
-                            (Local fc (Just False) _ First)
+                            var
                             !(nf rdefs scenv
-                                 (weaken {n=wargn} notreqty))
+                                 (weakenNs (mkSizeOf wargs) notreqty))
-         let bNotReq = Bind fc wargn (Pi fc top Explicit wvalTy) wtyScope
+         let bNotReq = binder wtyScope
 
          let Just (reqns, envns, wtype) = bindReq fc env' withSub [] bNotReq
              | Nothing => throw (InternalError "Impossible happened: With abstraction failure #4")
@@ -528,9 +528,20 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
          widx <- addDef wname (record {flags $= (SetTotal totreq ::)}
                                     (newDef fc wname (if isErased mult then erased else top)
                                       vars wtype vis None))
-         let rhs_in = apply (IVar fc wname)
+
-                        (map (IVar fc) envns ++
+         let toWarg : Maybe (PiInfo RawImp, Name) -> List (Maybe Name, RawImp)
-                         map (maybe wval_raw (\pn => IVar fc (snd pn))) wargNames)
+               := flip maybe (\pn => [(Nothing, IVar fc (snd pn))]) $
+                    (Nothing, wval_raw) ::
+                    case mprf of
+                      Nothing => []
+                      Just _  =>
+                       let fc = emptyFC in
+                       let refl = IVar fc (NS builtinNS (UN "Refl")) in
+                       [(mprf, INamedApp fc refl (UN "x") wval_raw)]
+
+         let rhs_in = gapply (IVar fc wname)
+                    $ map (\ nm => (Nothing, IVar fc nm)) envns
+                   ++ concatMap toWarg wargNames
 
          log "declare.def.clause" 3 $ "Applying to with argument " ++ show rhs_in
          rhs <- wrapErrorC opts (InRHS fc !(getFullName (Resolved n))) $
@@ -550,6 +561,67 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
 
          pure (Right (MkClause env' lhspat rhs))
   where
+    bindWithArgs :
+       (wvalTy : Term xs) -> Maybe (Name, Term xs) ->
+       (wvalEnv : Env Term xs) ->
+       Core (ext : List Name
+         ** ( Env Term (ext ++ xs)
+            , Term (ext ++ xs)
+            , (Term (ext ++ xs) -> Term xs)
+            ))
+    bindWithArgs {xs} wvalTy Nothing wvalEnv =
+      let wargn : Name
+          wargn = MN "warg" 0
+          wargs : List Name
+          wargs = [wargn]
+
+          scenv : Env Term (wargs ++ xs)
+                := Pi fc top Explicit wvalTy :: wvalEnv
+
+          var : Term (wargs ++ xs)
+              := Local fc (Just False) Z First
+
+          binder : Term (wargs ++ xs) -> Term xs
+                 := Bind fc wargn (Pi fc top Explicit wvalTy)
+
+      in pure (wargs ** (scenv, var, binder))
+
+    bindWithArgs {xs} wvalTy (Just (name, wval)) wvalEnv = do
+      defs <- get Ctxt
+
+      let eqName = NS builtinNS (UN "Equal")
+      Just (TCon t ar _ _ _ _ _ _) <- lookupDefExact eqName (gamma defs)
+        | _ => throw (InternalError "Cannot find builtin Equal")
+      let eqTyCon = Ref fc (TyCon t ar) eqName
+
+      let wargn : Name
+          wargn = MN "warg" 0
+          wargs : List Name
+          wargs = [name, wargn]
+
+          wvalTy' := weaken wvalTy
+          eqTy : Term (MN "warg" 0 :: xs)
+               := apply fc eqTyCon
+                           [ wvalTy'
+                           , wvalTy'
+                           , weaken wval
+                           , Local fc (Just False) Z First
+                           ]
+
+          scenv : Env Term (wargs ++ xs)
+                := Pi fc top Implicit eqTy
+                :: Pi fc top Explicit wvalTy
+                :: wvalEnv
+
+          var : Term (wargs ++ xs)
+              := Local fc (Just False) (S Z) (Later First)
+
+          binder : Term (wargs ++ xs) -> Term xs
+                 := \ t => Bind fc wargn (Pi fc top Explicit wvalTy)
+                         $ Bind fc name  (Pi fc top Implicit eqTy) t
+
+      pure (wargs ** (scenv, var, binder))
+
     -- If it's 'KeepCons/SubRefl' in 'outprf', that means it was in the outer
     -- environment so we need to keep it in the same place in the 'with'
     -- function. Hence, turn it to KeepCons whatever
@@ -572,9 +644,10 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
               (_ ** KeepCons rest)
 
     -- Rewrite the clauses in the block to use an updated LHS.
-    -- 'drop' is the number of additional with arguments we expect (i.e.
+    -- 'drop' is the number of additional with arguments we expect
-    -- the things to drop from the end before matching LHSs)
+    -- (i.e. the things to drop from the end before matching LHSs)
-    mkClauseWith : (drop : Nat) -> Name -> List (Maybe (PiInfo RawImp, Name)) ->
+    mkClauseWith : (drop : Nat) -> Name ->
+                   List (Maybe (PiInfo RawImp, Name)) ->
                    RawImp -> ImpClause ->
                    Core ImpClause
     mkClauseWith drop wname wargnames lhs (PatClause ploc patlhs rhs)
@@ -582,12 +655,12 @@ checkClause {vars} mult vis totreq hashit n opts nest env (WithClause fc lhs_in
              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)
+    mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs prf flags ws)
         = 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')
+             pure (WithClause ploc newlhs newrhs prf flags ws')
     mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs)
         = do log "declare.def.clause.with" 20 "ImpossibleClause"
              newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs

src/TTImp/Reflect.idr

@@ -378,12 +378,13 @@ mutual
                           y' <- reify defs !(evalClosure defs y)
                           z' <- reify defs !(evalClosure defs z)
                           pure (PatClause x' y' z')
-               (NS _ (UN "WithClause"), [w,x,y,z])
+               (NS _ (UN "WithClause"), [v,w,x,y,z])
-                    => do w' <- reify defs !(evalClosure defs w)
+                    => do v' <- reify defs !(evalClosure defs v)
+                          w' <- reify defs !(evalClosure defs w)
                           x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
                           z' <- reify defs !(evalClosure defs z)
-                          pure (WithClause w' x' y' [] z')
+                          pure (WithClause v' w' x' y' [] z')
                (NS _ (UN "ImpossibleClause"), [x,y])
                     => do x' <- reify defs !(evalClosure defs x)
                           y' <- reify defs !(evalClosure defs y)
@@ -705,12 +706,13 @@ mutual
              y' <- reflect fc defs lhs env y
              z' <- reflect fc defs lhs env z
              appCon fc defs (reflectionttimp "PatClause") [x', y', z']
-    reflect fc defs lhs env (WithClause v w x y z)
+    reflect fc defs lhs env (WithClause u v w x y z)
-        = do v' <- reflect fc defs lhs env v
+        = do u' <- reflect fc defs lhs env u
+             v' <- reflect fc defs lhs env v
              w' <- reflect fc defs lhs env w
              x' <- reflect fc defs lhs env x
              z' <- reflect fc defs lhs env z
-             appCon fc defs (reflectionttimp "WithClause") [v', w', x', z']
+             appCon fc defs (reflectionttimp "WithClause") [u', v', w', x', z']
     reflect fc defs lhs env (ImpossibleClause x y)
         = do x' <- reflect fc defs lhs env x
              y' <- reflect fc defs lhs env y

src/TTImp/TTImp.idr

@@ -317,7 +317,8 @@ mutual
   public export
   data ImpClause : Type where
        PatClause : FC -> (lhs : RawImp) -> (rhs : RawImp) -> ImpClause
-       WithClause : FC -> (lhs : RawImp) -> (wval : RawImp) ->
+       WithClause : FC -> (lhs : RawImp) ->
+                    (wval : RawImp) -> (prf : Maybe Name) ->
                     (flags : List WithFlag) ->
                     List ImpClause -> ImpClause
        ImpossibleClause : FC -> (lhs : RawImp) -> ImpClause
@@ -326,8 +327,11 @@ mutual
   Show ImpClause where
     show (PatClause fc lhs rhs)
        = show lhs ++ " = " ++ show rhs
-    show (WithClause fc lhs wval flags block)
+    show (WithClause fc lhs wval prf flags block)
-       = show lhs ++ " with " ++ show wval ++ "\n\t" ++ show block
+       = show lhs
+       ++ " with " ++ show wval
+       ++ maybe "" (\ nm => " proof " ++ show nm) prf
+       ++ "\n\t" ++ show block
     show (ImpossibleClause fc lhs)
        = show lhs ++ " impossible"
 
@@ -714,6 +718,16 @@ apply : RawImp -> List RawImp -> RawImp
 apply f [] = f
 apply f (x :: xs) = apply (IApp (getFC f) f x) xs
 
+export
+gapply : RawImp -> List (Maybe Name, RawImp) -> RawImp
+gapply f [] = f
+gapply f (x :: xs) = gapply (uncurry (app f) x) xs where
+
+  app : RawImp -> Maybe Name -> RawImp -> RawImp
+  app f Nothing x =  IApp (getFC f) f x
+  app f (Just nm) x = INamedApp (getFC f) f nm x
+
+
 export
 getFn : RawImp -> RawImp
 getFn (IApp _ f _) = getFn f
@@ -958,8 +972,13 @@ mutual
         = do tag 0; toBuf b fc; toBuf b lhs; toBuf b rhs
     toBuf b (ImpossibleClause fc lhs)
         = do tag 1; toBuf b fc; toBuf b lhs
-    toBuf b (WithClause fc lhs wval flags cs)
+    toBuf b (WithClause fc lhs wval prf flags cs)
-        = do tag 2; toBuf b fc; toBuf b lhs; toBuf b wval; toBuf b cs
+        = do tag 2
+             toBuf b fc
+             toBuf b lhs
+             toBuf b wval
+             toBuf b prf
+             toBuf b cs
 
     fromBuf b
         = case !getTag of
@@ -969,8 +988,9 @@ mutual
                1 => do fc <- fromBuf b; lhs <- fromBuf b;
                        pure (ImpossibleClause fc lhs)
                2 => do fc <- fromBuf b; lhs <- fromBuf b;
-                       wval <- fromBuf b; cs <- fromBuf b
+                       wval <- fromBuf b; prf <- fromBuf b;
-                       pure (WithClause fc lhs wval [] cs)
+                       cs <- fromBuf b
+                       pure (WithClause fc lhs wval prf [] cs)
                _ => corrupt "ImpClause"
 
   export

src/TTImp/Utils.idr

@@ -206,12 +206,12 @@ mutual
                      ++ bound in
             PatClause fc (substNames' bvar [] [] lhs)
                          (substNames' bvar bound' ps rhs)
-  substNamesClause' bvar bound ps (WithClause fc lhs wval flags cs)
+  substNamesClause' bvar bound ps (WithClause fc lhs wval prf flags cs)
       = let bound' = map UN (map snd (findBindableNames True bound [] lhs))
                      ++ findIBindVars lhs
                      ++ bound in
             WithClause fc (substNames' bvar [] [] lhs)
-                          (substNames' bvar bound' ps wval) flags cs
+                          (substNames' bvar bound' ps wval) prf flags cs
   substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
       = ImpossibleClause fc (substNames' bvar bound [] lhs)
 
@@ -304,9 +304,10 @@ mutual
   substLocClause fc' (PatClause fc lhs rhs)
       = PatClause fc' (substLoc fc' lhs)
                       (substLoc fc' rhs)
-  substLocClause fc' (WithClause fc lhs wval flags cs)
+  substLocClause fc' (WithClause fc lhs wval prf flags cs)
       = WithClause fc' (substLoc fc' lhs)
                        (substLoc fc' wval)
+                       prf
                        flags
                        (map (substLocClause fc') cs)
   substLocClause fc' (ImpossibleClause fc lhs)

tests/Main.idr

@@ -162,7 +162,7 @@ idrisTests = MkTestPool []
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
        -- The 'with' rule
-       "with001", "with002", "with004",
+       "with001", "with002", "with004", "with005",
        -- with-disambiguation
        "with003"]
 

tests/idris2/perror004/expected

@@ -1,5 +1,5 @@
 1/1: Building PError (PError.idr)
-Error: Wrong number of 'with' arguments.
+Error: Wrong number of 'with' arguments: expected 2 but got 3.
 
 PError.idr:4:33--4:34
  1 | foo : Nat -> Nat -> Bool

tests/idris2/with005/Issue893.idr

@@ -0,0 +1,25 @@
+module Issue893
+
+%default total
+
+foo : (a, b : Nat) -> Bool
+foo  Z    b = False
+foo (S _) b = False
+
+notFoo : (a, b : Nat) -> Not (foo a b = True)
+notFoo  Z    _ = uninhabited
+notFoo (S _) _ = uninhabited
+
+bar : (a, b : Nat) -> (foo a b) && c = foo a b
+bar a b with (foo a b) proof ab
+  bar a b | True  = absurd $ notFoo a b ab
+  bar a b | False = Refl
+
+goo : (a, b : Nat) -> Bool -> Bool
+goo a b True = True
+goo a b False = foo a b || foo a b
+
+bar2 : (a, b : Nat) -> goo a b (foo a b) = foo a b
+bar2 a b with (foo a b) proof ab
+  bar2 a b | True = Refl
+  bar2 a b | False = rewrite ab in Refl

tests/idris2/with005/WithProof.idr

@@ -0,0 +1,26 @@
+module WithProof
+
+%default total
+
+filter : (p : a -> Bool) -> (xs : List a) -> List a
+filter p [] = []
+filter p (x :: xs) with (p x)
+  filter p (x :: xs) | False = filter p xs
+  filter p (x :: xs) | True = x :: filter p xs
+
+
+filterSquared : (p : a -> Bool) -> (xs : List a) ->
+                filter p (filter p xs) === filter p xs
+filterSquared p [] = Refl
+{-
+filterSquared p (x :: xs) with (p x)
+  filterSquared p (x :: xs) | False = filterSquared p xs -- easy
+  filterSquared p (x :: xs) | True = ?a
+     -- argh! stuck on another with-block casing on (p x)!
+     -- we could check (p x) again but how do we prove it
+     -- can only ever be `True`?!
+-}
+filterSquared p (x :: xs) with (p x) proof eq
+  filterSquared p (x :: xs) | False = filterSquared p xs -- easy
+  filterSquared p (x :: xs) | True
+    = rewrite eq in cong (x ::) (filterSquared p xs)

tests/idris2/with005/expected

@@ -0,0 +1,2 @@
+1/1: Building WithProof (WithProof.idr)
+1/1: Building Issue893 (Issue893.idr)

tests/idris2/with005/run

@@ -0,0 +1,4 @@
+$1 --no-color --console-width 0 --no-banner --check WithProof.idr
+$1 --no-color --console-width 0 --no-banner --check Issue893.idr
+
+rm -rf build