From 43647934840223164655ae795be262c9aa4a7738 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Fri, 4 Dec 2020 04:45:27 +0300
Subject: [PATCH 01/28] Type definition from `Decidable.Equality` was moved to
 a separate module

This is done to make able for `Data.*` modules of datatypes declared in
prelude to import modules that have their own definitions of `DecEq`
inside them (i.e. modules of datatypes declared in the `base`).
---
 libs/base/Decidable/Equality.idr      | 28 ++------------------------
 libs/base/Decidable/Equality/Core.idr | 29 +++++++++++++++++++++++++++
 libs/base/base.ipkg                   |  1 +
 3 files changed, 32 insertions(+), 26 deletions(-)
 create mode 100644 libs/base/Decidable/Equality/Core.idr

diff --git a/libs/base/Decidable/Equality.idr b/libs/base/Decidable/Equality.idr
index 11c68ea89..1a021538d 100644
--- a/libs/base/Decidable/Equality.idr
+++ b/libs/base/Decidable/Equality.idr
@@ -6,34 +6,10 @@ import Data.Nat
 import Data.List
 import Data.List1
 
+import public Decidable.Equality.Core as Decidable.Equality
+
 %default total
 
---------------------------------------------------------------------------------
--- Decidable equality
---------------------------------------------------------------------------------
-
-||| Decision procedures for propositional equality
-public export
-interface DecEq t where
-  ||| Decide whether two elements of `t` are propositionally equal
-  decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
-
---------------------------------------------------------------------------------
--- Utility lemmas
---------------------------------------------------------------------------------
-
-||| The negation of equality is symmetric (follows from symmetry of equality)
-export
-negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
-negEqSym p h = p (sym h)
-
-||| Everything is decidably equal to itself
-export
-decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
-decEqSelfIsYes {x} with (decEq x x)
-  decEqSelfIsYes {x} | Yes Refl = Refl
-  decEqSelfIsYes {x} | No contra = absurd $ contra Refl
-
 --------------------------------------------------------------------------------
 --- Unit
 --------------------------------------------------------------------------------
diff --git a/libs/base/Decidable/Equality/Core.idr b/libs/base/Decidable/Equality/Core.idr
new file mode 100644
index 000000000..7bf75ef76
--- /dev/null
+++ b/libs/base/Decidable/Equality/Core.idr
@@ -0,0 +1,29 @@
+module Decidable.Equality.Core
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Decidable equality
+--------------------------------------------------------------------------------
+
+||| Decision procedures for propositional equality
+public export
+interface DecEq t where
+  ||| Decide whether two elements of `t` are propositionally equal
+  decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
+
+--------------------------------------------------------------------------------
+-- Utility lemmas
+--------------------------------------------------------------------------------
+
+||| The negation of equality is symmetric (follows from symmetry of equality)
+export
+negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
+negEqSym p h = p (sym h)
+
+||| Everything is decidably equal to itself
+export
+decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
+decEqSelfIsYes {x} with (decEq x x)
+  decEqSelfIsYes {x} | Yes Refl = Refl
+  decEqSelfIsYes {x} | No contra = absurd $ contra Refl
diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg
index 259d2ab3e..fb586e67b 100644
--- a/libs/base/base.ipkg
+++ b/libs/base/base.ipkg
@@ -49,6 +49,7 @@ modules = Control.App,
 
           Decidable.Decidable,
           Decidable.Equality,
+          Decidable.Equality.Core,
           Decidable.Order,
 
           Language.Reflection,

From 13cc27da1f57dac1c08025b084990d7f089a9cd1 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Fri, 4 Dec 2020 04:49:26 +0300
Subject: [PATCH 02/28] An alternative (Fin-based) indexing function was added
 for lists.

---
 libs/base/Data/Fin.idr  | 2 +-
 libs/base/Data/List.idr | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index 51e2bcf13..c58069d4d 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -2,7 +2,7 @@ module Data.Fin
 
 import public Data.Maybe
 import Data.Nat
-import Decidable.Equality
+import Decidable.Equality.Core
 
 %default total
 
diff --git a/libs/base/Data/List.idr b/libs/base/Data/List.idr
index e5cbb1491..e8efc95c8 100644
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@@ -2,6 +2,7 @@ module Data.List
 
 import Data.Nat
 import Data.List1
+import Data.Fin
 
 public export
 isNil : List a -> Bool
@@ -62,6 +63,11 @@ index : (n : Nat) -> (xs : List a) -> {auto 0 ok : InBounds n xs} -> a
 index Z (x :: xs) {ok = InFirst} = x
 index (S k) (_ :: xs) {ok = InLater _} = index k xs
 
+public export
+index' : (xs : List a) -> Fin (length xs) -> a
+index' (x::_)  FZ     = x
+index' (_::xs) (FS i) = index' xs i
+
 ||| Generate a list by repeatedly applying a partial function until exhausted.
 ||| @ f the function to iterate
 ||| @ x the initial value that will be the head of the list

