Experiment %syntactic flag on with

This means it abstracts over the value syntactically, rather than by
value, and can significantly speed up elaboration where large types are
involved, at a cost of being less general. Try it if "with" is slow.

There are more flags we want on with (well, at least one: "proof")

libs/base/Data/IORef.idr

@@ -18,10 +18,12 @@ newIORef val
     = do m <- primIO (prim__newIORef val)
          pure (MkRef m)
 
+%inline
 export
 readIORef : IORef a -> IO a
 readIORef (MkRef m) = primIO (prim__readIORef m)
 
+%inline
 export
 writeIORef : IORef a -> (1 val : a) -> IO ()
 writeIORef (MkRef m) val = primIO (prim__writeIORef m val)

libs/prelude/Prelude.idr

@@ -373,6 +373,7 @@ interface Num ty => Integral ty where
 
 -- Integer
 
+%inline
 public export
 Num Integer where
   (+) = prim__add_Integer
@@ -408,6 +409,7 @@ defaultInteger = %search
 
 -- Int
 
+%inline
 public export
 Num Int where
   (+) = prim__add_Int
@@ -914,11 +916,13 @@ public export
   Right x == Right x' = x == x'
   _ == _ = False
 
+%inline
 public export
 Functor (Either e) where
   map f (Left x) = Left x
   map f (Right x) = Right (f x)
 
+%inline
 public export
 Applicative (Either e) where
     pure = Right

src/Idris/Desugar.idr

@@ -499,11 +499,11 @@ mutual
                      (case ws of
                            [] => rhs'
                            _ => ILocal fc (concat ws) rhs')
-  desugarClause ps arg (MkWithClause fc lhs wval cs)
+  desugarClause ps arg (MkWithClause fc lhs wval flags cs)
       = do cs' <- traverse (desugarClause ps arg) cs
            (bound, blhs) <- bindNames arg !(desugar LHS ps lhs)
            wval' <- desugar AnyExpr (bound ++ ps) wval
-           pure $ WithClause fc blhs wval' cs'
+           pure $ WithClause fc blhs wval' flags cs'
   desugarClause ps arg (MkImpossible fc lhs)
       = do dlhs <- desugar LHS ps lhs
            pure $ ImpossibleClause fc (snd !(bindNames arg dlhs))
@@ -624,8 +624,8 @@ mutual
       toIDef : ImpClause -> Core ImpDecl
       toIDef (PatClause fc lhs rhs)
           = pure $ IDef fc !(getFn lhs) [PatClause fc lhs rhs]
-      toIDef (WithClause fc lhs rhs cs)
+      toIDef (WithClause fc lhs rhs flags cs)
-          = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs cs]
+          = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs flags cs]
       toIDef (ImpossibleClause fc lhs)
           = pure $ IDef fc !(getFn lhs) [ImpossibleClause fc lhs]
 

src/Idris/Elab/Implementation.idr

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

src/Idris/Elab/Interface.idr

@@ -395,9 +395,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 cs)
+        changeName dn (WithClause fc lhs wval flags cs)
             = WithClause fc (changeNameTerm dn lhs) wval
-                         (map (changeName dn) cs)
+                         flags (map (changeName dn) cs)
         changeName dn (ImpossibleClause fc lhs)
             = ImpossibleClause fc (changeNameTerm dn lhs)
 

src/Idris/Parser.idr

@@ -858,6 +858,13 @@ tyDecl fname indents
                atEnd indents
                pure (MkPTy (MkFC fname start end) n ty)
 
+withFlags : SourceEmptyRule (List WithFlag)
+withFlags
+    = do pragma "syntactic"
+         fs <- withFlags
+         pure $ Syntactic :: fs
+  <|> pure []
+
 mutual
   parseRHS : (withArgs : Nat) ->
              FileName -> FilePos -> Int ->
@@ -872,11 +879,12 @@ mutual
                  pure (MkPatClause (MkFC fname start end) lhs rhs ws)
      <|> do keyword "with"
             wstart <- location
+            flags <- withFlags
             symbol "("
             wval <- bracketedExpr fname wstart indents
             ws <- nonEmptyBlock (clause (S withArgs) fname)
             end <- location
-            pure (MkWithClause (MkFC fname start end) lhs wval ws)
+            pure (MkWithClause (MkFC fname start end) lhs wval flags ws)
      <|> do keyword "impossible"
             atEnd indents
             end <- location

src/Idris/REPL.idr

@@ -188,7 +188,7 @@ 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 csraw)
+printClause l i (WithClause _ lhsraw wvraw flags csraw)
     = do lhs <- pterm lhsraw
          wval <- pterm wvraw
          cs <- traverse (printClause l (i + 2)) csraw

src/Idris/Resugar.idr

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

src/Idris/Syntax.idr

