Merge branch 'master' of github.com:idris-lang/Idris2 into javascript

2024-11-28 11:05:17 +03:00 · 2020-06-10 11:32:01 +01:00 · 2020-06-10 11:32:01 +01:00 · c4e07f4caf
commit c4e07f4caf
parent 3266493293 90fb901c8f
82 changed files with 1902 additions and 552 deletions
--- a/INSTALL.md
+++ b/INSTALL.md
@ -1,12 +1,12 @@
 Installing
 ==========

-The easiest way to install is via the existing generated Scheme code. The
-requirements are:
+The easiest way to install is via the existing generated Scheme code.
+The requirements are:

-* A Scheme compiler; either Chez Scheme (default), or Racket
-* `bash`, with `realpath`. On Linux, you probably already have this. On
-  a Mac, you can install this with `brew install coreutils`.
+* A Scheme compiler; either Chez Scheme (default), or Racket.
+* `bash`, with `realpath`. On Linux, you probably already have this.
+  On a Mac, you can install this with `brew install coreutils`.

 On Windows, it has been reported that installing via `MSYS2` works
 (https://www.msys2.org/). On Windows older than Windows 8, you may need to
@ -16,6 +16,8 @@ On Raspberry Pi, you can bootstrap via Racket.

 By default, code generation is via Chez Scheme. You can use Racket instead,
 by setting the environment variable `IDRIS2_CG=racket` before running `make`.
+If you install Chez Scheme from source files, building it locally,
+make sure you run `./configure --threads` to build multithreading support in.

 1: Set the PREFIX
 -----------------
@ -59,7 +61,7 @@ If all is well, to install, type:
 ----------------------------------------------------

 If you have [Idris-2-in-Idris-1](https://github.com/edwinb/Idris2-boot)
-installed: 
+installed:

 * `make all IDRIS2_BOOT=idris2boot`
 * `make install IDRIS2_BOOT=idris2boot`
--- a/README.md
+++ b/README.md
@ -96,4 +96,8 @@ Things still missing
 Talks
 =====

+[![Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)](https://img.youtube.com/vi/mOtKD7ml0NU/0.jpg)](https://www.youtube.com/watch?v=mOtKD7ml0NU "Idris 2: Type-driven Development of Idris (Code Mesh LDN 18)")
+
 [![Idris 2 - Type-driven Development of Idris (Curry On - London 2019)](https://img.youtube.com/vi/DRq2NgeFcO0/0.jpg)](https://www.youtube.com/watch?v=DRq2NgeFcO0 "Idris 2 - Type-driven Development of Idris (Curry On - London 2019)")
+
+[![Scheme Workshop Keynote (ACM SIGPLAN)](https://img.youtube.com/vi/h9YAOaBWuIk/0.jpg)](https://www.youtube.com/watch?v=h9YAOaBWuIk "Scheme Workshop Keynote (ACM SIGPLAN)")
--- a/config.mk
+++ b/config.mk
@ -2,8 +2,6 @@

 PREFIX ?= $(HOME)/.idris2

-CC ?= clang
-
 # For Windows targets. Set to 1 to support Windows 7.
 OLD_WIN ?= 0

@ -34,9 +32,9 @@ else ifneq (, $(findstring bsd, $(MACHINE)))
 	SHLIB_SUFFIX := .so
 	CFLAGS += -fPIC
 else
-        OS := linux
-        SHLIB_SUFFIX := .so
-        CFLAGS += -fPIC
+	OS := linux
+	SHLIB_SUFFIX := .so
+	CFLAGS += -fPIC
 endif

 export OS
--- a/docs/source/ffi/ffi.rst
+++ b/docs/source/ffi/ffi.rst
@ -409,3 +409,31 @@ can convert between a ``void*`` and a ``char*`` in C:

    %foreign (pfn "getString")
    getString : Ptr String -> String
+
+
+Finalisers
+----------
+
+In some libraries, a foreign function creates a pointer and the caller is
+responsible for freeing it. In this case, you can make an explicit foreign
+call to ``free``. However, this is not always convenient, or even possible.
+Instead, you can ask the Idris run-time to be responsible for freeing the
+pointer when it is no longer accessible, using ``onCollect`` (or its
+typeless variant ``onCollectAny``) defined in the Prelude:
+
+.. code-block:: idris
+
+    onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
+    onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr
+
+A ``GCPtr t`` behaves exactly like ``Ptr t`` when passed to a foreign
+function (and, similarly, ``GCAnyPtr`` behaves like ``AnyPtr``). A foreign
+function cannot return a ``GCPtr`` however, because then we can no longer
+assume the pointer is completely managed by the Idris run-time.
+
+The finaliser is called either when the garbage collector determines that
+the pointer is no longer accessible, or at the end of execution.
+
+Note that finalisers might not be supported by all back ends, since they depend
+on the facilities offered by a specific back end's run time system. They are
+certainly supported in the Chez Scheme and Racket back ends.
--- a/docs/source/tutorial/packages.rst
+++ b/docs/source/tutorial/packages.rst
@ -82,6 +82,6 @@ a simple recipe for this trivial case:

    package myProject

-    pkgs = pruviloj, lightyear
+    depends = pruviloj, lightyear

 - In Atom, use the File menu to Open Folder myProject.
--- a/docs/source/updates/updates.rst
+++ b/docs/source/updates/updates.rst
@ -461,6 +461,34 @@ directory ``build/ttc``, in the root of the source tree, with the directory
 structure following the directory structure of the source.  Executables are
 placed in ``build/exec``.

+Packages
+--------
+
+Dependencies on other packages are now indicated with the ``depends`` field,
+the ``pkgs`` field is no longer recognized. Also, fields with URLS or other
+string data (other than module or package names), must be enclosed in double
+quotes.
+For example:
+
+::
+
+        package lightyear
+
+        sourceloc  = "git://git@github.com:ziman/lightyear.git"
+        bugtracker = "http://www.github.com/ziman/lightyear/issues"
+
+        depends = effects
+
+        modules = Lightyear
+                , Lightyear.Position
+                , Lightyear.Core
+                , Lightyear.Combinators
+                , Lightyear.StringFile
+                , Lightyear.Strings
+                , Lightyear.Char
+                , Lightyear.Testing
+
+
 .. _sect-new-features:

 New features
--- a/idris2.ipkg
+++ b/idris2.ipkg
@ -18,8 +18,6 @@ modules =
    Compiler.Scheme.Common,
    Compiler.VMCode,

-    Control.Delayed,
-
    Core.AutoSearch,
    Core.Binary,
    Core.CaseBuilder,
--- a/idris2api.ipkg
+++ b/idris2api.ipkg
@ -17,8 +17,6 @@ modules =
    Compiler.Scheme.Common,
    Compiler.VMCode,

-    Control.Delayed,
-
    Core.AutoSearch,
    Core.Binary,
    Core.CaseBuilder,
--- a/libs/base/Data/Fuel.idr
+++ b/libs/base/Data/Fuel.idr
@ -0,0 +1,20 @@
+module Data.Fuel
+
+%default total
+
+||| Fuel for running total operations potentially indefinitely.
+public export
+data Fuel = Dry | More (Lazy Fuel)
+
+||| Provide `n` units of fuel.
+export
+limit : Nat -> Fuel
+limit  Z    = Dry
+limit (S n) = More (limit n)
+
+||| Provide fuel indefinitely.
+||| This function is fundamentally partial.
+partial
+export
+forever : Fuel
+forever = More forever
--- a/libs/base/Data/List.idr
+++ b/libs/base/Data/List.idr
@ -635,5 +635,3 @@ implementation DecEq a => DecEq (List a) where
    decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
      decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)
      decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)
-
-
--- a/libs/base/Data/Nat.idr
+++ b/libs/base/Data/Nat.idr
@ -1,5 +1,7 @@
 module Data.Nat

+%default total
+
 export
 Uninhabited (Z = S n) where
  uninhabited Refl impossible
@ -157,14 +159,12 @@ maximum (S n) (S m) = S (maximum n m)
 -- Proofs on S

 export
-eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->
-         S left = S right
-eqSucc left _ Refl = Refl
+eqSucc : (left, right : Nat) -> left = right -> S left = S right
+eqSucc _ _ Refl = Refl

 export
-succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->
-                left = right
-succInjective left _ Refl = Refl
+succInjective : (left, right : Nat) -> S left = S right -> left = right
+succInjective _ _ Refl = Refl

 export
 SIsNotZ : (S x = Z) -> Void
@ -219,7 +219,7 @@ Integral Nat where
  div = divNat
  mod = modNat

-export
+export partial
 gcd : (a: Nat) -> (b: Nat) -> {auto ok: NotBothZero a b} -> Nat
 gcd a Z     = a
 gcd Z b     = b
@ -250,89 +250,80 @@ cmp (S x) (S y) with (cmp x y)
  cmp (S x) (S x)           | CmpEQ   = CmpEQ
  cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k

-- Proofs on
+-- Proofs on +

 export
 plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
-plusZeroLeftNeutral right = Refl
+plusZeroLeftNeutral _ = Refl

 export
 plusZeroRightNeutral : (left : Nat) -> left + 0 = left
 plusZeroRightNeutral Z     = Refl
-plusZeroRightNeutral (S n) =
-  let inductiveHypothesis = plusZeroRightNeutral n in
-    rewrite inductiveHypothesis in Refl
+plusZeroRightNeutral (S n) = rewrite plusZeroRightNeutral n in Refl

 export
-plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
-  S (left + right) = left + (S right)
-plusSuccRightSucc Z right        = Refl
-plusSuccRightSucc (S left) right =
-  let inductiveHypothesis = plusSuccRightSucc left right in
-    rewrite inductiveHypothesis in Refl
+plusSuccRightSucc : (left, right : Nat) -> S (left + right) = left + (S right)
+plusSuccRightSucc Z _ = Refl
+plusSuccRightSucc (S left) right = rewrite plusSuccRightSucc left right in Refl

 export
-plusCommutative : (left : Nat) -> (right : Nat) ->
-  left + right = right + left
-plusCommutative Z        right = rewrite plusZeroRightNeutral right in Refl
+plusCommutative : (left, right : Nat) -> left + right = right + left
+plusCommutative Z right = rewrite plusZeroRightNeutral right in Refl
 plusCommutative (S left) right =
-  let inductiveHypothesis = plusCommutative left right in
-    rewrite inductiveHypothesis in
-      rewrite plusSuccRightSucc right left in Refl
+  rewrite plusCommutative left right in
+    rewrite plusSuccRightSucc right left in
+      Refl

 export
-plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+plusAssociative : (left, centre, right : Nat) ->
  left + (centre + right) = (left + centre) + right
-plusAssociative Z        centre right = Refl
+plusAssociative Z _ _ = Refl
 plusAssociative (S left) centre right =
-  let inductiveHypothesis = plusAssociative left centre right in
-    rewrite inductiveHypothesis in Refl
+    rewrite plusAssociative left centre right in Refl

 export
-plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->
-  (p : left = right) -> left + c = right + c
-plusConstantRight left _ c Refl = Refl
+plusConstantRight : (left, right, c : Nat) -> left = right ->
+  left + c = right + c
+plusConstantRight _ _ _ Refl = Refl

 export
-plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->
-  (p : left = right) -> c + left = c + right
-plusConstantLeft left _ c Refl = Refl
+plusConstantLeft : (left, right, c : Nat) -> left = right ->
+  c + left = c + right
+plusConstantLeft _ _ _ Refl = Refl

 export
 plusOneSucc : (right : Nat) -> 1 + right = S right
-plusOneSucc n = Refl
+plusOneSucc _ = Refl

 export
-plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
-  (p : left + right = left + right') -> right = right'
-plusLeftCancel Z        right right' p = p
+plusLeftCancel : (left, right, right' : Nat) ->
+  left + right = left + right' -> right = right'
+plusLeftCancel Z _ _ p = p
 plusLeftCancel (S left) right right' p =
-  let inductiveHypothesis = plusLeftCancel left right right' in
-    inductiveHypothesis (succInjective _ _ p)
+    plusLeftCancel left right right' (succInjective _ _ p)

 export
-plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) ->
-  (p : left + right = left' + right) -> left = left'
-plusRightCancel left left' Z         p = rewrite sym (plusZeroRightNeutral left) in
-                                         rewrite sym (plusZeroRightNeutral left') in
-                                                 p
-plusRightCancel left left' (S right) p =
-  plusRightCancel left left' right
-    (succInjective _ _ (rewrite plusSuccRightSucc left right in
-                        rewrite plusSuccRightSucc left' right in p))
+plusRightCancel : (left, left', right : Nat) ->
+  left + right = left' + right -> left = left'
+plusRightCancel left left' right p =
+  plusLeftCancel right left left' $
+    rewrite plusCommutative right left in
+      rewrite plusCommutative right left' in
+        p

 export
-plusLeftLeftRightZero : (left : Nat) -> (right : Nat) ->
-  (p : left + right = left) -> right = Z
-plusLeftLeftRightZero Z        right p = p
-plusLeftLeftRightZero (S left) right p =
-  plusLeftLeftRightZero left right (succInjective _ _ p)
+plusLeftLeftRightZero : (left, right : Nat) ->
+  left + right = left -> right = Z
+plusLeftLeftRightZero left right p =
+  plusLeftCancel left right Z $
+    rewrite plusZeroRightNeutral left in
+      p

 -- Proofs on *

 export
 multZeroLeftZero : (right : Nat) -> Z * right = Z
-multZeroLeftZero right = Refl
+multZeroLeftZero _ = Refl

 export
 multZeroRightZero : (left : Nat) -> left * Z = Z
@ -340,97 +331,80 @@ multZeroRightZero Z        = Refl
 multZeroRightZero (S left) = multZeroRightZero left

 export
-multRightSuccPlus : (left : Nat) -> (right : Nat) ->
+multRightSuccPlus : (left, right : Nat) ->
  left * (S right) = left + (left * right)
-multRightSuccPlus Z        right = Refl
+multRightSuccPlus Z _ = Refl
 multRightSuccPlus (S left) right =
-  let inductiveHypothesis = multRightSuccPlus left right in
-    rewrite inductiveHypothesis in
-    rewrite plusAssociative left right (left * right) in
-    rewrite plusAssociative right left (left * right) in
-    rewrite plusCommutative right left in
-            Refl
+  rewrite multRightSuccPlus left right in
+  rewrite plusAssociative left right (left * right) in
+  rewrite plusAssociative right left (left * right) in
+  rewrite plusCommutative right left in
+          Refl

 export
-multLeftSuccPlus : (left : Nat) -> (right : Nat) ->
+multLeftSuccPlus : (left, right : Nat) ->
  (S left) * right = right + (left * right)
-multLeftSuccPlus left right = Refl
+multLeftSuccPlus _ _ = Refl

 export
-multCommutative : (left : Nat) -> (right : Nat) ->
-  left * right = right * left
-multCommutative Z right        = rewrite multZeroRightZero right in Refl
+multCommutative : (left, right : Nat) -> left * right = right * left
+multCommutative Z right = rewrite multZeroRightZero right in Refl
 multCommutative (S left) right =
-  let inductiveHypothesis = multCommutative left right in
-      rewrite inductiveHypothesis in
-      rewrite multRightSuccPlus right left in
-              Refl
+  rewrite multCommutative left right in
+  rewrite multRightSuccPlus right left in
+          Refl

 export
-multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
-  left * (centre + right) = (left * centre) + (left * right)
-multDistributesOverPlusRight Z        centre right = Refl
-multDistributesOverPlusRight (S left) centre right =
-  let inductiveHypothesis = multDistributesOverPlusRight left centre right in
-    rewrite inductiveHypothesis in
-    rewrite plusAssociative (centre + (left * centre)) right (left * right) in
-    rewrite sym (plusAssociative centre (left * centre) right) in
-    rewrite plusCommutative (left * centre) right in
-    rewrite plusAssociative centre right (left * centre) in
-    rewrite plusAssociative (centre + right) (left * centre) (left * right) in
-            Refl
-
-export
-multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+multDistributesOverPlusLeft : (left, centre, right : Nat) ->
  (left + centre) * right = (left * right) + (centre * right)
-multDistributesOverPlusLeft Z        centre right = Refl
-multDistributesOverPlusLeft (S left) centre right =
-  let inductiveHypothesis = multDistributesOverPlusLeft left centre right in
-    rewrite inductiveHypothesis in
-    rewrite plusAssociative right (left * right) (centre * right) in
-            Refl
+multDistributesOverPlusLeft Z _ _ = Refl
+multDistributesOverPlusLeft (S k) centre right =
+  rewrite multDistributesOverPlusLeft k centre right in
+    rewrite plusAssociative right (k * right) (centre * right) in
+      Refl

 export
-multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+multDistributesOverPlusRight : (left, centre, right : Nat) ->
+  left * (centre + right) = (left * centre) + (left * right)
+multDistributesOverPlusRight left centre right =
+  rewrite multCommutative left (centre + right) in
+    rewrite multCommutative left centre in
+      rewrite multCommutative left right in
+  multDistributesOverPlusLeft centre right left
+
+export
+multAssociative : (left, centre, right : Nat) ->
  left * (centre * right) = (left * centre) * right
-multAssociative Z        centre right = Refl
+multAssociative Z _ _ = Refl
 multAssociative (S left) centre right =
-  let inductiveHypothesis = multAssociative left centre right in
-    rewrite inductiveHypothesis in
-    rewrite multDistributesOverPlusLeft centre (left * centre) right in
-            Refl
+  rewrite multAssociative left centre right in
+    rewrite multDistributesOverPlusLeft centre (mult left centre) right in
+      Refl

 export
 multOneLeftNeutral : (right : Nat) -> 1 * right = right
-multOneLeftNeutral Z         = Refl
-multOneLeftNeutral (S right) =
-  let inductiveHypothesis = multOneLeftNeutral right in
-    rewrite inductiveHypothesis in
-            Refl
+multOneLeftNeutral right = plusZeroRightNeutral right

 export
 multOneRightNeutral : (left : Nat) -> left * 1 = left
-multOneRightNeutral Z        = Refl
-multOneRightNeutral (S left) =
-  let inductiveHypothesis = multOneRightNeutral left in
-    rewrite inductiveHypothesis in
-            Refl
+multOneRightNeutral left = rewrite multCommutative left 1 in multOneLeftNeutral left


-- Proofs on -
+-- Proofs on minus

 export
-minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right
-minusSuccSucc left right = Refl
+minusSuccSucc : (left, right : Nat) ->
+  minus (S left) (S right) = minus left right
+minusSuccSucc _ _ = Refl

 export
 minusZeroLeft : (right : Nat) -> minus 0 right = Z
-minusZeroLeft right = Refl
+minusZeroLeft _ = Refl

 export
 minusZeroRight : (left : Nat) -> minus left 0 = left
-minusZeroRight Z        = Refl
-minusZeroRight (S left) = Refl
+minusZeroRight Z     = Refl
+minusZeroRight (S _) = Refl

 export
 minusZeroN : (n : Nat) -> Z = minus n n
@ -445,53 +419,140 @@ minusOneSuccN (S n) = minusOneSuccN n
 export
 minusSuccOne : (n : Nat) -> minus (S n) 1 = n
 minusSuccOne Z     = Refl
-minusSuccOne (S n) = Refl
+minusSuccOne (S _) = Refl

 export
-minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = Z
-minusPlusZero Z     m = Refl
+minusPlusZero : (n, m : Nat) -> minus n (n + m) = Z
+minusPlusZero Z     _ = Refl
 minusPlusZero (S n) m = minusPlusZero n m

 export
-minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
+minusMinusMinusPlus : (left, centre, right : Nat) ->
  minus (minus left centre) right = minus left (centre + right)
-minusMinusMinusPlus Z        Z          right = Refl
-minusMinusMinusPlus (S left) Z          right = Refl
-minusMinusMinusPlus Z        (S centre) right = Refl
+minusMinusMinusPlus Z Z _ = Refl
+minusMinusMinusPlus (S _) Z _ = Refl
+minusMinusMinusPlus Z (S _) _ = Refl
 minusMinusMinusPlus (S left) (S centre) right =
-  let inductiveHypothesis = minusMinusMinusPlus left centre right in
-      rewrite inductiveHypothesis in
-              Refl
+  rewrite minusMinusMinusPlus left centre right in Refl

 export
-plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
+plusMinusLeftCancel : (left, right : Nat) -> (right' : Nat) ->
  minus (left + right) (left + right') = minus right right'
-plusMinusLeftCancel Z right right'        = Refl
+plusMinusLeftCancel Z _ _ = Refl
 plusMinusLeftCancel (S left) right right' =
-  let inductiveHypothesis = plusMinusLeftCancel left right right' in
-      rewrite inductiveHypothesis in
-              Refl
+  rewrite plusMinusLeftCancel left right right' in Refl

 export
-multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
-                               (minus left centre) * right = minus (left * right) (centre * right)
-multDistributesOverMinusLeft Z        Z          right = Refl
-multDistributesOverMinusLeft (S left) Z          right =
-  rewrite (minusZeroRight (plus right (mult left right))) in Refl
-multDistributesOverMinusLeft Z        (S centre) right = Refl
+multDistributesOverMinusLeft : (left, centre, right : Nat) ->
+  (minus left centre) * right = minus (left * right) (centre * right)
+multDistributesOverMinusLeft Z Z _ = Refl
+multDistributesOverMinusLeft (S left) Z right =
+  rewrite minusZeroRight (right + (left * right)) in Refl
+multDistributesOverMinusLeft Z (S _) _ = Refl
 multDistributesOverMinusLeft (S left) (S centre) right =
-  let inductiveHypothesis = multDistributesOverMinusLeft left centre right in
-      rewrite inductiveHypothesis in
-      rewrite plusMinusLeftCancel right (mult left right) (mult centre right) in
-              Refl
-
-export
-multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->
-                                left * (minus centre right) = minus (left * centre) (left * right)
-multDistributesOverMinusRight left centre right =
-  rewrite multCommutative left (minus centre right) in
-  rewrite multDistributesOverMinusLeft centre right left in
-  rewrite multCommutative centre left in
-  rewrite multCommutative right left in
+  rewrite multDistributesOverMinusLeft left centre right in
+  rewrite plusMinusLeftCancel right (left * right) (centre * right) in
          Refl

+export
+multDistributesOverMinusRight : (left, centre, right : Nat) ->
+  left * (minus centre right) = minus (left * centre) (left * right)
+multDistributesOverMinusRight left centre right =
+    rewrite multCommutative left (minus centre right) in
+    rewrite multDistributesOverMinusLeft centre right left in
+    rewrite multCommutative centre left in
+    rewrite multCommutative right left in
+            Refl
+
+-- power proofs
+
+multPowerPowerPlus : (base, exp, exp' : Nat) ->
+  power base (exp + exp') = (power base exp) * (power base exp')
+-- multPowerPowerPlus base Z       exp' =
+--     rewrite sym $ plusZeroRightNeutral (power base exp') in Refl
+-- multPowerPowerPlus base (S exp) exp' =
+--   rewrite multPowerPowerPlus base exp exp' in
+--     rewrite sym $ multAssociative base (power base exp) (power base exp') in
+--       Refl
+
+powerOneNeutral : (base : Nat) -> power base 1 = base
+powerOneNeutral base = rewrite multCommutative base 1 in multOneLeftNeutral base
+
+powerOneSuccOne : (exp : Nat) -> power 1 exp = 1
+powerOneSuccOne Z       = Refl
+powerOneSuccOne (S exp) = rewrite powerOneSuccOne exp in Refl
+
+powerPowerMultPower : (base, exp, exp' : Nat) ->
+  power (power base exp) exp' = power base (exp * exp')
+powerPowerMultPower _ exp Z = rewrite multZeroRightZero exp in Refl
+powerPowerMultPower base exp (S exp') =
+  rewrite powerPowerMultPower base exp exp' in
+  rewrite multRightSuccPlus exp exp' in
+  rewrite sym $ multPowerPowerPlus base exp (exp * exp') in
+          Refl
+
+-- minimum / maximum proofs
+
+maximumAssociative : (l, c, r : Nat) ->
+  maximum l (maximum c r) = maximum (maximum l c) r
+maximumAssociative Z _ _ = Refl
+maximumAssociative (S _) Z _ = Refl
+maximumAssociative (S _) (S _) Z = Refl
+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl
+
+maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l
+maximumCommutative Z Z = Refl
+maximumCommutative Z (S _) = Refl
+maximumCommutative (S _) Z = Refl
+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl
+
+maximumIdempotent : (n : Nat) -> maximum n n = n
+-- maximumIdempotent Z = Refl
+-- maximumIdempotent (S k) = cong $ maximumIdempotent k
+
+minimumAssociative : (l, c, r : Nat) ->
+  minimum l (minimum c r) = minimum (minimum l c) r
+minimumAssociative Z _ _ = Refl
+minimumAssociative (S _) Z _ = Refl
+minimumAssociative (S _) (S _) Z = Refl
+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl
+
+minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l
+minimumCommutative Z Z = Refl
+minimumCommutative Z (S _) = Refl
+minimumCommutative (S _) Z = Refl
+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl
+
+minimumIdempotent : (n : Nat) -> minimum n n = n
+-- minimumIdempotent Z = Refl
+-- minimumIdempotent (S k) = cong (minimumIdempotent k)
+
+minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z
+minimumZeroZeroLeft left = rewrite minimumCommutative left 0 in Refl
+
+minimumSuccSucc : (left, right : Nat) ->
+  minimum (S left) (S right) = S (minimum left right)
+minimumSuccSucc _ _ = Refl
+
+maximumZeroNLeft : (left : Nat) -> maximum left Z = left
+maximumZeroNLeft left = rewrite maximumCommutative left Z in Refl
+
+maximumSuccSucc : (left, right : Nat) ->
+  S (maximum left right) = maximum (S left) (S right)
+maximumSuccSucc _ _ = Refl
+
+sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
+-- sucMaxL Z = Refl
+-- sucMaxL (S l) = cong $ sucMaxL l
+
+sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
+-- sucMaxR Z = Refl
+-- sucMaxR (S l) = cong $ sucMaxR l
+
+sucMinL : (l : Nat) -> minimum (S l) l = l
+-- sucMinL Z = Refl
+-- sucMinL (S l) = cong $ sucMinL l
+
+sucMinR : (l : Nat) -> minimum l (S l) = l
+-- sucMinR Z = Refl
+-- sucMinR (S l) = cong $ sucMinR l
--- a/libs/base/Language/Reflection.idr
+++ b/libs/base/Language/Reflection.idr
@ -20,9 +20,9 @@ data Elab : Type -> Type where
     Quote : val -> Elab TTImp

     -- Elaborate under a lambda
-     Lambda : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
-     -- Elaborate under a forall
-     ForAll : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
+     Lambda : (0 x : Type) ->
+              {0 ty : x -> Type} ->
+              ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))

     -- Get the current goal type, if known 
     -- (it might need to be inferred from the solution)
@ -90,13 +90,11 @@ quote : val -> Elab TTImp
 quote = Quote

 export
-lambda : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
+lambda : (0 x : Type) ->
+         {0 ty : x -> Type} ->
+         ((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
 lambda = Lambda

-export
-forAll : (0 x : Type) -> (x -> Elab ty) -> Elab (x -> ty)
-forAll = ForAll
-
 export
 goal : Elab (Maybe TTImp)
 goal = Goal
--- a/libs/base/Language/Reflection/TT.idr
+++ b/libs/base/Language/Reflection/TT.idr
@ -47,9 +47,11 @@ data Constant
    | WorldType

 public export
-data Name = UN String
-          | MN String Int
-          | NS (List String) Name
+data Name = UN String -- user defined name
+          | MN String Int -- machine generated name
+          | NS (List String) Name -- name in a namespace
+          | DN String Name -- a name and how to display it
+          | RF String -- record field name

 export
 Show Name where
@ -61,6 +63,8 @@ Show Name where
      showSep sep (x :: xs) = x ++ sep ++ showSep sep xs
  show (UN x) = x
  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
+  show (DN str y) = str
+  show (RF n) = "." ++ n

 public export
 data Count = M0 | M1 | MW
--- a/libs/contrib/Data/Fin/Extra.idr
+++ b/libs/contrib/Data/Fin/Extra.idr
@ -0,0 +1,100 @@
+module Data.Fin.Extra
+
+import Data.Fin
+import Data.Nat
+
+%default total
+
+
+||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
+export
+elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
+elemSmallerThanBound FZ = LTESucc LTEZero
+elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)
+
+||| Proof that application of finToNat the last element of Fin **S n** gives **n**.
+export
+finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
+finToNatLastIsBound {n=Z} = Refl
+finToNatLastIsBound {n=S k} = rewrite finToNatLastIsBound {n=k} in Refl
+
+||| Proof that an element **n** of Fin **m** , when converted to Nat is smaller than the bound **m**.
+export
+finToNatWeakenNeutral : {m : Nat} -> {n : Fin m} -> finToNat (weaken n) = finToNat n
+finToNatWeakenNeutral {n=FZ} = Refl
+finToNatWeakenNeutral {m=S (S _)} {n=FS _} = cong S finToNatWeakenNeutral
+
+-- ||| Proof that it's possible to strengthen a weakened element of Fin **m**.
+-- export
+-- strengthenWeakenNeutral : {m : Nat} -> (n : Fin m) -> strengthen (weaken n) = Right n
+-- strengthenWeakenNeutral {m=S _} FZ = Refl
+-- strengthenWeakenNeutral {m=S (S _)} (FS k) = rewrite strengthenWeakenNeutral k in Refl
+
+||| Proof that it's not possible to strengthen the last element of Fin **n**.
+export
+strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Left (Fin.last {n})
+strengthenLastIsLeft {n=Z} = Refl
+strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl
+
+||| Enumerate elements of Fin **n** backwards.
+export
+invFin : {n : Nat} -> Fin n -> Fin n
+invFin FZ = last
+invFin {n=S (S _)} (FS k) = weaken (invFin k)
+
+||| Proof that an inverse of a weakened element of Fin **n** is a successive of an inverse of an original element.
+export
+invWeakenIsSucc : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
+invWeakenIsSucc FZ = Refl
+invWeakenIsSucc {n=S (S _)} (FS k) = rewrite invWeakenIsSucc k in Refl
+
+||| Proof that double inversion of Fin **n** gives the original.
+export
+doubleInvFinSame : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
+doubleInvFinSame {n=S Z} FZ = Refl
+doubleInvFinSame {n=S (S k)} FZ = rewrite doubleInvFinSame {n=S k} FZ in Refl
+doubleInvFinSame {n=S (S _)} (FS x) = trans (invWeakenIsSucc $ invFin x) (cong FS $ doubleInvFinSame x)
+
+||| Proof that an inverse of the last element of Fin (S **n**) in FZ.
+export
+invLastIsFZ : {n : Nat} -> invFin (Fin.last {n}) = FZ
+invLastIsFZ {n=Z} = Refl
+invLastIsFZ {n=S k} = rewrite invLastIsFZ {n=k} in Refl
+
+-- ||| Proof that it's possible to strengthen an inverse of a succesive element of Fin **n**.
+-- export
+-- strengthenNotLastIsRight : (m : Fin (S n)) -> strengthen (invFin (FS m)) = Right (invFin m)
+-- strengthenNotLastIsRight m = strengthenWeakenNeutral (invFin m)
+--
+||| Either tightens the bound on a Fin or proves that it's the last.
+export
+strengthen' : {n : Nat} -> (m : Fin (S n)) -> Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
+strengthen' {n = Z} FZ = Left Refl
+strengthen' {n = S k} FZ = Right (FZ ** Refl)
+strengthen' {n = S k} (FS m) = case strengthen' m of
+    Left eq => Left $ cong FS eq
+    Right (m' ** eq) => Right (FS m' ** cong S eq)
+
+||| A view of Nat as a quotient of some number and a finite remainder.
+public export
+data FractionView : (n : Nat) -> (d : Nat) -> Type where
+    Fraction : (n : Nat) -> (d : Nat) -> {auto ok: GT d Z} ->
+                (q : Nat) -> (r : Fin d) ->
+                q * d + finToNat r = n -> FractionView n d
+
+||| Converts Nat to the fractional view with a non-zero divisor.
+export
+divMod : (n, d : Nat) -> {auto ok: GT d Z} -> FractionView n d
+divMod Z (S d) = Fraction Z (S d) Z FZ Refl
+divMod {ok=_} (S n) (S d) =
+    let Fraction {ok=ok} n (S d) q r eq = divMod n (S d) in
+    case strengthen' r of
+        Left eq' => Fraction {ok=ok} (S n) (S d) (S q) FZ $
+            rewrite sym eq in
+                rewrite trans (cong finToNat eq') finToNatLastIsBound in
+                    cong S $ trans
+                        (plusZeroRightNeutral (d + q * S d))
+                        (plusCommutative d (q * S d))
+        Right (r' ** eq') => Fraction {ok=ok} (S n) (S d) q (FS r') $
+            rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
+                cong S $ trans (sym $ cong (plus (q * S d)) eq') eq
--- a/libs/contrib/Data/Nat/Equational.idr
+++ b/libs/contrib/Data/Nat/Equational.idr
@ -0,0 +1,70 @@
+module Data.Nat.Equational
+
+import Data.Nat
+
+%default total
+
+
+||| Subtract a number from both sides of an equation.
+||| Due to partial nature of subtraction in natural numbers, an equation of
+||| special form is required in order for subtraction to be total.
+export
+subtractEqLeft : (a : Nat) -> {b, c : Nat} -> a + b = a + c -> b = c
+subtractEqLeft 0 prf = prf
+subtractEqLeft (S k) prf = subtractEqLeft k $ succInjective (k + b) (k + c) prf
+
+||| Subtract a number from both sides of an equation.
+||| Due to partial nature of subtraction in natural numbers, an equation of
+||| special form is required in order for subtraction to be total.
+export
+subtractEqRight : {a, b : Nat} -> (c : Nat) -> a + c = b + c -> a = b
+subtractEqRight c prf =
+    subtractEqLeft c $
+    rewrite plusCommutative c a in
+    rewrite plusCommutative c b in
+    prf
+
+||| Add a number to both sides of an inequality
+export
+plusLteLeft : (a : Nat) -> {b, c : Nat} -> LTE b c -> LTE (a + b) (a + c)
+plusLteLeft 0 bLTEc = bLTEc
+plusLteLeft (S k) bLTEc = LTESucc $ plusLteLeft k bLTEc
+
+||| Add a number to both sides of an inequality
+export
+plusLteRight : {a, b : Nat} -> (c : Nat) -> LTE a b -> LTE (a + c) (b + c)
+plusLteRight c aLTEb =
+    rewrite plusCommutative a c in
+    rewrite plusCommutative b c in
+    plusLteLeft c aLTEb
+
+||| Subtract a number from both sides of an inequality.
+||| Due to partial nature of subtraction, we require an inequality of special form.
+export
+subtractLteLeft : (a : Nat) -> {b, c : Nat} -> LTE (a + b) (a + c) -> LTE b c
+subtractLteLeft 0 abLTEac = abLTEac
+subtractLteLeft (S k) abLTEac = subtractLteLeft k $ fromLteSucc abLTEac
+
+||| Subtract a number from both sides of an inequality.
+||| Due to partial nature of subtraction, we require an inequality of special form.
+export
+subtractLteRight : {a, b : Nat} -> (c : Nat) -> LTE (a + c) (b + c) -> LTE a b
+subtractLteRight c acLTEbc =
+    subtractLteLeft c $
+    rewrite plusCommutative c a in
+    rewrite plusCommutative c b in
+    acLTEbc
+
+||| If one of the factors of a product is greater than 0, then the other factor
+||| is less than or equal to the product..
+export
+rightFactorLteProduct : (a, b : Nat) -> LTE b (S a * b)
+rightFactorLteProduct a b = lteAddRight b
+
+||| If one of the factors of a product is greater than 0, then the other factor
+||| is less than or equal to the product..
+export
+leftFactorLteProduct : (a, b : Nat) -> LTE a (a * S b)
+leftFactorLteProduct a b =
+    rewrite multRightSuccPlus a b in
+    lteAddRight a
--- a/libs/contrib/Data/Nat/Factor.idr
+++ b/libs/contrib/Data/Nat/Factor.idr
@ -0,0 +1,497 @@
+module Data.Nat.Factor
+
+import Control.WellFounded
+import Data.Fin
+import Data.Fin.Extra
+import Data.Nat
+import Data.Nat.Equational
+import Syntax.PreorderReasoning
+
+%default total
+
+
+||| Factor n p is a witness that p is indeed a factor of n,
+||| i.e. there exists a q such that p * q = n.
+public export
+data Factor : Nat -> Nat -> Type where
+    CofactorExists : {p, n : Nat} -> (q : Nat) -> n = p * q -> Factor p n
+
+||| NotFactor n p is a witness that p is NOT a factor of n,
+||| i.e. there exist a q and an r, greater than 0 but smaller than p,
+||| such that p * q + r = n.
+public export
+data NotFactor : Nat -> Nat -> Type where
+    ZeroNotFactorS : (n : Nat) -> NotFactor Z (S n)
+    ProperRemExists : {p, n : Nat} -> (q : Nat) ->
+        (r : Fin (pred p)) ->
+        n = p * q + S (finToNat r) ->
+        NotFactor p n
+
+||| DecFactor n p is a result of the process which decides
+||| whether or not p is a factor on n.
+public export
+data DecFactor : Nat -> Nat -> Type where
+    ItIsFactor : Factor p n -> DecFactor p n
+    ItIsNotFactor : NotFactor p n -> DecFactor p n
+
+||| CommonFactor n m p is a witness that p is a factor of both n and m.
+public export
+data CommonFactor : Nat -> Nat -> Nat -> Type where
+    CommonFactorExists : {a, b : Nat} -> (p : Nat) -> Factor p a -> Factor p b -> CommonFactor p a b
+
+||| GCD n m p is a witness that p is THE greatest common factor of both n and m.
+||| The second argument to the constructor is a function which for all q being
+||| a factor of both n and m, proves that q is a factor of p.
+|||
+||| This is equivalent to a more straightforward definition, stating that for
+||| all q being a factor of both n and m, q is less than or equal to p, but more
+||| powerful and therefore more useful for further proofs. See below for a proof
+||| that if q is a factor of p then q must be less than or equal to p.
+public export
+data GCD : Nat -> Nat -> Nat -> Type where
+    MkGCD : {a, b, p : Nat} ->
+        {auto notBothZero : NotBothZero a b} ->
+        (CommonFactor p a b) ->
+        ((q : Nat) -> CommonFactor q a b -> Factor q p) ->
+        GCD p a b
+
+
+Uninhabited (Factor Z (S n)) where
+    uninhabited (CofactorExists q prf) = uninhabited prf
+
+||| Given a statement that p is factor of n, return its cofactor.
+export
+cofactor : Factor p n -> (q : Nat ** Factor q n)
+cofactor (CofactorExists {n} {p} q prf) =
+        (q ** CofactorExists p $ rewrite multCommutative q p in prf)
+
+||| 1 is a factor of any natural number.
+export
+oneIsFactor : (n : Nat) -> Factor 1 n
+oneIsFactor Z = CofactorExists Z Refl
+oneIsFactor (S k) = CofactorExists (S k) (rewrite plusZeroRightNeutral k in Refl)
+
+||| 1 is the only factor of itself
+export
+oneSoleFactorOfOne : (a : Nat) -> Factor a 1 -> a = 1
+oneSoleFactorOfOne Z (CofactorExists q prf) = absurd $ uninhabited prf
+oneSoleFactorOfOne (S Z) (CofactorExists _ _) = Refl
+oneSoleFactorOfOne (S (S k)) (CofactorExists Z prf) =
+        absurd . uninhabited $ replace {p = \x => 1 = x} (multZeroRightZero k) prf
+oneSoleFactorOfOne (S (S k)) (CofactorExists (S j) prf) =
+        absurd . uninhabited . succInjective 0 (S j + (j + (k * S j))) $
+        replace {p = \x => 1 = S x} (sym $ plusSuccRightSucc j (j + (k * S j))) prf
+
+||| Every natural number is factor of itself.
+export
+factorReflexive : (n : Nat) -> Factor n n
+factorReflexive a = CofactorExists 1 (rewrite multOneRightNeutral a in Refl)
+
+||| Factor relation is transitive. If b is factor of a and c is b factor of c
+||| is also a factor of a.
+export
+factorTransitive : (a, b, c : Nat) -> Factor a b -> Factor b c -> Factor a c
+factorTransitive a b c (CofactorExists qb prfAB) (CofactorExists qc prfBC) =
+    CofactorExists (qb * qc) (
+        rewrite prfBC in
+        rewrite prfAB in
+        rewrite multAssociative a qb qc in
+        Refl
+    )
+
+multOneSoleNeutral : (a, b : Nat) -> S a = S a * b -> b = 1
+multOneSoleNeutral Z b prf =
+        rewrite sym $ plusZeroRightNeutral b in
+        sym prf
+multOneSoleNeutral (S k) Z prf =
+        absurd . uninhabited $
+        replace {p = \x => S (S k) = x} (multZeroRightZero k) prf
+multOneSoleNeutral (S k) (S Z) prf = Refl
+multOneSoleNeutral (S k) (S (S j)) prf =
+        absurd . uninhabited .
+        subtractEqLeft k {b = 0} {c = S j + S (j + (k * S j))} $
+        rewrite plusSuccRightSucc j (S (j + (k * S j))) in
+        rewrite plusZeroRightNeutral k in
+        rewrite plusAssociative k j (S (S (j + (k * S j)))) in
+        rewrite sym $ plusCommutative j k in
+        rewrite sym $ plusAssociative j k (S (S (j + (k * S j)))) in
+        rewrite sym $ plusSuccRightSucc k (S (j + (k * S j))) in
+        rewrite sym $ plusSuccRightSucc k (j + (k * S j)) in
+        rewrite plusAssociative k j (k * S j) in
+        rewrite plusCommutative k j in
+        rewrite sym $ plusAssociative j k (k * S j) in
+        rewrite sym $ multRightSuccPlus k (S j) in
+        succInjective k (j + (S (S (j + (k * (S (S j))))))) $
+        succInjective (S k) (S (j + (S (S (j + (k * (S (S j)))))))) prf
+
+||| If a is a factor of b and b is a factor of a, then we can conclude a = b.
+export
+factorAntisymmetric : {a, b : Nat} -> Factor a b -> Factor b a -> a = b
+factorAntisymmetric {a = 0} (CofactorExists qa prfAB) (CofactorExists qb prfBA) = sym prfAB
+factorAntisymmetric {a = S a} {b = 0} (CofactorExists qa prfAB) (CofactorExists qb prfBA) = prfBA
+factorAntisymmetric {a = S a} {b = S b} (CofactorExists qa prfAB) (CofactorExists qb prfBA) =
+    let qIs1 = multOneSoleNeutral a (qa * qb) $
+            rewrite multAssociative (S a) qa qb in
+            rewrite sym prfAB in
+            prfBA
+    in
+    rewrite prfAB in
+    rewrite oneSoleFactorOfOne qa . CofactorExists qb $ sym qIs1 in
+    rewrite multOneRightNeutral a in
+    Refl
+
+||| No number can simultaneously be and not be a factor of another number.
+export
+factorNotFactorAbsurd : {n, p : Nat} -> Factor p n -> NotFactor p n -> Void
+factorNotFactorAbsurd {n = S k} {p = Z} (CofactorExists q prf) (ZeroNotFactorS k) =
+        uninhabited prf
+factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists q' r contra) with (cmp q q')
+    factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists (q + S d) r contra) | CmpLT d =
+        SIsNotZ .
+        subtractEqLeft (p * q) {b = S ((p * S d) + finToNat r)} {c = 0} $
+        rewrite plusZeroRightNeutral (p * q) in
+        rewrite plusSuccRightSucc (p * S d) (finToNat r) in
+        rewrite plusAssociative (p * q) (p * S d) (S (finToNat r)) in
+        rewrite sym $ multDistributesOverPlusRight p q (S d) in
+        rewrite sym contra in
+        rewrite sym prf in
+        Refl
+    factorNotFactorAbsurd {n} {p} (CofactorExists q prf) (ProperRemExists q r contra) | CmpEQ =
+        uninhabited .
+        subtractEqLeft (p * q) {b = (S (finToNat r))} {c = 0} $
+        rewrite plusZeroRightNeutral (p * q) in
+        rewrite sym contra in
+        prf
+    factorNotFactorAbsurd {n} {p} (CofactorExists (q + S d) prf) (ProperRemExists q r contra) | CmpGT d =
+        let srEQpPlusPD = the (plus p (mult p d) = S (finToNat r)) $
+                rewrite sym $ multRightSuccPlus p d in
+                subtractEqLeft (p * q) {b = p * (S d)} {c = S (finToNat r)} $
+                    rewrite sym $ multDistributesOverPlusRight p q (S d) in
+                    rewrite sym contra in
+                    sym prf
+        in
+        case p of
+            Z => uninhabited srEQpPlusPD
+            (S k) =>
+                succNotLTEzero .
+                subtractLteLeft k {b = S (d + (k * d))} {c = 0} $
+                rewrite sym $ plusSuccRightSucc k (d + (k * d)) in
+                rewrite plusZeroRightNeutral k in
+                rewrite srEQpPlusPD in
+                elemSmallerThanBound r
+
+
+||| Anything is a factor of 0.
+export
+anythingFactorZero : (a : Nat) -> Factor a 0
+anythingFactorZero a = CofactorExists 0 (sym $ multZeroRightZero a)
+
+||| For all natural numbers p and q, p is a factor of (p * q).
+export
+multFactor : (p, q : Nat) -> Factor p (p * q)
+multFactor p q = CofactorExists q Refl
+
+||| If n > 0 then any factor of n must be less than or equal to n.
+export
+factorLteNumber : Factor p n -> {auto positN : LTE 1 n} -> LTE p n
+factorLteNumber (CofactorExists {n} {p} Z prf) {positN} =
+        let nIsZero = replace {p = \x => n = x} (multZeroRightZero p) prf
+            oneLteZero = replace {p = LTE 1} nIsZero positN
+        in
+        absurd $ succNotLTEzero oneLteZero
+factorLteNumber (CofactorExists {n} {p} (S k) prf) =
+        rewrite prf in
+        leftFactorLteProduct p k
+
+||| If p is a factor of n, then it is also a factor of (n + p).
+export
+plusDivisorAlsoFactor : Factor p n -> Factor p (n + p)
+plusDivisorAlsoFactor (CofactorExists {n} {p} q prf) =
+        CofactorExists (S q) $
+            rewrite plusCommutative n p in
+            rewrite multRightSuccPlus p q in
+            cong (plus p) prf
+
+||| If p is NOT a factor of n, then it also is NOT a factor of (n + p).
+export
+plusDivisorNeitherFactor : NotFactor p n -> NotFactor p (n + p)
+plusDivisorNeitherFactor (ZeroNotFactorS k) =
+        rewrite plusZeroRightNeutral k in
+        ZeroNotFactorS k
+plusDivisorNeitherFactor (ProperRemExists {n} {p} q r remPrf) =
+        ProperRemExists (S q) r $
+            rewrite multRightSuccPlus p q in
+            rewrite sym $ plusAssociative p (p * q) (S $ finToNat r) in
+            rewrite plusCommutative p ((p * q) + S (finToNat r)) in
+            rewrite remPrf in
+            Refl
+
+||| If p is a factor of n, then it is also a factor of any multiply of n.
+export
+multNAlsoFactor : Factor p n -> (a : Nat) -> {auto aok : LTE 1 a} -> Factor p (n * a)
+multNAlsoFactor _ Z {aok} = absurd $ succNotLTEzero aok
+multNAlsoFactor (CofactorExists {n} {p} q prf) (S a) =
+        CofactorExists (q * S a) $
+            rewrite prf in
+            sym $ multAssociative p q (S a)
+
+||| If p is a factor of both n and m, then it is also a factor of their sum.
+export
+plusFactor : Factor p n -> Factor p m -> Factor p (n + m)
+plusFactor {n} {p} (CofactorExists qn prfN) (CofactorExists qm prfM) =
+        rewrite prfN in
+        rewrite prfM in
+        rewrite sym $ multDistributesOverPlusRight p qn qm in
+        multFactor p (qn + qm)
+
+||| If p is a factor of a sum (n + m) and a factor of n, then it is also
+||| a factor of m. This could be expressed more naturally with minus, but
+||| it would be more difficult to prove, since minus lacks certain properties
+||| that one would expect from decent subtraction.
+export
+minusFactor : {a, b, p : Nat} -> Factor p (a + b) -> Factor p a -> Factor p b
+minusFactor {a} {b} (CofactorExists qab prfAB) (CofactorExists qa prfA) =
+        CofactorExists (minus qab qa) (
+            rewrite multDistributesOverMinusRight p qab qa in
+            rewrite sym prfA in
+            rewrite sym prfAB in
+            replace {p = \x => b = minus (a + b) x} (plusZeroRightNeutral a) $
+            rewrite plusMinusLeftCancel a b 0 in
+            rewrite minusZeroRight b in
+            Refl
+        )
+
+||| A decision procedure for whether of not p is a factor of n.
+export
+decFactor : (n, d : Nat) -> DecFactor d n
+decFactor Z Z = ItIsFactor $ factorReflexive Z
+decFactor (S k) Z = ItIsNotFactor $ ZeroNotFactorS k
+decFactor n (S d) =
+        let Fraction n (S d) q r prf = Data.Fin.Extra.divMod n (S d) in
+        case r of
+            FZ =>
+                let prf =
+                        replace {p = \x => x = n} (plusZeroRightNeutral (q + (d * q))) $
+                        replace {p = \x => x + 0 = n} (multCommutative q (S d)) prf
+                in
+                ItIsFactor $ CofactorExists q (sym prf)
+
+            (FS pr) =>
+                ItIsNotFactor $ ProperRemExists q pr (
+                        rewrite multCommutative d q in
+                        rewrite sym $ multRightSuccPlus q d in
+                        sym prf
+                    )
+
+||| For all p greater than 1, if p is a factor of n, then it is NOT a factor
+||| of (n + 1).
+export
+factNotSuccFact : {n, p : Nat} -> GT p 1 -> Factor p n -> NotFactor p (S n)
+factNotSuccFact {n} {p = Z} pGt1 (CofactorExists q prf) =
+        absurd $ succNotLTEzero pGt1
+factNotSuccFact {n} {p = S Z} pGt1 (CofactorExists q prf) =
+        absurd . succNotLTEzero $ fromLteSucc pGt1
+factNotSuccFact {n} {p = S (S k)} pGt1 (CofactorExists q prf) =
+        ProperRemExists q FZ (
+            rewrite sym prf in
+            rewrite plusCommutative n 1 in
+            Refl
+        )
+
+||| The relation of common factor is symmetric, that is if p is a common factor
+||| of n and m, then it is also a common factor if m and n.
+export
+commonFactorSym : CommonFactor p a b -> CommonFactor p b a
+commonFactorSym (CommonFactorExists p pfa pfb) = CommonFactorExists p pfb pfa
+
+||| The relation of greates common divisor is symmetric.
+export
+gcdSym : GCD p a b -> GCD p b a
+gcdSym {a = Z} {b = Z} (MkGCD {notBothZero} _ _) impossible
+gcdSym {a = S a} {b} (MkGCD {notBothZero = LeftIsNotZero} cf greatest) =
+        MkGCD {notBothZero = RightIsNotZero} (commonFactorSym cf) $
+        \q, cf => greatest q (commonFactorSym cf)
+gcdSym {a} {b = S b} (MkGCD {notBothZero = RightIsNotZero} cf greatest) =
+        MkGCD {notBothZero = LeftIsNotZero} (commonFactorSym cf) $
+        \q, cf => greatest q (commonFactorSym cf)
+
+||| If p is a common factor of a and b, then it is also a factor of their GCD.
+||| This actually follows directly from the definition of GCD.
+export
+commonFactorAlsoFactorOfGCD : {p : Nat} -> Factor p a -> Factor p b -> GCD q a b -> Factor p q
+commonFactorAlsoFactorOfGCD {p} pfa pfb (MkGCD _ greatest) =
+        greatest p (CommonFactorExists p pfa pfb)
+
+
+||| 1 is a common factor of any pair of natural numbers.
+export
+oneCommonFactor : (a, b : Nat) -> CommonFactor 1 a b
+oneCommonFactor a b = CommonFactorExists 1
+        (CofactorExists a (rewrite plusZeroRightNeutral a in Refl))
+        (CofactorExists b (rewrite plusZeroRightNeutral b in Refl))
+
+||| Any natural number is a common factor of itself and itself.
+export
+selfIsCommonFactor : (a : Nat) -> {auto ok : LTE 1 a} -> CommonFactor a a a
+selfIsCommonFactor Z {ok} = absurd $ succNotLTEzero ok
+selfIsCommonFactor (S k) = CommonFactorExists (S k) (factorReflexive $ S k) (factorReflexive $ S k)
+
+
+-- Some helpers for the gcd function.
+data Search : Type where
+    SearchArgs : (a, b : Nat) -> LTE b a -> {auto bNonZero : LTE 1 b} -> Search
+
+left : Search -> Nat
+left (SearchArgs l _ _) = l
+
+right : Search -> Nat
+right (SearchArgs _ r _) = r
+
+Sized Search where
+    size (SearchArgs a b _) = a + b
+
+notLteAndGt : (a, b : Nat) -> LTE a b -> GT a b -> Void
+notLteAndGt Z b aLteB aGtB = succNotLTEzero aGtB
+notLteAndGt (S k) Z aLteB aGtB = succNotLTEzero aLteB
+notLteAndGt (S k) (S j) aLteB aGtB = notLteAndGt k j (fromLteSucc aLteB) (fromLteSucc aGtB)
+
+gcd_step : (x : Search) ->
+    (rec : (y : Search) -> Smaller y x ->  (f : Nat ** GCD f (left y) (right y))) ->
+    (f : Nat ** GCD f (left x) (right x))
+gcd_step (SearchArgs Z _ bLteA {bNonZero}) _ = absurd . succNotLTEzero $ lteTransitive bNonZero bLteA
+gcd_step (SearchArgs _ Z _ {bNonZero}) _ = absurd $ succNotLTEzero bNonZero
+gcd_step (SearchArgs (S a) (S b) bLteA {bNonZero}) rec = case divMod (S a) (S b) of
+    Fraction (S a) (S b) q FZ prf =>
+        let sbIsFactor = the (S a = plus q (mult b q)) $
+                rewrite multCommutative b q in
+                rewrite sym $ multRightSuccPlus q b in
+                replace {p = \x => S a = x} (plusZeroRightNeutral (q * S b)) $ sym prf
+            skDividesA = CofactorExists q sbIsFactor
+            skDividesB = factorReflexive (S b)
+            greatest = the
+                ((q' : Nat) -> CommonFactor q' (S a) (S b) -> Factor q' (S b))
+                (\q', (CommonFactorExists q' _ qfb) => qfb)
+        in
+        (S b ** MkGCD (CommonFactorExists (S b) skDividesA skDividesB) greatest)
+
+    Fraction (S a) (S b) q (FS r) prf =>
+            let rLtSb = lteSuccRight $ elemSmallerThanBound r
+                qGt1 = the (LTE 1 q) $ case q of
+                    Z => absurd . notLteAndGt (S $ finToNat r) b (elemSmallerThanBound r) $
+                        replace {p = LTE (S b)} (sym prf) bLteA
+                    (S k) => LTESucc LTEZero
+                smaller = the (LTE (S (S (plus b (S (finToNat r))))) (S (plus a (S b)))) $
+                    rewrite plusCommutative a (S b) in
+                    LTESucc . LTESucc . plusLteLeft b . fromLteSucc $ lteTransitive (elemSmallerThanBound $ FS r) bLteA
+                (f ** MkGCD (CommonFactorExists f prfSb prfRem) greatestSbSr) =
+                    rec (SearchArgs (S b) (S $ finToNat r) rLtSb) smaller
+                prfSa = the (Factor f (S a)) $
+                    rewrite sym prf in
+                    rewrite multCommutative q (S b) in
+                    plusFactor (multNAlsoFactor prfSb q) prfRem
+                greatest = the
+                    ((q' : Nat) -> CommonFactor q' (S a) (S b) -> Factor q' f)
+                    (\q', (CommonFactorExists q' qfa qfb) =>
+                        let sbfqSb =
+                                the (Factor (S b) (q * S b)) $
+                                rewrite multCommutative q (S b) in
+                                multFactor (S b) q
+                            rightPrf = minusFactor {a = q * S b} {b = S (finToNat r)}
+                                (rewrite prf in qfa)
+                                (factorTransitive q' (S b) (q * S b) qfb sbfqSb)
+                        in
+                        greatestSbSr q' (CommonFactorExists q' qfb rightPrf)
+                    )
+            in
+            (f ** MkGCD (CommonFactorExists f prfSa prfSb) greatest)
+
+||| An implementation of Euclidean Algorithm for computing greatest common
+||| divisors. It is proven correct and total; returns a proof that computed
+||| number actually IS the GCD. Unfortunately it's very slow, so improvements
+||| in terms of efficiency would be welcome.
+export
+gcd : (a, b : Nat) -> {auto ok : NotBothZero a b} -> (f : Nat ** GCD f a b)
+gcd Z Z impossible
+gcd Z b =
+    (b ** MkGCD (CommonFactorExists b (anythingFactorZero b) (factorReflexive b)) $
+        \q, (CommonFactorExists q _ prf) => prf
+    )
+gcd a Z =
+    (a ** MkGCD (CommonFactorExists a (factorReflexive a) (anythingFactorZero a)) $
+        \q, (CommonFactorExists q prf _) => prf
+    )
+gcd (S a) (S b) with (cmp (S a) (S b))
+    gcd (S (b + S d)) (S b) | CmpGT d =
+        let aGtB = the (LTE (S b) (S (b + S d))) $
+                rewrite sym $ plusSuccRightSucc b d in
+                LTESucc . lteSuccRight $ lteAddRight b
+        in
+        sizeInd gcd_step $ SearchArgs (S (b + S d)) (S b) aGtB
+    gcd (S a) (S a)         | CmpEQ =
+        let greatest = the
+                ((q : Nat) -> CommonFactor q (S a) (S a) -> Factor q (S a))
+                (\q, (CommonFactorExists q qfa _) => qfa)
+        in
+        (S a ** MkGCD (selfIsCommonFactor (S a)) greatest)
+    gcd (S a) (S (a + S d)) | CmpLT d =
+        let aGtB = the (LTE (S a) (S (plus a (S d)))) $
+                rewrite sym $ plusSuccRightSucc a d in
+                LTESucc . lteSuccRight $ lteAddRight a
+            (f ** MkGCD prf greatest) = sizeInd gcd_step $ SearchArgs (S (a + S d)) (S a) aGtB
+        in
+        (f ** MkGCD (commonFactorSym prf) (\q, cf => greatest q $ commonFactorSym cf))
+
+||| For every two natural numbers there is a unique greatest common divisor.
+export
+gcdUnique : {a, b, p, q : Nat} -> GCD p a b -> GCD q a b -> p = q
+gcdUnique (MkGCD pCFab greatestP) (MkGCD qCFab greatestQ) =
+    factorAntisymmetric (greatestQ p pCFab) (greatestP q qCFab)
+
+
+divByGcdHelper : (a, b, c : Nat) -> GCD (S a) (S a * S b) (S a * c) -> GCD 1 (S b) c
+divByGcdHelper a b c (MkGCD _ greatest) =
+    MkGCD (CommonFactorExists 1 (oneIsFactor (S b)) (oneIsFactor c)) $
+    \q, (CommonFactorExists q (CofactorExists qb prfQB) (CofactorExists qc prfQC)) =>
+        let qFab = CofactorExists {n = S a * S b} {p = q * S a} qb $
+                rewrite multCommutative q (S a) in
+                rewrite sym $ multAssociative (S a) q qb in
+                rewrite sym $ prfQB in
+                Refl
+            qFac = CofactorExists {n = S a * c} {p = q * S a} qc $
+                rewrite multCommutative q (S a) in
+                rewrite sym $ multAssociative (S a) q qc in
+                rewrite sym $ prfQC in
+                Refl
+            CofactorExists f prfQAfA =
+                greatest (q * S a) (CommonFactorExists (q * S a) qFab qFac)
+            qf1 = multOneSoleNeutral a (f * q) $
+                rewrite multCommutative f q in
+                rewrite multAssociative (S a) q f in
+                rewrite sym $ multCommutative q (S a) in
+                prfQAfA
+        in
+        CofactorExists f $
+            rewrite multCommutative q f in
+            sym qf1
+
+
+||| For every two natural numbers, if we divide both of them by their GCD,
+||| the GCD of resulting numbers will always be 1.
+export
+divByGcdGcdOne : {a, b, c : Nat} -> GCD a (a * b) (a * c) -> GCD 1 b c
+divByGcdGcdOne {a = Z} (MkGCD {notBothZero = LeftIsNotZero} _ _) impossible
+divByGcdGcdOne {a = Z} (MkGCD {notBothZero = RightIsNotZero} _ _) impossible
+divByGcdGcdOne {a = S a} {b = Z} {c = Z} (MkGCD {notBothZero} _ _) =
+        case replace {p = \x => NotBothZero x x} (multZeroRightZero (S a)) notBothZero of
+            LeftIsNotZero impossible
+            RightIsNotZero impossible
+divByGcdGcdOne {a = S a} {b = Z} {c = S c} gcdPrf@(MkGCD {notBothZero} _ _) =
+        case replace {p = \x => NotBothZero x (S a * S c)} (multZeroRightZero (S a)) notBothZero of
+            LeftIsNotZero impossible
+            RightIsNotZero => gcdSym $ divByGcdHelper a c Z $ gcdSym gcdPrf
+divByGcdGcdOne {a = S a} {b = S b} {c = Z} gcdPrf@(MkGCD {notBothZero} _ _) =
+        case replace {p = \x => NotBothZero (S a * S b) x} (multZeroRightZero (S a)) notBothZero of
+            RightIsNotZero impossible
+            LeftIsNotZero => divByGcdHelper a b Z gcdPrf
+divByGcdGcdOne {a = S a} {b = S b} {c = S c} gcdPrf =
+        divByGcdHelper a b (S c) gcdPrf
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@ -9,6 +9,9 @@ modules = Control.Delayed,
          Data.List.Palindrome,

          Data.Bool.Extra,
+          Data.Fin.Extra,
+          Data.Nat.Equational,
+          Data.Nat.Factor,
          Data.SortedMap,
          Data.SortedSet,
          Data.String.Extra,
--- a/libs/prelude/Builtin.idr
+++ b/libs/prelude/Builtin.idr
@ -6,22 +6,35 @@ module Builtin

 ||| Assert to the totality checker that the given expression will always
 ||| terminate.
+|||
+||| The multiplicity of its argument is 1, so `assert_total` won't affect how
+||| many times variables are used. If you're not writing a linear function,
+||| this doesn't make a difference.
+|||
 ||| Note: assert_total can reduce at compile time, if required for unification,
 ||| which might mean that it's no longer guarded a subexpression. Therefore,
 ||| it is best to use it around the smallest possible subexpression.
 %inline
 public export
-assert_total : {0 a : _} -> a -> a
+assert_total : (1 _ : a) -> a
 assert_total x = x

 ||| Assert to the totality checker that y is always structurally smaller than x
 ||| (which is typically a pattern argument, and *must* be in normal form for
 ||| this to work).
+|||
+||| The multiplicity of x is 0, so in a linear function, you can pass values to
+||| x even if they have already been used.
+||| The multiplicity of y is 1, so `assert_smaller` won't affect how many times
+||| its y argument is used.
+||| If you're not writing a linear function, the multiplicities don't make a
+||| difference.
+|||
 ||| @ x the larger value (typically a pattern argument)
 ||| @ y the smaller value (typically an argument to a recursive call)
 %inline
 public export
-assert_smaller : {0 a, b : _} -> (x : a) -> (y : b) -> b
+assert_smaller : (0 x : a) -> (1 y : b) -> b
 assert_smaller x y = y

 -- Unit type and pairs
--- a/libs/prelude/PrimIO.idr
+++ b/libs/prelude/PrimIO.idr
@ -56,6 +56,14 @@ data Ptr : Type -> Type where [external]
 public export
 data AnyPtr : Type where [external]

+-- As Ptr, but associated with a finaliser that is run on garbage collection
+public export
+data GCPtr : Type -> Type where [external]
+
+-- As AnyPtr, but associated with a finaliser that is run on garbage collection
+public export
+data GCAnyPtr : Type where [external]
+
 public export
 data ThreadID : Type where [external]

@ -96,6 +104,19 @@ export %inline
 prim__nullPtr : Ptr t -> Int -- can't pass 'type' to a foreign function
 prim__nullPtr p = prim__nullAnyPtr (prim__forgetPtr p)

+%extern
+prim__onCollectAny : AnyPtr -> (AnyPtr -> PrimIO ()) -> PrimIO GCAnyPtr
+%extern
+prim__onCollect : Ptr t -> (Ptr t -> PrimIO ()) -> PrimIO (GCPtr t)
+
+export
+onCollectAny : AnyPtr -> (AnyPtr -> IO ()) -> IO GCAnyPtr
+onCollectAny ptr c = primIO (prim__onCollectAny ptr (\x => toPrim (c x)))
+
+export
+onCollect : Ptr t -> (Ptr t -> IO ()) -> IO (GCPtr t)
+onCollect ptr c = primIO (prim__onCollect ptr (\x => toPrim (c x)))
+
 %foreign "C:idris2_getString, libidris2_support"
 export
 prim__getString : Ptr String -> String
--- a/src/Compiler/CompileExpr.idr
+++ b/src/Compiler/CompileExpr.idr
@ -370,9 +370,9 @@ mutual
 --                              let env : SubstCEnv args (MN "eff" 0 :: vars)
 --                                      = mkSubst 0 (CLocal fc First) pos args in
 --                              do sc' <- toCExpTree n sc
--                                 let scope = thin {outer=args}
--                                                  {inner=vars}
--                                                  (MN "eff" 0) sc'
+--                                 let scope = insertNames {outer=args}
+--                                                         {inner=vars}
+--                                                         [MN "eff" 0] sc'
 --                                 pure $ Just (CLet fc (MN "eff" 0) False scr
 --                                                   (substs env scope))
                _ => pure Nothing -- there's a normal match to do
@ -461,6 +461,7 @@ data NArgs : Type where
     Struct : String -> List (String, Closure []) -> NArgs
     NUnit : NArgs
     NPtr : NArgs
+     NGCPtr : NArgs
     NIORes : Closure [] -> NArgs

 getPArgs : Defs -> Closure [] -> Core (String, Closure [])
@ -491,6 +492,8 @@ getNArgs : Defs -> Name -> List (Closure []) -> Core NArgs
 getNArgs defs (NS _ (UN "IORes")) [arg] = pure $ NIORes arg
 getNArgs defs (NS _ (UN "Ptr")) [arg] = pure NPtr
 getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr
+getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr
+getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr
 getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit
 getNArgs defs (NS _ (UN "Struct")) [n, args]
    = do NPrimVal _ (Str n') <- evalClosure defs n
@ -536,6 +539,7 @@ nfToCFType _ s (NTCon fc n_in _ _ args)
                   pure (CFStruct n fs')
              NUnit => pure CFUnit
              NPtr => pure CFPtr
+              NGCPtr => pure CFGCPtr
              NIORes uarg =>
                do narg <- evalClosure defs uarg
                   carg <- nfToCFType fc s narg
--- a/src/Compiler/Scheme/Chez.idr
+++ b/src/Compiler/Scheme/Chez.idr
@ -82,7 +82,7 @@ schHeader chez libs
    "(let ()\n"

 schFooter : String
-schFooter = ")"
+schFooter = "(collect 4)\n(blodwen-run-finalisers))\n"

 showChezChar : Char -> String -> String
 showChezChar '\\' = ("\\\\" ++)
@ -108,11 +108,13 @@ mutual
  tySpec (NmCon fc (UN "Double") _ []) = pure "double"
  tySpec (NmCon fc (UN "Char") _ []) = pure "char"
  tySpec (NmCon fc (NS _ n) _ [_])
-     = cond [(n == UN "Ptr", pure "void*")]
+     = cond [(n == UN "Ptr", pure "void*"),
+             (n == UN "GCPtr", pure "void*")]
          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
  tySpec (NmCon fc (NS _ n) _ [])
     = cond [(n == UN "Unit", pure "void"),
-             (n == UN "AnyPtr", pure "void*")]
+             (n == UN "AnyPtr", pure "void*"),
+             (n == UN "GCAnyPtr", pure "void*")]
          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
  tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function"))

@ -154,6 +156,14 @@ mutual
      = pure "(error \"bad setField\")"
  chezExtPrim i SysCodegen []
      = pure $ "\"chez\""
+  chezExtPrim i OnCollect [_, p, c, world]
+      = do p' <- schExp chezExtPrim chezString 0 p
+           c' <- schExp chezExtPrim chezString 0 c
+           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
+  chezExtPrim i OnCollectAny [p, c, world]
+      = do p' <- schExp chezExtPrim chezString 0 p
+           c' <- schExp chezExtPrim chezString 0 c
+           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i prim args
      = schExtCommon chezExtPrim chezString i prim args

@ -171,6 +181,7 @@ cftySpec fc CFString = pure "string"
 cftySpec fc CFDouble = pure "double"
 cftySpec fc CFChar = pure "char"
 cftySpec fc CFPtr = pure "void*"
+cftySpec fc CFGCPtr = pure "void*"
 cftySpec fc (CFFun s t) = pure "void*"
 cftySpec fc (CFIORes t) = cftySpec fc t
 cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
@ -181,6 +192,10 @@ cCall : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> (cfn : String) -> (clib : String) ->
        List (Name, CFType) -> CFType -> Core (String, String)
+cCall appdir fc cfn clib args (CFIORes CFGCPtr)
+    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
+cCall appdir fc cfn clib args CFGCPtr
+    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
 cCall appdir fc cfn clib args ret
    = do loaded <- get Loaded
         lib <- if clib `elem` loaded
@ -238,6 +253,7 @@ cCall appdir fc cfn clib args ret

    buildArg : (Name, CFType) -> Core String
    buildArg (n, CFFun s t) = callback (schName n) [s] t
+    buildArg (n, CFGCPtr) = pure $ "(car " ++ schName n ++ ")"
    buildArg (n, _) = pure $ schName n

 schemeCall : FC -> (sfn : String) ->
@ -364,6 +380,7 @@ compileToSS c appdir tm outfile
         let scm = schHeader chez (map snd libs) ++
                   support ++ code ++
                   concat (map fst fgndefs) ++
+                   "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
                   main ++ schFooter
         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
--- a/src/Compiler/Scheme/Common.idr
+++ b/src/Compiler/Scheme/Common.idr
@ -183,6 +183,8 @@ data ExtPrim = CCall | SchemeCall
             | GetField | SetField
             | VoidElim
             | SysOS | SysCodegen
+             | OnCollect
+             | OnCollectAny
             | Unknown Name

 export
@ -200,6 +202,8 @@ Show ExtPrim where
  show VoidElim = "VoidElim"
  show SysOS = "SysOS"
  show SysCodegen = "SysCodegen"
+  show OnCollect = "OnCollect"
+  show OnCollectAny = "OnCollectAny"
  show (Unknown n) = "Unknown " ++ show n

 ||| Match on a user given name to get the scheme primitive
@ -217,7 +221,9 @@ toPrim pn@(NS _ n)
            (n == UN "prim__setField", SetField),
            (n == UN "void", VoidElim),
            (n == UN "prim__os", SysOS),
-            (n == UN "prim__codegen", SysCodegen)
+            (n == UN "prim__codegen", SysCodegen),
+            (n == UN "prim__onCollect", OnCollect),
+            (n == UN "prim__onCollectAny", OnCollectAny)
            ]
           (Unknown pn)
 toPrim pn = Unknown pn
--- a/src/Compiler/Scheme/Racket.idr
+++ b/src/Compiler/Scheme/Racket.idr
@ -50,7 +50,7 @@ schHeader libs
    "(let ()\n"

 schFooter : String
-schFooter = ")"
+schFooter = ") (collect-garbage)"

 showRacketChar : Char -> String -> String
 showRacketChar '\\' = ("\\\\" ++)
@ -93,6 +93,14 @@ mutual
      = pure "(error \"bad setField\")"
  racketPrim i SysCodegen []
      = pure $ "\"racket\""
+  racketPrim i OnCollect [_, p, c, world]
+      = do p' <- schExp racketPrim racketString 0 p
+           c' <- schExp racketPrim racketString 0 c
+           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
+  racketPrim i OnCollectAny [p, c, world]
+      = do p' <- schExp racketPrim racketString 0 p
+           c' <- schExp racketPrim racketString 0 c
+           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  racketPrim i prim args
      = schExtCommon racketPrim racketString i prim args

@ -113,6 +121,7 @@ cftySpec fc CFString = pure "_string/utf-8"
 cftySpec fc CFDouble = pure "_double"
 cftySpec fc CFChar = pure "_int8"
 cftySpec fc CFPtr = pure "_pointer"
+cftySpec fc CFGCPtr = pure "_pointer"
 cftySpec fc (CFIORes t) = cftySpec fc t
 cftySpec fc (CFStruct n t) = pure $ "_" ++ n ++ "-pointer"
 cftySpec fc (CFFun s t) = funTySpec [s] t
@ -159,6 +168,10 @@ cCall : {auto f : Ref Done (List String) } ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> (cfn : String) -> (clib : String) ->
        List (Name, CFType) -> CFType -> Core (String, String)
+cCall appdir fc cfn clib args (CFIORes CFGCPtr)
+    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
+cCall appdir fc cfn clib args CFGCPtr
+    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
 cCall appdir fc cfn libspec args ret
    = do loaded <- get Loaded
         bound <- get Done
@ -181,7 +194,7 @@ cCall appdir fc cfn libspec args ret
                                    " (_fun " ++ showSep " " (map snd argTypes) ++ " -> " ++
                                        retType ++ "))\n"
         let call = "(" ++ cfn ++ " " ++
-                    showSep " " !(traverse useArg argTypes) ++ ")"
+                    showSep " " !(traverse useArg (map fst argTypes)) ++ ")"

         pure (lib ++ cbind, case ret of
                                  CFIORes rt => handleRet rt call
@ -216,9 +229,9 @@ cCall appdir fc cfn libspec args ret
             retType <- cftySpec fc retty
             pure $ mkFun args retty n

-    useArg : ((Name, CFType), String) -> Core String
-    useArg ((n, CFFun s t), _) = callback (schName n) [s] t
-    useArg ((n, ty), _)
+    useArg : (Name, CFType) -> Core String
+    useArg (n, CFFun s t) = callback (schName n) [s] t
+    useArg (n, ty)
        = pure $ rktToC ty (schName n)

 schemeCall : FC -> (sfn : String) ->
--- a/src/Control/Delayed.idr
+++ b/src/Control/Delayed.idr
@ -1,16 +0,0 @@
-||| Utilities functions for contitionally delaying values.
-module Control.Delayed
-
-%default total
-
-||| Type-level function for a conditionally infinite type.
-public export
-inf : Bool -> Type -> Type
-inf False t = t
-inf True t = Inf t
-
-||| Type-level function for a conditionally lazy type.
-public export
-lazy : Bool -> Type -> Type
-lazy False t = t
-lazy True t = Lazy t
--- a/src/Core/CaseBuilder.idr
+++ b/src/Core/CaseBuilder.idr
@ -16,10 +16,10 @@ import Decidable.Equality
 %default covering

 public export
-data Phase = CompileTime | RunTime
+data Phase = CompileTime RigCount | RunTime

 Eq Phase where
-  CompileTime == CompileTime = True
+  CompileTime r == CompileTime r' = r == r'
  RunTime == RunTime = True
  _ == _ = False

@ -95,10 +95,6 @@ updatePats env nf (p :: ps)
               pure (record { argType = Stuck !(quote empty env nf) } p :: ps)
         _ => pure (p :: ps)

-mkEnv : FC -> (vs : List Name) -> Env Term vs
-mkEnv fc [] = []
-mkEnv fc (n :: ns) = PVar top Explicit (Erased fc False) :: mkEnv fc ns
-
 substInPatInfo : {pvar, vars, todo : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 FC -> Name -> Term vars -> PatInfo pvar vars ->
@ -257,8 +253,9 @@ clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs)
    clauseType' _                 = VarClause

    getClauseType : Phase -> Pat -> ArgType vars -> ClauseType
-    getClauseType CompileTime (PCon _ _ _ _ xs) (Known r t)
-        = if isErased r && all (namesIn (pvars ++ concatMap namesFrom (getPatInfo rest))) xs
+    getClauseType (CompileTime cr) (PCon _ _ _ _ xs) (Known r t)
+        = if isErased r && not (isErased cr) &&
+             all (namesIn (pvars ++ concatMap namesFrom (getPatInfo rest))) xs
             then VarClause
             else ConClause
    getClauseType phase (PAs _ _ p) t = getClauseType phase p t
--- a/src/Core/CaseTree.idr
+++ b/src/Core/CaseTree.idr
@ -142,16 +142,6 @@ mutual
  insertCaseAltNames ns (DefaultCase ct)
      = DefaultCase (insertCaseNames ns ct)

-export
-thinTree : {outer, inner : _} ->
-           (n : Name) -> CaseTree (outer ++ inner) -> CaseTree (outer ++ n :: inner)
-thinTree n (Case idx prf scTy alts)
-    = let MkNVar prf' = insertNVar {n} _ prf in
-          Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts)
-thinTree n (STerm i tm) = STerm i (thin n tm)
-thinTree n (Unmatched msg) = Unmatched msg
-thinTree n Impossible = Impossible
-
 export
 Weaken CaseTree where
  weakenNs ns t = insertCaseNames {outer = []} ns t
--- a/src/Core/CompileExpr.idr
+++ b/src/Core/CompileExpr.idr
@ -116,6 +116,7 @@ data CFType : Type where
     CFDouble : CFType
     CFChar : CFType
     CFPtr : CFType
+     CFGCPtr : CFType
     CFWorld : CFType
     CFFun : CFType -> CFType -> CFType
     CFIORes : CFType -> CFType
@ -296,6 +297,7 @@ Show CFType where
  show CFDouble = "Double"
  show CFChar = "Char"
  show CFPtr = "Ptr"
+  show CFGCPtr = "GCPtr"
  show CFWorld = "%World"
  show (CFFun s t) = show s ++ " -> " ++ show t
  show (CFIORes t) = "IORes " ++ show t
@ -324,53 +326,6 @@ Show NamedDef where
        show args ++ " -> " ++ show ret
  show (MkNmError exp) = "Error: " ++ show exp

-mutual
-  export
-  thin : {outer : _} ->
-         (n : Name) -> CExp (outer ++ inner) -> CExp (outer ++ n :: inner)
-  thin n (CLocal fc prf)
-      = let MkNVar var' = insertNVar {n} _ prf in
-            CLocal fc var'
-  thin _ (CRef fc x) = CRef fc x
-  thin {outer} {inner} n (CLam fc x sc)
-      = let sc' = thin {outer = x :: outer} {inner} n sc in
-            CLam fc x sc'
-  thin {outer} {inner} n (CLet fc x inl val sc)
-      = let sc' = thin {outer = x :: outer} {inner} n sc in
-            CLet fc x inl (thin n val) sc'
-  thin n (CApp fc x xs)
-      = CApp fc (thin n x) (assert_total (map (thin n) xs))
-  thin n (CCon fc x tag xs)
-      = CCon fc x tag (assert_total (map (thin n) xs))
-  thin n (COp fc x xs)
-      = COp fc x (assert_total (map (thin n) xs))
-  thin n (CExtPrim fc p xs)
-      = CExtPrim fc p (assert_total (map (thin n) xs))
-  thin n (CForce fc x) = CForce fc (thin n x)
-  thin n (CDelay fc x) = CDelay fc (thin n x)
-  thin n (CConCase fc sc xs def)
-      = CConCase fc (thin n sc) (assert_total (map (thinConAlt n) xs))
-                 (assert_total (map (thin n) def))
-  thin n (CConstCase fc sc xs def)
-      = CConstCase fc (thin n sc) (assert_total (map (thinConstAlt n) xs))
-                   (assert_total (map (thin n) def))
-  thin _ (CPrimVal fc x) = CPrimVal fc x
-  thin _ (CErased fc) = CErased fc
-  thin _ (CCrash fc x) = CCrash fc x
-
-  thinConAlt : {outer : _} ->
-               (n : Name) -> CConAlt (outer ++ inner) -> CConAlt (outer ++ n :: inner)
-  thinConAlt {outer} {inner} n (MkConAlt x tag args sc)
-        = let sc' : CExp ((args ++ outer) ++ inner)
-                  = rewrite sym (appendAssociative args outer inner) in sc in
-              MkConAlt x tag args
-               (rewrite appendAssociative args outer (n :: inner) in
-                        thin n sc')
-
-  thinConstAlt : {outer : _} ->
-                 (n : Name) -> CConstAlt (outer ++ inner) -> CConstAlt (outer ++ n :: inner)
-  thinConstAlt n (MkConstAlt x sc) = MkConstAlt x (thin n sc)
-
 mutual
  export
  insertNames : {outer, inner : _} ->
@ -501,7 +456,6 @@ mutual

 export
 Weaken CExp where
-  weaken = thin {outer = []} _
  weakenNs ns tm = insertNames {outer = []} ns tm

 -- Substitute some explicit terms for names in a term, and remove those
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@ -2016,6 +2016,13 @@ setAmbigLimit max
    = do defs <- get Ctxt
         put Ctxt (record { options->elabDirectives->ambigLimit = max } defs)

+export
+setAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
+                       Nat -> Core ()
+setAutoImplicitLimit max
+    = do defs <- get Ctxt
+         put Ctxt (record { options->elabDirectives->autoImplicitLimit = max } defs)
+
 export
 isLazyActive : {auto c : Ref Ctxt Defs} ->
               Core Bool
@ -2049,6 +2056,13 @@ getAmbigLimit
    = do defs <- get Ctxt
         pure (ambigLimit (elabDirectives (options defs)))

+export
+getAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
+                       Core Nat
+getAutoImplicitLimit
+    = do defs <- get Ctxt
+         pure (autoImplicitLimit (elabDirectives (options defs)))
+
 export
 setPair : {auto c : Ref Ctxt Defs} ->
          FC -> (pairType : Name) -> (fstn : Name) -> (sndn : Name) ->
--- a/src/Core/Directory.idr
+++ b/src/Core/Directory.idr
@ -113,9 +113,10 @@ mkdirAll dir = if parse dir == emptyPath
                  else do exist <- dirExists dir
                          if exist 
                             then pure (Right ())
-                             else do case parent dir of
+                             else do Right () <- case parent dir of
                                          Just parent => mkdirAll parent
                                          Nothing => pure (Right ()) 
+                                        | err => pure err
                                     createDir dir

 -- Given a namespace (i.e. a module name), make the build directory for the
--- a/src/Core/Env.idr
+++ b/src/Core/Env.idr
@ -233,5 +233,63 @@ shrinkEnv env SubRefl = Just env
 shrinkEnv (b :: env) (DropCons p) = shrinkEnv env p
 shrinkEnv (b :: env) (KeepCons p)
    = do env' <- shrinkEnv env p
-         b' <- shrinkBinder b p
+         b' <- assert_total (shrinkBinder b p)
         pure (b' :: env')
+
+-- Make a dummy environment, if we genuinely don't care about the values
+-- and types of the contents.
+-- We use this when building and comparing case trees.
+export
+mkEnv : FC -> (vs : List Name) -> Env Term vs
+mkEnv fc [] = []
+mkEnv fc (n :: ns) = PVar top Explicit (Erased fc False) :: mkEnv fc ns
+
+-- Update an environment so that all names are guaranteed unique. In the
+-- case of a clash, the most recently bound is left unchanged.
+export
+uniqifyEnv : {vars : _} ->
+             Env Term vars ->
+             (vars' ** (Env Term vars', CompatibleVars vars vars'))
+uniqifyEnv env = uenv [] env
+  where
+    next : Name -> Name
+    next (MN n i) = MN n (i + 1)
+    next (UN n) = MN n 0
+    next (NS ns n) = NS ns (next n)
+    next n = MN (show n) 0
+
+    uniqueLocal : List Name -> Name -> Name
+    uniqueLocal vs n
+       = if n `elem` vs
+                 -- we'll find a new name eventualy since the list of names
+                 -- is empty, and next generates something new. But next has
+                 -- to be correct... an exercise for someone: this could
+                 -- probebly be done without an assertion by making a stream of
+                 -- possible names...
+            then assert_total (uniqueLocal vs (next n))
+            else n
+
+    uenv : {vars : _} ->
+           List Name -> Env Term vars ->
+           (vars' ** (Env Term vars', CompatibleVars vars vars'))
+    uenv used [] = ([] ** ([], CompatPre))
+    uenv used {vars = v :: vs} (b :: bs)
+        = if v `elem` used
+             then let v' = uniqueLocal used v
+                      (vs' ** (env', compat)) = uenv (v' :: used) bs
+                      b' = map (renameVars compat) b in
+                  (v' :: vs' ** (b' :: env', CompatExt compat))
+             else let (vs' ** (env', compat)) = uenv (v :: used) bs
+                      b' = map (renameVars compat) b in
+                  (v :: vs' ** (b' :: env', CompatExt compat))
+
+export
+allVars : {vars : _} -> Env Term vars -> List (Var vars)
+allVars [] = []
+allVars (v :: vs) = MkVar First :: map weaken (allVars vs)
+
+export
+allVarsNoLet : {vars : _} -> Env Term vars -> List (Var vars)
+allVarsNoLet [] = []
+allVarsNoLet (Let _ _ _ :: vs) = map weaken (allVars vs)
+allVarsNoLet (v :: vs) = MkVar First :: map weaken (allVars vs)
--- a/src/Core/Name.idr
+++ b/src/Core/Name.idr
@ -199,4 +199,3 @@ namesEq (x :: xs) (y :: ys)
         rewrite ps
         Just Refl
 namesEq _ _ = Nothing
-
--- a/src/Core/Normalise.idr
+++ b/src/Core/Normalise.idr
@ -86,6 +86,11 @@ updateLimit Func n opts
             else (x, l) :: set n v xs
 updateLimit t n opts = pure (Just opts)

+data CaseResult a
+     = Result a
+     | NoMatch -- case alternative didn't match anything
+     | GotStuck -- alternative matched, but got stuck later
+
 parameters (defs : Defs, topopts : EvalOpts)
  mutual
    eval : {free, vars : _} ->
@ -251,54 +256,54 @@ parameters (defs : Defs, topopts : EvalOpts)
                 (args : List Name) ->
                 List (Closure free) ->
                 CaseTree (args ++ more) ->
-                 (defval : Core (NF free)) ->
-                 Core (NF free)
-    evalConAlt env loc opts fc stk args args' sc def
-         = maybe def (\bound => evalTree env bound opts fc stk sc def)
-                     (getCaseBound args' args loc)
+                 Core (CaseResult (NF free))
+    evalConAlt env loc opts fc stk args args' sc
+         = do let Just bound = getCaseBound args' args loc
+                   | Nothing => pure GotStuck
+              evalTree env bound opts fc stk sc

    tryAlt : {free, more : _} ->
             Env Term free ->
             LocalEnv free more -> EvalOpts -> FC ->
             Stack free -> NF free -> CaseAlt more ->
-             (defval : Core (NF free)) -> Core (NF free)
+             Core (CaseResult (NF free))
    -- Ordinary constructor matching
-    tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc) def
+    tryAlt {more} env loc opts fc stk (NDCon _ nm tag' arity args') (ConCase x tag args sc)
         = if tag == tag'
-              then evalConAlt env loc opts fc stk args args' sc def
-              else def
+              then evalConAlt env loc opts fc stk args args' sc
+              else pure NoMatch
    -- Type constructor matching, in typecase
-    tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc) def
+    tryAlt {more} env loc opts fc stk (NTCon _ nm tag' arity args') (ConCase nm' tag args sc)
         = if nm == nm'
-              then evalConAlt env loc opts fc stk args args' sc def
-              else def
+              then evalConAlt env loc opts fc stk args args' sc
+              else pure NoMatch
    -- Primitive type matching, in typecase
-    tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase (UN x) tag [] sc) def
+    tryAlt env loc opts fc stk (NPrimVal _ c) (ConCase (UN x) tag [] sc)
         = if show c == x
-              then evalTree env loc opts fc stk sc def
-              else def
+              then evalTree env loc opts fc stk sc
+              else pure NoMatch
    -- Type of type matching, in typecase
-    tryAlt env loc opts fc stk (NType _) (ConCase (UN "Type") tag [] sc) def
-         = evalTree env loc opts fc stk sc def
+    tryAlt env loc opts fc stk (NType _) (ConCase (UN "Type") tag [] sc)
+         = evalTree env loc opts fc stk sc
    -- Arrow matching, in typecase
    tryAlt {more}
-           env loc opts fc stk (NBind pfc x (Pi r e aty) scty) (ConCase (UN "->") tag [s,t] sc) def
+           env loc opts fc stk (NBind pfc x (Pi r e aty) scty) (ConCase (UN "->") tag [s,t] sc)
       = evalConAlt {more} env loc opts fc stk [s,t]
                  [MkNFClosure aty,
                   MkNFClosure (NBind pfc x (Lam r e aty) scty)]
-                  sc def
+                  sc
    -- Delay matching
-    tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc) def
-         = evalTree env (ty :: arg :: loc) opts fc stk sc def
+    tryAlt env loc opts fc stk (NDelay _ _ ty arg) (DelayCase tyn argn sc)
+         = evalTree env (ty :: arg :: loc) opts fc stk sc
    -- Constant matching
-    tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc) def
-         = if c == c' then evalTree env loc opts fc stk sc def
-                      else def
+    tryAlt env loc opts fc stk (NPrimVal _ c') (ConstCase c sc)
+         = if c == c' then evalTree env loc opts fc stk sc
+                      else pure NoMatch
    -- Default case matches against any *concrete* value
-    tryAlt env loc opts fc stk val (DefaultCase sc) def
+    tryAlt env loc opts fc stk val (DefaultCase sc)
         = if concrete val
-              then evalTree env loc opts fc stk sc def
-              else def
+              then evalTree env loc opts fc stk sc
+              else pure GotStuck
      where
        concrete : NF free -> Bool
        concrete (NDCon _ _ _ _ _) = True
@ -307,33 +312,38 @@ parameters (defs : Defs, topopts : EvalOpts)
        concrete (NBind _ _ _ _) = True
        concrete (NType _) = True
        concrete _ = False
-    tryAlt _ _ _ _ _ _ _ def = def
+    tryAlt _ _ _ _ _ _ _ = pure GotStuck

    findAlt : {args, free : _} ->
              Env Term free ->
              LocalEnv free args -> EvalOpts -> FC ->
              Stack free -> NF free -> List (CaseAlt args) ->
-              (defval : Core (NF free)) -> Core (NF free)
-    findAlt env loc opts fc stk val [] def = def
-    findAlt env loc opts fc stk val (x :: xs) def
-         = tryAlt env loc opts fc stk val x (findAlt env loc opts fc stk val xs def)
+              Core (CaseResult (NF free))
+    findAlt env loc opts fc stk val [] = pure GotStuck
+    findAlt env loc opts fc stk val (x :: xs)
+         = do Result val <- tryAlt env loc opts fc stk val x
+                   | NoMatch => findAlt env loc opts fc stk val xs
+                   | GotStuck => pure GotStuck
+              pure (Result val)

    evalTree : {args, free : _} -> Env Term free -> LocalEnv free args ->
               EvalOpts -> FC ->
               Stack free -> CaseTree args ->
-               (defval : Core (NF free)) -> Core (NF free)
-    evalTree env loc opts fc stk (Case idx x _ alts) def
+               Core (CaseResult (NF free))
+    evalTree env loc opts fc stk (Case idx x _ alts)
      = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc
           let loc' = updateLocal idx (varExtend x) loc xval
-           findAlt env loc' opts fc stk xval alts def
-    evalTree env loc opts fc stk (STerm _ tm) def
+           findAlt env loc' opts fc stk xval alts
+    evalTree env loc opts fc stk (STerm _ tm)
          = case fuel opts of
-                 Nothing => evalWithOpts defs opts env loc (embed tm) stk
-                 Just Z => def
+                 Nothing => do res <- evalWithOpts defs opts env loc (embed tm) stk
+                               pure (Result res)
+                 Just Z => pure GotStuck
                 Just (S k) =>
                      do let opts' = record { fuel = Just k } opts
-                         evalWithOpts defs opts' env loc (embed tm) stk
-    evalTree env loc opts fc stk _ def = def
+                         res <- evalWithOpts defs opts' env loc (embed tm) stk
+                         pure (Result res)
+    evalTree env loc opts fc stk _ = pure GotStuck

    -- Take arguments from the stack, as long as there's enough.
    -- Returns the arguments, and the rest of the stack
@ -403,7 +413,9 @@ parameters (defs : Defs, topopts : EvalOpts)
             then case argsFromStack args stk of
                       Nothing => pure def
                       Just (locs', stk') =>
-                            evalTree env locs' opts fc stk' tree (pure def)
+                            do Result res <- evalTree env locs' opts fc stk' tree
+                                    | _ => pure def
+                               pure res
             else pure def
    evalDef env opts meta fc rigd (Builtin op) flags stk def
        = evalOp (getOp op) stk def
@ -694,6 +706,47 @@ interface Convert (tm : List Name -> Type) where
      = do q <- newRef QVar 0
           convGen q defs env tm tm'

+tryUpdate : {vars, vars' : _} ->
+            List (Var vars, Var vars') ->
+            Term vars -> Maybe (Term vars')
+tryUpdate ms (Local fc l idx p)
+    = do MkVar p' <- findIdx ms idx
+         pure $ Local fc l _ p'
+  where
+    findIdx : List (Var vars, Var vars') -> Nat -> Maybe (Var vars')
+    findIdx [] _ = Nothing
+    findIdx ((MkVar {i} _, v) :: ps) n
+        = if i == n then Just v else findIdx ps n
+tryUpdate ms (Ref fc nt n) = pure $ Ref fc nt n
+tryUpdate ms (Meta fc n i args) = pure $ Meta fc n i !(traverse (tryUpdate ms) args)
+tryUpdate ms (Bind fc x b sc)
+    = do b' <- tryUpdateB b
+         pure $ Bind fc x b' !(tryUpdate (map weakenP ms) sc)
+  where
+    tryUpdatePi : PiInfo (Term vars) -> Maybe (PiInfo (Term vars'))
+    tryUpdatePi Explicit = pure Explicit
+    tryUpdatePi Implicit = pure Implicit
+    tryUpdatePi AutoImplicit = pure AutoImplicit
+    tryUpdatePi (DefImplicit t) = pure $ DefImplicit !(tryUpdate ms t)
+
+    tryUpdateB : Binder (Term vars) -> Maybe (Binder (Term vars'))
+    tryUpdateB (Lam r p t) = pure $ Lam r !(tryUpdatePi p) !(tryUpdate ms t)
+    tryUpdateB (Let r v t) = pure $ Let r !(tryUpdate ms v) !(tryUpdate ms t)
+    tryUpdateB (Pi r p t) = pure $ Pi r !(tryUpdatePi p) !(tryUpdate ms t)
+    tryUpdateB _ = Nothing
+
+    weakenP : {n : _} -> (Var vars, Var vars') ->
+              (Var (n :: vars), Var (n :: vars'))
+    weakenP (v, vs) = (weaken v, weaken vs)
+tryUpdate ms (App fc f a) = pure $ App fc !(tryUpdate ms f) !(tryUpdate ms a)
+tryUpdate ms (As fc s a p) = pure $ As fc s !(tryUpdate ms a) !(tryUpdate ms p)
+tryUpdate ms (TDelayed fc r tm) = pure $ TDelayed fc r !(tryUpdate ms tm)
+tryUpdate ms (TDelay fc r ty tm) = pure $ TDelay fc r !(tryUpdate ms ty) !(tryUpdate ms tm)
+tryUpdate ms (TForce fc r tm) = pure $ TForce fc r !(tryUpdate ms tm)
+tryUpdate ms (PrimVal fc c) = pure $ PrimVal fc c
+tryUpdate ms (Erased fc i) = pure $ Erased fc i
+tryUpdate ms (TType fc) = pure $ TType fc
+
 mutual
  allConv : {vars : _} ->
            Ref QVar Int -> Defs -> Env Term vars ->
@ -703,6 +756,87 @@ mutual
      = pure $ !(convGen q defs env x y) && !(allConv q defs env xs ys)
  allConv q defs env _ _ = pure False

+  -- If the case trees match in structure, get the list of variables which
+  -- have to match in the call
+  getMatchingVarAlt : {args, args' : _} ->
+                      Defs ->
+                      List (Var args, Var args') ->
+                      CaseAlt args -> CaseAlt args' ->
+                      Core (Maybe (List (Var args, Var args')))
+  getMatchingVarAlt defs ms (ConCase n tag cargs t) (ConCase n' tag' cargs' t')
+      = if n == n'
+           then do let Just ms' = extend cargs cargs' ms
+                        | Nothing => pure Nothing
+                   Just ms <- getMatchingVars defs ms' t t'
+                        | Nothing => pure Nothing
+                   -- drop the prefix from cargs/cargs' since they won't
+                   -- be in the caller
+                   pure (Just (mapMaybe (dropP cargs cargs') ms))
+           else pure Nothing
+    where
+      weakenP : {c, c', args, args' : _} ->
+                (Var args, Var args') ->
+                (Var (c :: args), Var (c' :: args'))
+      weakenP (v, vs) = (weaken v, weaken vs)
+
+      extend : (cs : List Name) -> (cs' : List Name) ->
+               (List (Var args, Var args')) ->
+               Maybe (List (Var (cs ++ args), Var (cs' ++ args')))
+      extend [] [] ms = pure ms
+      extend (c :: cs) (c' :: cs') ms
+          = do rest <- extend cs cs' ms
+               pure ((MkVar First, MkVar First) :: map weakenP rest)
+      extend _ _ _ = Nothing
+
+      dropV : forall args .
+              (cs : List Name) -> Var (cs ++ args) -> Maybe (Var args)
+      dropV [] v = Just v
+      dropV (c :: cs) (MkVar First) = Nothing
+      dropV (c :: cs) (MkVar (Later x))
+          = dropV cs (MkVar x)
+
+      dropP : (cs : List Name) -> (cs' : List Name) ->
+              (Var (cs ++ args), Var (cs' ++ args')) ->
+              Maybe (Var args, Var args')
+      dropP cs cs' (x, y) = pure (!(dropV cs x), !(dropV cs' y))
+
+  getMatchingVarAlt defs ms (ConstCase c t) (ConstCase c' t')
+      = if c == c'
+           then getMatchingVars defs ms t t'
+           else pure Nothing
+  getMatchingVarAlt defs ms (DefaultCase t) (DefaultCase t')
+      = getMatchingVars defs ms t t'
+  getMatchingVarAlt defs _ _ _ = pure Nothing
+
+  getMatchingVarAlts : {args, args' : _} ->
+                       Defs ->
+                       List (Var args, Var args') ->
+                       List (CaseAlt args) -> List (CaseAlt args') ->
+                       Core (Maybe (List (Var args, Var args')))
+  getMatchingVarAlts defs ms [] [] = pure (Just ms)
+  getMatchingVarAlts defs ms (a :: as) (a' :: as')
+      = do Just ms <- getMatchingVarAlt defs ms a a'
+                | Nothing => pure Nothing
+           getMatchingVarAlts defs ms as as'
+  getMatchingVarAlts defs _ _ _ = pure Nothing
+
+  getMatchingVars : {args, args' : _} ->
+                    Defs ->
+                    List (Var args, Var args') ->
+                    CaseTree args -> CaseTree args' ->
+                    Core (Maybe (List (Var args, Var args')))
+  getMatchingVars defs ms (Case _ p _ alts) (Case _ p' _ alts')
+      = getMatchingVarAlts defs ((MkVar p, MkVar p') :: ms) alts alts'
+  getMatchingVars defs ms (STerm i tm) (STerm i' tm')
+      = do let Just tm'' = tryUpdate ms tm
+               | Nothing => pure Nothing
+           if !(convert defs (mkEnv (getLoc tm) args') tm'' tm')
+              then pure (Just ms)
+              else pure Nothing
+  getMatchingVars defs ms (Unmatched _) (Unmatched _) = pure (Just ms)
+  getMatchingVars defs ms Impossible Impossible = pure (Just ms)
+  getMatchingVars _ _ _ _ = pure Nothing
+
  chkSameDefs : {vars : _} ->
                Ref QVar Int -> Defs -> Env Term vars ->
                Name -> Name ->
@ -712,9 +846,32 @@ mutual
               | _ => pure False
          Just (PMDef _ args' ct' rt' _) <- lookupDefExact n' (gamma defs)
               | _ => pure False
-          if (length args == length args' && eqTree rt rt')
-             then allConv q defs env nargs nargs'
-             else pure False
+
+          -- If the two case blocks match in structure, get which variables
+          -- correspond. If corresponding variables convert, the two case
+          -- blocks convert.
+          Just ms <- getMatchingVars defs [] ct ct'
+               | Nothing => pure False
+          convertMatches ms
+     where
+       -- We've only got the index into the argument list, and the indices
+       -- don't match up, which is annoying. But it'll always be there!
+       getArgPos : Nat -> List (Closure vars) -> Maybe (Closure vars)
+       getArgPos _ [] = Nothing
+       getArgPos Z (c :: cs) = pure c
+       getArgPos (S k) (c :: cs) = getArgPos k cs
+
+       convertMatches : {vs, vs' : _} ->
+                        List (Var vs, Var vs') ->
+                        Core Bool
+       convertMatches [] = pure True
+       convertMatches ((MkVar {i} p, MkVar {i=i'} p') :: vs)
+          = do let Just varg = getArgPos i nargs
+                   | Nothing => pure False
+               let Just varg' = getArgPos i' nargs'
+                   | Nothing => pure False
+               pure $ !(convGen q defs env varg varg') &&
+                      !(convertMatches vs)

  -- If two names are standing for case blocks, check the blocks originate
  -- from the same place, and have the same scrutinee
--- a/src/Core/Options.idr
+++ b/src/Core/Options.idr
@ -104,6 +104,7 @@ record ElabDirectives where
  totality : TotalReq
  ambigLimit : Nat
  undottedRecordProjections : Bool
+  autoImplicitLimit : Nat

 public export
 record Session where
@ -153,7 +154,7 @@ defaultSession = MkSessionOpts False False False Chez 0 False False

 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 True 50

 export
 defaults : Options
--- a/src/Core/Reflect.idr
+++ b/src/Core/Reflect.idr
@ -228,6 +228,13 @@ Reify Name where
                 => do ns' <- reify defs !(evalClosure defs ns)
                       n' <- reify defs !(evalClosure defs n)
                       pure (NS ns' n')
+             (NS _ (UN "DN"), [str, n])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       n' <- reify defs !(evalClosure defs n)
+                       pure (DN str' n')
+             (NS _ (UN "RF"), [str])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       pure (RF str')
             _ => cantReify val "Name"
  reify defs val = cantReify val "Name"

@ -244,6 +251,13 @@ Reflect Name where
      = do ns' <- reflect fc defs lhs env ns
           n' <- reflect fc defs lhs env n
           appCon fc defs (reflectiontt "NS") [ns', n']
+  reflect fc defs lhs env (DN str n)
+      = do str' <- reflect fc defs lhs env str
+           n' <- reflect fc defs lhs env n
+           appCon fc defs (reflectiontt "DN") [str', n']
+  reflect fc defs lhs env (RF x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "RF") [x']
  reflect fc defs lhs env (Resolved i)
      = case !(full (gamma defs) (Resolved i)) of
             Resolved _ => cantReflect fc "Name"
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@ -711,42 +711,6 @@ insertNVarNames {ns} {outer = (y :: xs)} (S i) (Later x)
    = let MkNVar prf = insertNVarNames {ns} i x in
          MkNVar (Later prf)

-export
-thin : {outer, inner : _} ->
-       (n : Name) -> Term (outer ++ inner) -> Term (outer ++ n :: inner)
-thin n (Local fc r idx prf)
-    = let MkNVar var' = insertNVar {n} idx prf in
-          Local fc r _ var'
-thin n (Ref fc nt name) = Ref fc nt name
-thin n (Meta fc name idx args) = Meta fc name idx (map (thin n) args)
-thin {outer} {inner} n (Bind fc x b scope)
-    = let sc' = thin {outer = x :: outer} {inner} n scope in
-          Bind fc x (thinBinder n b) sc'
-  where
-    thinPi : (n : Name) -> PiInfo (Term (outer ++ inner)) ->
-             PiInfo (Term (outer ++ n :: inner))
-    thinPi n Explicit = Explicit
-    thinPi n Implicit = Implicit
-    thinPi n AutoImplicit = AutoImplicit
-    thinPi n (DefImplicit t) = DefImplicit (thin n t)
-
-    thinBinder : (n : Name) -> Binder (Term (outer ++ inner)) ->
-                 Binder (Term (outer ++ n :: inner))
-    thinBinder n (Lam c p ty) = Lam c (thinPi n p) (thin n ty)
-    thinBinder n (Let c val ty) = Let c (thin n val) (thin n ty)
-    thinBinder n (Pi c p ty) = Pi c (thinPi n p) (thin n ty)
-    thinBinder n (PVar c p ty) = PVar c (thinPi n p) (thin n ty)
-    thinBinder n (PLet c val ty) = PLet c (thin n val) (thin n ty)
-    thinBinder n (PVTy c ty) = PVTy c (thin n ty)
-thin n (App fc fn arg) = App fc (thin n fn) (thin n arg)
-thin n (As fc s nm tm) = As fc s (thin n nm) (thin n tm)
-thin n (TDelayed fc r ty) = TDelayed fc r (thin n ty)
-thin n (TDelay fc r ty tm) = TDelay fc r (thin n ty) (thin n tm)
-thin n (TForce fc r tm) = TForce fc r (thin n tm)
-thin n (PrimVal fc c) = PrimVal fc c
-thin n (Erased fc i) = Erased fc i
-thin n (TType fc) = TType fc
-
 export
 insertNames : {outer, inner : _} ->
              (ns : List Name) -> Term (outer ++ inner) ->
@ -774,7 +738,6 @@ insertNames ns (TType fc) = TType fc

 export
 Weaken Term where
-  weaken tm = thin {outer = []} _ tm
  weakenNs ns tm = insertNames {outer = []} ns tm

 export
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@ -688,6 +688,7 @@ TTC CFType where
  toBuf b (CFIORes t) = do tag 9; toBuf b t
  toBuf b (CFStruct n a) = do tag 10; toBuf b n; toBuf b a
  toBuf b (CFUser n a) = do tag 11; toBuf b n; toBuf b a
+  toBuf b CFGCPtr = tag 12

  fromBuf b
      = case !getTag of
@ -703,6 +704,7 @@ TTC CFType where
             9 => do t <- fromBuf b; pure (CFIORes t)
             10 => do n <- fromBuf b; a <- fromBuf b; pure (CFStruct n a)
             11 => do n <- fromBuf b; a <- fromBuf b; pure (CFUser n a)
+             12 => pure CFGCPtr
             _ => corrupt "CFType"

 export
--- a/src/Core/Termination.idr
+++ b/src/Core/Termination.idr
@ -157,6 +157,9 @@ mutual
      = findSC defs env g pats tm
  findSC defs env g pats tm
      = do let (fn, args) = getFnArgs tm
+           -- if it's a 'case' or 'if' just go straight into the arguments
+           Nothing <- handleCase fn args
+               | Just res => pure res
           fn' <- conIfGuarded fn -- pretend it's a data constructor if
                                  -- it has the AllGuarded flag
           case (g, fn', args) of
@ -186,6 +189,14 @@ mutual
                 do scs <- traverse (findSC defs env Unguarded pats) args
                    pure (concat scs)
      where
+        handleCase : Term vars -> List (Term vars) -> Core (Maybe (List SCCall))
+        handleCase (Ref fc nt n) args
+            = do n' <- toFullNames n
+                 if caseFn n'
+                    then Just <$> findSCcall defs env g pats fc n 4 args
+                    else pure Nothing
+        handleCase _ _ = pure Nothing
+
        conIfGuarded : Term vars -> Core (Term vars)
        conIfGuarded (Ref fc Func n)
            = do defs <- get Ctxt
--- a/src/Core/Unify.idr
+++ b/src/Core/Unify.idr
@ -380,13 +380,13 @@ patternEnv {vars} env args
               Nothing => updateVars ps svs
               Just p' => p' :: updateVars ps svs

-getVarsBelowTm : Nat -> List (Term vars) -> Maybe (List (Var vars))
-getVarsBelowTm max [] = Just []
-getVarsBelowTm max (Local fc r idx v :: xs)
-    = if idx >= max then Nothing
-         else do xs' <- getVarsBelowTm idx xs
+getVarsTm : List Nat -> List (Term vars) -> Maybe (List (Var vars))
+getVarsTm got [] = Just []
+getVarsTm got (Local fc r idx v :: xs)
+    = if idx `elem` got then Nothing
+         else do xs' <- getVarsTm (idx :: got) xs
                 pure (MkVar v :: xs')
-getVarsBelowTm _ (_ :: xs) = Nothing
+getVarsTm _ (_ :: xs) = Nothing

 export
 patternEnvTm : {auto c : Ref Ctxt Defs} ->
@ -398,7 +398,7 @@ patternEnvTm : {auto c : Ref Ctxt Defs} ->
 patternEnvTm {vars} env args
    = do defs <- get Ctxt
         empty <- clearDefs defs
-         case getVarsBelowTm 1000000 args of
+         case getVarsTm [] args of
              Nothing => pure Nothing
              Just vs =>
                 let (newvars ** svs) = toSubVars _ vs in
@ -450,6 +450,22 @@ occursCheck fc env mode mname tm
               (Ref _ _ _, args) => traverse_ (failOnStrongRigid True err) args
               (f, args) => traverse_ (failOnStrongRigid bad err) args

+-- How the variables in a metavariable definition map to the variables in
+-- the solution term (the Var newvars)
+data IVars : List Name -> List Name -> Type where
+     INil : IVars [] newvars
+     ICons : Maybe (Var newvars) -> IVars vs newvars ->
+             IVars (v :: vs) newvars
+
+Weaken (IVars vs) where
+  weaken INil = INil
+  weaken (ICons Nothing ts) = ICons Nothing (weaken ts)
+  weaken (ICons (Just t) ts) = ICons (Just (weaken t)) (weaken ts)
+
+getIVars : IVars vs ns -> List (Maybe (Var ns))
+getIVars INil = []
+getIVars (ICons v vs) = v :: getIVars vs
+
 -- Instantiate a metavariable by binding the variables in 'newvars'
 -- and returning the term
 -- If the type of the metavariable doesn't have enough arguments, fail, because
@ -474,13 +490,13 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
         let ty = type mdef -- assume all pi binders we need are there since
                            -- it was built from an environment, so no need
                            -- to normalise
-         defs <- get Ctxt
-         rhs <- mkDef [] newvars (snocList newvars)
-                     (rewrite appendNilRightNeutral newvars in locs)
-                     (rewrite appendNilRightNeutral newvars in tm)
-                     ty
-         logTerm 5 ("Instantiated: " ++ show mname) ty
+         logTerm 5 ("Type: " ++ show mname) ty
+         log 5 ("With locs: " ++ show locs)
         log 5 ("From vars: " ++ show newvars)
+
+         defs <- get Ctxt
+         rhs <- mkDef locs INil tm ty
+
         logTerm 5 "Definition" rhs
         let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs)
         let newdef = record { definition =
@ -498,63 +514,95 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
    isSimple (TType _) = True
    isSimple _ = False

-    updateLoc : {v : Nat} -> List (Var vs) -> (0 p : IsVar name v vs') ->
-                Maybe (Var vs)
-    updateLoc [] el = Nothing
-    updateLoc (p :: ps) First = Just p
-    updateLoc (p :: ps) (Later prf) = updateLoc ps prf
+    updateIVar : {v : Nat} ->
+                 forall vs, newvars . IVars vs newvars -> (0 p : IsVar name v newvars) ->
+                 Maybe (Var vs)
+    updateIVar {v} (ICons Nothing rest) prf
+        = do MkVar prf' <- updateIVar rest prf
+             Just (MkVar (Later prf'))
+    updateIVar {v} (ICons (Just (MkVar {i} p)) rest) prf
+        = if v == i
+             then Just (MkVar First)
+             else do MkVar prf' <- updateIVar rest prf
+                     Just (MkVar (Later prf'))
+    updateIVar _ _ = Nothing

-    -- Since the order of variables is not necessarily the same in the solution,
-    -- this is to make sure the variables point to the right argument, given
-    -- the argument list we got from the application of the hole.
-    updateLocs : List (Var vs) -> Term vs -> Maybe (Term vs)
-    updateLocs locs (Local fc r idx p)
-        = do MkVar p' <- updateLoc locs p
+    updateIVars : {vs, newvars : _} ->
+                  IVars vs newvars -> Term newvars -> Maybe (Term vs)
+    updateIVars ivs (Local fc r idx p)
+        = do MkVar p' <- updateIVar ivs p
             Just (Local fc r _ p')
-    updateLocs {vs} locs (Bind fc x b sc)
-        = do b' <- updateLocsB b
-             sc' <- updateLocs
-                       (MkVar First :: map (\ (MkVar p) => (MkVar (Later p))) locs)
-                       sc
+    updateIVars ivs (Ref fc nt n) = pure $ Ref fc nt n
+    updateIVars ivs (Meta fc n i args)
+        = pure $ Meta fc n i !(traverse (updateIVars ivs) args)
+    updateIVars {vs} ivs (Bind fc x b sc)
+        = do b' <- updateIVarsB ivs b
+             sc' <- updateIVars (ICons (Just (MkVar First)) (weaken ivs)) sc
             Just (Bind fc x b' sc')
      where
-        updateLocsB : Binder (Term vs) -> Maybe (Binder (Term vs))
-        updateLocsB (Lam c p t) = Just (Lam c p !(updateLocs locs t))
-        updateLocsB (Let c v t) = Just (Let c !(updateLocs locs v) !(updateLocs locs t))
+        updateIVarsPi : {vs, newvars : _} ->
+                        IVars vs newvars -> PiInfo (Term newvars) -> Maybe (PiInfo (Term vs))
+        updateIVarsPi ivs Explicit = Just Explicit
+        updateIVarsPi ivs Implicit = Just Implicit
+        updateIVarsPi ivs AutoImplicit = Just AutoImplicit
+        updateIVarsPi ivs (DefImplicit t)
+            = do t' <- updateIVars ivs t
+                 Just (DefImplicit t')
+
+        updateIVarsB : {vs, newvars : _} ->
+                       IVars vs newvars -> Binder (Term newvars) -> Maybe (Binder (Term vs))
+        updateIVarsB ivs (Lam c p t)
+            = do p' <- updateIVarsPi ivs p
+                 Just (Lam c p' !(updateIVars ivs t))
+        updateIVarsB ivs (Let c v t) = Just (Let c !(updateIVars ivs v) !(updateIVars ivs t))
        -- Make 'pi' binders have multiplicity W when we infer a Rig1 metavariable,
        -- since this is the most general thing to do if it's unknown.
-        updateLocsB (Pi rig p t) = if isLinear rig
-            then  do t' <- updateLocs locs t
-                     pure $ if inLam mode
-                        then (Pi linear p t')
-                        else (Pi top p t')
-            else Just (Pi rig p !(updateLocs locs t))
-        updateLocsB (PVar c p t) = Just (PVar c p !(updateLocs locs t))
-        updateLocsB (PLet c v t) = Just (PLet c !(updateLocs locs v) !(updateLocs locs t))
-        updateLocsB (PVTy c t) = Just (PVTy c !(updateLocs locs t))
+        updateIVarsB ivs (Pi rig p t)
+            = do p' <- updateIVarsPi ivs p
+                 if isLinear rig
+                    then do t' <- updateIVars ivs t
+                            pure $ if inLam mode
+                               then (Pi linear p' t')
+                               else (Pi top p' t')
+                    else Just (Pi rig p' !(updateIVars ivs t))
+        updateIVarsB ivs (PVar c p t)
+            = do p' <- updateIVarsPi ivs p
+                 Just (PVar c p' !(updateIVars ivs t))
+        updateIVarsB ivs (PLet c v t) = Just (PLet c !(updateIVars ivs v) !(updateIVars ivs t))
+        updateIVarsB ivs (PVTy c t) = Just (PVTy c !(updateIVars ivs t))
+    updateIVars ivs (App fc f a)
+        = Just (App fc !(updateIVars ivs f) !(updateIVars ivs a))
+    updateIVars ivs (As fc u a p)
+        = Just (As fc u !(updateIVars ivs a) !(updateIVars ivs p))
+    updateIVars ivs (TDelayed fc r arg)
+        = Just (TDelayed fc r !(updateIVars ivs arg))
+    updateIVars ivs (TDelay fc r ty arg)
+        = Just (TDelay fc r !(updateIVars ivs ty) !(updateIVars ivs arg))
+    updateIVars ivs (TForce fc r arg)
+        = Just (TForce fc r !(updateIVars ivs arg))
+    updateIVars ivs (PrimVal fc c) = Just (PrimVal fc c)
+    updateIVars ivs (Erased fc i) = Just (Erased fc i)
+    updateIVars ivs (TType fc) = Just (TType fc)

-    updateLocs locs (App fc f a)
-        = Just (App fc !(updateLocs locs f) !(updateLocs locs a))
-    updateLocs locs tm = Just tm
-
-    mkDef : (got : List Name) -> (vs : List Name) -> SnocList vs ->
-            List (Var (vs ++ got)) -> Term (vs ++ got) ->
-            Term ts -> Core (Term got)
-    mkDef got [] Empty locs tm ty
-        = do let Just tm' = updateLocs (reverse locs) tm
-                    | Nothing => ufail loc ("Can't make solution for " ++ show mname)
-             pure tm'
-    mkDef got vs rec locs tm (Bind _ _ (Let _ _ _) sc)
-        = mkDef got vs rec locs tm sc
-    mkDef got (vs ++ [v]) (Snoc v vs rec) locs tm (Bind bfc x (Pi c _ ty) sc)
-        = do defs <- get Ctxt
-             sc' <- mkDef (v :: got) vs rec
-                       (rewrite appendAssociative vs [v] got in locs)
-                       (rewrite appendAssociative vs [v] got in tm)
-                       sc
-             pure (Bind bfc v (Lam c Explicit (Erased bfc False)) sc')
-    mkDef got (vs ++ [v]) (Snoc v vs rec) locs tm ty
-        = ufail loc $ "Can't make solution for " ++ show mname
+    mkDef : {vs, newvars : _} ->
+            List (Var newvars) ->
+            IVars vs newvars -> Term newvars -> Term vs ->
+            Core (Term vs)
+    mkDef (v :: vs) vars soln (Bind bfc x (Pi c _ ty) sc)
+       = do sc' <- mkDef vs (ICons (Just v) vars) soln sc
+            pure $ Bind bfc x (Lam c Explicit (Erased bfc False)) sc'
+    mkDef vs vars soln (Bind bfc x b@(Let c val ty) sc)
+       = do sc' <- mkDef vs (ICons Nothing vars) soln sc
+            let Just scs = shrinkTerm sc' (DropCons SubRefl)
+                | Nothing => pure $ Bind bfc x b sc'
+            pure scs
+    mkDef [] vars soln ty
+       = do let Just soln' = updateIVars vars soln
+                | Nothing => ufail loc ("Can't make solution for " ++ show mname
+                                           ++ " " ++ show (getIVars vars, soln))
+            pure soln'
+    mkDef _ _ _ ty = ufail loc $ "Can't make solution for " ++ show mname
+                             ++ " at " ++ show ty

 export
 solveIfUndefined : {vars : _} ->
--- a/src/Core/UnifyState.idr
+++ b/src/Core/UnifyState.idr
@ -310,6 +310,37 @@ mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns
    mkVar [] = First
    mkVar (w :: ws) = Later (mkVar ws)

+mkConstantAppArgsSub : {vars : _} ->
+                       Bool -> FC -> Env Term vars ->
+                       SubVars smaller vars ->
+                       (wkns : List Name) ->
+                       List (Term (wkns ++ (vars ++ done)))
+mkConstantAppArgsSub lets fc [] p wkns = []
+mkConstantAppArgsSub {done} {vars = x :: xs}
+                        lets fc (b :: env) SubRefl wkns
+    = rewrite appendAssociative wkns [x] (xs ++ done) in
+              mkConstantAppArgs lets fc env (wkns ++ [x])
+mkConstantAppArgsSub {done} {vars = x :: xs}
+                        lets fc (b :: env) (DropCons p) wkns
+    = rewrite appendAssociative wkns [x] (xs ++ done) in
+              mkConstantAppArgsSub lets fc env p (wkns ++ [x])
+mkConstantAppArgsSub {done} {vars = x :: xs}
+                        lets fc (b :: env) (KeepCons p) wkns
+    = let rec = mkConstantAppArgsSub {done} lets fc env p (wkns ++ [x]) in
+          if lets || not (isLet b)
+             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
+                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
+             else rewrite appendAssociative wkns [x] (xs ++ done) in rec
+  where
+    isLet : Binder (Term vars) -> Bool
+    isLet (Let _ _ _) = True
+    isLet _ = False
+
+    mkVar : (wkns : List Name) ->
+            IsVar name (length wkns) (wkns ++ name :: vars ++ done)
+    mkVar [] = First
+    mkVar (w :: ws) = Later (mkVar ws)
+
 mkConstantAppArgsOthers : {vars : _} ->
                          Bool -> FC -> Env Term vars ->
                          SubVars smaller vars ->
@ -356,6 +387,14 @@ applyToFull fc tm env
  = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

+export
+applyToSub : {vars : _} ->
+             FC -> Term vars -> Env Term vars ->
+             SubVars smaller vars -> Term vars
+applyToSub fc tm env sub
+  = let args = reverse (mkConstantAppArgsSub {done = []} True fc env sub []) in
+        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)
+
 export
 applyToOthers : {vars : _} ->
                FC -> Term vars -> Env Term vars ->
--- a/src/Idris/Desugar.idr
+++ b/src/Idris/Desugar.idr
@ -392,10 +392,14 @@ mutual
  expandDo side ps topfc (DoExp fc tm :: rest)
      = do tm' <- desugar side ps tm
           rest' <- expandDo side ps topfc rest
+           -- A free standing 'case' block must return ()
+           let ty = case tm' of
+                         ICase _ _ _ _ => IVar fc (UN "Unit")
+                         _ => Implicit fc False
           gam <- get Ctxt
           pure $ IApp fc (IApp fc (IVar fc (UN ">>=")) tm')
                          (ILam fc top Explicit Nothing
-                                (Implicit fc False) rest')
+                                ty rest')
  expandDo side ps topfc (DoBind fc n tm :: rest)
      = do tm' <- desugar side ps tm
           rest' <- expandDo side ps topfc rest
@ -810,6 +814,7 @@ mutual
             UndottedRecordProjections b => do
               pure [IPragma (\nest, env => setUndottedRecordProjections b)]
             AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
+             AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
             PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]
             RewriteName eq rw => pure [IPragma (\nest, env => setRewrite fc eq rw)]
             PrimInteger n => pure [IPragma (\nest, env => setFromInteger n)]
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@ -1096,6 +1096,10 @@ directive fname indents
         lvl <- intLit
         atEnd indents
         pure (AmbigDepth (fromInteger lvl))
+  <|> do pragma "auto_implicit_depth"
+         dpt <- intLit
+         atEnd indents
+         pure (AutoImplicitDepth (fromInteger dpt))
  <|> do pragma "pair"
         ty <- name
         f <- name
@ -1707,6 +1711,9 @@ data CmdArg : Type where
     ||| The command takes an expression.
     ExprArg : CmdArg

+     ||| The command takes a list of declarations
+     DeclsArg : CmdArg
+
     ||| The command takes a number.
     NumberArg : CmdArg

@ -1721,6 +1728,7 @@ Show CmdArg where
  show NoArg = ""
  show NameArg = "<name>"
  show ExprArg = "<expr>"
+  show DeclsArg = "<decls>"
  show NumberArg = "<number>"
  show OptionArg = "<option>"
  show FileArg = "<filename>"
@ -1785,6 +1793,18 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
      tm <- expr pdef "(interactive)" init
      pure (command tm)

+declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition
+declsArgCmd parseCmd command doc = (names, DeclsArg, doc, parse)
+  where
+    names : List String
+    names = extractNames parseCmd
+    parse : Rule REPLCmd
+    parse = do
+      symbol ":"
+      runParseCmd parseCmd
+      tm <- topDecl "(interactive)" init
+      pure (command tm)
+
 optArgCmd : ParseCmd -> (REPLOpt -> REPLCmd) -> Bool -> String -> CommandDefinition
 optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
  where
@ -1845,6 +1865,7 @@ parserCommandsForHelp =
  , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars "Show remaining proof obligations (metavariables or holes)"
  , noArgCmd (ParseREPLCmd ["version"]) ShowVersion "Display the Idris version"
  , noArgCmd (ParseREPLCmd ["?", "h", "help"]) Help "Display this help text"
+  , declsArgCmd (ParseKeywordCmd "let") NewDefn "Define a new value"
  ]

 export
--- a/src/Idris/REPL.idr
+++ b/src/Idris/REPL.idr
@ -426,6 +426,7 @@ data REPLResult : Type where
  OptionsSet : List REPLOpt -> REPLResult
  LogLevelSet : Nat -> REPLResult
  VersionIs : Version -> REPLResult
+  DefDeclared : REPLResult
  Exited : REPLResult
  Edited : EditResult -> REPLResult

@ -445,6 +446,20 @@ execExp ctm
         pure $ Executed ctm


+execDecls : {auto c : Ref Ctxt Defs} ->
+            {auto u : Ref UST UState} ->
+            {auto s : Ref Syn SyntaxInfo} ->
+            {auto m : Ref MD Metadata} ->
+            List PDecl -> Core REPLResult
+execDecls decls = do
+  traverse_ execDecl decls
+  pure DefDeclared
+  where
+    execDecl : PDecl -> Core ()
+    execDecl decl = do
+      i <- desugarDecl [] decl
+      traverse_ (processDecl [] (MkNested []) []) i
+
 export
 compileExp : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
@ -494,6 +509,7 @@ process : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          REPLCmd -> Core REPLResult
+process (NewDefn decls) = execDecls decls
 process (Eval itm)
    = do opts <- get ROpts
         case evalMode opts of
--- a/src/Idris/Syntax.idr
+++ b/src/Idris/Syntax.idr
@ -168,6 +168,7 @@ mutual
       Extension : LangExt -> Directive
       DefaultTotality : TotalReq -> Directive
       UndottedRecordProjections : Bool -> Directive
+       AutoImplicitDepth : Nat -> Directive

  public export
  data PField : Type where
@ -304,6 +305,7 @@ data EditCmd : Type where

 public export
 data REPLCmd : Type where
+     NewDefn : List PDecl -> REPLCmd 
     Eval : PTerm -> REPLCmd
     Check : PTerm -> REPLCmd
     PrintDef : Name -> REPLCmd
--- a/src/TTImp/Elab/App.idr
+++ b/src/TTImp/Elab/App.idr
@ -99,9 +99,9 @@ getVarType rigc nest env fc x
                             tyenv = useVars (getArgs tm)
                                             (embed (type ndef)) in
                             do checkVisibleNS fc (fullname ndef) (visibility ndef)
-                                logTerm 10 ("Type of " ++ show n') tyenv
-                                logTerm 10 ("Expands to") tm
-                                log 10 $ "Arg length " ++ show arglen
+                                logTerm 5 ("Type of " ++ show n') tyenv
+                                logTerm 5 ("Expands to") tm
+                                log 5 $ "Arg length " ++ show arglen
                                pure (tm, arglen, gnf env tyenv)
    where
      useVars : {vars : _} ->
@ -195,7 +195,8 @@ mutual
                   -- so we might as well calculate the whole thing now
                   metaty <- quote defs env aty
                   est <- get EST
-                   metaval <- searchVar fc argRig 50 (Resolved (defining est))
+                   lim <- getAutoImplicitLimit
+                   metaval <- searchVar fc argRig lim (Resolved (defining est))
                                        env nm metaty
                   let fntm = App fc tm metaval
                   fnty <- sc defs (toClosure defaultOpts env metaval)
--- a/src/TTImp/Elab/Case.idr
+++ b/src/TTImp/Elab/Case.idr
@ -127,22 +127,27 @@ findScrutinee {vs = n' :: _} (b :: bs) (IVar loc' n)
    notLet _ = True
 findScrutinee _ _ = Nothing

-getNestData : (Name, (Maybe Name, List Name, a)) ->
-              (Name, Maybe Name, List Name)
+getNestData : (Name, (Maybe Name, List (Var vars), a)) ->
+              (Name, Maybe Name, List (Var vars))
 getNestData (n, (mn, enames, _)) = (n, mn, enames)

-bindCaseLocals : FC -> List (Name, Maybe Name, List Name) ->
+bindCaseLocals : FC -> List (Name, Maybe Name, List (Var vars)) ->
                 List (Name, Name)-> RawImp -> RawImp
 bindCaseLocals fc [] args rhs = rhs
 bindCaseLocals fc ((n, mn, envns) :: rest) argns rhs
-    = --trace ("Case local " ++ show (renvns ++ " from " ++ show argns) $
+    = -- trace ("Case local " ++ show (n,mn,envns) ++ " from " ++ show argns) $
        ICaseLocal fc n (fromMaybe n mn)
-                 (map getNameFrom (reverse envns))
+                 (map getNameFrom envns)
                 (bindCaseLocals fc rest argns rhs)
  where
-    getNameFrom : Name -> Name
-    getNameFrom n
-        = case lookup n argns of
+    getArg : List (Name, Name) -> Nat -> Maybe Name
+    getArg [] _ = Nothing
+    getArg ((_, x) :: xs) Z = Just x
+    getArg (x :: xs) (S k) = getArg xs k
+
+    getNameFrom : Var vars -> Name
+    getNameFrom (MkVar {i} _)
+        = case getArg argns i of
               Nothing => n
               Just n' => n'

@ -307,7 +312,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected

    -- Get a name update for the LHS (so that if there's a nested data declaration
    -- the constructors are applied to the environment in the case block)
-    nestLHS : FC -> (Name, (Maybe Name, List Name, a)) -> (Name, RawImp)
+    nestLHS : FC -> (Name, (Maybe Name, List (Var vars), a)) -> (Name, RawImp)
    nestLHS fc (n, (mn, ns, t))
        = (n, apply (IVar fc (fromMaybe n mn))
                    (map (const (Implicit fc False)) ns))
@ -326,7 +331,7 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
              lhs' = apply (IVar loc' casen) args' in
              PatClause loc' (applyNested nest lhs')
                        (bindCaseLocals loc' (map getNestData (names nest))
-                                        (reverse ns) rhs)
+                                        ns rhs)
    -- With isn't allowed in a case block but include for completeness
    updateClause casen splitOn nest env (WithClause loc' lhs wval flags cs)
        = let (_, args) = addEnv 0 env (usedIn lhs)
--- a/src/TTImp/Elab/Local.idr
+++ b/src/TTImp/Elab/Local.idr
@ -11,6 +11,7 @@ import Core.TT
 import Core.Value

 import TTImp.Elab.Check
+import TTImp.Elab.Utils
 import TTImp.TTImp

 import Data.List
@ -60,14 +61,14 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty
             else b :: dropLinear bs

    applyEnv : Int -> Name ->
-               Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vars))
+               Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))
    applyEnv outer inner
          = do ust <- get UST
               put UST (record { nextName $= (+1) } ust)
               let nestedName_in = Nested (outer, nextName ust) inner
               nestedName <- inCurrentNS nestedName_in
               n' <- addName nestedName
-               pure (inner, (Just nestedName, vars,
+               pure (inner, (Just nestedName, reverse (allVars env),
                        \fc, nt => applyToFull fc
                               (Ref fc nt (Resolved n')) env))

@ -102,12 +103,15 @@ checkLocal {vars} rig elabinfo nest env fc nestdecls scope expty

 getLocalTerm : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
-               FC -> Env Term vars -> Term vars -> List Name -> Core (Term vars)
-getLocalTerm fc env f [] = pure f
+               FC -> Env Term vars -> Term vars -> List Name ->
+               Core (Term vars, List (Var vars))
+getLocalTerm fc env f [] = pure (f, [])
 getLocalTerm fc env f (a :: as)
    = case defined a env of
           Just (MkIsDefined rigb lv) =>
-                getLocalTerm fc env (App fc f (Local fc Nothing _ lv)) as
+                do (tm, vs) <- getLocalTerm fc env
+                                   (App fc f (Local fc Nothing _ lv)) as
+                   pure (tm, MkVar lv :: vs)
           Nothing => throw (InternalError "Case Local failed")

 export
@ -130,10 +134,10 @@ checkCaseLocal {vars} rig elabinfo nest env fc uname iname args sc expty
                         DCon t a _ => Ref fc (DataCon t a) iname
                         TCon t a _ _ _ _ _ _ => Ref fc (TyCon t a) iname
                         _ => Ref fc Func iname
-         app <- getLocalTerm fc env name args
+         (app, args) <- getLocalTerm fc env name args
         log 5 $ "Updating case local " ++ show uname ++ " " ++ show args
-         logTermNF 10 "To" env app
-         let nest' = record { names $= ((uname, (Just iname, reverse args,
+         logTermNF 5 "To" env app
+         let nest' = record { names $= ((uname, (Just iname, args,
                                                (\fc, nt => app))) :: ) }
                            nest
         check rig elabinfo nest' env sc expty
--- a/src/TTImp/Elab/RunElab.idr
+++ b/src/TTImp/Elab/RunElab.idr
@ -93,7 +93,7 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
             defs <- get Ctxt
             empty <- clearDefs defs
             scriptRet !(unelabUniqueBinders env !(quote empty env tm'))
-    elabCon defs "Lambda" [_, x, scope]
+    elabCon defs "Lambda" [x, _, scope]
        = do empty <- clearDefs defs
             NBind bfc x (Lam c p ty) sc <- evalClosure defs scope
                   | _ => throw (GenericMsg fc "Not a lambda")
@ -114,27 +114,6 @@ elabScript fc nest env (NDCon nfc nm t ar args) exp
         quotePi Implicit = pure Implicit
         quotePi AutoImplicit = pure AutoImplicit
         quotePi (DefImplicit t) = throw (GenericMsg fc "Can't add default lambda")
-    elabCon defs "ForAll" [_, x, scope]
-        = do empty <- clearDefs defs
-             NBind bfc x (Pi c p ty) sc <- evalClosure defs scope
-                   | _ => throw (GenericMsg fc "Not a lambda")
-             n <- genVarName "x"
-             sc' <- sc defs (toClosure withAll env (Ref bfc Bound n))
-             qsc <- quote empty env sc'
-             let lamsc = refToLocal n x qsc
-             qp <- quotePi p
-             qty <- quote empty env ty
-             let env' = Pi c qp qty :: env
-
-             runsc <- elabScript fc (weaken nest) env'
-                                 !(nf defs env' lamsc) Nothing -- (map weaken exp)
-             nf empty env (Bind bfc x (Pi c qp qty) !(quote empty env' runsc))
-       where
-         quotePi : PiInfo (NF vars) -> Core (PiInfo (Term vars))
-         quotePi Explicit = pure Explicit
-         quotePi Implicit = pure Implicit
-         quotePi AutoImplicit = pure AutoImplicit
-         quotePi (DefImplicit t) = throw (GenericMsg fc "Can't add default lambda")
    elabCon defs "Goal" []
        = do let Just gty = exp
                 | Nothing => nfOpts withAll defs env
--- a/src/TTImp/Elab/Utils.idr
+++ b/src/TTImp/Elab/Utils.idr
@ -73,3 +73,45 @@ wrapErrorC opts err
    = if InCase `elem` opts
         then id
         else wrapError err
+
+plicit : Binder (Term vars) -> PiInfo RawImp
+plicit (Pi _ p _) = forgetDef p
+plicit (PVar _ p _) = forgetDef p
+plicit _ = Explicit
+
+export
+bindNotReq : {vs : _} ->
+             FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
+             List (PiInfo RawImp, Name) ->
+             Term vs -> (List (PiInfo RawImp, Name), Term pre)
+bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
+bindNotReq fc i (b :: env) SubRefl ns tm
+   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
+         (ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in
+         (ns', refToLocal (MN "arg" i) _ btm)
+bindNotReq fc i (b :: env) (KeepCons p) ns tm
+   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
+         (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in
+         (ns', refToLocal (MN "arg" i) _ btm)
+bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
+   = bindNotReq fc i env p ((plicit b, n) :: ns)
+       (Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm)
+
+export
+bindReq : {vs : _} ->
+          FC -> Env Term vs -> (sub : SubVars pre vs) ->
+          List (PiInfo RawImp, Name) ->
+          Term pre -> Maybe (List (PiInfo RawImp, Name), List Name, ClosedTerm)
+bindReq {vs} fc env SubRefl ns tm
+    = pure (ns, notLets [] _ env, abstractEnvType fc env tm)
+  where
+    notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
+    notLets acc [] _ = acc
+    notLets acc (v :: vs) (Let _ _ _ :: env) = notLets acc vs env
+    notLets acc (v :: vs) (_ :: env) = notLets (v :: acc) vs env
+bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
+    = do b' <- shrinkBinder b p
+         bindReq fc env p ((plicit b, n) :: ns)
+            (Bind fc _ (Pi (multiplicity b) Explicit (binderType b')) tm)
+bindReq fc (b :: env) (DropCons p) ns tm
+    = bindReq fc env p ns tm
--- a/src/TTImp/ProcessDef.idr
+++ b/src/TTImp/ProcessDef.idr
@ -321,46 +321,6 @@ checkLHS {vars} trans mult hashit n opts nest env fc lhs_in
         ext <- extendEnv env SubRefl nest lhstm_lin lhsty_lin
         pure (lhs, ext)

-plicit : Binder (Term vars) -> PiInfo RawImp
-plicit (Pi _ p _) = forgetDef p
-plicit (PVar _ p _) = forgetDef p
-plicit _ = Explicit
-
-bindNotReq : {vs : _} ->
-             FC -> Int -> Env Term vs -> (sub : SubVars pre vs) ->
-             List (PiInfo RawImp, Name) ->
-             Term vs -> (List (PiInfo RawImp, Name), Term pre)
-bindNotReq fc i [] SubRefl ns tm = (ns, embed tm)
-bindNotReq fc i (b :: env) SubRefl ns tm
-   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
-         (ns', btm) = bindNotReq fc (1 + i) env SubRefl ns tmptm in
-         (ns', refToLocal (MN "arg" i) _ btm)
-bindNotReq fc i (b :: env) (KeepCons p) ns tm
-   = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm
-         (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in
-         (ns', refToLocal (MN "arg" i) _ btm)
-bindNotReq {vs = n :: _} fc i (b :: env) (DropCons p) ns tm
-   = bindNotReq fc i env p ((plicit b, n) :: ns)
-       (Bind fc _ (Pi (multiplicity b) Explicit (binderType b)) tm)
-
-bindReq : {vs : _} ->
-          FC -> Env Term vs -> (sub : SubVars pre vs) ->
-          List (PiInfo RawImp, Name) ->
-          Term pre -> Maybe (List (PiInfo RawImp, Name), List Name, ClosedTerm)
-bindReq {vs} fc env SubRefl ns tm
-    = pure (ns, notLets [] _ env, abstractEnvType fc env tm)
-  where
-    notLets : List Name -> (vars : List Name) -> Env Term vars -> List Name
-    notLets acc [] _ = acc
-    notLets acc (v :: vs) (Let _ _ _ :: env) = notLets acc vs env
-    notLets acc (v :: vs) (_ :: env) = notLets (v :: acc) vs env
-bindReq {vs = n :: _} fc (b :: env) (KeepCons p) ns tm
-    = do b' <- shrinkBinder b p
-         bindReq fc env p ((plicit b, n) :: ns)
-            (Bind fc _ (Pi (multiplicity b) Explicit (binderType b')) tm)
-bindReq fc (b :: env) (DropCons p) ns tm
-    = bindReq fc env p ns tm
-
 -- Return whether any of the pattern variables are in a trivially empty
 -- type, where trivally empty means one of:
 --  * No constructors
@ -378,10 +338,10 @@ hasEmptyPat defs env _ = pure False
 applyEnv : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           Env Term vars -> Name ->
-           Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vars))
+           Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars))
 applyEnv env withname
    = do n' <- resolveName withname
-         pure (withname, (Just withname, namesNoLet env,
+         pure (withname, (Just withname, reverse (allVarsNoLet env),
                  \fc, nt => applyTo fc
                         (Ref fc nt (Resolved n')) env))

@ -740,7 +700,7 @@ processDef opts nest env fc n_in cs_in
         let pats = map toPats (rights cs)

         (cargs ** (tree_ct, unreachable)) <-
-             getPMDef fc CompileTime n ty (rights cs)
+             getPMDef fc (CompileTime mult) n ty (rights cs)

         traverse_ warnUnreachable unreachable

@ -847,7 +807,7 @@ processDef opts nest env fc n_in cs_in
        = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses
             let covcs = mapMaybe id covcs'
             (_ ** (ctree, _)) <-
-                 getPMDef fc CompileTime (Resolved n) ty covcs
+                 getPMDef fc (CompileTime mult) (Resolved n) ty covcs
             log 3 $ "Working from " ++ show !(toFullNames ctree)
             missCase <- if any catchAll covcs
                            then do log 3 $ "Catch all case in " ++ show n
--- a/src/TTImp/ProcessParams.idr
+++ b/src/TTImp/ProcessParams.idr
@ -12,6 +12,8 @@ import TTImp.Elab
 import TTImp.Elab.Check
 import TTImp.TTImp

+import Data.List
+
 %default covering

 extend : {extvs : _} ->
@ -60,9 +62,9 @@ processParams {vars} {c} {m} {u} nest env fc ps ds

    applyEnv : {vs : _} ->
               Env Term vs -> Name ->
-               Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vs))
+               Core (Name, (Maybe Name, List (Var vs), FC -> NameType -> Term vs))
    applyEnv {vs} env n
          = do n' <- resolveName n -- it'll be Resolved by expandAmbigName
-               pure (Resolved n', (Nothing, vs,
+               pure (Resolved n', (Nothing, reverse (allVars env),
                        \fc, nt => applyToFull fc
                               (Ref fc nt (Resolved n')) env))
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@ -21,16 +21,17 @@ record NestedNames (vars : List Name) where
  -- Takes the location and name type, because we don't know them until we
  -- elaborate the name at the point of use
  names : List (Name, (Maybe Name,  -- new name if there is one
-                       List Name, -- names used from the environment
+                       List (Var vars), -- names used from the environment
                       FC -> NameType -> Term vars))

 export
 Weaken NestedNames where
  weaken (MkNested ns) = MkNested (map wknName ns)
    where
-      wknName : (Name, (Maybe Name, List Name, FC -> NameType -> Term vars)) ->
-                (Name, (Maybe Name, List Name, FC -> NameType -> Term (n :: vars)))
-      wknName (n, (mn, len, rep)) = (n, (mn, len, \fc, nt => weaken (rep fc nt)))
+      wknName : (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars)) ->
+                (Name, (Maybe Name, List (Var (n :: vars)), FC -> NameType -> Term (n :: vars)))
+      wknName (n, (mn, vars, rep))
+          = (n, (mn, map weaken vars, \fc, nt => weaken (rep fc nt)))

 -- Unchecked terms, with implicit arguments
 -- This is the raw, elaboratable form.
@ -124,11 +125,11 @@ mutual
    Show RawImp where
      show (IVar fc n) = show n
      show (IPi fc c p n arg ret)
-         = "(%pi " ++ show c ++ " " ++ show p ++
-           " " ++ show n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
+         = "(%pi " ++ show c ++ " " ++ show p ++ " " ++
+           showPrec App n ++ " " ++ show arg ++ " " ++ show ret ++ ")"
      show (ILam fc c p n arg sc)
-         = "(%lam " ++ show c ++ " " ++ show p ++
-           " " ++ show n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
+         = "(%lam " ++ show c ++ " " ++ show p ++ " " ++
+           showPrec App n ++ " " ++ show arg ++ " " ++ show sc ++ ")"
      show (ILet fc c n ty val sc)
         = "(%let " ++ show c ++ " " ++ " " ++ show n ++ " " ++ show ty ++
           " " ++ show val ++ " " ++ show sc ++ ")"
--- a/support/chez/support.ss
+++ b/support/chez/support.ss
@ -267,3 +267,18 @@
        (if (> k 0)
              (random k)
              (assertion-violationf 'blodwen-random "invalid range argument ~a" k)))]))
+
+;; For finalisers
+
+(define blodwen-finaliser (make-guardian))
+(define (blodwen-register-object obj proc)
+  (let [(x (cons obj proc))]
+       (blodwen-finaliser x)
+       x))
+(define blodwen-run-finalisers
+  (lambda ()
+    (let run ()
+      (let ([x (blodwen-finaliser)])
+        (when x
+          (((cdr x) (car x)) 'erased)
+          (run))))))
--- a/support/racket/support.rkt
+++ b/support/racket/support.rkt
@ -263,3 +263,9 @@
    [(k) (if (> k 0)
           (random k)
           (raise 'blodwen-random-invalid-range-argument))]))
+
+;; For finalisers
+
+(define (blodwen-register-object obj proc)
+   (register-finalizer obj (lambda (ptr) ((proc ptr) 'erased)))
+   obj)
--- a/tests/Main.idr
+++ b/tests/Main.idr
@ -64,7 +64,7 @@ idrisTests
       "interface009", "interface010", "interface011", "interface012",
       "interface013", "interface014", "interface015",
       -- Miscellaneous REPL
-       "interpreter001",
+       "interpreter001", "interpreter002",
       -- Implicit laziness, lazy evaluation
       "lazy001",
       -- QTT and linearity related
@ -91,7 +91,8 @@ idrisTests
       -- Miscellaneous regressions
       "reg001", "reg002", "reg003", "reg004", "reg005", "reg006", "reg007",
       "reg008", "reg009", "reg010", "reg011", "reg012", "reg013", "reg014",
-       "reg015", "reg016", "reg017", "reg018", "reg019", "reg020",
+       "reg015", "reg016", "reg017", "reg018", "reg019", "reg020", "reg021",
+       "reg022", "reg023",
       -- Totality checking
       "total001", "total002", "total003", "total004", "total005",
       "total006", "total007", "total008",
@ -111,7 +112,7 @@ chezTests
   = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
      "chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
      "chez013", "chez014", "chez015", "chez016", "chez017", "chez018",
-      "chez019", "chez020", "chez021",
+      "chez019", "chez020", "chez021", "chez022",
      "reg001"]

 ideModeTests : List String
@ -198,8 +199,8 @@ runTest opts testPath
              ]
            Just exp => do
              putStrLn "Golden value differs from actual value."
-              code <- system "git diff expected output"
-              when (code /= 0) $ printExpectedVsOutput exp out
+              code <- system "git diff --exit-code expected output"
+              when (code < 0) $ printExpectedVsOutput exp out
              putStrLn "Accept actual value as new golden value? [yn]"
          b <- getAnswer
          when b $ do Right _ <- writeFile "expected" out
@ -221,6 +222,9 @@ runTest opts testPath
                     | Left err => do print err
                                      pure False
                 let result = normalize out == normalize exp
+                 -- The issue #116 that made this necessary is fixed, but
+                 -- please resist putting 'result' here until it's also
+                 -- fixed in Idris2-boot!
                 if normalize out == normalize exp
                    then putStrLn "success"
                    else do
--- a/tests/chez/chez022/Makefile
+++ b/tests/chez/chez022/Makefile
@ -0,0 +1,28 @@
+include ../../../config.mk
+
+TARGET = libmkalloc
+
+SRCS = $(wildcard *.c)
+OBJS = $(SRCS:.c=.o)
+DEPS = $(OBJS:.o=.d)
+
+
+all: $(TARGET)$(SHLIB_SUFFIX)
+
+$(TARGET)$(SHLIB_SUFFIX): $(OBJS)
+	$(CC) -shared $(LDFLAGS) -o $@ $^
+
+
+-include $(DEPS)
+
+%.d: %.c
+	@$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@
+
+
+.PHONY: clean
+
+clean :
+	$(RM) $(OBJS) $(TARGET)$(SHLIB_SUFFIX)
+
+cleandep: clean
+	$(RM) $(DEPS)
--- a/tests/chez/chez022/expected
+++ b/tests/chez/chez022/expected
@ -0,0 +1,9 @@
+Hello
+Hello
+Done
+Free X
+Freeing 0 Hello
+Free Y
+Freeing 1 Hello
+1/1: Building usealloc (usealloc.idr)
+Main> Main> Bye for now!
--- a/tests/chez/chez022/input
+++ b/tests/chez/chez022/input
@ -0,0 +1,2 @@
+:exec main
+:q
--- a/tests/chez/chez022/mkalloc.c
+++ b/tests/chez/chez022/mkalloc.c
@ -0,0 +1,27 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+
+typedef struct {
+    int val;
+    char* str;
+} Stuff;
+
+Stuff* mkThing() {
+    static int num = 0;
+    Stuff* x = malloc(sizeof(Stuff));
+    x->val = num++;
+    x->str = malloc(20);
+    strcpy(x->str,"Hello");
+    return x;
+}
+
+char* getStr(Stuff* x) {
+    return x->str;
+}
+
+void freeThing(Stuff* x) {
+    printf("Freeing %d %s\n", x->val, x->str);
+    free(x->str);
+    free(x);
+}
--- a/tests/chez/chez022/run
+++ b/tests/chez/chez022/run
@ -0,0 +1,4 @@
+make all > /dev/null
+$1 --no-banner usealloc.idr < input
+rm -rf build
+make clean > /dev/null
--- a/tests/chez/chez022/usealloc.idr
+++ b/tests/chez/chez022/usealloc.idr
@ -0,0 +1,32 @@
+%foreign "C:mkThing, libmkalloc"
+prim__mkThing : PrimIO AnyPtr
+%foreign "C:getStr, libmkalloc"
+prim__getStr : GCAnyPtr -> PrimIO String
+%foreign "C:freeThing, libmkalloc"
+prim__freeThing : AnyPtr -> PrimIO ()
+
+mkThing : IO AnyPtr
+mkThing = primIO prim__mkThing
+
+getThingStr : GCAnyPtr -> IO String
+getThingStr t = primIO (prim__getStr t)
+
+freeThing : AnyPtr -> IO ()
+freeThing t = primIO (prim__freeThing t)
+
+doThings : IO ()
+doThings 
+     = do xp <- mkThing
+          yp <- mkThing
+
+          x <- onCollectAny xp (\p => do putStrLn "Free X"
+                                         freeThing p)
+          y <- onCollectAny yp (\p => do putStrLn "Free Y"
+                                         freeThing p)
+
+          putStrLn !(getThingStr x)
+          putStrLn !(getThingStr y)
+
+main : IO ()
+main = do doThings
+          putStrLn "Done"
--- 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 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((: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 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 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:263}_[] ?{_:264}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 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:260}_[] ?{_:261}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
--- 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 25)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 8 1)) ((: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 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:263} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:264}_[]")))))) 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:263}_[] ?{_:264}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 38)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:260} a)")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 11)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:261}_[]")))))) 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:260}_[] ?{_:261}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:262}_[] ?{_:261}_[])")))))) 1)
 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1)
-0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:251}_[] ?{_:250}_[])")))))) 1)
+0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:241} : (Main.Vect n[0] a[1])) -> (({arg:242} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:849:1--856:1 n[2] m[4]) a[3])))")))))) 1)
 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)
--- a/tests/idris2/coverage008/expected
+++ b/tests/idris2/coverage008/expected
@ -1,6 +1,6 @@
 1/1: Building wcov (wcov.idr)
 Main> Main.tfoo is total
 Main> Main.wfoo is total
-Main> Main.wbar is not covering due to call to function Main.with block in 1368
+Main> Main.wbar is not covering due to call to function Main.with block in 1376
 Main> Main.wbar1 is total
 Main> Bye for now!
--- a/tests/idris2/coverage010/expected
+++ b/tests/idris2/coverage010/expected
@ -1,3 +1,3 @@
 1/1: Building casetot (casetot.idr)
 casetot.idr:12:1--13:1:main is not covering:
-	Calls non covering function Main.case block in 2079(290)
+	Calls non covering function Main.case block in 2087(287)
--- a/tests/idris2/interpreter002/expected
+++ b/tests/idris2/interpreter002/expected
@ -0,0 +1,3 @@
+Main> Main> Main> "Privet, mir!"
+Main> 
+Bye for now!
--- a/tests/idris2/interpreter002/input
+++ b/tests/idris2/interpreter002/input
@ -0,0 +1,3 @@
+:let i : String
+:let i = "Privet, mir!"
+i
--- a/tests/idris2/interpreter002/run
+++ b/tests/idris2/interpreter002/run
@ -0,0 +1,3 @@
+$1 --no-banner --no-prelude < input
+
+rm -rf build
--- a/tests/idris2/reflection003/expected
+++ b/tests/idris2/reflection003/expected
@ -1,8 +1,8 @@
 1/1: Building refprims (refprims.idr)
 LOG 0: Name: Prelude.List.++
-LOG 0: Type: (%pi Rig0 Implicit Just a %type (%pi Rig1 Explicit Just _ (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
+LOG 0: Type: (%pi Rig0 Implicit (Just a) %type (%pi Rig1 Explicit (Just _) (Prelude.List a) (%pi RigW Explicit Nothing (Prelude.List a) (Prelude.List a))))
 LOG 0: Name: Prelude.Strings.++
-LOG 0: Type: (%pi Rig1 Explicit Just _ String (%pi Rig1 Explicit Just _ String String))
+LOG 0: Type: (%pi Rig1 Explicit (Just _) String (%pi Rig1 Explicit (Just _) String String))
 LOG 0: Resolved name: Prelude.Nat
 LOG 0: Constructors: [Prelude.Z, Prelude.S]
 refprims.idr:37:10--39:1:While processing right hand side of dummy1 at refprims.idr:37:1--39:1:
@ -12,4 +12,4 @@ Error during reflection: Still not trying
 refprims.idr:43:10--45:1:While processing right hand side of dummy3 at refprims.idr:43:1--45:1:
 Error during reflection: Undefined name
 refprims.idr:46:10--48:1:While processing right hand side of dummy4 at refprims.idr:46:1--48:1:
-Error during reflection: failed after generating Main.{plus:5841}
+Error during reflection: failed after generating Main.{plus:6078}
--- a/tests/idris2/reg021/case.idr
+++ b/tests/idris2/reg021/case.idr
@ -0,0 +1,12 @@
+twice : Char -> Char -> Char -> Char -> Nat -> (Nat, Nat)
+twice w x y z Z = (Z, Z)
+twice m n o p (S x)
+    = case twice m n o p x of
+           (a, b) => (S a, S b)
+
+bothS : Int -> String -> (Nat, Nat) -> (Nat, Nat)
+bothS test dummy = \(c, d) => (S c, S d)
+
+pf : (x : Nat) -> twice 'a' 'b' 'c' 'd' (S x) 
+                     = bothS 99 "red balloons" (twice 'a' 'b' 'c' 'd' x)
+pf k = Refl -- Refl
--- a/tests/idris2/reg021/expected
+++ b/tests/idris2/reg021/expected
@ -0,0 +1 @@
+1/1: Building case (case.idr)
--- a/tests/idris2/reg021/run
+++ b/tests/idris2/reg021/run
@ -0,0 +1,3 @@
+$1 --check case.idr
+
+rm -rf build
--- a/tests/idris2/reg022/case.idr
+++ b/tests/idris2/reg022/case.idr
@ -0,0 +1,5 @@
+-- Previously this gave an 'unreachable case warning' and evaluated
+-- to the first case! Should give foo : Nat -> Nat
+foo : (x : Nat) -> case S x of
+                        Z => Nat -> Nat
+                        (S k) => Nat
--- a/tests/idris2/reg022/expected
+++ b/tests/idris2/reg022/expected
@ -0,0 +1 @@
+1/1: Building case (case.idr)
--- a/tests/idris2/reg022/input
+++ b/tests/idris2/reg022/input
@ -0,0 +1,2 @@
+:t foo
+:q
--- a/tests/idris2/reg022/run
+++ b/tests/idris2/reg022/run
@ -0,0 +1,3 @@
+$1 --check case.idr
+
+rm -rf build
--- a/tests/idris2/reg023/boom.idr
+++ b/tests/idris2/reg023/boom.idr
@ -0,0 +1,27 @@
+import Data.Vect
+
+%default total
+
+infix 3 .<=.
+(.<=.) : Int -> Int -> Bool
+(.<=.) p q = case (p, q) of
+  (0, _) => True
+  _ => False
+
+countGreater : (thr : Int) -> (ctx : Vect n Int) -> Nat
+countGreater thr [] = Z
+countGreater thr (x :: xs) with (x .<=. thr)
+  countGreater thr (x :: xs) | True = countGreater thr xs
+  countGreater thr (x :: xs) | False = S $ countGreater thr xs
+
+-- map a variable from the old context to the erased context
+-- where we erase all bindings less than or equal to the threshold
+eraseVar : (thr : Int) -> (ctx : Vect n Int) -> Fin n -> Maybe (Fin (countGreater thr ctx))
+eraseVar thr (x :: xs) j with (x .<=. thr)
+  eraseVar thr (x :: xs) FZ | True = Nothing
+  eraseVar thr (x :: xs) FZ | False = Just FZ
+  eraseVar thr (x :: xs) (FS i) | True = FS <$> eraseVar thr xs i
+  eraseVar thr (x :: xs) (FS i) | False = FS <$> eraseVar thr xs i
+
+boom : Maybe (Fin 1)
+boom = eraseVar 0 [0, 1] (FS FZ)
--- a/tests/idris2/reg023/expected
+++ b/tests/idris2/reg023/expected
@ -0,0 +1,6 @@
+1/1: Building boom (boom.idr)
+boom.idr:23:42--24:3:While processing right hand side of with block in eraseVar at boom.idr:23:3--24:3:
+Can't solve constraint between:
+	S (countGreater thr xs)
+and
+	countGreater thr xs
--- a/tests/idris2/reg023/run
+++ b/tests/idris2/reg023/run
@ -0,0 +1,3 @@
+$1 --check boom.idr
+
+rm -rf build
--- a/tests/ttimp/basic003/expected
+++ b/tests/ttimp/basic003/expected
@ -1,8 +1,8 @@
 Processing as TTImp
 Written TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!
 Processing as TTC
 Read TTC
-Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
+Yaffle> Main.foo : (%pi Rig0 Explicit (Just m) Main.Nat (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just {k:26}) Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit (Just _) Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
 Yaffle> Bye for now!
--- a/tests/ttimp/eta001/expected
+++ b/tests/ttimp/eta001/expected
@ -1,5 +1,5 @@
 Processing as TTImp
 Written TTC
 Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
-Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
+Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit (Just x) Integer (%lam RigW Explicit (Just y) Integer ((Main.MkTest x) y))))
 Yaffle> Bye for now!
--- a/tests/ttimp/qtt001/expected
+++ b/tests/ttimp/qtt001/expected
@ -1,8 +1,8 @@
 Processing as TTImp
 QTT.yaff:14:1--16:1:When elaborating right hand side of Main.dupbad:
 QTT.yaff:14:13--16:1:There are 2 uses of linear name x
-Yaffle> Main.foo : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
-Yaffle> Main.bar : (%pi Rig0 Explicit Just a %type (%pi Rig1 Explicit Just _ a a))
-Yaffle> Main.baz1 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
-Yaffle> Main.baz2 : (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just _ a a))
+Yaffle> Main.foo : (%pi Rig0 Explicit (Just a) %type (%pi Rig1 Explicit (Just _) a a))
+Yaffle> Main.bar : (%pi Rig0 Explicit (Just a) %type (%pi Rig1 Explicit (Just _) a a))
+Yaffle> Main.baz1 : (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just _) a a))
+Yaffle> Main.baz2 : (%pi Rig0 Explicit (Just a) %type (%pi Rig0 Explicit (Just _) a a))
 Yaffle> Bye for now!
--- a/tests/ttimp/record002/expected
+++ b/tests/ttimp/record002/expected
@ -1,7 +1,7 @@
 Processing as TTImp
 Written TTC
 Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 11) 10))
-Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit Just n Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
-Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit Just n Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
+Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
+Yaffle> ((((Main.MkMyDPair [Just a = Main.Nat]) [Just p = (%lam RigW Explicit (Just n) Main.Nat ((Main.Vect n) Integer))]) (Main.S (Main.S (Main.S (Main.S Main.Z))))) ((((Main.Cons [Just k = (Main.S (Main.S (Main.S Main.Z)))]) [Just a = Integer]) 10) ((((Main.Cons [Just k = (Main.S (Main.S Main.Z))]) [Just a = Integer]) 1) ((((Main.Cons [Just k = (Main.S Main.Z)]) [Just a = Integer]) 2) ((((Main.Cons [Just k = Main.Z]) [Just a = Integer]) 3) (Main.Nil [Just a = Integer]))))))
 Yaffle> ((((Main.MkPerson "Fred") 1337) 10) ((Main.MkStats 10) 94))
 Yaffle> Bye for now!