From 9e22a6e07b0849828e89a93f7c1a26c22618afeb Mon Sep 17 00:00:00 2001
From: Andy Lok <andylokandy@hotmail.com>
Date: Sun, 6 Dec 2020 17:54:58 +0800
Subject: [PATCH 03/28] Add javascript FFI for `fastUnpack` (#816)

---
 libs/base/Data/Strings.idr | 1 +
 1 file changed, 1 insertion(+)

diff --git a/libs/base/Data/Strings.idr b/libs/base/Data/Strings.idr
index 8c66181f5..4296ccb0c 100644
--- a/libs/base/Data/Strings.idr
+++ b/libs/base/Data/Strings.idr
@@ -20,6 +20,7 @@ foldl1 f (x::xs) = foldl f x xs
 -- If you need to unpack strings at compile time, use Prelude.unpack.
 %foreign
   "scheme:string-unpack"
+  "javascript:lambda:(str)=>__prim_js2idris_array(Array.from(str))"
 export
 fastUnpack : String -> List Char
 

From aeab632c7e483fcd67db604984a337455de39c57 Mon Sep 17 00:00:00 2001
From: Andor Penzes <andor.penzes@gmail.com>
Date: Sun, 6 Dec 2020 18:23:54 +0100
Subject: [PATCH 04/28] [doc] JS FFI examples.

---
 docs/source/backends/javascript.rst | 149 +++++++++++++++++++++++++++-
 1 file changed, 147 insertions(+), 2 deletions(-)

diff --git a/docs/source/backends/javascript.rst b/docs/source/backends/javascript.rst
index f6e0b9a83..6c333df9e 100644
--- a/docs/source/backends/javascript.rst
+++ b/docs/source/backends/javascript.rst
@@ -44,8 +44,8 @@ For completion below an example of a foreign available only with ``browser`` cod
     prim__setBodyInnerHTML : String -> PrimIO ()
 
 
-Full Example
-------------
+Short Example
+-------------
 
 An interesting example is creating a foreign for the setTimeout function:
 
@@ -59,3 +59,148 @@ An interesting example is creating a foreign for the setTimeout function:
 
 An important note here is that the codegen is using ``BigInt`` to represent
 idris ``Int``, that's why we need to apply ``Number`` to the ``delay``.
+
+Browser Example
+===============
+
+To build JavaScript aimed to use in the browser, the code must be compiled with
+the javascript codegen option. The compiler produces a JavaScript or an HTML file.
+The browser needs an HTML file to load. This HTML file can be created in two ways
+
+- If the ``.html`` suffix is given to the output file the compiler generates an HTML file
+  which includes a wrapping around the generated JavaScript.
+- If *no* ``.html`` suffix is given, the generated file only contains the JavaScript code.
+  In this case manual wrapping is needed.
+
+Example of the wrapper HTML:
+
+.. code-block:: html
+
+    <html>
+     <head><meta charset='utf-8'></head>
+     <body>
+      <script type='text/javascript'>
+      JS code goes here
+      </script>
+     </body>
+    </html>
+
+As our intention is to develop something that runs in the browser questions naturally arise:
+
+- How to interact with HTML elements?
+- More importantly, when does the generated Idris code start?
+
+Starting point of the Idris generated code
+------------------------------------------
+
+The generated JavaScript for your program contains an entry point. The ``main`` function is compiled
+to a JavaScript top-level expression, which will be evaluated during the loading of the ``script``
+tag and that is the entry point for Idris generated program starting in the browser.
+
+Interaction with HTML elements
+------------------------------
+
+As sketched in the Short Example section, the FFI must be used when interaction happens between Idris
+generated code and the rest of the Browser/JS ecosystem. Information handled by the FFI is
+separated into two categories. Primitive types in Idris FFI, such as Int, and everything else.
+The everything else part is accessed via AnyPtr. The ``%foreign`` construction should be used
+to give implementation on the JavaScript side. And an Idris function declaration  to give ``Type``
+declaration on the Idris side. The syntax is ``%foreign "browser:lambda:js-lambda-expression"`` .
+On the Idris side, primitive types and ``PrimIO t`` types should be used as parameters,
+when defining ``%foreign``. This declaration is a helper function which needs to be called
+behind the ``primIO`` function. More on this can be found in the FFI chapter.
+
+Examples for JavaScript FFI
+---------------------------
+
+console.log
+-----------
+
+.. code-block:: idris
+
+    %foreign "browser:lambda: x => console.log(x)"
+    prim__consoleLog : String -> PrimIO ()
+
+    consoleLog : HasIO io => String -> io ()
+    consoleLog x = primIO $ prim__consoleLog x
+
+String is a primitive type in Idris and it is represented as a JavaScript String. There is no need
+for any conversion between the Idris and the JavaScript.
+
+setInterval
+-----------
+
+.. code-block:: idris
+
+    %foreign "browser:lambda: (a,i)=>setInterval(a,Number(i))"
+    prim__setInterval : PrimIO () -> Int -> PrimIO ()
+
+    setInterval : (HasIO io) => IO () -> Int -> io ()
+    setInterval a i = primIO $ prim__setInterval (toPrim a) i
+
+The ``setInterval`` JavaScript function executes the given function in every ``x`` millisecond.
+We can use Idris generated functions in the callback as far as they have the type ``IO ()`` .
+But there is a difference in the parameter for the time interval. On the JavaScript side it
+expects a number, meanwhile ``Int`` in Idris is represented as a ``BigInt`` in JavaScript,
+for that reason the implementation of the ``%foreign`` needs to make the conversion.
+
+HTML Dom elements
+-----------------
+
+Lets turn our attention to the Dom elements and events. As said above, anything that is not a
+primitive type should be handled via the ``AnyPtr`` type in the FFI. Anything complex that is
+returned by a JavaScript function should be captured in an ``AnyPtr`` value. It is advisory to
+separate the ``AnyPtr`` values into categories.
+
+.. code-block:: idris
+
+    data DomNode = MkNode AnyPtr
+
+    %foreign "browser:lambda: () => document.body"
+    prim__body : () -> PrimIO AnyPtr
+
+    body : HasIO io => io DomNode
+    body = map MkNode $ primIO $ prim__body ()
+
+We create a ``DomNode`` type which holds an ``AnyPtr``. The ``prim__body`` function wraps a
+lambda function with no parameters. In the Idris function ``body`` we pass an extra ``()`` parameter
+and the we wrap the result in the ``DomNode`` type using the ``MkNode`` data constructor.
+
+Primitive values originated in JavaScript
+-----------------------------------------
+
+As a countinuation of the previous example, the ``width`` attribute of a DOM element can be
+retrieved via the FFI.
+
+.. code-block:: idris
+
+    %foreign "browser:lambda: n=>(BigInt(n.width))"
+    prim__width : AnyPtr -> PrimIO Int
+
+    width : HasIO io => DomNode -> io Int
+    width (MkNode p) = primIO $ prim__width p
+
+
+Note the ``BigInt`` conversation from the JavaScript. The ``n.width`` returns a JavaScript
+``Number`` and the corresponding ``Int`` of Idris is repersented as a ``BigInt`` in JavaScript.
+The implementor of the FFI function must keep these conversions in mind.
+
+Handling JavaScript events
+--------------------------
+
+.. code-block:: idris
+
+    data DomEvent = MkEvent AnyPtr
+
+    %foreign "browser:lambda: (event, callback, node) => node.addEventListener(event, x=>callback(x)())"
+    prim__addEventListener : String -> (AnyPtr -> PrimIO ()) -> AnyPtr -> PrimIO ()
+
+    addEventListener : HasIO io => String -> DomNode -> (DomEvent -> IO ()) -> io ()
+    addEventListener event (MkNode n) callback =
+      primIO $ prim__addEventListener event (\ptr => toPrim $ callback $ MkEvent ptr) n
+
+
+In this example shows how to attach an event handler to a particular DOM element. Values of events
+are also associated with ``AnyPtr`` on the Idris side. To seperate ``DomNode`` form ``DomEvent``
+we create two different types. Also it demonstrates how a simple callback function defined in
+Idris can be used on the JavaScript side.

From c6abab438cf149e42c94a901101aaf08f0cb5e49 Mon Sep 17 00:00:00 2001
From: David Smith <shmish111+github@gmail.com>
Date: Mon, 7 Dec 2020 10:53:01 +0000
Subject: [PATCH 05/28] export a function to parse ipkg files (#822)

---
 src/Idris/Package.idr | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr
index fd74f0540..0301f5913 100644
--- a/src/Idris/Package.idr
+++ b/src/Idris/Package.idr
@@ -40,6 +40,7 @@ import IdrisPaths
 
 %default covering
 
+public export
 record PkgDesc where
   constructor MkPkgDesc
   name : String
@@ -67,6 +68,7 @@ record PkgDesc where
   preclean : Maybe (FC, String) -- Script to run before cleaning
   postclean : Maybe (FC, String) -- Script to run after cleaning
 
+export
 Show PkgDesc where
   show pkg = "Package: " ++ name pkg ++ "\n" ++
              "Version: " ++ version pkg ++ "\n" ++
@@ -496,6 +498,17 @@ runRepl fname = do
             displayErrors errs
   repl {u} {s}
 
+export
+parsePkgFile : {auto c : Ref Ctxt Defs} ->
+               String -> Core PkgDesc
+parsePkgFile file = do
+  Right (pname, fs) <- coreLift $ parseFile file
+                                          (do desc <- parsePkgDesc file
+                                              eoi
+                                              pure desc)
+                     | Left (FileFail err) => throw (FileErr file err)
+                     | Left err => throw (ParseFail (getParseErrorLoc file err) err)
+  addFields fs (initPkgDesc pname)
 
 processPackage : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->

From d30e984137b49dab695f591b16e4fb1ee80b920c Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 10:45:48 +0000
Subject: [PATCH 06/28] [ debug ] Give the option to log off

---
 src/Core/Context.idr                    |  8 +++++---
 src/Idris/Desugar.idr                   |  2 +-
 src/Idris/Parser.idr                    | 23 ++++++++++++++---------
 src/Idris/REPL.idr                      |  5 +++--
 src/Idris/Syntax.idr                    |  4 ++--
 src/TTImp/Parser.idr                    | 12 +++++++++---
 src/TTImp/ProcessDecls.idr              |  2 +-
 src/TTImp/TTImp.idr                     |  5 +++--
 tests/idris2/positivity002/Issue660.idr |  4 ++++
 9 files changed, 42 insertions(+), 23 deletions(-)

diff --git a/src/Core/Context.idr b/src/Core/Context.idr
index 0fcca7475..ae2298078 100644
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@@ -2214,10 +2214,12 @@ getPrimitiveNames = pure $ catMaybes [!fromIntegerName, !fromStringName, !fromCh
 
 export
 addLogLevel : {auto c : Ref Ctxt Defs} ->
-              LogLevel -> Core ()
-addLogLevel l
+              Maybe LogLevel -> Core ()
+addLogLevel lvl
     = do defs <- get Ctxt
-         put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
+         case lvl of
+           Nothing => put Ctxt (record { options->session->logLevel = defaultLogLevel } defs)
+           Just l  => put Ctxt (record { options->session->logLevel $= insertLogLevel l } defs)
 
 export
 withLogLevel : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 7216074af..5bd0007c5 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -824,7 +824,7 @@ mutual
   desugarDecl ps (PDirective fc d)
       = case d of
              Hide n => pure [IPragma (\nest, env => hide fc n)]
-             Logging i => pure [ILog (topics i, verbosity i)]
+             Logging i => pure [ILog ((\ i => (topics i, verbosity i)) <$> i)]
              LazyOn a => pure [IPragma (\nest, env => lazyActive a)]
              UnboundImplicits a => do
                setUnboundImplicits a
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 93fab247c..3b395a0c2 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -951,6 +951,13 @@ totalityOpt
   <|> (keyword "total" *> pure Total)
   <|> (keyword "covering" *> pure CoveringOnly)
 
+logLevel : Rule (Maybe LogLevel)
+logLevel
+  = (Nothing <$ exactIdent "off")
+    <|> do topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
+           lvl <- intLit
+           pure (Just (mkLogLevel' topic (fromInteger lvl)))
+
 directive : FileName -> IndentInfo -> Rule Directive
 directive fname indents
     = do pragma "hide"
@@ -962,10 +969,9 @@ directive fname indents
 --          atEnd indents
 --          pure (Hide True n)
   <|> do pragma "logging"
-         topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
-         lvl <- intLit
+         lvl <- logLevel
          atEnd indents
-         pure (Logging (mkLogLevel' topic (fromInteger lvl)))
+         pure (Logging lvl)
   <|> do pragma "auto_lazy"
          b <- onoff
          atEnd indents
@@ -1401,9 +1407,9 @@ collectDefs [] = []
 collectDefs (PDef annot cs :: ds)
     = let (csWithFC, rest) = spanBy isPDef ds
           cs' = cs ++ concat (map snd csWithFC)
-          annot' = foldr 
+          annot' = foldr
                    (\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
-                   annot 
+                   annot
                    (map fst csWithFC)
       in
           PDef annot' cs' :: assert_total (collectDefs rest)
@@ -1768,7 +1774,7 @@ compileArgsCmd parseCmd command doc
       tm <- expr pdef "(interactive)" init
       pure (command tm n)
 
-loggingArgCmd : ParseCmd -> (LogLevel -> REPLCmd) -> String -> CommandDefinition
+loggingArgCmd : ParseCmd -> (Maybe LogLevel -> REPLCmd) -> String -> CommandDefinition
 loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, parse) where
 
   names : List String
@@ -1778,9 +1784,8 @@ loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, p
   parse = do
     symbol ":"
     runParseCmd parseCmd
-    topic <- optional ((:::) <$> unqualifiedName <*> many aDotIdent)
-    lvl <- intLit
-    pure (command (mkLogLevel' topic (fromInteger lvl)))
+    lvl <- logLevel
+    pure (command lvl)
 
 parserCommandsForHelp : CommandTable
 parserCommandsForHelp =
diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr
index 873564646..316766f6f 100644
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@@ -530,7 +530,7 @@ data REPLResult : Type where
   CheckedTotal : List (Name, Totality) -> REPLResult
   FoundHoles : List HoleData -> REPLResult
   OptionsSet : List REPLOpt -> REPLResult
-  LogLevelSet : LogLevel -> REPLResult
+  LogLevelSet : Maybe LogLevel -> REPLResult
   ConsoleWidthSet : Maybe Nat -> REPLResult
   ColorSet : Bool -> REPLResult
   VersionIs : Version -> REPLResult
@@ -965,7 +965,8 @@ mutual
   displayResult (FoundHoles xs) = do
     let holes = concatWith (surround (pretty ", ")) (pretty . name <$> xs)
     printResult (pretty (length xs) <++> pretty "holes" <+> colon <++> holes)
-  displayResult (LogLevelSet k) = printResult (reflow "Set loglevel to" <++> pretty k)
+  displayResult (LogLevelSet Nothing) = printResult (reflow "Logging turned off")
+  displayResult (LogLevelSet (Just k)) = printResult (reflow "Set log level to" <++> pretty k)
   displayResult (ConsoleWidthSet (Just k)) = printResult (reflow "Set consolewidth to" <++> pretty k)
   displayResult (ConsoleWidthSet Nothing) = printResult (reflow "Set consolewidth to auto")
   displayResult (ColorSet b) = printResult (reflow (if b then "Set color on" else "Set color off"))
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index edd58fd55..befa3b43f 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -225,7 +225,7 @@ mutual
   public export
   data Directive : Type where
        Hide : Name -> Directive
-       Logging : LogLevel -> Directive
+       Logging : Maybe LogLevel -> Directive
        LazyOn : Bool -> Directive
        UnboundImplicits : Bool -> Directive
        AmbigDepth : Nat -> Directive
@@ -442,7 +442,7 @@ data REPLCmd : Type where
      Total : Name -> REPLCmd
      Doc : Name -> REPLCmd
      Browse : Namespace -> REPLCmd
-     SetLog : LogLevel -> REPLCmd
+     SetLog : Maybe LogLevel -> REPLCmd
      SetConsoleWidth : Maybe Nat -> REPLCmd
      SetColor : Bool -> REPLCmd
      Metavars : REPLCmd
diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr
index bc3acc88e..6d96104f4 100644
--- a/src/TTImp/Parser.idr
+++ b/src/TTImp/Parser.idr
@@ -647,14 +647,20 @@ namespaceDecl
          commit
          namespaceId
 
+logLevel : Rule (Maybe (List String, Nat))
+logLevel
+  = (Nothing <$ exactIdent "off")
+    <|> do topic <- option [] ((::) <$> unqualifiedName <*> many aDotIdent)
+           lvl <- intLit
+           pure (Just (topic, fromInteger lvl))
+
 directive : FileName -> IndentInfo -> Rule ImpDecl
 directive fname indents
     = do pragma "logging"
          commit
-         topic <- ((::) <$> unqualifiedName <*> many aDotIdent)
-         lvl <- intLit
+         lvl <- logLevel
          atEnd indents
-         pure (ILog (topic, integerToNat lvl))
+         pure (ILog lvl)
          {- Can't do IPragma due to lack of Ref Ctxt. Should we worry about this?
   <|> do pragma "pair"
          commit
diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr
index 810dc7c0c..c43c8db97 100644
--- a/src/TTImp/ProcessDecls.idr
+++ b/src/TTImp/ProcessDecls.idr
@@ -59,7 +59,7 @@ process eopts nest env (IRunElabDecl fc tm)
 process eopts nest env (IPragma act)
     = act nest env
 process eopts nest env (ILog lvl)
-    = addLogLevel (uncurry unsafeMkLogLevel lvl)
+    = addLogLevel (uncurry unsafeMkLogLevel <$> lvl)
 
 TTImp.Elab.Check.processDecl = process
 
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index cc041e7b6..4a6dddc9d 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -347,7 +347,7 @@ mutual
        IPragma : ({vars : _} ->
                   NestedNames vars -> Env Term vars -> Core ()) ->
                  ImpDecl
-       ILog : (List String, Nat) -> ImpDecl
+       ILog : Maybe (List String, Nat) -> ImpDecl
 
   export
   Show ImpDecl where
@@ -366,7 +366,8 @@ mutual
     show (IRunElabDecl _ tm)
         = "%runElab " ++ show tm
     show (IPragma _) = "[externally defined pragma]"
-    show (ILog (topic, lvl)) = "%logging " ++ case topic of
+    show (ILog Nothing) = "%logging off"
+    show (ILog (Just (topic, lvl))) = "%logging " ++ case topic of
       [] => show lvl
       _  => concat (intersperse "." topic) ++ " " ++ show lvl
 
diff --git a/tests/idris2/positivity002/Issue660.idr b/tests/idris2/positivity002/Issue660.idr
index 0c44ed0ce..4297c30ea 100644
--- a/tests/idris2/positivity002/Issue660.idr
+++ b/tests/idris2/positivity002/Issue660.idr
@@ -9,3 +9,7 @@ data C : Type -> Type where
 
 data D : Type -> Type where
   MkD : {0 a : Type} -> let 0 b = List a in b -> D a
+
+%logging off
+
+data E : Type where

From b3542d66fcd8a0ae08ef19501d3e9a049db586b6 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Mon, 7 Dec 2020 14:34:48 +0300
Subject: [PATCH 07/28] Have lambda-case available everywhere lambda is (#819)

---
 src/Idris/Parser.idr           |  1 +
 tests/Main.idr                 |  2 +-
 tests/idris2/basic050/Ilc.idr  | 15 +++++++++++++++
 tests/idris2/basic050/expected |  6 ++++++
 tests/idris2/basic050/input    |  3 +++
 tests/idris2/basic050/run      |  3 +++
 6 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/basic050/Ilc.idr
 create mode 100644 tests/idris2/basic050/expected
 create mode 100644 tests/idris2/basic050/input
 create mode 100755 tests/idris2/basic050/run

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 3b395a0c2..82382942b 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -742,6 +742,7 @@ mutual
     <|> implicitPi fname indents
     <|> explicitPi fname indents
     <|> lam fname indents
+    <|> lambdaCase fname indents
 
   typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
   typeExpr q fname indents
diff --git a/tests/Main.idr b/tests/Main.idr
index 08952d50c..852573e32 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -44,7 +44,7 @@ idrisTests = MkTestPool []
        "basic031", "basic032", "basic033", "basic034", "basic035",
        "basic036", "basic037", "basic038", "basic039", "basic040",
        "basic041", "basic042", "basic043", "basic044", "basic045",
-       "basic046", "basic047", "basic048", "basic049",
+       "basic046", "basic047", "basic048", "basic049", "basic050",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
diff --git a/tests/idris2/basic050/Ilc.idr b/tests/idris2/basic050/Ilc.idr
new file mode 100644
index 000000000..76bd4d5ac
--- /dev/null
+++ b/tests/idris2/basic050/Ilc.idr
@@ -0,0 +1,15 @@
+f : (Int -> Bool) -> Int
+f p = case (p 0, p 1) of
+        (False, False) => 0
+        (False, True)  => 1
+        (True , False) => 2
+        (True , True)  => 4
+
+il : Int
+il = f \x => x > 0
+
+lc : Int
+lc = f $ \case 0 => True ; _ => False
+
+ilc : Int
+ilc = f \case 0 => True; _ => False
diff --git a/tests/idris2/basic050/expected b/tests/idris2/basic050/expected
new file mode 100644
index 000000000..9115acd20
--- /dev/null
+++ b/tests/idris2/basic050/expected
@@ -0,0 +1,6 @@
+1/1: Building Ilc (Ilc.idr)
+Main> 1
+Main> 2
+Main> 2
+Main> 
+Bye for now!
diff --git a/tests/idris2/basic050/input b/tests/idris2/basic050/input
new file mode 100644
index 000000000..f9a6b1d47
--- /dev/null
+++ b/tests/idris2/basic050/input
@@ -0,0 +1,3 @@
+il
+lc
+ilc
diff --git a/tests/idris2/basic050/run b/tests/idris2/basic050/run
new file mode 100755
index 000000000..b2057c25c
--- /dev/null
+++ b/tests/idris2/basic050/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner Ilc.idr < input
+
+rm -rf build

From ef6cbcf65850239363fca44ac7516c5f1b4a8304 Mon Sep 17 00:00:00 2001
From: "Nicolas A. Schmidt" <35599990+mr-infty@users.noreply.github.com>
Date: Mon, 7 Dec 2020 12:41:47 +0100
Subject: [PATCH 08/28] Auto-implicit `__con` now added before implicits.
 (#659)

---
 src/Idris/Elab/Interface.idr     | 12 ++++--------
 tests/Main.idr                   |  2 +-
 tests/idris2/reg035/Implicit.idr |  3 +++
 tests/idris2/reg035/expected     |  1 +
 tests/idris2/reg035/run          |  3 +++
 5 files changed, 12 insertions(+), 9 deletions(-)
 create mode 100644 tests/idris2/reg035/Implicit.idr
 create mode 100644 tests/idris2/reg035/expected
 create mode 100755 tests/idris2/reg035/run

diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index 190acd52d..7479497c2 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/src/Idris/Elab/Interface.idr
@@ -104,13 +104,9 @@ getMethDecl {vars} env nest params mnames (fc, c, opts, n, (d, ty))
              else IPi fc r p mn arg (stripParams ps ret)
     stripParams ps ty = ty
 
--- bind the auto implicit for the interface - put it after all the other
--- implicits
+-- bind the auto implicit for the interface - put it first, as it may be needed
+-- in other method variables, including implicit variables
 bindIFace : FC -> RawImp -> RawImp -> RawImp
-bindIFace _ ity (IPi fc rig Implicit n ty sc)
-       = IPi fc rig Implicit n ty (bindIFace fc ity sc)
-bindIFace _ ity (IPi fc rig AutoImplicit n ty sc)
-       = IPi fc rig AutoImplicit n ty (bindIFace fc ity sc)
 bindIFace fc ity sc = IPi fc top AutoImplicit (Just (UN "__con")) ity sc
 
 -- Get the top level function for implementing a method
@@ -129,8 +125,8 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
          -- Make the constraint application explicit for any method names
          -- which appear in other method types
          let ty_constr =
-             bindPs params $ substNames vars (map applyCon allmeths) ty
-         ty_imp <- bindTypeNames [] vars (bindIFace fc ity ty_constr)
+             substNames vars (map applyCon allmeths) ty
+         ty_imp <- bindTypeNames [] vars (bindPs params $ bindIFace fc ity ty_constr)
          cn <- inCurrentNS n
          let tydecl = IClaim fc c vis (if d then [Inline, Invertible]
                                             else [Inline])
diff --git a/tests/Main.idr b/tests/Main.idr
index 852573e32..aa1aa17a7 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -114,7 +114,7 @@ idrisTests = MkTestPool []
        "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
        "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
        "reg022", "reg023", "reg024", "reg025", "reg026", "reg027", "reg028",
-       "reg029", "reg030", "reg031", "reg032", "reg033", "reg034",
+       "reg029", "reg030", "reg031", "reg032", "reg033", "reg034", "reg035",
        -- Totality checking
        "total001", "total002", "total003", "total004", "total005",
        "total006", "total007", "total008", "total009", "total010",
diff --git a/tests/idris2/reg035/Implicit.idr b/tests/idris2/reg035/Implicit.idr
new file mode 100644
index 000000000..a40cbc897
--- /dev/null
+++ b/tests/idris2/reg035/Implicit.idr
@@ -0,0 +1,3 @@
+interface A where
+  x : Nat
+  f : {auto pf : x = 0} -> ()
diff --git a/tests/idris2/reg035/expected b/tests/idris2/reg035/expected
new file mode 100644
index 000000000..d69c981b0
--- /dev/null
+++ b/tests/idris2/reg035/expected
@@ -0,0 +1 @@
+1/1: Building Implicit (Implicit.idr)
diff --git a/tests/idris2/reg035/run b/tests/idris2/reg035/run
new file mode 100755
index 000000000..803592018
--- /dev/null
+++ b/tests/idris2/reg035/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 Implicit.idr --check
+
+rm -rf build

From 9c5198cde3b9bc58079ff888c0fb64c27e5985fe Mon Sep 17 00:00:00 2001
From: Jan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk>
Date: Fri, 4 Dec 2020 15:46:43 +0000
Subject: [PATCH 09/28] Fixed docs and improved Literate mode.

+ Expanded the documentation on how to use literate modes.
+ Added invisible code blocks in Markdown using specially tagged comment blocks: `<!-- idris -->`.
+ Fixed OrgMode specificaton to recognise comment blocks properly.
---
 docs/source/reference/literate.rst | 89 ++++++++++++++++++++++++++----
 src/Parser/Unlit.idr               |  6 +-
 tests/idris2/literate011/IEdit.md  | 17 +++++-
 3 files changed, 95 insertions(+), 17 deletions(-)

diff --git a/docs/source/reference/literate.rst b/docs/source/reference/literate.rst
index 3b0f712de..e65159968 100644
--- a/docs/source/reference/literate.rst
+++ b/docs/source/reference/literate.rst
@@ -9,6 +9,7 @@ Idris2 supports several types of literate mode styles.
 The unlit'n has been designed based such that we assume that we are parsing markdown-like languages
 The unlit'n is performed by a Lexer that uses a provided literate style to recognise code blocks and code lines.
 Anything else is ignored.
+Idris2 also provides support for recognising both 'visible' and 'invisible' code blocks using 'native features' of each literate style.
 
 A literate style consists of:
 
@@ -25,35 +26,99 @@ But more importantly, a more intelligent processing of literate documents using
 Bird Style Literate Files
 =========================
 
-Bird notation is a classic literate mode found in Haskell, (and Orwell) in which code lines begin with ``>``.
+We treat files with an extension of ``.lidr`` as bird style literate files.
+
+Bird notation is a classic literate mode found in Haskell, (and Orwell) in which visible code lines begin with ``>`` and hidden lines with ``<``.
 Other lines are treated as documentation.
 
-We treat files with an extension of ``.lidr`` as bird style literate files.
+
+
+.. note::
+   We have diverged from ``lhs2tex`` in which ``<`` is traditionally used to display inactive code.
+   Bird-style is presented as is, and we recommended use of the other styles for much more comprehensive literate mode.
 
 Embedding in Markdown-like documents
 ====================================
 
 While Bird Style literate mode is useful, it does not lend itself well
 to more modern markdown-like notations such as Org-Mode and CommonMark.
-
 Idris2 also provides support for recognising both 'visible' and 'invisible'
-code blocks and lines in both CommonMark and OrgMode documents.
+code blocks and lines in both CommonMark and OrgMode documents using native code blocks and lines..
 
-'Visible' content will be kept in the pretty printer's output while
-the 'invisible' blocks and lines will be removed.
+The idea being is that:
+
+1. **Visible** content will be kept in the pretty printer's output;
+2. **Invisible** content will be removed; and
+3. **Specifications** will be displayed *as is* and not touched by the compiler.
 
 OrgMode
 *******
 
-+ Org mode source blocks for idris are recognised as visible code blocks,
-+ Comment blocks that begin with ``#+COMMENT: idris`` are treated as invisible code blocks.
-+ Invisible code lines are denoted with ``#+IDRIS:``.
+We treat files with an extension of ``.org`` as org-style literate files.
+Each of the following markup is recognised regardless of case:
 
-We treat files with an extension of ``.org`` as org-mode style literate files.
++ Org mode source blocks for idris sans options are recognised as visible code blocks::
+
+    #+begin_src idris
+    data Nat = Z | S Nat
+    #+end_src
+
++ Comment blocks that begin with ``#+BEGIN_COMMENT idris`` are treated as invisible code blocks::
+
+    #+begin_comment idris
+    data Nat = Z | S Nat
+    #+end_comment
+
++ Visible code lines, and specifications, are not supported. Invisible code lines are denoted with ``#+IDRIS:``::
+
+    #+IDRIS: data Nat = Z | S Nat
+
++ Specifications can be given using OrgModes plain source or example blocks::
+
+    #+begin_src
+    map : (f : a -> b)
+       -> List a
+       -> List b
+    map f _ = Nil
+    #+end_src
 
 CommonMark
 ************
 
-Only code blocks denoted by standard code blocks labelled as idris are recognised.
-
 We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark style literate files.
+
++ CommonMark source blocks for idris sans options are recognised as visible code blocks::
+
+    ```idris
+    data Nat = Z | S Nat
+    ```
+
+    ~~~idris
+    data Nat = Z | S Nat
+    ~~~
+
++ Comment blocks of the form ``<!-- idris\n ... \n -->`` are treated as invisible code blocks::
+
+    <!-- idris
+    data Nat = Z | S Nat
+    -->
+
++ Code lines are not supported.
+
++ Specifications can be given using CommonMark's pre-formatted blocks (indented by four spaces) or unlabelled code blocks.::
+
+    Compare
+
+    ```
+    map : (f : a -> b)
+       -> List a
+       -> List b
+    map f _ = Nil
+    ```
+
+    with
+
+        map : (f : a -> b)
+           -> List a
+           -> List b
+        map f _ = Nil
diff --git a/src/Parser/Unlit.idr b/src/Parser/Unlit.idr
index 23e80c973..622125b23 100644
--- a/src/Parser/Unlit.idr
+++ b/src/Parser/Unlit.idr
@@ -17,15 +17,15 @@ styleOrg : LiterateStyle
 styleOrg = MkLitStyle
               [ ("#+BEGIN_SRC idris","#+END_SRC")
               , ("#+begin_src idris","#+end_src")
-              , ("#+COMMENT idris","#+END_COMMENT")
-              , ("#+comment idris","#+end_comment")]
+              , ("#+BEGIN_COMMENT idris","#+END_COMMENT")
+              , ("#+begin_comment idris","#+end_comment")]
               ["#+IDRIS:"]
               [".org"]
 
 export
 styleCMark : LiterateStyle
 styleCMark = MkLitStyle
-              [("```idris", "```"), ("~~~idris", "~~~")]
+              [("```idris", "```"), ("~~~idris", "~~~"), ("<!-- idris", "-->")]
               Nil
               [".md", ".markdown"]
 
diff --git a/tests/idris2/literate011/IEdit.md b/tests/idris2/literate011/IEdit.md
index 42c604159..ccbc3adad 100644
--- a/tests/idris2/literate011/IEdit.md
+++ b/tests/idris2/literate011/IEdit.md
@@ -4,9 +4,9 @@ data Vect : Nat -> Type -> Type where
      (::) : a -> Vect k a -> Vect (S k) a
 ```
 
-```idris
+<!-- idris
 %name Vect xs, ys, zs
-```
+-->
 
 ```idris
 dupAll : Vect n a -> Vect n (a, a)
@@ -14,3 +14,16 @@ dupAll xs = zipHere xs xs
   where
     zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)
 ```
+
+
+<!-- idris
+
+data Foobar = MkFoo
+
+-->
+
+
+```idris
+showFooBar : Foobar -> String
+showFooBar MkFoo = "MkFoo"
+```

From 3a6e779acff2fe1e73193428122aa197a87bf341 Mon Sep 17 00:00:00 2001
From: Jan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk>
Date: Fri, 4 Dec 2020 16:13:31 +0000
Subject: [PATCH 10/28] Extended Literate support to include LaTeX.

---
 docs/source/reference/literate.rst  | 36 ++++++++++++++++++++++++++++-
 src/Parser/Unlit.idr                | 15 ++++++++++--
 tests/idris2/literate013/LitTeX.tex | 36 +++++++++++++++++++++++++++++
 tests/idris2/literate013/expected   |  1 +
 tests/idris2/literate013/run        |  2 +-
 5 files changed, 86 insertions(+), 4 deletions(-)
 create mode 100644 tests/idris2/literate013/LitTeX.tex

diff --git a/docs/source/reference/literate.rst b/docs/source/reference/literate.rst
index e65159968..2da7dc7d6 100644
--- a/docs/source/reference/literate.rst
+++ b/docs/source/reference/literate.rst
@@ -83,7 +83,7 @@ Each of the following markup is recognised regardless of case:
     #+end_src
 
 CommonMark
-************
+**********
 
 We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark style literate files.
 
@@ -122,3 +122,37 @@ We treat files with an extension of ``.md`` and ``.markdown`` as CommonMark styl
            -> List a
            -> List b
         map f _ = Nil
+
+LaTeX
+*****
+
+We treat files with an extension of ``.tex`` and ``.ltx`` as LaTeX style literate files.
+
++ We treat environments named ``code`` as visible code blocks::
+
+    \begin{code}
+    data Nat = Z | S Nat
+    \end{code}
+
+
++ We treat environments named ``hidden`` as invisible code blocks::
+
+    \begin{hidden}
+    data Nat = Z | S Nat
+    \end{hidden}
+
++ Code lines are not supported.
+
++ Specifications can be given using user defined environments.
+
+We do not provide definitions for these code blocks and ask the user to define them.
+With one such example using ``fancyverbatim`` and ``comment`` packages as::
+
+    \usepackage{fancyvrb}
+    \DefineVerbatimEnvironment
+      {code}{Verbatim}
+      {}
+
+    \usepackage{comment}
+
+    \excludecomment{hidden}
diff --git a/src/Parser/Unlit.idr b/src/Parser/Unlit.idr
index 622125b23..310bb5e7e 100644
--- a/src/Parser/Unlit.idr
+++ b/src/Parser/Unlit.idr
@@ -29,6 +29,13 @@ styleCMark = MkLitStyle
               Nil
               [".md", ".markdown"]
 
+export
+styleTeX : LiterateStyle
+styleTeX = MkLitStyle
+              [("\\begin{code}", "\\end{code}"), ("\\begin{hidden}", "\\end{hidden}")]
+              Nil
+              [".tex", ".ltx"]
+
 export
 isLitFile : String -> Maybe LiterateStyle
 isLitFile fname =
@@ -36,7 +43,9 @@ isLitFile fname =
       Just s => Just s
       Nothing => case isStyle styleOrg of
                      Just s => Just s
-                     Nothing => isStyle styleCMark
+                     Nothing => case isStyle styleCMark of
+                                     Just s => Just s
+                                     Nothing => isStyle styleTeX
 
   where
    hasSuffix : String -> Bool
@@ -57,7 +66,9 @@ isLitLine str =
                     (Just l, s) => (Just l, s)
                     otherwise => case isLiterateLine styleCMark str of
                                    (Just l, s) => (Just l, s)
-                                   otherwise => (Nothing, str)
+                                   otherwise => case isLiterateLine styleTeX str of
+                                                   (Just l, s) => (Just l, s)
+                                                   otherwise => (Nothing, str)
 
 export
 unlit : Maybe LiterateStyle -> String -> Either LiterateError String
diff --git a/tests/idris2/literate013/LitTeX.tex b/tests/idris2/literate013/LitTeX.tex
new file mode 100644
index 000000000..dd298c146
--- /dev/null
+++ b/tests/idris2/literate013/LitTeX.tex
@@ -0,0 +1,36 @@
+\documentclass{article}
+
+\usepackage{fancyvrb}
+
+\usepackage{comment}
+
+\DefineVerbatimEnvironment
+  {code}{Verbatim}
+  {} % Add fancy options here if you like.
+
+\excludecomment{hidden}
+
+\begin{hidden}
+module LitTeX
+
+%default total
+\end{hidden}
+
+\begin{document}
+
+\begin{code}
+data V a = Empty | Extend a (V a)
+\end{code}
+
+\begin{code}
+isCons : V a -> Bool
+isCons Empty = False
+isCons (Extend _ _) = True
+\end{code}
+
+\begin{hidden}
+namespace Hidden
+  data U a = Empty | Extend a (U a)
+\end{hidden}
+
+\end{document}
diff --git a/tests/idris2/literate013/expected b/tests/idris2/literate013/expected
index e973c66d6..6f199b0d5 100644
--- a/tests/idris2/literate013/expected
+++ b/tests/idris2/literate013/expected
@@ -1 +1,2 @@
 1/1: Building Lit (Lit.lidr)
+1/1: Building LitTeX (LitTeX.tex)
diff --git a/tests/idris2/literate013/run b/tests/idris2/literate013/run
index cb309a9ab..333c3452e 100755
--- a/tests/idris2/literate013/run
+++ b/tests/idris2/literate013/run
@@ -1,3 +1,3 @@
 $1 --no-color --console-width 0 --no-banner --check Lit.lidr
-
+$1 --no-color --console-width 0 --no-banner --check LitTeX.tex
 rm -rf build

From 1dba32a0c4b4c88ac256557291fb696fbc0e0761 Mon Sep 17 00:00:00 2001
From: Ruslan Feizerahmanov <russoulmc@gmail.com>
Date: Mon, 7 Dec 2020 21:59:49 +0300
Subject: [PATCH 11/28] [ doc ] new application syntax (#820)

---
 CONTRIBUTORS                    |  59 ++++++------
 docs/source/updates/updates.rst | 160 ++++++++++++++++++++++++++++++++
 2 files changed, 190 insertions(+), 29 deletions(-)

diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index b631592ac..461ddf1ff 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -1,46 +1,47 @@
 Thanks to the following for their help and contributions to Idris 2:
 
 Abdelhakim Qbaich
-Alex Gryzlov 
-Alex Silva 
-Andre Kuhlenschmidt 
-André Videla 
+Alex Gryzlov
+Alex Silva
+Andre Kuhlenschmidt
+André Videla
 Andy Lok
 Anthony Lodi
-Arnaud Bailly 
-Brian Wignall 
-Christian Rasmussen 
-David Smith 
-Edwin Brady 
+Arnaud Bailly
+Brian Wignall
+Christian Rasmussen
+David Smith
+Edwin Brady
 Fabián Heredia Montiel
 George Pollard
-GhiOm 
+GhiOm
 Guillaume Allais
-Ilya Rezvov 
-Jan de Muijnck-Hughes 
+Ilya Rezvov
+Jan de Muijnck-Hughes
 Jeetu
 Johann Rudloff
-Kamil Shakirov 
+Kamil Shakirov
 Bryn Keller
-Kevin Boulain 
-LuoChen 
+Kevin Boulain
+LuoChen
 Marc Petit-Huguenin
 MarcelineVQ
-Marshall Bowers 
-Matthew Wilson 
-Matus Tejiscak 
-Michael Morgan 
-Milan Kral 
-Molly Miller 
-Mounir Boudia 
+Marshall Bowers
+Matthew Wilson
+Matus Tejiscak
+Michael Morgan
+Milan Kral
+Molly Miller
+Mounir Boudia
 Nicolas Biri
-Niklas Larsson 
-Ohad Kammar 
-Peter Hajdu 
+Niklas Larsson
+Ohad Kammar
+Peter Hajdu
 Rohit Grover
 Rui Barreiro
-Simon Chatterjee 
+Ruslan Feizerahmanov
+Simon Chatterjee
 then0rTh
-Theo Butler 
-Tim Süberkrüb 
-Timmy Jose 
+Theo Butler
+Tim Süberkrüb
+Timmy Jose
diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst
index cbb5c10e7..f8d1aca12 100644
--- a/docs/source/updates/updates.rst
+++ b/docs/source/updates/updates.rst
@@ -579,6 +579,149 @@ Idris 1 took a different approach here: names which were parameters to data
 types were in scope, other names were not. The Idris 2 approach is, we hope,
 more consistent and easier to understand.
 
+.. _sect-app-syntax-additions:
+
+Function application syntax additions
+-------------------------------------
+
+From now on you can utilise the new syntax of function applications:
+
+.. code-block:: idris
+
+    f {x1 [= e1], x2 [= e2], ...}
+
+There are three additions here:
+
+1. More than one argument can be written in braces, separated with commas:
+
+.. code-block:: idris
+
+    record Dog where
+      constructor MkDog
+      name : String
+      age : Nat
+
+    -- Notice that `name` and `age` are explicit arguments.
+    -- See paragraph (2)
+    haveADog : Dog
+    haveADog = MkDog {name = "Max", age = 3}
+
+    pairOfStringAndNat : (String, Nat)
+    pairOfStringAndNat = MkPair {x = "year", y = 2020}
+
+    myPlus : (n : Nat) -> (k : Nat) -> Nat
+    myPlus {n = Z   , k} = k
+    myPlus {n = S n', k} = S (myPlus n' k)
+
+    twoPlusTwoIsFour : myPlus {n = 2, k = 2} === 4
+    twoPlusTwoIsFour = Refl
+
+2. Arguments in braces can now correspond to explicit, implicit and auto implicit
+   dependent function types (``Pi`` types), provided the domain type is named:
+
+.. code-block:: idris
+
+    myPointlessFunction : (exp : String) -> {imp : String} -> {auto aut : String} -> String
+    myPointlessFunction exp = exp ++ imp ++ aut
+
+    callIt : String
+    callIt = myPointlessFunction {imp = "a ", exp = "Just ", aut = "test"}
+
+Order of the arguments doesn't matter as long as they are in braces and the names are distinct.
+It is better to stick named arguments in braces at the end of your argument list, because
+regular unnamed explicit arguments are processed first and take priority:
+
+.. code-block:: idris
+
+    myPointlessFunction' : (a : String) -> String -> (c : String) -> String
+    myPointlessFunction' a b c = a ++ b ++ c
+
+    badCall : String
+    badCall = myPointlessFunction' {a = "a", c = "c"} "b"
+
+This snippet won't type check, because "b" in ``badCall`` is passed first,
+although logically we want it to be second.
+Idris will tell you that it couldn't find a spot for ``a = "a"`` (because "b" took its place),
+so the application is ill-formed.
+
+Thus if you want to use the new syntax, it is worth naming your ``Pi`` types.
+
+3. Multiple explicit arguments can be "skipped" more easily with the following syntax:
+
+.. code-block:: idris
+
+    f {x1 [= e1], x2 [= e2], ..., xn [= en], _}
+
+or
+
+.. code-block:: idris
+
+    f {}
+
+in case none of the named arguments are wanted.
+
+Examples:
+
+.. code-block:: idris
+
+    import Data.Nat
+
+    record Four a b c d where
+      constructor MkFour
+      x : a
+      y : b
+      z : c
+      w : d
+
+    firstTwo : Four a b c d -> (a, b)
+    firstTwo $ MkFour {x, y, _} = (x, y)
+    -- firstTwo $ MkFour {x, y, z = _, w = _} = (x, y)
+
+    dontCare : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
+    dontCare {} = plusCommutative {}
+    --dontCare _ _ _ _ _ = plusCommutative _ _
+
+Last rule worth noting is the case of named applications with repeated argument names, e.g:
+
+.. code-block:: idris
+
+    data WeirdPair : Type -> Type -> Type where
+      MkWeirdPair : (x : a) -> (x : b) -> WeirdPair a b
+
+    weirdSnd : WeirdPair a b -> b
+    --weirdSnd $ MkWeirdPair {x, x} = x
+    --                        ^
+    -- Error: "Non linear pattern variable"
+    -- But that one is okay:
+    weirdSnd $ MkWeirdPair {x = _, x} = x
+
+In this example the name ``x`` is given repeatedly to the ``Pi`` types of the data constructor ``MkWeirdPair``.
+In order to deconstruct the ``WeirdPair a b`` in ``weirdSnd``, while writing the left-hand side of the pattern-matching clause
+in a named manner (via the new syntax), we have to rename the first occurrence of ``x`` to any fresh name or the ``_`` as we did.
+Then the definition type checks normally.
+
+In general, duplicate names are bound sequentially on the left-hand side and must be renamed for the pattern expression to be valid.
+
+The situation is similar on the right-hand side of pattern-matching clauses:
+
+.. code-block:: idris
+
+   0 TypeOf : a -> Type
+   TypeOf _ = a
+
+   weirdId : {0 a : Type} -> (1 a : a) -> TypeOf a
+   weirdId a = a
+
+   zero : Nat
+   -- zero = weirdId { a = Z }
+   --                      ^
+   -- Error: "Mismatch between: Nat and Type"
+   -- But this works:
+   zero = weirdId { a = Nat, a = Z }
+
+Named arguments should be passed sequentially in the order they were defined in the ``Pi`` types,
+regardless of their (imp)explicitness.
+
 Better inference
 ----------------
 
@@ -656,6 +799,23 @@ correspondingly:
     addEntry val = record { length $= S,
                             content $= (val :: ) }
 
+Another novelty - new update syntax (previous one still functional):
+
+.. code-block:: idris
+
+    record Three a b c where
+      constructor MkThree
+      x : a
+      y : b
+      z : c
+
+    -- Yet another contrived example
+    mapSetMap : Three a b c -> (a -> a') -> b' -> (c -> c') -> Three a' b' c'
+    mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three
+
+The ``record`` keyword has been discarded for brevity, symbol ``:=`` replaces ``=``
+  in order to not introduce any ambiguity.
+
 Generate definition
 -------------------
 

From 87358f19daf9c33f9affaec4cd86c265412a1712 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= <fabianhjr@protonmail.com>
Date: Mon, 7 Dec 2020 14:33:56 -0600
Subject: [PATCH 12/28] Increase timings of concurrency tests due to flaky
 windows runs

---
 tests/chez/concurrency001/Futures.idr | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/tests/chez/concurrency001/Futures.idr b/tests/chez/concurrency001/Futures.idr
index 574ff9ca5..abb9a70d0 100644
--- a/tests/chez/concurrency001/Futures.idr
+++ b/tests/chez/concurrency001/Futures.idr
@@ -11,11 +11,11 @@ constant = do
   let a = await $ fork "String"
   putStrLn a
 
--- Issue related to usleep in MacOS brew sleep
+-- Issue related to usleep in MacOS brew chez
 macsleep : (us : Int) -> So (us >= 0) => IO ()
 macsleep us =
   if (os == "darwin")
-    then sleep (us `div` 1000)
+    then sleep (us `div` 10000)
     else usleep us
 
 partial
@@ -28,7 +28,7 @@ futureHelloWorld (us, n) with (choose (us >= 0))
 partial
 simpleIO : IO (List Unit)
 simpleIO = do
-  futures <- sequence $ futureHelloWorld <$> [(3000, "World"), (1000, "Bar"), (0, "Foo"), (2000, "Idris")]
+  futures <- sequence $ futureHelloWorld <$> [(30000, "World"), (10000, "Bar"), (0, "Foo"), (20000, "Idris")]
   let awaited = await <$> futures
   pure awaited
 
@@ -40,16 +40,16 @@ erasureAndNonbindTest = do
   _ <- forkIO $ do
     putStrLn "This line is printed"
   notUsed <- forkIO $ do
-    macsleep 1000
+    macsleep 10000
     putStrLn "This line is also printed"
   let _ = nonbind
   let n = nonbind
-  macsleep 2000 -- Even if not explicitly awaited, we should let threads finish before exiting
+  macsleep 20000 -- Even if not explicitly awaited, we should let threads finish before exiting
 
 map : IO ()
 map = do
   future1 <- forkIO $ do
-    macsleep 1000
+    macsleep 10000
     putStrLn "#2"
   let future3 = map (const "#3") future1
   future2 <- forkIO $ do

From a1b624a3bcd96c5c0af4e2c42af8b25860bbbcac Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Tue, 8 Dec 2020 10:35:07 +0300
Subject: [PATCH 13/28] Tiny fix of the formatting in the recently added
 documentation.

---
 docs/source/updates/updates.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst
index f8d1aca12..631bdf1b9 100644
--- a/docs/source/updates/updates.rst
+++ b/docs/source/updates/updates.rst
@@ -814,7 +814,7 @@ Another novelty - new update syntax (previous one still functional):
     mapSetMap three@(MkThree x y z) f y' g = {x $= f, y := y', z $= g} three
 
 The ``record`` keyword has been discarded for brevity, symbol ``:=`` replaces ``=``
-  in order to not introduce any ambiguity.
+in order to not introduce any ambiguity.
 
 Generate definition
 -------------------

From 98674fc40aba87d791e0b654bb8a0706429f90f4 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:00:27 +0000
Subject: [PATCH 14/28] [ cleanup ] use pattern-matching binds in monadic code

---
 src/Compiler/RefC/RefC.idr | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index 24a486122..924ab5805 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -29,11 +29,11 @@ import Utils.Path
 
 findCC : IO String
 findCC
-    = do Just cc <- getEnv "IDRIS2_CC"
-              | Nothing => do Just cc <- getEnv "CC"
-                                   | Nothing => pure "cc"
-                              pure cc
-         pure cc
+    = do Nothing <- getEnv "IDRIS2_CC"
+           | Just cc => pure cc
+         Nothing <- getEnv "CC"
+           | Just cc => pure cc
+         pure "cc"
 
 toString : List Char -> String
 toString [] = ""
@@ -1123,14 +1123,13 @@ compileExpr ANF c _ outputDir tm outfile =
                        clibdirs (lib_dirs dirs)
 
      coreLift $ putStrLn runccobj
-     ok <- coreLift $ system runccobj
-     if ok == 0
-        then do coreLift $ putStrLn runcc
-                ok <- coreLift $ system runcc
-                if ok == 0
-                   then pure (Just outexec)
-                   else pure Nothing
-        else pure Nothing
+     0 <- coreLift $ system runccobj
+       | _ => pure Nothing
+     coreLift $ putStrLn runcc
+     0 <- coreLift $ system runcc
+       | _ => pure Nothing
+     pure (Just outexec)
+
   where
     fullprefix_dir : Dirs -> String -> String
     fullprefix_dir dirs sub

From e5c6dfac5b2c60915ff9aa72aeaacde0c429e262 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:02:15 +0000
Subject: [PATCH 15/28] [ refactor ] remove toString, natMinus

* toString is an inefficient fastPack
* natMinus is an inefficient minus (we have already checked isLTE)
---
 src/Compiler/RefC/RefC.idr | 16 ++++------------
 1 file changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index 924ab5805..ee200412a 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -35,15 +35,6 @@ findCC
            | Just cc => pure cc
          pure "cc"
 
-toString : List Char -> String
-toString [] = ""
-toString (c :: cx) = cast c ++ toString cx
-
-natMinus : (a,b:Nat) -> Nat
-natMinus a b = case isLTE b a of
-    (Yes prf) => minus a b
-    (No _) => 0
-
 showcCleanStringChar : Char -> String -> String
 showcCleanStringChar '+' = ("_plus" ++)
 showcCleanStringChar '-' = ("__" ++)
@@ -75,9 +66,10 @@ showcCleanStringChar c
   where
     pad : String -> String
     pad str
-        = case isLTE (length str) 4 of
-               Yes _ => toString (List.replicate (natMinus 4 (length str)) '0') ++ str
-               No _ => str
+        = let n = length str in
+          case isLTE n 4 of
+             Yes _ => fastPack (List.replicate (minus 4 n) '0') ++ str
+             No _ => str
 
 showcCleanString : List Char -> String -> String
 showcCleanString [] = id

From f8c248dc7a738803dd4aee537617e5471951c676 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:03:24 +0000
Subject: [PATCH 16/28] [ refactor ] introduce Core.update

---
 src/Compiler/RefC/RefC.idr | 30 +++++++-----------------------
 src/Core/Core.idr          |  6 ++++++
 2 files changed, 13 insertions(+), 23 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index ee200412a..18c23f23d 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -307,20 +307,13 @@ getNextCounter = do
 registerVariableForAutomaticFreeing : {auto t : Ref TemporaryVariableTracker (List (List String))}
                                    -> String
                                    -> Core ()
-registerVariableForAutomaticFreeing var = do
-    lists <- get TemporaryVariableTracker
-    case lists of
-        [] => do
-            put TemporaryVariableTracker ([[var]])
-            pure ()
-        (l :: ls) => do
-                put TemporaryVariableTracker ((var :: l) :: ls)
-                pure ()
+registerVariableForAutomaticFreeing var
+  = update TemporaryVariableTracker $ \case
+      [] => [[var]]
+      (l :: ls) => ((var :: l) :: ls)
 
 newTemporaryVariableLevel : {auto t : Ref TemporaryVariableTracker (List (List String))} -> Core ()
-newTemporaryVariableLevel = do
-    lists <- get TemporaryVariableTracker
-    put TemporaryVariableTracker ([] :: lists)
+newTemporaryVariableLevel = update TemporaryVariableTracker ([] ::)
 
 
 getNewVar : {auto a : Ref ArgCounter Nat} -> {auto t : Ref TemporaryVariableTracker (List (List String))} -> Core String
@@ -351,19 +344,10 @@ lJust line fillPos filler =
         (No _) => line
 
 increaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()
-increaseIndentation = do
-    iLevel <- get IndentLevel
-    put IndentLevel (S iLevel)
-    pure ()
+increaseIndentation = update IndentLevel S
 
 decreaseIndentation : {auto il : Ref IndentLevel Nat} -> Core ()
-decreaseIndentation = do
-    iLevel <- get IndentLevel
-    case iLevel of
-        Z => pure ()
-        (S k) => do
-            put IndentLevel k
-            pure ()
+decreaseIndentation = update IndentLevel pred
 
 indentation : {auto il : Ref IndentLevel Nat} -> Core String
 indentation = do
diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index 3edf9b74c..689d7f1f0 100644
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@@ -635,6 +635,12 @@ export %inline
 put : (x : label) -> {auto ref : Ref x a} -> a -> Core ()
 put x {ref = MkRef io} val = coreLift (writeIORef io val)
 
+export %inline
+update : (x : label) -> {auto ref : Ref x a} -> (a -> a) -> Core ()
+update x f
+  = do v <- get x
+       put x (f v)
+
 export
 cond : List (Lazy Bool, Lazy a) -> a -> a
 cond [] def = def

From 39f26e7ed6516ec36b7de9a0260d9a95889ea1d9 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:04:04 +0000
Subject: [PATCH 17/28] [ minor ] avoid repetition

---
 src/Compiler/RefC/RefC.idr | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index 18c23f23d..e454413f6 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -335,9 +335,10 @@ maxLineLengthForComment = 60
 
 lJust : (line:String) -> (fillPos:Nat) -> (filler:Char) -> String
 lJust line fillPos filler =
-    case isLTE (length line) fillPos of
+    let n = length line in
+    case isLTE n fillPos of
         (Yes prf) =>
-            let missing = minus fillPos (length line)
+            let missing = minus fillPos n
                 fillBlock = pack (replicate missing filler)
             in
             line ++ fillBlock

From 243ed5df2c39f559bfcf4e9aa42e5c3d8f659390 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:04:41 +0000
Subject: [PATCH 18/28] [ cleanup ] remove trailing "pure ()"

---
 src/Compiler/RefC/RefC.idr | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index e454413f6..f4d49191b 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -383,7 +383,6 @@ freeTmpVars = do
         (vars :: varss) => do
             traverse (\v => emit EmptyFC $ "removeReference(" ++ v ++ ");" ) vars
             put TemporaryVariableTracker varss
-            pure ()
         [] => pure ()
 
 
@@ -943,7 +942,6 @@ createCFunctions n (MkAFun args anf) = do
 
 createCFunctions n (MkACon tag arity) = do
   emit EmptyFC $ ( "// Constructor tag " ++ show tag ++ " arity " ++ show arity) -- Nothing to compile here
-  pure ()
 
 
 createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do
@@ -1046,7 +1044,6 @@ footer = do
     emit EmptyFC "   trampoline(mainExprVal);"
     emit EmptyFC "   return 0; // bye bye"
     emit EmptyFC "}"
-    pure ()
 
 export
 executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core ()

From 3c0ff432bdc1821d2a1f355e115eb3f9c30f9a78 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:05:24 +0000
Subject: [PATCH 19/28] [ cleanup ] redundant parens, language keyword

---
 src/Compiler/RefC/RefC.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index f4d49191b..11eddcd0d 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -411,7 +411,7 @@ makeArglist missing xs = do
     emit EmptyFC $  "Value_Arglist *"
                  ++ arglist
                  ++ " = newArglist(" ++ show missing
-                 ++ "," ++ show ((length xs) + missing)
+                 ++ "," ++ show (length xs + missing)
                  ++ ");"
     pushArgToArglist arglist xs 0
     pure arglist
@@ -434,9 +434,9 @@ fillConstructorArgs : {auto oft : Ref OutfileText (List String)}
                    -> Nat
                    -> Core ()
 fillConstructorArgs _ [] _ = pure ()
-fillConstructorArgs constructor (v :: vars) k = do
-    emit EmptyFC $ constructor ++ "->args["++ show k ++ "] = newReference(" ++ varName v ++");"
-    fillConstructorArgs constructor vars (S k)
+fillConstructorArgs cons (v :: vars) k = do
+    emit EmptyFC $ cons ++ "->args["++ show k ++ "] = newReference(" ++ varName v ++");"
+    fillConstructorArgs cons vars (S k)
 
 
 showTag : Maybe Int -> String

From 89daa5c1f60ffad6677a2d33d2184e01e1d69e12 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:06:28 +0000
Subject: [PATCH 20/28] [ cleanup ] existing list function & needlessly
 effectfule ones

---
 src/Compiler/RefC/RefC.idr | 27 +++++++++++----------------
 1 file changed, 11 insertions(+), 16 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index 11eddcd0d..e810fbd7a 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -799,9 +799,9 @@ functionDefSignatureArglist : {auto c : Ref Ctxt Defs} -> Name  -> Core String
 functionDefSignatureArglist n = pure $  "Value *"  ++ (cName !(getFullName n)) ++ "_arglist(Value_Arglist* arglist)"
 
 
-getArgsNrList : {0 ty:Type} -> List ty -> Nat -> Core $ List Nat
-getArgsNrList [] _ = pure []
-getArgsNrList (x :: xs) k = pure $ k :: !(getArgsNrList xs (S k))
+getArgsNrList : List ty -> Nat -> List Nat
+getArgsNrList [] _ = []
+getArgsNrList (x :: xs) k = k :: getArgsNrList xs (S k)
 
 
 cTypeOfCFType : CFType -> Core $ String
@@ -823,17 +823,15 @@ cTypeOfCFType (CFIORes x)     = pure $ "void *"
 cTypeOfCFType (CFStruct x ys) = pure $ "void *"
 cTypeOfCFType (CFUser x ys)   = pure $ "void *"
 
-varNamesFromList : {0 ty : Type} -> List ty -> Nat -> Core (List String)
-varNamesFromList [] _ = pure []
-varNamesFromList (x :: xs) k = pure $ ("var_" ++ show k) :: !(varNamesFromList xs (S k))
+varNamesFromList : List ty -> Nat -> List String
+varNamesFromList str k = map (("var_" ++) . show) (getArgsNrList str k)
 
 createFFIArgList : List CFType
                 -> Core $ List (String, String, CFType)
 createFFIArgList cftypeList = do
     sList <- traverse cTypeOfCFType cftypeList
-    varList <- varNamesFromList cftypeList 1
-    let z = zip3 sList varList cftypeList
-    pure z
+    let varList = varNamesFromList cftypeList 1
+    pure $ zip3 sList varList cftypeList
 
 emitFDef : {auto oft : Ref OutfileText (List String)}
         -> {auto il : Ref IndentLevel Nat}
@@ -888,12 +886,9 @@ packCFType (CFIORes x)     varName = packCFType x varName
 packCFType (CFStruct x xs) varName = "makeStruct(" ++ varName ++ ")"
 packCFType (CFUser x xs)   varName = "makeCustomUser(" ++ varName ++ ")"
 
-discardLastArgument : {0 ty:Type} -> List ty -> List ty
+discardLastArgument : List ty -> List ty
 discardLastArgument [] = []
-discardLastArgument (x :: []) = []
-discardLastArgument (x :: y :: ys) = x :: (discardLastArgument (y :: ys))
-
-
+discardLastArgument xs@(_ :: _) = init xs
 
 createCFunctions : {auto c : Ref Ctxt Defs}
                 -> {auto a : Ref ArgCounter Nat}
@@ -911,7 +906,7 @@ createCFunctions n (MkAFun args anf) = do
     otherDefs <- get FunctionDefinitions
     put FunctionDefinitions ((fn ++ ";\n") :: (fn' ++ ";\n") :: otherDefs)
     newTemporaryVariableLevel
-    argsNrs <- getArgsNrList args Z
+    let argsNrs = getArgsNrList args Z
     emit EmptyFC fn
     emit EmptyFC "{"
     increaseIndentation
@@ -964,7 +959,7 @@ createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do
           increaseIndentation
           emit EmptyFC $ "("
           increaseIndentation
-          let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") !(getArgsNrList fargs Z))
+          let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") (getArgsNrList fargs Z))
           traverse (emit EmptyFC) commaSepArglist
           decreaseIndentation
           emit EmptyFC ");"

From 0675e58ccabe0c58ef1ab5ba1d0f87b3aea7a5a8 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 18:07:19 +0000
Subject: [PATCH 21/28] [ error ] crash rather than generating garbage

---
 src/Compiler/RefC/RefC.idr | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index e810fbd7a..478ddc751 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -88,7 +88,8 @@ cName (Nested i n) = "n__" ++ cCleanString (show i) ++ "_" ++ cName n
 cName (CaseBlock x y) = "case__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
 cName (WithBlock x y) = "with__" ++ cCleanString (show x) ++ "_" ++ cCleanString (show y)
 cName (Resolved i) = "fn__" ++ cCleanString (show i)
-cName _ = "UNKNOWNNAME"
+cName n = assert_total $ idris_crash ("INTERNAL ERROR: Unsupported name in C backend " ++ show n)
+-- not really total but this way this internal error does not contaminate everything else
 
 escapeChar : Char -> String
 escapeChar '\DEL' = "127"
@@ -153,7 +154,6 @@ where
     showCString (c ::cs) = (showCChar c) . showCString cs
 
 
-
 cConstant : Constant -> String
 cConstant (I x) = "(Value*)makeInt32("++ show x ++")" -- (constant #:type 'i32 #:val " ++ show x ++ ")"
 cConstant (BI x) = "(Value*)makeInt64("++ show x ++")" --"(constant #:type 'i64 #:val " ++ show x ++ ")"
@@ -176,7 +176,8 @@ cConstant Bits8Type = "Bits8"
 cConstant Bits16Type = "Bits16"
 cConstant Bits32Type = "Bits32"
 cConstant Bits64Type = "Bits64"
-cConstant _ = "UNKNOWN"
+cConstant n = assert_total $ idris_crash ("INTERNAL ERROR: Unknonw constant in C backend: " ++ show n)
+-- not really total but this way this internal error does not contaminate everything else
 
 extractConstant : Constant -> String
 extractConstant (I x) = show x
@@ -284,7 +285,7 @@ toPrim pn@(NS _ n)
             (n == UN "prim__onCollectAny", OnCollectAny)
             ]
            (Unknown pn)
-toPrim pn = Unknown pn
+toPrim pn = Unknown pn -- todo: crash rather than generate garbage?
 
 
 varName : AVar -> String

From 5de647cc3fdf7ac1b95cacbeb47778e572ff7557 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Mon, 7 Dec 2020 17:23:13 +0000
Subject: [PATCH 22/28] [ refactor ] use difference list for efficient append

---
 idris2api.ipkg             |  1 +
 src/Compiler/RefC/RefC.idr | 68 +++++++++++++++++++++-----------------
 src/Data/DList.idr         | 40 ++++++++++++++++++++++
 3 files changed, 78 insertions(+), 31 deletions(-)
 create mode 100644 src/Data/DList.idr

diff --git a/idris2api.ipkg b/idris2api.ipkg
index 8d3caad98..36ab914cb 100644
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@@ -71,6 +71,7 @@ modules =
     Data.Bool.Extra,
 
     Data.List.Extra,
+    Data.DList,
 
     IdrisPaths,
 
diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr
index 478ddc751..4965e4e27 100644
--- a/src/Compiler/RefC/RefC.idr
+++ b/src/Compiler/RefC/RefC.idr
@@ -14,6 +14,7 @@ import Core.TT
 
 import Data.IORef
 import Data.List
+import Data.DList
 import Data.NameMap
 import Data.Nat
 import Data.Strings
@@ -295,10 +296,19 @@ varName (ANull)    = "NULL"
 data ArgCounter : Type where
 data FunctionDefinitions : Type where
 data TemporaryVariableTracker : Type where
-data OutfileText : Type where
 data IndentLevel : Type where
 data ExternalLibs : Type where
 
+------------------------------------------------------------------------
+-- Output generation: using a difference list for efficient append
+
+data OutfileText : Type where
+
+Output : Type
+Output = DList String
+
+------------------------------------------------------------------------
+
 getNextCounter : {auto a : Ref ArgCounter Nat} -> Core Nat
 getNextCounter = do
     c <- get ArgCounter
@@ -356,26 +366,24 @@ indentation = do
     iLevel <- get IndentLevel
     pure $ pack $ replicate (4 * iLevel) ' '
 
-
-emit : {auto oft : Ref OutfileText (List String)} -> {auto il : Ref IndentLevel Nat} -> FC -> String -> Core ()
+emit
+  : {auto oft : Ref OutfileText Output} ->
+    {auto il : Ref IndentLevel Nat} ->
+    FC -> String -> Core ()
 emit EmptyFC line = do
-    lines <- get OutfileText
     indent <- indentation
-    put OutfileText (lines ++ [indent ++ line])
-    pure ()
-emit fc line' = do
+    update OutfileText (flip snoc (indent ++ line))
+emit fc line = do
     let comment = "// " ++ show fc
-    lines <- get OutfileText
     indent <- indentation
-    let line = line'
-    case isLTE (length (indent ++ line)) maxLineLengthForComment of
-        (Yes _) => put OutfileText (lines ++ [ (lJust (indent ++ line) maxLineLengthForComment ' ') ++ " " ++ comment]        )
-        (No _)  => put OutfileText (lines ++ [indent ++ line, ((lJust ""   maxLineLengthForComment ' ') ++ " " ++ comment)] )
-    pure ()
+    let indentedLine = indent ++ line
+    update OutfileText $ case isLTE (length indentedLine) maxLineLengthForComment of
+        (Yes _) => flip snoc (lJust indentedLine maxLineLengthForComment ' ' ++ " " ++ comment)
+        (No _)  => flip appendR [indentedLine, (lJust ""   maxLineLengthForComment ' ' ++ " " ++ comment)]
 
 
 freeTmpVars : {auto t : Ref TemporaryVariableTracker (List (List String))}
-           -> {auto oft : Ref OutfileText (List String)}
+           -> {auto oft : Ref OutfileText Output}
            -> {auto il : Ref IndentLevel Nat}
            -> Core $ ()
 freeTmpVars = do
@@ -401,7 +409,7 @@ addExternalLib extLib = do
 
 makeArglist : {auto a : Ref ArgCounter Nat}
            -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-           -> {auto oft : Ref OutfileText (List String)}
+           -> {auto oft : Ref OutfileText Output}
            -> {auto il : Ref IndentLevel Nat}
            -> Nat
            -> List AVar
@@ -428,7 +436,7 @@ where
                     ++ " newReference(" ++ varName arg ++");"
         pushArgToArglist arglist args (S k)
 
-fillConstructorArgs : {auto oft : Ref OutfileText (List String)}
+fillConstructorArgs : {auto oft : Ref OutfileText Output}
                    -> {auto il : Ref IndentLevel Nat}
                    -> String
                    -> List AVar
@@ -495,7 +503,7 @@ record ReturnStatement where
 mutual
     copyConstructors : {auto a : Ref ArgCounter Nat}
                     -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-                    -> {auto oft : Ref OutfileText (List String)}
+                    -> {auto oft : Ref OutfileText Output}
                     -> {auto il : Ref IndentLevel Nat}
                     -> String
                     -> List AConAlt
@@ -518,7 +526,7 @@ mutual
 
     conBlocks : {auto a : Ref ArgCounter Nat}
              -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-             -> {auto oft : Ref OutfileText (List String)}
+             -> {auto oft : Ref OutfileText Output}
              -> {auto il : Ref IndentLevel Nat}
              -> (scrutinee:String)
              -> List AConAlt
@@ -550,7 +558,7 @@ mutual
 
     constBlockSwitch : {auto a : Ref ArgCounter Nat}
                        -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-                       -> {auto oft : Ref OutfileText (List String)}
+                       -> {auto oft : Ref OutfileText Output}
                        -> {auto il : Ref IndentLevel Nat}
                        -> (alts:List AConstAlt)
                        -> (retValVar:String)
@@ -575,7 +583,7 @@ mutual
 
     constDefaultBlock : {auto a : Ref ArgCounter Nat}
                      -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-                     -> {auto oft : Ref OutfileText (List String)}
+                     -> {auto oft : Ref OutfileText Output}
                      -> {auto il : Ref IndentLevel Nat}
                      -> (def:Maybe ANF)
                      -> (retValVar:String)
@@ -597,7 +605,7 @@ mutual
     makeNonIntSwitchStatementConst :
                     {auto a : Ref ArgCounter Nat}
                  -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-                 -> {auto oft : Ref OutfileText (List String)}
+                 -> {auto oft : Ref OutfileText Output}
                  -> {auto il : Ref IndentLevel Nat}
                  -> List AConstAlt
                  -> (k:Int)
@@ -631,7 +639,7 @@ mutual
 
     cStatementsFromANF : {auto a : Ref ArgCounter Nat}
                       -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-                      -> {auto oft : Ref OutfileText (List String)}
+                      -> {auto oft : Ref OutfileText Output}
                       -> {auto il : Ref IndentLevel Nat}
                       -> ANF
                       -> Core ReturnStatement
@@ -834,7 +842,7 @@ createFFIArgList cftypeList = do
     let varList = varNamesFromList cftypeList 1
     pure $ zip3 sList varList cftypeList
 
-emitFDef : {auto oft : Ref OutfileText (List String)}
+emitFDef : {auto oft : Ref OutfileText Output}
         -> {auto il : Ref IndentLevel Nat}
         -> (funcName:Name)
         -> (arglist:List (String, String, CFType))
@@ -895,7 +903,7 @@ createCFunctions : {auto c : Ref Ctxt Defs}
                 -> {auto a : Ref ArgCounter Nat}
                 -> {auto f : Ref FunctionDefinitions (List String)}
                 -> {auto t : Ref TemporaryVariableTracker (List (List String))}
-                -> {auto oft : Ref OutfileText (List String)}
+                -> {auto oft : Ref OutfileText Output}
                 -> {auto il : Ref IndentLevel Nat}
                 -> {auto e : Ref ExternalLibs (List String)}
                 -> Name
@@ -1014,7 +1022,7 @@ createCFunctions n (MkAError exp) = do
 
 
 header : {auto f : Ref FunctionDefinitions (List String)}
-      -> {auto o : Ref OutfileText (List String)}
+      -> {auto o : Ref OutfileText Output}
       -> {auto il : Ref IndentLevel Nat}
       -> {auto e : Ref ExternalLibs (List String)}
       -> Core ()
@@ -1026,11 +1034,9 @@ header = do
     let extLibLines = map (\lib => "// add header(s) for library: " ++ lib ++ "\n") extLibs
     traverse (\l => coreLift (putStrLn $ " header for " ++ l ++ " needed")) extLibs
     fns <- get FunctionDefinitions
-    outText <- get OutfileText
-    put OutfileText (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns ++ outText)
-    pure ()
+    update OutfileText (appendL (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns))
 
-footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText (List String)} -> Core ()
+footer : {auto il : Ref IndentLevel Nat} -> {auto f : Ref OutfileText Output} -> Core ()
 footer = do
     emit EmptyFC ""
     emit EmptyFC " // main function"
@@ -1067,14 +1073,14 @@ compileExpr ANF c _ outputDir tm outfile =
      newRef ArgCounter 0
      newRef FunctionDefinitions []
      newRef TemporaryVariableTracker []
-     newRef OutfileText []
+     newRef OutfileText DList.Nil
      newRef ExternalLibs []
      newRef IndentLevel 0
      traverse (\(n, d) => createCFunctions n d) defs
      header -- added after the definition traversal in order to add all encountered function defintions
      footer
      fileContent <- get OutfileText
-     let code = fastAppend (map (++ "\n") fileContent)
+     let code = fastAppend (map (++ "\n") (reify fileContent))
 
      coreLift (writeFile outn code)
      coreLift $ putStrLn $ "Generated C file " ++ outn
diff --git a/src/Data/DList.idr b/src/Data/DList.idr
new file mode 100644
index 000000000..8c295354d
--- /dev/null
+++ b/src/Data/DList.idr
@@ -0,0 +1,40 @@
+module Data.DList
+
+%default total
+
+-- Do not re-export the type so that it does not get unfolded in goals
+-- and error messages!
+export
+DList : Type -> Type
+DList a = List a -> List a
+
+export
+Nil : DList a
+Nil = id
+
+export
+(::) : a -> DList a -> DList a
+(::) a as = (a ::) . as
+
+export
+snoc : DList a -> a -> DList a
+snoc as a = as . (a ::)
+
+export
+appendR : DList a -> List a -> DList a
+appendR as bs = as . (bs ++)
+
+export
+appendL : List a -> DList a -> DList a
+appendL as bs = (as ++) . bs
+
+export
+(++) : DList a -> DList a -> DList a
+(++) = (.)
+
+export
+reify : DList a -> List a
+reify as = as []
+
+-- NB: No Functor instance because it's too expensive to reify, map, put back
+-- Consider using a different data structure if you need mapping (e.g. a rope)

From 0a685f8d2c512763e783fae0cbbd379fa09c3a26 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Thu, 10 Dec 2020 14:27:02 +0000
Subject: [PATCH 23/28] [ debug ] remove `max` from log

Users should be allowed to de-escalate the level of detail they're
getting.
---
 src/Core/Options/Log.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Core/Options/Log.idr b/src/Core/Options/Log.idr
index 56b1cee02..259801ac4 100644
--- a/src/Core/Options/Log.idr
+++ b/src/Core/Options/Log.idr
@@ -116,7 +116,7 @@ defaultLogLevel = singleton [] 0
 
 export
 insertLogLevel : LogLevel -> LogLevels -> LogLevels
-insertLogLevel (MkLogLevel ps n) = insertWith ps (maybe n (max n))
+insertLogLevel (MkLogLevel ps n) = insert ps n
 
 ----------------------------------------------------------------------------------
 -- CHECKING WHETHER TO LOG

From 40258965725bf50be632764fe7701244e86cdd74 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Thu, 10 Dec 2020 17:09:16 +0000
Subject: [PATCH 24/28] [ fix #833, #677 ] bound variables start with a
 lowercase letter

---
 src/Idris/Desugar.idr              | 10 ++++++++--
 tests/Main.idr                     |  1 +
 tests/idris2/basic051/Issue833.idr | 17 +++++++++++++++++
 tests/idris2/basic051/expected     |  1 +
 tests/idris2/basic051/run          |  3 +++
 5 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 tests/idris2/basic051/Issue833.idr
 create mode 100644 tests/idris2/basic051/expected
 create mode 100755 tests/idris2/basic051/run

diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 5bd0007c5..34ab619cd 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -26,6 +26,7 @@ import TTImp.TTImp
 import TTImp.Utils
 
 import Utils.Shunting
+import Utils.String
 
 import Control.Monad.State
 import Data.List
@@ -149,10 +150,15 @@ mutual
             pure $ IPi fc rig !(traverse (desugar side ps') p)
                               mn !(desugarB side ps argTy)
                                  !(desugarB side ps' retTy)
-  desugarB side ps (PLam fc rig p (PRef _ n@(UN _)) argTy scope)
-      = pure $ ILam fc rig !(traverse (desugar side ps) p)
+  desugarB side ps (PLam fc rig p pat@(PRef _ n@(UN nm)) argTy scope)
+      =  if lowerFirst nm || nm == "_"
+           then pure $ ILam fc rig !(traverse (desugar side ps) p)
                            (Just n) !(desugarB side ps argTy)
                                     !(desugar side (n :: ps) scope)
+           else pure $ ILam fc rig !(traverse (desugar side ps) p)
+                   (Just (MN "lamc" 0)) !(desugarB side ps argTy) $
+                 ICase fc (IVar fc (MN "lamc" 0)) (Implicit fc False)
+                     [!(desugarClause ps True (MkPatClause fc pat scope []))]
   desugarB side ps (PLam fc rig p (PRef _ n@(MN _ _)) argTy scope)
       = pure $ ILam fc rig !(traverse (desugar side ps) p)
                            (Just n) !(desugarB side ps argTy)
diff --git a/tests/Main.idr b/tests/Main.idr
index aa1aa17a7..adf0b792f 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -45,6 +45,7 @@ idrisTests = MkTestPool []
        "basic036", "basic037", "basic038", "basic039", "basic040",
        "basic041", "basic042", "basic043", "basic044", "basic045",
        "basic046", "basic047", "basic048", "basic049", "basic050",
+       "basic051",
        -- Coverage checking
        "coverage001", "coverage002", "coverage003", "coverage004",
        "coverage005", "coverage006", "coverage007", "coverage008",
diff --git a/tests/idris2/basic051/Issue833.idr b/tests/idris2/basic051/Issue833.idr
new file mode 100644
index 000000000..35c3e27d9
--- /dev/null
+++ b/tests/idris2/basic051/Issue833.idr
@@ -0,0 +1,17 @@
+module Issue833
+
+import Data.Fin
+
+%default total
+
+data Singleton : Nat -> Type where
+  Sing : {n : Nat} -> Singleton n
+
+f : (n : Singleton Z) -> n === Sing
+f = \ Sing => Refl
+
+g : (k : Fin 1) -> k === FZ
+g = \ FZ => Refl
+
+sym : {t, u : a} -> t === u -> u === t
+sym = \Refl => Refl
diff --git a/tests/idris2/basic051/expected b/tests/idris2/basic051/expected
new file mode 100644
index 000000000..dd1237c35
--- /dev/null
+++ b/tests/idris2/basic051/expected
@@ -0,0 +1 @@
+1/1: Building Issue833 (Issue833.idr)
diff --git a/tests/idris2/basic051/run b/tests/idris2/basic051/run
new file mode 100755
index 000000000..b49e559db
--- /dev/null
+++ b/tests/idris2/basic051/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner --check Issue833.idr
+
+rm -rf build

From 4356d377c5df40a82be196e00abe622305d24fb7 Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Thu, 10 Dec 2020 17:10:36 +0000
Subject: [PATCH 25/28] [ refactor ] parser for lambda & lambdacase

---
 src/Idris/Parser.idr | 47 ++++++++++++++++++++++++--------------------
 1 file changed, 26 insertions(+), 21 deletions(-)

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 82382942b..f3549057b 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -116,7 +116,7 @@ mutual
   appExpr q fname indents
       = case_ fname indents
     <|> doBlock fname indents
-    <|> lambdaCase fname indents
+    <|> lam fname indents
     <|> lazy fname indents
     <|> if_ fname indents
     <|> with_ fname indents
@@ -537,18 +537,38 @@ mutual
   lam : FileName -> IndentInfo -> Rule PTerm
   lam fname indents
       = do symbol "\\"
-           binders <- bindList fname indents
-           symbol "=>"
-           mustContinue indents Nothing
-           scope <- expr pdef fname indents
-           pure (bindAll binders scope)
+           commit
+           switch <- optional (bounds $ keyword "case")
+           case switch of
+             Nothing => continueLam
+             Just r  => continueLamCase r
+
      where
+
        bindAll : List (RigCount, WithBounds PTerm, PTerm) -> PTerm -> PTerm
        bindAll [] scope = scope
        bindAll ((rig, pat, ty) :: rest) scope
            = PLam (boundToFC fname pat) rig Explicit pat.val ty
                   (bindAll rest scope)
 
+       continueLam : Rule PTerm
+       continueLam = do
+           binders <- bindList fname indents
+           symbol "=>"
+           mustContinue indents Nothing
+           scope <- expr pdef fname indents
+           pure (bindAll binders scope)
+
+       continueLamCase : WithBounds () -> Rule PTerm
+       continueLamCase endCase = do
+           b <- bounds (forget <$> nonEmptyBlock (caseAlt fname))
+           pure
+            (let fc = boundToFC fname b
+                 fcCase = boundToFC fname endCase
+                 n = MN "lcase" 0 in
+              PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
+                PCase fc (PRef fcCase n) b.val)
+
   letBlock : FileName -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
   letBlock fname indents = bounds (letBinder <||> letDecl) where
 
@@ -585,20 +605,6 @@ mutual
            (scr, alts) <- pure b.val
            pure (PCase (boundToFC fname b) scr alts)
 
-  lambdaCase : FileName -> IndentInfo -> Rule PTerm
-  lambdaCase fname indents
-      = do b <- bounds (do endCase <- bounds (symbol "\\" *> keyword "case")
-                           commit
-                           alts <- block (caseAlt fname)
-                           pure (endCase, alts))
-           (endCase, alts) <- pure b.val
-           pure $
-            (let fc = boundToFC fname b
-                 fcCase = boundToFC fname endCase
-                 n = MN "lcase" 0 in
-              PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
-                PCase fc (PRef fcCase n) alts)
-
   caseAlt : FileName -> IndentInfo -> Rule PClause
   caseAlt fname indents
       = do lhs <- bounds (opExpr plhs fname indents)
@@ -742,7 +748,6 @@ mutual
     <|> implicitPi fname indents
     <|> explicitPi fname indents
     <|> lam fname indents
-    <|> lambdaCase fname indents
 
   typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
   typeExpr q fname indents

From 88aa55e875ce92e2133cfb7d95c31efe6938b4f5 Mon Sep 17 00:00:00 2001
From: Dong Tsing-hsuen <68433824+alissa42@users.noreply.github.com>
Date: Fri, 11 Dec 2020 02:04:23 +0800
Subject: [PATCH 26/28] [ new ] null method in Foldable (#832)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
---
 libs/base/Control/Monad/Either.idr   | 2 ++
 libs/base/Data/List1.idr             | 1 +
 libs/base/Data/Vect.idr              | 3 +++
 libs/contrib/Data/SortedMap.idr      | 8 +++-----
 libs/contrib/Data/SortedSet.idr      | 6 ++----
 libs/prelude/Prelude/Interfaces.idr  | 3 +++
 libs/prelude/Prelude/Types.idr       | 7 +++++++
 tests/typedd-book/chapter07/Tree.idr | 3 +++
 8 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/libs/base/Control/Monad/Either.idr b/libs/base/Control/Monad/Either.idr
index 231e90ad5..979a228e6 100644
--- a/libs/base/Control/Monad/Either.idr
+++ b/libs/base/Control/Monad/Either.idr
@@ -112,6 +112,8 @@ Foldable m => Foldable (EitherT e m) where
   foldr f acc (MkEitherT e)
     = foldr (\x,xs => either (const acc) (`f` xs) x) acc e
 
+  null (MkEitherT e) = null e
+
 public export
 Traversable m => Traversable (EitherT e m) where
   traverse f (MkEitherT x)
diff --git a/libs/base/Data/List1.idr b/libs/base/Data/List1.idr
index 5644c9d1e..c6a4d2fc4 100644
--- a/libs/base/Data/List1.idr
+++ b/libs/base/Data/List1.idr
@@ -117,6 +117,7 @@ Monad List1 where
 export
 Foldable List1 where
   foldr c n (x ::: xs) = c x (foldr c n xs)
+  null _ = False
 
 export
 Show a => Show (List1 a) where
diff --git a/libs/base/Data/Vect.idr b/libs/base/Data/Vect.idr
index f9894c944..463928334 100644
--- a/libs/base/Data/Vect.idr
+++ b/libs/base/Data/Vect.idr
@@ -407,6 +407,9 @@ public export
 implementation Foldable (Vect n) where
   foldr f e xs = foldrImpl f e id xs
 
+  null [] = True
+  null _ = False
+
 --------------------------------------------------------------------------------
 -- Special folds
 --------------------------------------------------------------------------------
diff --git a/libs/contrib/Data/SortedMap.idr b/libs/contrib/Data/SortedMap.idr
index 0bc95955a..00f672cb4 100644
--- a/libs/contrib/Data/SortedMap.idr
+++ b/libs/contrib/Data/SortedMap.idr
@@ -254,11 +254,6 @@ export
 values : SortedMap k v -> List v
 values = map snd . toList
 
-export
-null : SortedMap k v -> Bool
-null Empty = True
-null (M _ _) = False
-
 treeMap : (a -> b) -> Tree n k a o -> Tree n k b o
 treeMap f (Leaf k v) = Leaf k (f v)
 treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
@@ -289,6 +284,9 @@ export
 implementation Foldable (SortedMap k) where
   foldr f z = foldr f z . values
 
+  null Empty = True
+  null (M _ _) = False
+
 export
 implementation Traversable (SortedMap k) where
   traverse _ Empty = pure Empty
diff --git a/libs/contrib/Data/SortedSet.idr b/libs/contrib/Data/SortedSet.idr
index 9346c8816..06575ce56 100644
--- a/libs/contrib/Data/SortedSet.idr
+++ b/libs/contrib/Data/SortedSet.idr
@@ -34,6 +34,8 @@ export
 Foldable SortedSet where
   foldr f e xs = foldr f e (Data.SortedSet.toList xs)
 
+  null (SetWrapper m) = null m
+
 ||| Set union. Inserts all elements of x into y
 export
 union : (x, y : SortedSet k) -> SortedSet k
@@ -69,7 +71,3 @@ keySet = SetWrapper . map (const ())
 export
 singleton : Ord k => k -> SortedSet k
 singleton k = insert k empty
-
-export
-null : SortedSet k -> Bool
-null (SetWrapper m) = SortedMap.null m
diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr
index d49f9ef61..f4a74292f 100644
--- a/libs/prelude/Prelude/Interfaces.idr
+++ b/libs/prelude/Prelude/Interfaces.idr
@@ -217,6 +217,9 @@ interface Foldable (t : Type -> Type) where
   foldl : (func : acc -> elem -> acc) -> (init : acc) -> (input : t elem) -> acc
   foldl f z t = foldr (flip (.) . flip f) id t z
 
+  ||| Test whether the structure is empty.
+  null : t elem -> Bool
+
 ||| Similar to `foldl`, but uses a function wrapping its result in a `Monad`.
 ||| Consequently, the final value is wrapped in the same `Monad`.
 public export
diff --git a/libs/prelude/Prelude/Types.idr b/libs/prelude/Prelude/Types.idr
index 5b496d5ac..9fe9e2cba 100644
--- a/libs/prelude/Prelude/Types.idr
+++ b/libs/prelude/Prelude/Types.idr
@@ -180,6 +180,8 @@ public export
 Foldable Maybe where
   foldr _ z Nothing  = z
   foldr f z (Just x) = f x z
+  null Nothing = True
+  null (Just _) = False
 
 public export
 Traversable Maybe where
@@ -272,6 +274,8 @@ public export
 Foldable (Either e) where
   foldr f acc (Left _) = acc
   foldr f acc (Right x) = f x acc
+  null (Left _) = True
+  null (Right _) = False
 
 public export
 Traversable (Either e) where
@@ -341,6 +345,9 @@ Foldable List where
   foldl f q [] = q
   foldl f q (x::xs) = foldl f (f q x) xs
 
+  null [] = True
+  null (_::_) = False
+
 public export
 Applicative List where
   pure x = [x]
diff --git a/tests/typedd-book/chapter07/Tree.idr b/tests/typedd-book/chapter07/Tree.idr
index e946bbd8f..2f838244c 100644
--- a/tests/typedd-book/chapter07/Tree.idr
+++ b/tests/typedd-book/chapter07/Tree.idr
@@ -19,3 +19,6 @@ Foldable Tree where
   foldr f acc (Node left e right) = let leftfold = foldr f acc left
                                         rightfold = foldr f leftfold right in
                                         f e rightfold
+
+  null Empty = True
+  null _ = False

From 3f6b99e97971dd6dc5c6a6921d748569be20d091 Mon Sep 17 00:00:00 2001
From: "G. Allais" <guillaume.allais@ens-lyon.org>
Date: Fri, 11 Dec 2020 11:58:26 +0000
Subject: [PATCH 27/28] [ fix #657 ] RigCount for interface parameters (#808)

---
 docs/source/tutorial/interfaces.rst        | 55 ++++++++++++++++--
 libs/base/Control/Monad/Reader.idr         |  2 +-
 libs/base/Control/Monad/State.idr          |  2 +-
 libs/base/Control/Monad/Trans.idr          |  3 +-
 libs/base/Control/WellFounded.idr          |  6 +-
 libs/base/Data/Fin/Order.idr               |  4 +-
 libs/base/Data/Nat/Order.idr               |  2 +-
 libs/base/Data/Ref.idr                     |  6 +-
 libs/base/Decidable/Decidable.idr          |  8 +--
 libs/base/Decidable/Order.idr              | 23 ++++----
 libs/contrib/Data/HVect.idr                |  4 +-
 libs/contrib/Decidable/Decidable/Extra.idr | 27 +++++----
 libs/contrib/Decidable/Order/Strict.idr    | 21 ++++---
 libs/contrib/Text/Token.idr                |  2 +-
 libs/prelude/Prelude/Interfaces.idr        |  5 +-
 src/Core/Core.idr                          |  4 +-
 src/Core/Normalise.idr                     |  8 +--
 src/Core/TT.idr                            |  4 +-
 src/Core/Unify.idr                         |  4 +-
 src/Idris/Desugar.idr                      | 27 +++++----
 src/Idris/Elab/Implementation.idr          | 34 +++++++----
 src/Idris/Elab/Interface.idr               | 67 +++++++++++++---------
 src/Idris/Parser.idr                       | 17 +++---
 src/Idris/Syntax.idr                       |  6 +-
 src/TTImp/Utils.idr                        |  6 +-
 src/Text/Token.idr                         |  2 +-
 tests/Main.idr                             |  2 +-
 tests/idris2/basic013/Implicits.idr        |  2 +-
 tests/idris2/interface003/Do.idr           |  3 +-
 tests/idris2/interface004/Do.idr           |  3 +-
 tests/idris2/interface006/Apply.idr        |  2 +-
 tests/idris2/interface006/Bimonad.idr      |  2 +-
 tests/idris2/interface018/Sized.idr        | 26 +++++++++
 tests/idris2/interface018/Sized2.idr       | 18 ++++++
 tests/idris2/interface018/Sized3.idr       | 20 +++++++
 tests/idris2/interface018/expected         |  7 +++
 tests/idris2/interface018/input            |  3 +
 tests/idris2/interface018/run              |  5 ++
 tests/idris2/reg029/lqueue.idr             | 12 ++--
 39 files changed, 299 insertions(+), 155 deletions(-)
 create mode 100644 tests/idris2/interface018/Sized.idr
 create mode 100644 tests/idris2/interface018/Sized2.idr
 create mode 100644 tests/idris2/interface018/Sized3.idr
 create mode 100644 tests/idris2/interface018/expected
 create mode 100644 tests/idris2/interface018/input
 create mode 100755 tests/idris2/interface018/run

diff --git a/docs/source/tutorial/interfaces.rst b/docs/source/tutorial/interfaces.rst
index fe595df38..1f19c6dc7 100644
--- a/docs/source/tutorial/interfaces.rst
+++ b/docs/source/tutorial/interfaces.rst
@@ -177,6 +177,50 @@ interface declaration, it elaborates the interface header but none of the
 method types on the first pass, and elaborates the method types and any
 default definitions on the second pass.
 
+Quantities for Parameters
+=========================
+
+By default parameters that are not explicitly ascribed a type in an ``interface``
+declaration are assigned the quantity ``0``. This means that the parameter is not
+available to use at runtime in the methods' definitions.
+
+For instance, ``Show a`` gives rise to a ``0``-quantified type variable ``a`` in
+the type of the ``show`` method:
+
+::
+
+     Main> :set showimplicits
+     Main> :t show
+     Prelude.show : {0 a : Type} -> Show a => a -> String
+
+However some use cases require that some of the parameters are available at runtime.
+We may for instance want to declare an interface for ``Storable`` types. The constraint
+``Storable a size`` means that we can store values of type ``a`` in a ``Buffer`` in
+exactly ``size`` bytes.
+
+If the user provides a method to read a value for such a type ``a`` at a given offset,
+then we can read the ``k``th element stored in the buffer by computing the appropriate
+offset from ``k`` and ``size``. This is demonstrated by providing a default implementation
+for the method ``peekElementOff`` implemented in terms of ``peekByteOff`` and the parameter
+``size``.
+
+.. code-block:: idris
+
+    data ForeignPtr : Type -> Type where
+      MkFP : Buffer -> ForeignPtr a
+
+    interface Storable (0 a : Type) (size : Nat) | a where
+      peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
+
+      peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
+      peekElemOff fp k = peekByteOff fp (k * cast size)
+
+
+Note that ``a`` is explicitly marked as runtime irrelevant so that it is erased by the
+compiler. Equivalently we could have written ``interface Sotrable a (size : Nat)``.
+The meaning of ``| a`` is explained in :ref:`DeterminingParameters`.
+
+
 Functors and Applicatives
 =========================
 
@@ -189,9 +233,10 @@ prelude:
 
 .. code-block:: idris
 
-    interface Functor (f : Type -> Type) where
+    interface Functor (0 f : Type -> Type) where
         map : (m : a -> b) -> f a -> f b
 
+
 A functor allows a function to be applied across a structure, for
 example to apply a function to every element in a ``List``:
 
@@ -213,7 +258,7 @@ abstracts the notion of function application:
 
     infixl 2 <*>
 
-    interface Functor f => Applicative (f : Type -> Type) where
+    interface Functor f => Applicative (0 f : Type -> Type) where
         pure  : a -> f a
         (<*>) : f (a -> b) -> f a -> f b
 
@@ -410,7 +455,7 @@ has an implementation of both ``Monad`` and ``Alternative``:
 
 .. code-block:: idris
 
-    interface Applicative f => Alternative (f : Type -> Type) where
+    interface Applicative f => Alternative (0 f : Type -> Type) where
         empty : f a
         (<|>) : f a -> f a -> f a
 
@@ -670,6 +715,8 @@ do this with a ``using`` clause in the implementation as follows:
 The ``using PlusNatSemi`` clause indicates that ``PlusNatMonoid`` should
 extend ``PlusNatSemi`` specifically.
 
+.. _DeterminingParameters:
+
 Determining Parameters
 ======================
 
@@ -678,7 +725,7 @@ parameters used to find an implementation are restricted. For example:
 
 .. code-block:: idris
 
-    interface Monad m => MonadState s (m : Type -> Type) | m where
+    interface Monad m => MonadState s (0 m : Type -> Type) | m where
       get : m s
       put : s -> m ()
 
diff --git a/libs/base/Control/Monad/Reader.idr b/libs/base/Control/Monad/Reader.idr
index db27f4e00..65ecb90eb 100644
--- a/libs/base/Control/Monad/Reader.idr
+++ b/libs/base/Control/Monad/Reader.idr
@@ -5,7 +5,7 @@ import Control.Monad.Trans
 
 ||| A computation which runs in a static context and produces an output
 public export
-interface Monad m => MonadReader stateType (m : Type -> Type) | m where
+interface Monad m => MonadReader stateType m | m where
   ||| Get the context
   ask : m stateType
 
diff --git a/libs/base/Control/Monad/State.idr b/libs/base/Control/Monad/State.idr
index 42da4a7fc..c47246ca3 100644
--- a/libs/base/Control/Monad/State.idr
+++ b/libs/base/Control/Monad/State.idr
@@ -5,7 +5,7 @@ import public Control.Monad.Trans
 
 ||| A computation which runs in a context and produces an output
 public export
-interface Monad m => MonadState stateType (m : Type -> Type) | m where
+interface Monad m => MonadState stateType m | m where
     ||| Get the context
     get : m stateType
     ||| Write a new context/output
diff --git a/libs/base/Control/Monad/Trans.idr b/libs/base/Control/Monad/Trans.idr
index c8342c35e..701ac7a86 100644
--- a/libs/base/Control/Monad/Trans.idr
+++ b/libs/base/Control/Monad/Trans.idr
@@ -1,6 +1,5 @@
 module Control.Monad.Trans
 
 public export
-interface MonadTrans (t : (Type -> Type) -> Type -> Type) where
+interface MonadTrans t where
     lift : Monad m => m a -> t m a
-
diff --git a/libs/base/Control/WellFounded.idr b/libs/base/Control/WellFounded.idr
index a270b3636..7a850532c 100644
--- a/libs/base/Control/WellFounded.idr
+++ b/libs/base/Control/WellFounded.idr
@@ -9,7 +9,7 @@ data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
            Accessible rel x
 
 public export
-interface WellFounded (rel : a -> a -> Type) where
+interface WellFounded a rel where
   wellFounded : (x : a) -> Accessible rel x
 
 export
@@ -27,13 +27,13 @@ accInd step z (Access f) =
   step z $ \y, lt => accInd step y (f y lt)
 
 export
-wfRec : WellFounded rel =>
+wfRec : WellFounded a rel =>
         (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
         a -> b
 wfRec step x = accRec step x (wellFounded {rel} x)
 
 export
-wfInd : WellFounded rel => {0 P : a -> Type} ->
+wfInd : WellFounded a rel => {0 P : a -> Type} ->
         (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
         (myz : a) -> P myz
 wfInd step myz = accInd step myz (wellFounded {rel} myz)
diff --git a/libs/base/Data/Fin/Order.idr b/libs/base/Data/Fin/Order.idr
index e675ee5b1..ce02034ed 100644
--- a/libs/base/Data/Fin/Order.idr
+++ b/libs/base/Data/Fin/Order.idr
@@ -11,7 +11,7 @@ import Decidable.Order
 
 using (k : Nat)
   data FinLTE : Fin k -> Fin k -> Type where
-    FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
+    FromNatPrf : {m, n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n
 
   implementation Preorder (Fin k) FinLTE where
     transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
@@ -22,7 +22,7 @@ using (k : Nat)
     antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
       finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)
 
-  implementation Decidable [Fin k, Fin k] FinLTE where
+  implementation Decidable 2 [Fin k, Fin k] FinLTE where
     decide m n with (decideLTE (finToNat m) (finToNat n))
       decide m n | Yes prf    = Yes (FromNatPrf prf)
       decide m n | No  disprf = No (\ (FromNatPrf prf) => disprf prf)
diff --git a/libs/base/Data/Nat/Order.idr b/libs/base/Data/Nat/Order.idr
index b5958cefe..b5458cd2e 100644
--- a/libs/base/Data/Nat/Order.idr
+++ b/libs/base/Data/Nat/Order.idr
@@ -62,7 +62,7 @@ decideLTE (S x)   (S y) with (decEq (S x) (S y))
   decideLTE (S x)   (S y) | No _   | No  nGTm  = No (ltesuccinjective nGTm)
 
 public export
-implementation Decidable [Nat,Nat] LTE where
+implementation Decidable 2 [Nat,Nat] LTE where
   decide = decideLTE
 
 public export
diff --git a/libs/base/Data/Ref.idr b/libs/base/Data/Ref.idr
index 153240afa..a8774db64 100644
--- a/libs/base/Data/Ref.idr
+++ b/libs/base/Data/Ref.idr
@@ -4,9 +4,9 @@ import public Data.IORef
 import public Control.Monad.ST
 
 public export
-interface Ref m (r : Type -> Type) | m where
-  newRef : a -> m (r a)
-  readRef : r a -> m a
+interface Ref m r | m where
+  newRef : {0 a : Type} -> a -> m (r a)
+  readRef : {0 a : Type} -> r a -> m a
   writeRef : r a -> a -> m ()
 
 export
diff --git a/libs/base/Decidable/Decidable.idr b/libs/base/Decidable/Decidable.idr
index 41e375ff8..3ced56056 100644
--- a/libs/base/Decidable/Decidable.idr
+++ b/libs/base/Decidable/Decidable.idr
@@ -3,16 +3,14 @@ module Decidable.Decidable
 import Data.Rel
 import Data.Fun
 
-
-
 ||| Interface for decidable n-ary Relations
 public export
-interface Decidable (ts : Vect k Type) (p : Rel ts) where
-  total decide : liftRel ts p Dec
+interface Decidable k ts p where
+  total decide : liftRel (the (Vect k Type) ts) (the (Rel ts) p) Dec
 
 ||| Given a `Decidable` n-ary relation, provides a decision procedure for
 ||| this relation.
-decision : (ts : Vect k Type) -> (p : Rel ts) -> (Decidable ts p) => liftRel ts p Dec
+decision : (ts : Vect k Type) -> (p : Rel ts) -> (Decidable k ts p) => liftRel ts p Dec
 decision ts p = decide {ts} {p}
 
 using (a : Type, x : a)
diff --git a/libs/base/Decidable/Order.idr b/libs/base/Decidable/Order.idr
index 3fceb31ad..b72f462af 100644
--- a/libs/base/Decidable/Order.idr
+++ b/libs/base/Decidable/Order.idr
@@ -17,28 +17,25 @@ import Data.Rel
 --------------------------------------------------------------------------------
 
 public export
-interface Preorder t (po : t -> t -> Type) where
-  total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
+interface Preorder t po where
+  total transitive : (a, b, c : t) -> po a b -> po b c -> po a c
   total reflexive : (a : t) -> po a a
 
 public export
-interface (Preorder t po) => Poset t (po : t -> t -> Type) where
-  total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
+interface (Preorder t po) => Poset t po where
+  total antisymmetric : (a, b : t) -> po a b -> po b a -> a = b
 
 public export
-interface (Poset t to) => Ordered t (to : t -> t -> Type) where
-  total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
+interface (Poset t to) => Ordered t to where
+  total order : (a, b : t) -> Either (to a b) (to b a)
 
 public export
-interface (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
-  total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a
+interface (Preorder t eq) => Equivalence t eq where
+  total symmetric : (a, b : t) -> eq a b -> eq b a
 
 public export
-interface (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
-  total congruent : (a : t) ->
-                    (b : t) ->
-                    eq a b ->
-                    eq (f a) (f b)
+interface (Equivalence t eq) => Congruence t f eq where
+  total congruent : (a, b : t) -> eq a b -> eq (f a) (f b)
 
 public export
 minimum : (Ordered t to) => t -> t -> t
diff --git a/libs/contrib/Data/HVect.idr b/libs/contrib/Data/HVect.idr
index 469e9dffe..dd13ad418 100644
--- a/libs/contrib/Data/HVect.idr
+++ b/libs/contrib/Data/HVect.idr
@@ -99,8 +99,8 @@ public export
     decEq (x :: xs) (y :: ys) | No contra = No (contra . consInjective1)
 
 public export
-interface Shows (k : Nat) (ts : Vect k Type) where
-  shows : HVect ts -> Vect k String
+interface Shows k ts where
+  shows : HVect {k} ts -> Vect k String
 
 public export
 Shows Z [] where
diff --git a/libs/contrib/Decidable/Decidable/Extra.idr b/libs/contrib/Decidable/Decidable/Extra.idr
index e8fe02f72..5e6c2bef4 100644
--- a/libs/contrib/Decidable/Decidable/Extra.idr
+++ b/libs/contrib/Decidable/Decidable/Extra.idr
@@ -9,26 +9,26 @@ import Decidable.Decidable
 
 public export
 NotNot : {n : Nat} -> {ts : Vect n Type} -> (r : Rel ts) -> Rel ts
-NotNot r = map @{Nary} (Not . Not) r 
+NotNot r = map @{Nary} (Not . Not) r
 
-[DecidablePartialApplication] {x : t} -> (tts : Decidable (t :: ts) r) => Decidable ts (r x) where
+[DecidablePartialApplication] {x : t} -> (tts : Decidable (S n) (t :: ts) r) => Decidable n ts (r x) where
   decide = decide @{tts} x
 
 public export
-doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
-  (witness : HVect ts) -> 
-  uncurry (NotNot {ts} r) witness -> 
+doubleNegationElimination : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
+  (witness : HVect ts) ->
+  uncurry (NotNot {ts} r) witness ->
   uncurry              r  witness
-doubleNegationElimination {ts = []     } @{dec} [] prfnn = 
+doubleNegationElimination {ts = []     } @{dec} [] prfnn =
   case decide @{dec} of
     Yes prf   => prf
     No  prfn => absurd $ prfnn prfn
-doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn = 
+doubleNegationElimination {ts = t :: ts} @{dec} (w :: witness) prfnn =
   doubleNegationElimination {ts} {r = r w} @{ DecidablePartialApplication @{dec} } witness prfnn
 
-doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
+doubleNegationForall : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
   All ts (NotNot {ts} r) -> All ts r
-doubleNegationForall @{dec} forall_prf = 
+doubleNegationForall @{dec} forall_prf =
   let prfnn : (witness : HVect ts) -> uncurry (NotNot {ts} r) witness
       prfnn = uncurryAll forall_prf
       prf   : (witness : HVect ts) -> uncurry              r  witness
@@ -36,15 +36,14 @@ doubleNegationForall @{dec} forall_prf =
   in curryAll prf
 
 public export
-doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable ts r =>
-  Ex ts (NotNot {ts} r) -> 
+doubleNegationExists : {n : Nat} -> {0 ts : Vect n Type} -> {r : Rel ts} -> Decidable n ts r =>
+  Ex ts (NotNot {ts} r) ->
   Ex ts r
-doubleNegationExists {ts} {r} @{dec} nnxs = 
+doubleNegationExists {ts} {r} @{dec} nnxs =
   let witness : HVect ts
-      witness = extractWitness nnxs 
+      witness = extractWitness nnxs
       witnessingnn : uncurry (NotNot {ts} r) witness
       witnessingnn = extractWitnessCorrect nnxs
       witnessing   : uncurry              r  witness
       witnessing   = doubleNegationElimination @{dec} witness witnessingnn
   in introduceWitness witness witnessing
-
diff --git a/libs/contrib/Decidable/Order/Strict.idr b/libs/contrib/Decidable/Order/Strict.idr
index 611166591..23ab4a6a0 100644
--- a/libs/contrib/Decidable/Order/Strict.idr
+++ b/libs/contrib/Decidable/Order/Strict.idr
@@ -12,13 +12,13 @@ import Decidable.Equality
 %default total
 
 public export
-interface StrictPreorder t (spo : t -> t -> Type) where
+interface StrictPreorder t spo where
   transitive : (a, b, c : t) -> a `spo` b -> b `spo` c -> a `spo` c
   irreflexive : (a : t) -> Not (a `spo` a)
-  
+
 public export
 asymmetric : StrictPreorder t spo => (a, b : t) -> a `spo` b -> Not (b `spo` a)
-asymmetric a b aLTb bLTa = irreflexive a $ 
+asymmetric a b aLTb bLTa = irreflexive a $
                            Strict.transitive a b a aLTb bLTa
 
 public export
@@ -35,10 +35,10 @@ public export
 
 [MkPoset] {antisym : (a,b : t) -> a `leq` b -> b `leq` a -> a = b} -> Preorder t leq => Poset t leq where
   antisymmetric = antisym
-           
+
 %hint
 public export
-InferPoset : {t : Type} -> {spo : t -> t -> Type} -> StrictPreorder t spo => Poset t (EqOr spo) 
+InferPoset : {t : Type} -> {spo : t -> t -> Type} -> StrictPreorder t spo => Poset t (EqOr spo)
 InferPoset {t} {spo} = MkPoset @{MkPreorder} {antisym = antisym}
   where
     antisym : (a,b : t) -> EqOr spo a b -> EqOr spo b a -> a = b
@@ -51,11 +51,11 @@ public export
 data DecOrdering : {lt : t -> t -> Type} -> (a,b : t) -> Type where
   DecLT : forall lt . (a `lt` b) -> DecOrdering {lt = lt} a b
   DecEQ : forall lt . (a  =   b) -> DecOrdering {lt = lt} a b
-  DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b 
+  DecGT : forall lt . (b `lt` a) -> DecOrdering {lt = lt} a b
 
 public export
-interface StrictPreorder t spo => StrictOrdered t (spo : t -> t -> Type) where
-  order : (a,b : t) -> DecOrdering {lt = spo} a b 
+interface StrictPreorder t spo => StrictOrdered t spo where
+  order : (a,b : t) -> DecOrdering {lt = spo} a b
 
 [MkOrdered] {ord : (a,b : t) -> Either (a `leq` b) (b `leq` a)} -> Poset t leq => Ordered t leq where
   order = ord
@@ -76,9 +76,8 @@ public export
 (tot : StrictOrdered t lt) => (pre : StrictPreorder t lt) => DecEq t where
   decEq x y = case order @{tot} x y of
     DecEQ x_eq_y => Yes x_eq_y
-    DecLT xlty => No $ \x_eq_y => absurd $ irreflexive @{pre} y 
+    DecLT xlty => No $ \x_eq_y => absurd $ irreflexive @{pre} y
                                          $ replace {p = \u => u `lt` y} x_eq_y xlty
-    -- Similarly                                         
+    -- Similarly
     DecGT yltx => No $ \x_eq_y => absurd $ irreflexive @{pre} y
                                          $ replace {p = \u => y `lt` u} x_eq_y yltx
-    
diff --git a/libs/contrib/Text/Token.idr b/libs/contrib/Text/Token.idr
index 8308c4c0b..ce06d31e5 100644
--- a/libs/contrib/Text/Token.idr
+++ b/libs/contrib/Text/Token.idr
@@ -16,7 +16,7 @@ module Text.Token
 |||   tokValue SKComma x = ()
 ||| ```
 public export
-interface TokenKind (k : Type) where
+interface TokenKind k where
   ||| The type that a token of this kind converts to.
   TokType : k -> Type
 
diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr
index f4a74292f..a69165fb3 100644
--- a/libs/prelude/Prelude/Interfaces.idr
+++ b/libs/prelude/Prelude/Interfaces.idr
@@ -200,7 +200,7 @@ when False f = pure ()
 ||| function, into a single result.
 ||| @ t The type of the 'Foldable' parameterised type.
 public export
-interface Foldable (t : Type -> Type) where
+interface Foldable t where
   ||| Successively combine the elements in a parameterised type using the
   ||| provided function, starting with the element that is in the final position
   ||| i.e. the right-most position.
@@ -331,7 +331,7 @@ choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
 choiceMap f = foldr (\e, a => f e <|> a) empty
 
 public export
-interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where
+interface (Functor t, Foldable t) => Traversable t where
   ||| Map each element of a structure to a computation, evaluate those
   ||| computations and combine the results.
   traverse : Applicative f => (a -> f b) -> t a -> f (t b)
@@ -345,4 +345,3 @@ sequence = traverse id
 public export
 for : (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
 for = flip traverse
-
diff --git a/src/Core/Core.idr b/src/Core/Core.idr
index 689d7f1f0..c747e1f69 100644
--- a/src/Core/Core.idr
+++ b/src/Core/Core.idr
@@ -486,8 +486,8 @@ unless = when . not
 -- Control.Catchable in Idris 1, just copied here (but maybe no need for
 -- it since we'll only have the one instance for Core Error...)
 public export
-interface Catchable (m : Type -> Type) t | m where
-    throw : t -> m a
+interface Catchable m t | m where
+    throw : {0 a : Type} -> t -> m a
     catch : m a -> (t -> m a) -> m a
 
 export
diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr
index 72e90a31c..328a4dea6 100644
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@@ -500,9 +500,9 @@ export
 data QVar : Type where
 
 public export
-interface Quote (tm : List Name -> Type) where
+interface Quote tm where
     quote : {auto c : Ref Ctxt Defs} ->
-            {vars : _} ->
+            {vars : List Name} ->
             Defs -> Env Term vars -> tm vars -> Core (Term vars)
     quoteGen : {auto c : Ref Ctxt Defs} ->
                {vars : _} ->
@@ -767,9 +767,9 @@ etaContract tm = do
         _ => pure tm
 
 public export
-interface Convert (tm : List Name -> Type) where
+interface Convert tm where
   convert : {auto c : Ref Ctxt Defs} ->
-            {vars : _} ->
+            {vars : List Name} ->
             Defs -> Env Term vars ->
             tm vars -> tm vars -> Core Bool
   convGen : {auto c : Ref Ctxt Defs} ->
diff --git a/src/Core/TT.idr b/src/Core/TT.idr
index 7aade2aa4..e0d64cb59 100644
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@@ -651,8 +651,8 @@ eqTerm (TType _) (TType _) = True
 eqTerm _ _ = False
 
 public export
-interface Weaken (tm : List Name -> Type) where
-  weaken : tm vars -> tm (n :: vars)
+interface Weaken tm where
+  weaken : {0 vars : List Name} -> tm vars -> tm (n :: vars)
   weakenNs : SizeOf ns -> tm vars -> tm (ns ++ vars)
 
   weakenNs p t = case sizedView p of
diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr
index afeec0f03..79881623f 100644
--- a/src/Core/Unify.idr
+++ b/src/Core/Unify.idr
@@ -120,9 +120,9 @@ solvedHole : Int -> UnifyResult
 solvedHole n = MkUnifyResult [] True [n] NoLazy
 
 public export
-interface Unify (tm : List Name -> Type) where
+interface Unify tm where
   -- Unify returns a list of ids referring to newly added constraints
-  unifyD : {vars : _} ->
+  unifyD : {vars : List Name} ->
            Ref Ctxt Defs ->
            Ref UST UState ->
            UnifyInfo ->
diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr
index 34ab619cd..b68568fde 100644
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@@ -687,28 +687,33 @@ mutual
 --       pure [IReflect fc !(desugar AnyExpr ps tm)]
   desugarDecl ps (PInterface fc vis cons_in tn doc params det conname body)
       = do addDocString tn doc
+           let paramNames = map fst params
+
            let cons = concatMap expandConstraint cons_in
-           cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ map fst params)
+           cons' <- traverse (\ ntm => do tm' <- desugar AnyExpr (ps ++ paramNames)
                                                          (snd ntm)
                                           pure (fst ntm, tm')) cons
-           params' <- traverse (\ ntm => do tm' <- desugar AnyExpr ps (snd ntm)
-                                            pure (fst ntm, tm')) params
+           params' <- traverse (\ (nm, (rig, tm)) =>
+                         do tm' <- desugar AnyExpr ps tm
+                            pure (nm, (rig, tm')))
+                      params
            -- Look for bindable names in all the constraints and parameters
            let mnames = map dropNS (definedIn body)
            let bnames = ifThenElse !isUnboundImplicits
                           (concatMap (findBindableNames True
-                                      (ps ++ mnames ++ map fst params) [])
+                                      (ps ++ mnames ++ paramNames) [])
                                   (map Builtin.snd cons') ++
                            concatMap (findBindableNames True
-                                      (ps ++ mnames ++ map fst params) [])
-                                  (map Builtin.snd params'))
+                                      (ps ++ mnames ++ paramNames) [])
+                                  (map (snd . snd) params'))
                           []
-           let paramsb = map (\ ntm => (Builtin.fst ntm,
-                                        doBind bnames (Builtin.snd ntm))) params'
-           let consb = map (\ ntm => (Builtin.fst ntm,
-                                      doBind bnames (Builtin.snd ntm))) cons'
+           let paramsb = map (\ (nm, (rig, tm)) =>
+                                 let tm' = doBind bnames tm in
+                                 (nm, (rig, tm')))
+                         params'
+           let consb = map (\ (nm, tm) => (nm, doBind bnames tm)) cons'
 
-           body' <- traverse (desugarDecl (ps ++ mnames ++ map fst params)) body
+           body' <- traverse (desugarDecl (ps ++ mnames ++ paramNames)) body
            pure [IPragma (\nest, env =>
                              elabInterface fc vis env nest consb
                                            tn paramsb det conname
diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr
index c01afa2b3..e0047269e 100644
--- a/src/Idris/Elab/Implementation.idr
+++ b/src/Idris/Elab/Implementation.idr
@@ -51,13 +51,18 @@ bindImpls fc [] ty = ty
 bindImpls fc ((n, r, ty) :: rest) sc
     = IPi fc r Implicit (Just n) ty (bindImpls fc rest sc)
 
-addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->
+addDefaults : FC -> Name ->
+              (params : List (Name, RawImp)) -> -- parameters have been specialised, use them!
+              (allMethods : List Name) ->
+              (defaults : List (Name, List ImpClause)) ->
               List ImpDecl ->
               (List ImpDecl, List Name) -- Updated body, list of missing methods
-addDefaults fc impName allms defs body
+addDefaults fc impName params allms defs body
     = let missing = dropGot allms body in
           extendBody [] missing body
   where
+    specialiseMeth : Name -> (Name, RawImp)
+    specialiseMeth n = (n, INamedApp fc (IVar fc n) (UN "__con") (IVar fc impName))
     -- Given the list of missing names, if any are among the default definitions,
     -- add them to the body
     extendBody : List Name -> List Name -> List ImpDecl ->
@@ -73,10 +78,12 @@ addDefaults fc impName allms defs body
                     -- That is, default method implementations could depend on
                     -- other methods.
                     -- (See test idris2/interface014 for an example!)
-                    let mupdates
-                            = map (\n => (n, INamedApp fc (IVar fc n)
-                                                          (UN "__con")
-                                                          (IVar fc impName))) allms
+
+                    -- Similarly if any parameters appear in the clauses, they should
+                    -- be substituted for the actual parameters because they are going
+                    -- to be referring to unbound variables otherwise.
+                    -- (See test idris2/interface018 for an example!)
+                    let mupdates = params ++ map specialiseMeth allms
                         cs' = map (substNamesClause [] mupdates) cs in
                         extendBody ms ns
                              (IDef fc n (map (substLocClause fc) cs') :: body)
@@ -140,11 +147,12 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
 
          logTerm "elab.implementation" 3 ("Found interface " ++ show cn) ity
          log "elab.implementation" 3 $
-                 " with params: " ++ show (params cdata)
-                 ++ " and parents: " ++ show (parents cdata)
-                 ++ " using implicits: " ++ show impsp
-                 ++ " and methods: " ++ show (methods cdata) ++ "\n"
-                 ++ "Constructor: " ++ show (iconstructor cdata) ++ "\n"
+                 "\n  with params: " ++ show (params cdata)
+                 ++ "\n  specialised to: " ++ show ps
+                 ++ "\n  and parents: " ++ show (parents cdata)
+                 ++ "\n  using implicits: " ++ show impsp
+                 ++ "\n  and methods: " ++ show (methods cdata) ++ "\n"
+                 ++ "\nConstructor: " ++ show (iconstructor cdata) ++ "\n"
          logTerm "elab.implementation" 3 "Constructor type: " conty
          log "elab.implementation" 5 $ "Making implementation " ++ show impName
 
@@ -180,7 +188,9 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu
 
                -- 1.5. Lookup default definitions and add them to to body
                let (body, missing)
-                     = addDefaults fc impName (map (dropNS . fst) (methods cdata))
+                     = addDefaults fc impName
+                                      (zip (params cdata) ps)
+                                      (map (dropNS . fst) (methods cdata))
                                       (defaults cdata) body_in
 
                log "elab.implementation" 5 $ "Added defaults: body is " ++ show body
diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr
index 7479497c2..c16409f75 100644
--- a/src/Idris/Elab/Interface.idr
+++ b/src/Idris/Elab/Interface.idr
@@ -30,32 +30,33 @@ import Data.Maybe
 -- TODO: Check all the parts of the body are legal
 -- TODO: Deal with default superclass implementations
 
-mkDataTy : FC -> List (Name, RawImp) -> RawImp
+mkDataTy : FC -> List (Name, (RigCount, RawImp)) -> RawImp
 mkDataTy fc [] = IType fc
-mkDataTy fc ((n, ty) :: ps)
+mkDataTy fc ((n, (_, ty)) :: ps)
     = IPi fc top Explicit (Just n) ty (mkDataTy fc ps)
 
 mkIfaceData : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               FC -> Visibility -> Env Term vars ->
               List (Maybe Name, RigCount, RawImp) ->
-              Name -> Name -> List (Name, RawImp) ->
+              Name -> Name -> List (Name, (RigCount, RawImp)) ->
               List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl
 mkIfaceData {vars} fc vis env constraints n conName ps dets meths
     = let opts = if isNil dets
                     then [NoHints, UniqueSearch]
                     else [NoHints, UniqueSearch, SearchBy dets]
-          retty = apply (IVar fc n) (map (IVar fc) (map fst ps))
+          pNames = map fst ps
+          retty = apply (IVar fc n) (map (IVar fc) pNames)
           conty = mkTy Implicit (map jname ps) $
                   mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty)
-          con = MkImpTy fc conName !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars) conty) in
+          con = MkImpTy fc conName !(bindTypeNames [] (pNames ++ map fst meths ++ vars) conty) in
           pure $ IData fc vis (MkImpData fc n
-                                  !(bindTypeNames [] (map fst ps ++ map fst meths ++ vars)
+                                  !(bindTypeNames [] (pNames ++ map fst meths ++ vars)
                                                   (mkDataTy fc ps))
                                   opts [con])
   where
-    jname : (Name, RawImp) -> (Maybe Name, RigCount, RawImp)
-    jname (n, t) = (Just n, erased, t)
+    jname : (Name, (RigCount, RawImp)) -> (Maybe Name, RigCount, RawImp)
+    jname (n, rig, t) = (Just n, rig, t)
 
     bname : (Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)
     bname (n, c, t) = (Just n, c, IBindHere (getFC t) (PI erased) t)
@@ -86,13 +87,14 @@ namePis i ty = ty
 getMethDecl : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               Env Term vars -> NestedNames vars ->
-              (params : List (Name, RawImp)) ->
+              (params : List (Name, (RigCount, RawImp))) ->
               (mnames : List Name) ->
               (FC, RigCount, List FnOpt, n, (Bool, RawImp)) ->
               Core (n, RigCount, RawImp)
 getMethDecl {vars} env nest params mnames (fc, c, opts, n, (d, ty))
-    = do ty_imp <- bindTypeNames [] (map fst params ++ mnames ++ vars) ty
-         pure (n, c, stripParams (map fst params) ty_imp)
+    = do let paramNames = map fst params
+         ty_imp <- bindTypeNames [] (paramNames ++ mnames ++ vars) ty
+         pure (n, c, stripParams paramNames ty_imp)
   where
     -- We don't want the parameters to explicitly appear in the method
     -- type in the record for the interface (they are parameters of the
@@ -116,12 +118,13 @@ getMethToplevel : {vars : _} ->
                   Name -> Name ->
                   (constraints : List (Maybe Name)) ->
                   (allmeths : List Name) ->
-                  (params : List (Name, RawImp)) ->
+                  (params : List (Name, (RigCount, RawImp))) ->
                   (FC, RigCount, List FnOpt, Name, (Bool, RawImp)) ->
                   Core (List ImpDecl)
 getMethToplevel {vars} env vis iname cname constraints allmeths params
                 (fc, c, opts, n, (d, ty))
-    = do let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
+    = do let paramNames = map fst params
+         let ity = apply (IVar fc iname) (map (IVar fc) paramNames)
          -- Make the constraint application explicit for any method names
          -- which appear in other method types
          let ty_constr =
@@ -146,10 +149,10 @@ getMethToplevel {vars} env vis iname cname constraints allmeths params
   where
     -- Bind the type parameters given explicitly - there might be information
     -- in there that we can't infer after all
-    bindPs : List (Name, RawImp) -> RawImp -> RawImp
+    bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
     bindPs [] ty = ty
-    bindPs ((n, pty) :: ps) ty
-        = IPi (getFC pty) erased Implicit (Just n) pty (bindPs ps ty)
+    bindPs ((n, rig, pty) :: ps) ty
+        = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)
 
     applyCon : Name -> (Name, RawImp)
     applyCon n = (n, INamedApp fc (IVar fc n)
@@ -270,7 +273,7 @@ elabInterface : {vars : _} ->
                 Env Term vars -> NestedNames vars ->
                 (constraints : List (Maybe Name, RawImp)) ->
                 Name ->
-                (params : List (Name, RawImp)) ->
+                (params : List (Name, (RigCount, RawImp))) ->
                 (dets : List Name) ->
                 (conName : Maybe Name) ->
                 List ImpDecl ->
@@ -299,9 +302,12 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
          let implParams = getImplParams ty
 
          updateIfaceSyn ns_iname conName
-                        implParams (map fst params) (map snd constraints)
+                        implParams paramNames (map snd constraints)
                         ns_meths ds
   where
+    paramNames : List Name
+    paramNames = map fst params
+
     nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)
     nameCons i [] = []
     nameCons i ((_, ty) :: rest)
@@ -366,25 +372,25 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
                           Just (r, _, _, t) => pure (r, t)
                           Nothing => throw (GenericMsg fc ("No method named " ++ show n ++ " in interface " ++ show iname))
 
-             let ity = apply (IVar fc iname) (map (IVar fc) (map fst params))
+             let ity = apply (IVar fc iname) (map (IVar fc) paramNames)
 
              -- Substitute the method names with their top level function
              -- name, so they don't get implicitly bound in the name
              methNameMap <- traverse (\n =>
                                 do cn <- inCurrentNS n
-                                   pure (n, applyParams (IVar fc cn)
-                                                     (map fst params)))
+                                   pure (n, applyParams (IVar fc cn) paramNames))
                                (map fst tydecls)
-             let dty = substNames vars methNameMap dty
+             let dty = bindPs params    -- bind parameters
+                     $ bindIFace fc ity -- bind interface (?!)
+                     $ substNames vars methNameMap dty
 
-             dty_imp <- bindTypeNames [] (map fst tydecls ++ vars)
-                                      (bindIFace fc ity dty)
-             log "elab.interface" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
+             dty_imp <- bindTypeNames [] (map fst tydecls ++ vars) dty
+             log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp
              let dtydecl = IClaim fc rig vis [] (MkImpTy fc dn dty_imp)
              processDecl [] nest env dtydecl
 
              let cs' = map (changeName dn) cs
-             log "elab.interface" 5 $ "Default method body " ++ show cs'
+             log "elab.interface.default" 5 $ "Default method body " ++ show cs'
 
              processDecl [] nest env (IDef fc dn cs')
              -- Reset the original context, we don't need to keep the definition
@@ -392,6 +398,13 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
 --              put Ctxt orig
              pure (n, cs)
       where
+        -- Bind the type parameters given explicitly - there might be information
+        -- in there that we can't infer after all
+        bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
+        bindPs [] ty = ty
+        bindPs ((n, (rig, pty)) :: ps) ty
+          = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)
+
         applyParams : RawImp -> List Name -> RawImp
         applyParams tm [] = tm
         applyParams tm (UN n :: ns)
@@ -425,7 +438,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body
              chints <- traverse (getConstraintHint fc env vis iname conName
                                                  (map fst nconstraints)
                                                  meth_names
-                                                 (map fst params)) nconstraints
+                                                 paramNames) nconstraints
              log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints
              traverse (processDecl [] nest env) (concatMap snd chints)
              traverse_ (\n => do mn <- inCurrentNS n
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index f3549057b..f32f5a8b6 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -416,11 +416,8 @@ mutual
 
   multiplicity : SourceEmptyRule (Maybe Integer)
   multiplicity
-      = do c <- intLit
-           pure (Just c)
---     <|> do symbol "&"
---            pure (Just 2) -- Borrowing, not implemented
-    <|> pure Nothing
+      = optional $ intLit
+--     <|> 2 <$ symbol "&" Borrowing, not implemented
 
   getMult : Maybe Integer -> SourceEmptyRule RigCount
   getMult (Just 0) = pure erased
@@ -1195,16 +1192,18 @@ implBinds fname indents
          pure ((n, rig, tm) :: more)
   <|> pure []
 
-ifaceParam : FileName -> IndentInfo -> Rule (List Name, PTerm)
+ifaceParam : FileName -> IndentInfo -> Rule (List Name, (RigCount, PTerm))
 ifaceParam fname indents
     = do symbol "("
+         m <- multiplicity
+         rig <- getMult m
          ns <- sepBy1 (symbol ",") name
          symbol ":"
          tm <- expr pdef fname indents
          symbol ")"
-         pure (ns, tm)
+         pure (ns, (rig, tm))
   <|> do n <- bounds name
-         pure ([n.val], PInfer (boundToFC fname n))
+         pure ([n.val], (erased, PInfer (boundToFC fname n)))
 
 ifaceDecl : FileName -> IndentInfo -> Rule PDecl
 ifaceDecl fname indents
@@ -1216,7 +1215,7 @@ ifaceDecl fname indents
                          cons   <- constraints fname indents
                          n      <- name
                          paramss <- many (ifaceParam fname indents)
-                         let params = concatMap (\ (ns, t) => map (\ n => (n, t)) ns) paramss
+                         let params = concatMap (\ (ns, rt) => map (\ n => (n, rt)) ns) paramss
                          det    <- option []
                                      (do symbol "|"
                                          sepBy (symbol ",") name)
diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr
index befa3b43f..c5791499d 100644
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@@ -286,7 +286,7 @@ mutual
                     (constraints : List (Maybe Name, PTerm)) ->
                     Name ->
                     (doc : String) ->
-                    (params : List (Name, PTerm)) ->
+                    (params : List (Name, (RigCount, PTerm))) ->
                     (det : List Name) ->
                     (conName : Maybe Name) ->
                     List PDecl ->
@@ -973,11 +973,11 @@ mapPTermM f = goPTerm where
       PUsing fc <$> goPairedPTerms mnts
                 <*> goPDecls ps
     goPDecl (PReflect fc t) = PReflect fc <$> goPTerm t
-    goPDecl (PInterface fc v mnts n doc nts ns mn ps) =
+    goPDecl (PInterface fc v mnts n doc nrts ns mn ps) =
       PInterface fc v <$> goPairedPTerms mnts
                       <*> pure n
                       <*> pure doc
-                      <*> goPairedPTerms nts
+                      <*> go3TupledPTerms nrts
                       <*> pure ns
                       <*> pure mn
                       <*> goPDecls ps
diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr
index 097399429..5414af82e 100644
--- a/src/TTImp/Utils.idr
+++ b/src/TTImp/Utils.idr
@@ -202,12 +202,14 @@ mutual
                       ImpClause -> ImpClause
   substNamesClause' bvar bound ps (PatClause fc lhs rhs)
       = let bound' = map UN (map snd (findBindableNames True bound [] lhs))
-                        ++ bound in
+                     ++ findIBindVars lhs
+                     ++ bound in
             PatClause fc (substNames' bvar [] [] lhs)
                          (substNames' bvar bound' ps rhs)
   substNamesClause' bvar bound ps (WithClause fc lhs wval flags cs)
       = let bound' = map UN (map snd (findBindableNames True bound [] lhs))
-                        ++ bound in
+                     ++ findIBindVars lhs
+                     ++ bound in
             WithClause fc (substNames' bvar [] [] lhs)
                           (substNames' bvar bound' ps wval) flags cs
   substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
diff --git a/src/Text/Token.idr b/src/Text/Token.idr
index 1327e8aea..e032e139c 100644
--- a/src/Text/Token.idr
+++ b/src/Text/Token.idr
@@ -18,7 +18,7 @@ module Text.Token
 |||   tokValue SKComma x = ()
 ||| ```
 public export
-interface TokenKind (k : Type) where
+interface TokenKind k where
   ||| The type that a token of this kind converts to.
   TokType : k -> Type
 
diff --git a/tests/Main.idr b/tests/Main.idr
index adf0b792f..42f7926f2 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -71,7 +71,7 @@ idrisTests = MkTestPool []
        "interface005", "interface006", "interface007", "interface008",
        "interface009", "interface010", "interface011", "interface012",
        "interface013", "interface014", "interface015", "interface016",
-       "interface017",
+       "interface017", "interface018",
        -- Miscellaneous REPL
        "interpreter001", "interpreter002", "interpreter003", "interpreter004",
        "interpreter005",
diff --git a/tests/idris2/basic013/Implicits.idr b/tests/idris2/basic013/Implicits.idr
index ec95ac274..da3b50864 100644
--- a/tests/idris2/basic013/Implicits.idr
+++ b/tests/idris2/basic013/Implicits.idr
@@ -1,5 +1,5 @@
 public export
-interface Do (m : Type) where
+interface Do (0 m : Type) where
   Next : m -> Type
   bind : (x : m) -> Next x
 
diff --git a/tests/idris2/interface003/Do.idr b/tests/idris2/interface003/Do.idr
index 2e6557e63..3a5e08daf 100644
--- a/tests/idris2/interface003/Do.idr
+++ b/tests/idris2/interface003/Do.idr
@@ -1,5 +1,5 @@
 public export
-interface Do (m : Type) where
+interface Do (0 m : Type) where
   Next : (a : Type) -> (b : Type) -> m -> Type
   bind : (x : m) -> Next a b x
 
@@ -9,4 +9,3 @@ public export
 Monad m => Do (m a) where
   Next a b x = (a -> m b) -> m b
   bind x = ?foo
-
diff --git a/tests/idris2/interface004/Do.idr b/tests/idris2/interface004/Do.idr
index 04a9dce08..88c2770fc 100644
--- a/tests/idris2/interface004/Do.idr
+++ b/tests/idris2/interface004/Do.idr
@@ -1,5 +1,5 @@
 public export
-interface Do (m : Type) where
+interface Do (0 m : Type) where
   Next : m -> Type
   bind : (x : m) -> Next x
 
@@ -12,4 +12,3 @@ foo : Maybe Int -> Maybe Int -> Maybe Int
 foo x y
    = bind x (\x' =>
      bind y (\y' => Just (x' + y')))
-
diff --git a/tests/idris2/interface006/Apply.idr b/tests/idris2/interface006/Apply.idr
index 3183548e5..92407dfc2 100644
--- a/tests/idris2/interface006/Apply.idr
+++ b/tests/idris2/interface006/Apply.idr
@@ -26,7 +26,7 @@ export
 ||| Biapplys (not to be confused with Biapplicatives)
 ||| @p The action of the Biapply on pairs of objects
 public export
-interface Bifunctor p => Biapply (p : Type -> Type -> Type) where
+interface Bifunctor p => Biapply (0 p : Type -> Type -> Type) where
 
   ||| Applys a Bifunctor of functions to another Bifunctor of the same type
   |||
diff --git a/tests/idris2/interface006/Bimonad.idr b/tests/idris2/interface006/Bimonad.idr
index cdaded2a0..d0eef33fc 100644
--- a/tests/idris2/interface006/Bimonad.idr
+++ b/tests/idris2/interface006/Bimonad.idr
@@ -8,7 +8,7 @@ infixl 4 >>==
 ||| @p the action of the first Bifunctor component on pairs of objects
 ||| @q the action of the second Bifunctor component on pairs of objects
 interface (Biapplicative p, Biapplicative q) =>
-      Bimonad (p : Type -> Type -> Type) (q : Type -> Type -> Type) where
+      Bimonad (0 p : Type -> Type -> Type) (0 q : Type -> Type -> Type) where
 
   bijoin : (p (p a b) (q a b), q (p a b) (q a b)) -> (p a b, q a b)
   bijoin p = p >>== (id, id)
diff --git a/tests/idris2/interface018/Sized.idr b/tests/idris2/interface018/Sized.idr
new file mode 100644
index 000000000..1eb9813f6
--- /dev/null
+++ b/tests/idris2/interface018/Sized.idr
@@ -0,0 +1,26 @@
+import Data.Buffer
+
+%default total
+
+public export
+interface Singleton (n : Nat) where
+  sing : (m : Nat ** m === n)
+  sing = (n ** Refl)
+
+Singleton 3 where
+Singleton 5 where
+
+export
+data ForeignPtr : Type -> Type where
+  MkFP : Buffer -> ForeignPtr a
+
+public export
+interface Storable (0 a : Type) (n : Nat) | a where
+  constructor MkStorable
+  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
+
+  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
+  peekElemOff fp off = peekByteOff fp (off * cast n)
+
+Storable Bits8 8 where
+  peekByteOff (MkFP b) off = getBits8 b off
diff --git a/tests/idris2/interface018/Sized2.idr b/tests/idris2/interface018/Sized2.idr
new file mode 100644
index 000000000..a1dbaffb8
--- /dev/null
+++ b/tests/idris2/interface018/Sized2.idr
@@ -0,0 +1,18 @@
+import Data.Buffer
+
+export
+data ForeignPtr : Type -> Type where
+  MkFP : Buffer -> ForeignPtr a
+
+public export
+interface Storable a where
+  size : Int
+
+  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
+
+  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
+  peekElemOff fp off = peekByteOff fp (off * size {a})
+
+Storable Bits8 where
+  size = 8
+  peekByteOff (MkFP b) off = getBits8 b off
diff --git a/tests/idris2/interface018/Sized3.idr b/tests/idris2/interface018/Sized3.idr
new file mode 100644
index 000000000..848f36206
--- /dev/null
+++ b/tests/idris2/interface018/Sized3.idr
@@ -0,0 +1,20 @@
+import Data.Buffer
+
+export
+data ForeignPtr : Type -> Type where
+  MkFP : Buffer -> ForeignPtr a
+
+public export
+interface Storable a where
+
+  size : ForeignPtr a -> Int
+
+  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a
+
+  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
+  peekElemOff fp off = peekByteOff fp (off * size fp)
+
+Storable Bits8 where
+
+  size _ = 8
+  peekByteOff (MkFP b) off = getBits8 b off
diff --git a/tests/idris2/interface018/expected b/tests/idris2/interface018/expected
new file mode 100644
index 000000000..fb5bbd0ef
--- /dev/null
+++ b/tests/idris2/interface018/expected
@@ -0,0 +1,7 @@
+1/1: Building Sized (Sized.idr)
+Main> 3
+Main> 5
+Main> 
+Bye for now!
+1/1: Building Sized2 (Sized2.idr)
+1/1: Building Sized3 (Sized3.idr)
diff --git a/tests/idris2/interface018/input b/tests/idris2/interface018/input
new file mode 100644
index 000000000..8cbb65d03
--- /dev/null
+++ b/tests/idris2/interface018/input
@@ -0,0 +1,3 @@
+fst (the (m : Nat ** m === 3) sing)
+fst (the (m : Nat ** m === 5) sing)
+:q
\ No newline at end of file
diff --git a/tests/idris2/interface018/run b/tests/idris2/interface018/run
new file mode 100755
index 000000000..bf127297f
--- /dev/null
+++ b/tests/idris2/interface018/run
@@ -0,0 +1,5 @@
+$1 --no-color --no-banner --console-width 0 Sized.idr < input
+$1 --no-color --console-width 0 Sized2.idr --check
+$1 --no-color --console-width 0 Sized3.idr --check
+
+rm -rf build
diff --git a/tests/idris2/reg029/lqueue.idr b/tests/idris2/reg029/lqueue.idr
index 2c156f722..d69b3cccb 100644
--- a/tests/idris2/reg029/lqueue.idr
+++ b/tests/idris2/reg029/lqueue.idr
@@ -1,14 +1,14 @@
-interface Queue (q: Type -> Type) where   
-  empty : q a 
+interface Queue (0 q: Type -> Type) where
+  empty : q a
   isEmpty : q a -> Bool
-  snoc : q a -> a -> q a 
+  snoc : q a -> a -> q a
   head : q a -> a
   tail : q a -> q a
 
 data CatList : (Type -> Type) -> Type -> Type where
-  E : CatList q a 
+  E : CatList q a
   C : {0 q : Type -> Type} -> a -> q (Lazy (CatList q a)) -> CatList q a
-  
-link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a 
+
+link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a
 link E s = s -- Just to satisfy totality for now.
 link (C x xs) s = C x (snoc xs s)

From daff1f2fb8a3977bbca7851111edcfb416cf8f40 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Sun, 13 Dec 2020 17:06:18 +0100
Subject: [PATCH 28/28] Added assert_linear. (#844)

Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
---
 libs/prelude/Builtin.idr          |  9 +++++++++
 tests/ideMode/ideMode001/expected | 12 ++++++------
 tests/ideMode/ideMode003/expected | 12 ++++++------
 3 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/libs/prelude/Builtin.idr b/libs/prelude/Builtin.idr
index 33afd1742..3cc6c7f12 100644
--- a/libs/prelude/Builtin.idr
+++ b/libs/prelude/Builtin.idr
@@ -182,6 +182,15 @@ public export
 believe_me : a -> b
 believe_me = prim__believe_me _ _
 
+||| Assert to the usage checker that the given function uses its argument linearly.
+public export
+assert_linear : (1 f : a -> b) -> (1 val : a) -> b
+assert_linear = believe_me id
+  where
+    id : (1 f : a -> b) -> a -> b
+    id f = f
+
+
 export partial
 idris_crash : String -> a
 idris_crash = prim__crash _
diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected
index d721d95cf..dfeaf0ead 100644
--- a/tests/ideMode/ideMode001/expected
+++ b/tests/ideMode/ideMode001/expected
@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:372} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:373}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:372}_[] ?{_:373}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:374}_[] ?{_:373}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:384} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:385}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:384}_[] ?{_:385}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:386}_[] ?{_:385}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((: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 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:363}_[] ?{_:362}_[])")))))) 1)
-0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:353} : (Main.Vect n[0] a[1])) -> ({arg:354} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:375}_[] ?{_:374}_[])")))))) 1)
+0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:365} : (Main.Vect n[0] a[1])) -> ({arg:366} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(: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.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected
index c7a995d9f..0a4f023e2 100644
--- a/tests/ideMode/ideMode003/expected
+++ b/tests/ideMode/ideMode003/expected
@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:372} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:373}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:372}_[] ?{_:373}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:374}_[] ?{_:373}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:384} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:385}_[]")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:384}_[] ?{_:385}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:386}_[] ?{_:385}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((: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 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:363}_[] ?{_:362}_[])")))))) 1)
-0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:353} : (Main.Vect n[0] a[1])) -> ({arg:354} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:375}_[] ?{_:374}_[])")))))) 1)
+0001ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 5 48)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:365} : (Main.Vect n[0] a[1])) -> ({arg:366} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:64:1--69:33 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(: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.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)