@@ -145,7 +145,7 @@ mutual
        MkPatClause : FC -> (lhs : PTerm) -> (rhs : PTerm) ->
                      (whereblock : List PDecl) -> PClause
        MkWithClause : FC -> (lhs : PTerm) -> (wval : PTerm) ->
-                        List PClause -> PClause
+                      List WithFlag -> List PClause -> PClause
        MkImpossible : FC -> (lhs : PTerm) -> PClause
 
   public export
@@ -350,7 +350,7 @@ showCount = elimSemi
 mutual
   showAlt : PClause -> String
   showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
-  showAlt (MkWithClause _ lhs wval cs) = " | <<with alts not possible>>;"
+  showAlt (MkWithClause _ lhs wval flags cs) = " | <<with alts not possible>>;"
   showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;"
 
   showDo : PDo -> String
@@ -403,7 +403,7 @@ mutual
       where
         showAlt : PClause -> String
         showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";"
-        showAlt (MkWithClause _ lhs rhs _) = " | <<with alts not possible>>"
+        showAlt (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
         showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;"
     showPrec _ (PCase _ tm cs)
         = "case " ++ show tm ++ " of { " ++
@@ -411,7 +411,7 @@ mutual
       where
         showCase : PClause -> String
         showCase (MkPatClause _ lhs rhs _) = show lhs ++ " => " ++ show rhs
-        showCase (MkWithClause _ lhs rhs _) = " | <<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
@@ -810,9 +810,10 @@ mapPTermM f = goPTerm where
       MkPatClause fc <$> goPTerm lhs
                      <*> goPTerm rhs
                      <*> goPDecls wh
-    goPClause (MkWithClause fc lhs wVal cls) =
+    goPClause (MkWithClause fc lhs wVal flags cls) =
       MkWithClause fc <$> goPTerm lhs
                       <*> goPTerm wVal
+                      <*> pure flags
                       <*> goPClauses cls
     goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs
 

src/TTImp/Elab/Case.idr

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

src/TTImp/Interactive/GenerateDef.idr

@@ -82,7 +82,7 @@ expandClause loc 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 cs) rhs = WithClause fc lhs wval cs
+    updateRHS (WithClause fc lhs wval flags cs) rhs = WithClause fc lhs wval flags cs
     updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs
 
     dropLams : {vars : _} ->
@@ -143,7 +143,7 @@ generateSplits : {auto m : Ref MD Metadata} ->
                  FC -> Int -> ImpClause ->
                  Core (List (Name, List ImpClause))
 generateSplits loc fn (ImpossibleClause fc lhs) = pure []
-generateSplits loc fn (WithClause fc lhs wval cs) = pure []
+generateSplits loc fn (WithClause fc lhs wval flags cs) = pure []
 generateSplits {c} {m} {u} loc fn (PatClause fc lhs rhs)
     = do (lhstm, _) <-
                 elabTerm fn (InLHS linear) [] (MkNested []) []

src/TTImp/Parser.idr

@@ -502,7 +502,7 @@ mutual
            ws <- nonEmptyBlock (clause (S withArgs) fname)
            end <- location
            let fc = MkFC fname start end
-           pure (!(getFn lhs), WithClause fc lhs wval (map snd ws))
+           pure (!(getFn lhs), WithClause fc lhs wval [] (map snd ws))
 
     <|> do keyword "impossible"
            atEnd indents

src/TTImp/ProcessDef.idr

@@ -78,14 +78,10 @@ export
 impossibleErrOK : {auto c : Ref Ctxt Defs} ->
                   Defs -> Error -> Core Bool
 impossibleErrOK defs (CantConvert fc env l r)
-    = do logTerm 10 "Impossible" !(normalise defs env l)
+    = impossibleOK defs !(nf defs env l)
-         logTerm 10 "    ...and" !(normalise defs env r)
-         impossibleOK defs !(nf defs env l)
                         !(nf defs env r)
 impossibleErrOK defs (CantSolveEq fc env l r)
-    = do logTerm 10 "Impossible" !(normalise defs env l)
+    = impossibleOK defs !(nf defs env l)
-         logTerm 10 "    ...and" !(normalise defs env r)
-         impossibleOK defs !(nf defs env l)
                         !(nf defs env r)
 impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True
 impossibleErrOK defs (CyclicMeta _ _ _ _) = pure True
@@ -122,14 +118,10 @@ export
 recoverableErr : {auto c : Ref Ctxt Defs} ->
                  Defs -> Error -> Core Bool
 recoverableErr defs (CantConvert fc env l r)
-    = do logTerm 10 "Impossible" !(normalise defs env l)
+    = recoverable defs !(nf defs env l)
-         logTerm 10 "    ...and" !(normalise defs env r)
-         recoverable defs !(nf defs env l)
                        !(nf defs env r)
 recoverableErr defs (CantSolveEq fc env l r)
-    = do logTerm 10 "Impossible" !(normalise defs env l)
+    = recoverable defs !(nf defs env l)
-         logTerm 10 "    ...and" !(normalise defs env r)
-         recoverable defs !(nf defs env l)
                        !(nf defs env r)
 recoverableErr defs (BadDotPattern _ _ ErasedArg _ _) = pure True
 recoverableErr defs (CyclicMeta _ _ _ _) = pure True
@@ -453,7 +445,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs)
 
          pure (Right (MkClause env' lhstm' rhstm))
 -- TODO: (to decide) With is complicated. Move this into its own module?
-checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs)
+checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs)
     = do (lhs, (vars'  ** (sub', env', nest', lhspat, reqty))) <-
              checkLHS False mult hashit n opts nest env fc lhs_in
          let wmode
@@ -492,9 +484,12 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
          let notreqns = fst bnr
          let notreqty = snd bnr
 
-         wtyScope <- replace defs scenv !(nf defs scenv (weaken wval))
+         rdefs <- if Syntactic `elem` flags
+                     then clearDefs defs
+                     else pure defs
+         wtyScope <- replace rdefs scenv !(nf rdefs scenv (weaken wval))
                             (Local fc (Just False) _ First)
-                            !(nf defs scenv
+                            !(nf rdefs scenv
                                  (weaken {n=wargn} notreqty))
          let bNotReq = Bind fc wargn (Pi top Explicit wvalTy) wtyScope
 
@@ -567,11 +562,11 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs
         = do 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 ws)
+    mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs flags ws)
         = do 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 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
              pure (ImpossibleClause ploc newlhs)

src/TTImp/TTImp.idr

@@ -292,10 +292,19 @@ mutual
           " " ++ show con ++ "\n\t" ++
           showSep "\n\t" (map show fields) ++ "\n"
 
+  public export
+  data WithFlag
+         = Syntactic -- abstract syntactically, rather than by value
+
+  export
+  Eq WithFlag where
+      Syntactic == Syntactic = True
+
   public export
   data ImpClause : Type where
        PatClause : FC -> (lhs : RawImp) -> (rhs : RawImp) -> ImpClause
        WithClause : FC -> (lhs : RawImp) -> (wval : RawImp) ->
+                    (flags : List WithFlag) ->
                     List ImpClause -> ImpClause
        ImpossibleClause : FC -> (lhs : RawImp) -> ImpClause
 
@@ -303,7 +312,7 @@ mutual
   Show ImpClause where
     show (PatClause fc lhs rhs)
        = show lhs ++ " = " ++ show rhs
-    show (WithClause fc lhs wval block)
+    show (WithClause fc lhs wval flags block)
        = show lhs ++ " with " ++ show wval ++ "\n\t" ++ show block
     show (ImpossibleClause fc lhs)
        = show lhs ++ " impossible"
@@ -835,7 +844,7 @@ 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 cs)
+    toBuf b (WithClause fc lhs wval flags cs)
         = do tag 2; toBuf b fc; toBuf b lhs; toBuf b wval; toBuf b cs
 
     fromBuf b
@@ -847,7 +856,7 @@ mutual
                        pure (ImpossibleClause fc lhs)
                2 => do fc <- fromBuf b; lhs <- fromBuf b;
                        wval <- fromBuf b; cs <- fromBuf b
-                       pure (WithClause fc lhs wval cs)
+                       pure (WithClause fc lhs wval [] cs)
                _ => corrupt "ImpClause"
 
   export

src/TTImp/Utils.idr

@@ -150,11 +150,11 @@ mutual
                         ++ bound in
             PatClause fc (substNames [] [] lhs)
                          (substNames bound' ps rhs)
-  substNamesClause bound ps (WithClause fc lhs wval cs)
+  substNamesClause bound ps (WithClause fc lhs wval flags cs)
       = let bound' = map UN (map snd (findBindableNames True bound [] lhs))
                         ++ bound in
             WithClause fc (substNames [] [] lhs)
-                          (substNames bound' ps wval) cs
+                          (substNames bound' ps wval) flags cs
   substNamesClause bound ps (ImpossibleClause fc lhs)
       = ImpossibleClause fc (substNames bound [] lhs)
 
@@ -230,9 +230,10 @@ mutual
   substLocClause fc' (PatClause fc lhs rhs)
       = PatClause fc' (substLoc fc' lhs)
                       (substLoc fc' rhs)
-  substLocClause fc' (WithClause fc lhs wval cs)
+  substLocClause fc' (WithClause fc lhs wval flags cs)
       = WithClause fc' (substLoc fc' lhs)
                        (substLoc fc' wval)
+                       flags
                        (map (substLocClause fc') cs)
   substLocClause fc' (ImpossibleClause fc lhs)
       = ImpossibleClause fc' (substLoc fc' lhs)

tests/ideMode/ideMode001/expected

@@ -8,7 +8,7 @@
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:759:1--766:1 n[2] m[4]) a[3])))")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -8,7 +8,7 @@
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:759:1--766:1 n[2] m[4]) a[3])))")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)