[Typer] [Git][monnier/typer][ja-barszcz] 30 commits: * btl/builtins.typer (Eq_comm): Update FIXME

19 Aoû 2020


      Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer
Commits:
2bd6aa15 by Stefan Monnier at 2020-08-10T23:52:31-04:00
* btl/builtins.typer (Eq_comm): Update FIXME
- - - - -
f04cab52 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00
Delay parsing of declarations until elaboration for define-operator
* elab.ml (lexp_p_decls): Add a parameter for unparsed tokens, so that
later declarations can be parsed in a context with newly declared
operators
- - - - -
456370bc by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00
Remove the parsing error for tightly binding postfix operators
- - - - -
8beb9266 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00
Dump the evaluation context when the variable names don&#39;t match
- - - - -
2e00884b by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00
Assign the builtins Int.+, etc to suitable variables Int_+, etc.
_+_ can be Int.+ by default, but we should also keep that value in
Int_+ in case _+_ gets reassigned (with a num typeclass, for
instance).
- - - - -
baeefc84 by Jean-Alexandre Barszcz at 2020-08-19T17:14:33-04:00
Apply the instanciated metavariable substs when displaying lexps
- - - - -
785f7194 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Replace instanciated metavars when checking syntactic equality
- - - - -
5dc41cb5 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Make unification symmetric
- - - - -
b24651cf by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Handle variables earlier during unification
- - - - -
ff15b9bf by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] experiments with Decidable and proofs
- - - - -
7f3efef9 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] unify instead of conv_p in sform_lambda
- - - - -
e0cc1ee7 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] proof of Decidable (a &lt; b)
- - - - -
b3cf0b55 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] First draft of an instance search algorithm
- - - - -
82322188 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
WIP WIP WIP
- - - - -
824bf9af by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
WIP WIP getting there
- - - - -
1d95d938 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Add a set of typeclasses to the elab context
- - - - -
d3956bb9 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Add a syntax for records
- - - - -
5d320fcb by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Extend the Decidable sample with conjunction (dep on records)
- - - - -
2b9a43b2 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Resolve instances in the REPL (since exprs. are not generalized)
- - - - -
63c21f3c by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Resolve instances for recursive definitions
- - - - -
a11fe53d by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Do the set_getenv
IIRC these were missing to correctly handle the elab context for macro
expansion and Elab_... primitives. Perhaps it would be simpler to call
set_getenv once before macro expansion rather than everywhere where
the context can change. Needs some experimentation and tests.
- - - - -
59739897 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Num class example
- - - - -
18f5ae08 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Num class (with records)
- - - - -
cb4d6cba by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Allow non-inductives to be typeclasses (Eq for instance)
- - - - -
be4bf5b6 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Move the Eq builtin to debruijn.ml to make it available for elab.
- - - - -
9776b75d by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Make Eq.refl available to the ocaml code
* src/debruijn.ml : Add a definition of the lexp for Eq.refl
* src/builtin.ml : Register the constant Eq.refl
* btl/builtins.typer (Eq_refl) : Use the builtin variable ##Eq.refl
instead of registering the builtin with the `Built-in` form. This
ensures that we have the right variable and type, and might help to
keep things in sync between the ocaml and typer code.
- - - - -
a8488c58 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Add Eq to case
- - - - -
81c414f9 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Adding Eq to Case: mutual rec for (whnf &amp; get_type) + conv_p of case?
- - - - -
2d37bcab by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
[WIP] Fix whnf of case??
TODO test and explain the problem
- - - - -
a6e5e687 by Jean-Alexandre Barszcz at 2020-08-19T17:41:38-04:00
Algebra classes sample with proof of associativity of +
- - - - -
23 changed files:
- btl/builtins.typer
- btl/pervasive.typer
- + btl/records.typer
- + samples/alg_classes.typer
- + samples/decidable.typer
- + samples/num_class.typer
- + samples/num_class_recs.typer
- src/REPL.ml
- src/builtin.ml
- src/debruijn.ml
- src/debug_util.ml
- src/elab.ml
- src/env.ml
- src/eval.ml
- + src/instances.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/log.ml
- src/myers.ml
- src/opslexp.ml
- src/sexp.ml
- src/unification.ml
- tests/unify_test.ml
Changes:
=====================================
btl/builtins.typer
=====================================
@@ -47,8 +47,8 @@ Void = typecons Void;
%% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l
 %% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l
-Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error!
-Eq_refl = Built-in "Eq.refl";
+Eq_refl : ((x : ?t) ≡> Eq x x);
+Eq_refl = ##Eq.refl;
Eq_cast : (x : ?) ≡> (y : ?)
           ≡> (p : Eq x y)
@@ -63,8 +63,11 @@ Eq_cast = Built-in "Eq.cast";
 %%     Eq_comm : Eq ?x ?y -> Eq ?y ?x`;
 Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x;
 Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x)
-                    %% FIXME: I can't figure out how `(p := p)`
-                    %% gets inferred here, yet it seems to work!?!
+                    %% FIXME: The code is incorrectly accepted even without
+                    %% this `(p := p)` because we just get a metavar which
+                    %% remains uninstantiated and undetected (and then gets
+                    %% throw away by erasure)!
+                    (p := p)
                     Eq_refl;
%% General recursion!!
@@ -77,7 +80,7 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x)
 %%
 %% But this is not sufficient, because you could use `Y` to create
 %% new recursive *types* which then let you construct new arbitrary
-%% recursive values of previously uninhabited types.
+%% recursive values of previously non-existent types.
 %% E.g. you could create `Y <something> = ((... → t) -> t) -> t`
 %% and then give the term `λx. x x` inhabiting that type, and from that
 %% get a proof of False.
@@ -100,10 +103,15 @@ true = datacons Bool true;
 false = datacons Bool false;
%% Basic operators
-_+_ = Built-in "Int.+" : Int -> Int -> Int;
-_-_ = Built-in "Int.-" : Int -> Int -> Int;
-_*_ = Built-in "Int.*" : Int -> Int -> Int;
-_/_ = Built-in "Int./" : Int -> Int -> Int;
+Int_+ = Built-in "Int.+" : Int -> Int -> Int;
+Int_- = Built-in "Int.-" : Int -> Int -> Int;
+Int_* = Built-in "Int.*" : Int -> Int -> Int;
+Int_/ = Built-in "Int./" : Int -> Int -> Int;
+
+_+_ = Int_+;
+_-_ = Int_-;
+_*_ = Int_*;
+_/_ = Int_/;
%% modulo
 Int_mod = Built-in "Int.mod" : Int -> Int -> Int;
@@ -355,6 +363,12 @@ Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool;
 Elab_isconstructor = Built-in "Elab.isconstructor"
   : String -> Elab_Context -> Bool;
+%%
+%% Check if a symbol is an inductive in a particular context
+%%
+Elab_isinductive = Built-in "Elab.isinductive"
+  : String -> Elab_Context -> Bool;
+
 %%
 %% Check if the n'th field of a constructor is erasable
 %% If the constructor isn't defined it will always return false
@@ -381,6 +395,20 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin
 %%
 Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int;
+%%
+%% Get the position of a field in a constructor
+%% It return -1 in case the field isn't defined
+%% see pervasive.typer for a more convenient function
+%%
+Elab_ind-ctor-arg-pos' = Built-in "Elab.ind-ctor-arg-pos" : String -> String -> String -> Elab_Context -> Int;
+
+%%
+%% Get the number of fields in a constructor
+%% It return -1 in case the field isn't defined
+%% see pervasive.typer for a more convenient function
+%%
+Elab_count-ctor-args' = Built-in "Elab.count-ctor-args" : String -> String -> Elab_Context -> Int;
+
 %%
 %% Get the docstring associated with a symbol
 %%
=====================================
btl/pervasive.typer
=====================================
@@ -394,7 +394,7 @@ BoolMod = (##datacons
 Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
 pair = datacons Pair pair;
-__.__ =
+dot-impl =
   let mksel o f =
         let constructor = Sexp_node (Sexp_symbol "##datacons")
                                     (cons (Sexp_symbol "?")
@@ -411,14 +411,15 @@ __.__ =
                      (cons (Sexp_node (Sexp_symbol "_|_")
                                       (cons o (cons branch nil)))
                            nil)
-  in macro (lambda args
-            -> IO_return
-                   case args
-                   | cons o tail
-                     => (case tail
-                         | cons f _ => mksel o f
-                         | nil => Sexp_error)
-                   | nil => Sexp_error);
+  in (lambda args ->
+      IO_return case args
+                | cons o tail
+                  => (case tail
+                      | cons f _ => mksel o f
+                      | nil => Sexp_error)
+                | nil => Sexp_error);
+
+__.__ = macro dot-impl;
%% Triplet (tuple with 3 values)
 type Triplet (a : Type) (b : Type) (c : Type)
@@ -458,7 +459,8 @@ Not prop = prop -> False;
 %% We don't use the `type` macro here because it would make these `true`
 %% and `false` constructors override `Bool`'s, and we currently don't
 %% want that.
-Decidable = typecons (Decidable (prop : Type_ ?ℓ))
+%% FIXME generalize typecons formal arguments
+Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ))
                      (true (p ::: prop)) (false (p ::: Not prop));
%% Testing generalization in inductive type constructors.
@@ -547,6 +549,32 @@ in case (Int_eq r (-1))
      | true  => (none)
      | false => (some r);
+%%
+%% If `Elab_ind-ctor-arg-pos'` returns (-1) it means:
+%%   A- The constructor isn't defined, or
+%%   B- The constructor has no argument named like this
+%%
+%% So in those case this function returns `none`
+%%
+Elab_ind-ctor-arg-pos a b c d = let
+  r = Elab_ind-ctor-arg-pos' a b c d;
+in case (Int_eq r (-1))
+     | true  => (none)
+     | false => (some r);
+
+%%
+%% If `Elab_count-ctor-args'` returns (-1) it means:
+%%   A- The constructor isn't defined, or
+%%   B- The constructor has no argument named like this
+%%
+%% So in those case this function returns `none`
+%%
+Elab_count-ctor-args a b c = let
+  r = Elab_count-ctor-args' a b c;
+in case (Int_eq r (-1))
+     | true  => (none)
+     | false => (some r);
+
 %%%%
 %%%% Common library
 %%%%
@@ -634,6 +662,15 @@ plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro;
 %%
 _|_ = let lib = load "btl/polyfun.typer" in lib._|_;
+%%
+%% records : a simple datatype when there is only one case
+%%
+define-operator "#" 200 ();
+records = load "btl/records.typer";
+record = records.record;
+__.__ = records.__.__;
+_# = records._#;
+
 %%%% Unit tests function for doing file
%% It's hard to do a primitive which execute test file
=====================================
btl/records.typer
=====================================
@@ -0,0 +1,82 @@
+record-impl : List Sexp -> IO Sexp;
+record-impl args =
+  let 
+      %% Get a name (symbol) from a sexp
+      %%   - (name t) -> name
+      %%   - name -> name
+      get-name : Sexp -> Sexp;
+      get-name sxp =
+        case Sexp_wrap sxp
+        | node op _ => get-name op
+        | symbol _ => sxp
+        | _ => Sexp_error;
+
+      %% head is (Sexp_node type-name (arg list))
+      name-args = List_head Sexp_error args;
+      fields = List_tail args;
+
+      type-name = get-name name-args;
+
+      %% Create the inductive type definition.
+      inductive = Sexp_node (Sexp_symbol "typecons")
+                            (cons name-args
+                                  (cons (Sexp_node (Sexp_symbol "rec") fields)
+                                        nil));
+
+      decl  = make-decl type-name inductive;
+
+  in IO_return decl;
+         
+record = macro record-impl;
+
+record-get-impl : List Sexp -> IO Sexp;
+record-get-impl args =
+  let
+      get tc f idx nargs ectx =
+        let arg_pats : Sexp -> Int -> Int -> List Sexp;
+            arg_pats s i n =
+              if (Int_eq n 0) then nil
+              else (if (Int_eq i 0)
+                    then (cons s (arg_pats s (i - 1) (n - 1)))
+                    else (cons (Sexp_symbol "_") (arg_pats s (i - 1) (n - 1))));
+
+            pat = (Sexp_node (quote (datacons (uquote (Sexp_symbol tc)) rec))
+                             (arg_pats (Sexp_symbol "v") idx nargs));
+
+            branch = (quote ((uquote pat) => v));
+        in
+            (quote (lambda rec -> (##case_ (_|_ rec (uquote branch)))));
+
+      try-rec-get : List Sexp -> Elab_Context -> Option Sexp;
+      try-rec-get arg ectx =
+        case args
+        | (cons tc (cons f nil)) =>
+            (case (Sexp_wrap tc, Sexp_wrap f)
+             | (symbol tcstr, symbol fstr) =>
+                 (case (Elab_count-ctor-args tcstr "rec" ectx,
+                        Elab_ind-ctor-arg-pos tcstr "rec" fstr ectx)
+                  | (some nargs, some idx) => some (get tcstr fstr idx nargs ectx)
+                  | _ => none)
+             | _ => none)
+        | _ => none;
+  in
+  do {
+          ectx <- Elab_getenv ();
+          case try-rec-get args ectx
+          | some sxp => IO_return sxp
+          | _ => dot-impl args; %% Fallback on default dot implementation
+      };
+
+__.__ = macro record-get-impl;
+
+record-make-impl : List Sexp -> IO Sexp;
+record-make-impl args =
+  IO_return case args
+            | (cons tc nil) => (quote (datacons (uquote tc) rec))
+            | _ => Sexp_error;
+
+_# = macro record-make-impl; %% I was going for a syntax close to
+                             %% Erlang's, but the # doesn't separate
+                             %% tokens ... Meh.
+
+record (Pair (a : Type) (b : Type)) (fst : a) (snd : a);
=====================================
samples/alg_classes.typer
=====================================
@@ -0,0 +1,84 @@
+case_ = ##case_; %% To ease debugging
+
+type Magma (α : Type)
+  | mkMagma (op : α -> α -> α);
+
+typeclass Magma;
+
+magma_op =
+  lambda magma_inst =>
+    case magma_inst
+    | mkMagma op => op;
+
+Associativity (op : ?α -> ?α -> ?α) =
+  (x : ?α) -> (y : ?α) -> (z : ?α) -> Eq (op (op x y) z) (op x (op y z));
+
+type Semigroup (α : Type)
+  | mkSemigroup (magma : Magma α) (assoc ::: Associativity magma_op);
+
+typeclass Semigroup;
+
+semigroup_magma =
+  lambda semigroup_inst =>
+    case semigroup_inst
+    | mkSemigroup magma => magma;
+
+IsLeftIdentity (id : ?α) (op : ?α -> ?α -> ?α) =
+  (x : ?α) -> Eq (op id x) x;
+
+IsRightIdentity (id : ?α) (op : ?α -> ?α -> ?α) =
+  (x : ?α) -> Eq (op x id) x;
+
+IsIdentity (id : ?α) (op : ?α -> ?α -> ?α) =
+  (Pair (IsLeftIdentity id op) (IsRightIdentity id op));
+
+type Monoid (α : Type)
+  | mkMonoid (semigroup : Semigroup α)
+             (identity : α)
+             (isIdent ::: IsIdentity identity magma_op);
+
+typeclass Monoid;
+
+type Nat
+  | Zero
+  | Succ Nat;
+
+plus : Nat -> Nat -> Nat;
+plus x y =
+  case x
+  | Zero => y
+  | Succ x' => Succ (plus x' y);
+
+natAdditiveMagma =
+  mkMagma plus;
+
+Eq_cong : % not sure about levels here
+  (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡>
+  (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡>
+  (f : (t -> r)) -> (Eq (f x) (f y));
+Eq_cong f =
+  Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl;
+
+natPlusAssoc : Associativity plus;
+natPlusAssoc x y z =
+  let
+      typeclass Eq
+  in
+      case x
+      | Zero => Eq_cast
+                    (x := Zero)
+                    (y := x)
+                    (p := Eq_comm (instance ()))
+                    (f := (lambda (Zx : Nat) -> Eq (plus (plus Zx y) z) (plus Zx (plus y z))))
+                    Eq_refl
+      | Succ x' =>
+          Eq_cast
+              (x := Succ x')
+              (y := x)
+              (p := Eq_comm (instance ()))
+              (f := (lambda (sx'x : Nat) -> Eq (plus (plus sx'x y) z) (plus sx'x (plus y z))))
+              (Eq_cong (p := natPlusAssoc x' y z) Succ);
+
+natAdditiveSemigroup : Semigroup Nat;
+natAdditiveSemigroup =
+  mkSemigroup natAdditiveMagma (assoc := natPlusAssoc);
=====================================
samples/decidable.typer
=====================================
@@ -0,0 +1,168 @@
+False = Void;
+True = Unit;
+
+% FIXME improved "case" fails with no branches
+exfalso : False -> ?a;
+exfalso f = ##case_ f;
+
+%type Decidable (prop : Type)
+%  | yes (p ::: prop)
+%  | no (p ::: Not prop);
+yes = datacons Decidable true;
+no = datacons Decidable false;
+
+typeclass Decidable;
+
+Eq_trans :
+  (x : ?t) => (y : ?t) => (a : ?t) ->
+  (ax : Eq a x) => (ay : Eq a y) => Eq x y;
+Eq_trans a =
+  lambda (ax : Eq a x) (ay : Eq a y) =>
+    Eq_cast (f := lambda ax -> Eq ax y) ay;
+
+Eq_cong : % not sure about levels here
+  (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡>
+  (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡>
+  (f : (t -> r)) -> (Eq (f x) (f y));
+Eq_cong f =
+  Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl;
+
+discriminate_nocheck =
+  macro (lambda args ->
+    case args
+    | cons x (cons y nil) =>
+      do {
+        sd <- gensym ();
+        sp <- gensym ();
+        IO_return
+          (quote ((lambda (uquote sp) ->
+                     (Eq_cast (p := (uquote sp))
+                              (f := (lambda (uquote sd) ->
+                                       (case uquote sd
+                                        | (uquote x) => True
+                                        | _ => False)))
+                              ())) : Not (Eq (uquote x) (uquote y))))
+      }
+    | _ => IO_return Sexp_error);
+
+discriminate =
+  macro (lambda args ->
+    case args
+    | cons x (cons y nil) =>
+      (case (Sexp_wrap x, Sexp_wrap y)
+       | (symbol sx, symbol sy) => % FIXME get the constructor even when its a call
+         do {
+           env <- Elab_getenv ();
+           if (and (Elab_isconstructor sx env)
+                (and (Elab_isconstructor sy env)
+                  (not (Sexp_eq x y))))
+           then
+             Macro_expand discriminate_nocheck args
+           else (IO_return Sexp_error)
+         }
+       | _ => IO_return Sexp_error)
+    | _ => IO_return Sexp_error);
+
+test : (Not (Eq true false));
+test = discriminate true false;
+
+absurd =
+  lambda (p : ?prop) ->
+    lambda (contra : (Not ?prop)) ->
+      contra p;
+
+%   We can't (usefully) have a `Decidable Bool` because it's
+% impossible to have a `Not Bool`. Instead, we can decide boolean
+% equality:
+
+decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b);
+decideBoolEq =
+  lambda (a : Bool) (b : Bool) =>
+  case (a, b)
+  | (false, false) => yes (p := Eq_trans false)
+  | (false,  true) => no (p := lambda (p : Eq a b) ->
+       absurd (Eq_trans (ax := Eq_trans a) b) (discriminate false true))
+  | (true,  false) => no (p := lambda (p : Eq a b) ->
+       absurd (Eq_trans (ax := Eq_trans a) b) (discriminate true false))
+  | (true,   true) => yes (p := Eq_trans true);
+
+type Nat
+  | zero
+  | succ Nat;
+
+type even (a : Nat)
+  | eZ (p ::: Eq a zero)
+  | eSS (p :: even ?a) (pss ::: Eq a (succ (succ ?a)));
+
+decideEven : (a : Nat) => Decidable (even a);
+decideEven =
+  lambda (a : Nat) =>
+    case a
+    | zero => yes (p := eZ)
+    | succ zero => no (p :=
+        lambda (p : even a) ->
+          case p
+          | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ zero))
+          | eSS => absurd (Eq_trans a) (discriminate_nocheck (succ (succ ?)) (succ zero)))
+    | succ (succ a') =>
+        case (decideEven : Decidable (even a'))
+        | yes => yes (p := eSS)
+        | no => no (p :=
+          lambda (p : even a) ->
+            case p
+            | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ (succ ?)))
+            | eSS => absurd (? : even a') (? : Not (even a')));
+
+type _<_ (a : Nat) (b : Nat)
+  | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b))
+  | ltS (p :: (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b));
+
+decideLT : (a : Nat) => (b : Nat) => Decidable (a < b);
+decideLT =
+  lambda a b =>
+  case b
+  | zero => no (p :=
+      lambda (p : (a < b)) ->
+        case p
+        | ltZ => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?))
+	| ltS => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?)))
+  | succ b' =>
+    case a
+    | zero => yes (p := ltZ)
+    | succ a' =>
+      case (decideLT : (Decidable (a' < b')))
+      | yes => yes (p := ltS)
+      | no => no (p :=
+        lambda (p : (a < b)) ->
+          case p
+          | ltZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ ?))
+          | ltS => absurd (? : (a' < b')) (? : Not (a' < b')));
+
+define-operator "∧" 111 130;
+
+record ((a : Type) ∧ (b : Type)) (fst : a) (snd : b);
+
+decideAnd : (P : Type) ≡> (Q : Type) ≡>
+            (Decidable P) => (Decidable Q) => (Decidable (P ∧ Q));
+decideAnd =
+  lambda P Q ≡>
+  lambda (decP : Decidable P) (decQ : Decidable Q) =>
+  case (decP, decQ)
+  | (yes (p := pP), yes (p := pQ)) => yes (p := _∧_ # pP pQ)
+  | (no (p := nP), _) =>
+      no (p := (lambda (proofs : P ∧ Q) -> absurd (_∧_.fst proofs) nP))
+  | (_, no (p := nQ)) =>
+      no (p := (lambda (proofs : P ∧ Q) -> absurd (_∧_.snd proofs) nQ));
+
+if_then_else_
+  = macro (lambda args ->
+           let e1 = List_nth 0 args Sexp_error;
+               e2 = List_nth 1 args Sexp_error;
+               e3 = List_nth 2 args Sexp_error;
+           in IO_return (quote (case (instance () : (Decidable (uquote e1)))
+                                | yes => uquote e2
+                                | no => uquote e3)));
+
+test2 : Bool;
+test2 = if ((even (succ zero)) ∧ (zero < zero)) then false else true;
+
=====================================
samples/num_class.typer
=====================================
@@ -0,0 +1,39 @@
+type Num (α : Type)
+  | mkNum (Num_+ : α -> α -> α)
+          (Num_- : α -> α -> α)
+          (Num_* : α -> α -> α)
+          (Num_/ : α -> α -> α);
+
+typeclass Num;
+
+_+_ = lambda numInst => case numInst | mkNum _+_ _ _ _ => _+_;
+_-_ = lambda numInst => case numInst | mkNum _ _-_ _ _ => _-_;
+_*_ = lambda numInst => case numInst | mkNum _ _ _*_ _ => _*_;
+_/_ = lambda numInst => case numInst | mkNum _ _ _ _/_ => _/_;
+
+IntNum : Num Int;
+IntNum =
+  mkNum (Num_+ := Int_+) (Num_- := Int_-) (Num_* := Int_*) (Num_/ := Int_/);
+
+IntegerNum : Num Integer;
+IntegerNum =
+  mkNum (Num_+ := Integer_+) (Num_- := Integer_-)
+        (Num_* := Integer_*) (Num_/ := Integer_/);
+
+FloatNum : Num Float;
+FloatNum =
+  mkNum (Num_+ := Float_+) (Num_- := Float_-)
+        (Num_* := Float_*) (Num_/ := Float_/);
+
+type FromInt (α : Type)
+  | mkFromInt (FromInt_fromInt : Int -> α);
+
+typeclass FromInt;
+
+fromInt = lambda fromIntInst => case fromIntInst | mkFromInt fromInt => fromInt;
+
+IntFromInt : FromInt Int;
+IntFromInt = mkFromInt (lambda x -> x);
+
+IntegerFromInt : FromInt Integer;
+IntegerFromInt = mkFromInt Int->Integer;
=====================================
samples/num_class_recs.typer
=====================================
@@ -0,0 +1,33 @@
+record (Num (α : Type))
+       (_+_ : α -> α -> α)
+       (_-_ : α -> α -> α)
+       (_*_ : α -> α -> α)
+       (_/_ : α -> α -> α);
+
+typeclass Num;
+
+_+_ = lambda numInst => Num._+_ numInst;
+_-_ = lambda numInst => Num._-_ numInst;
+_*_ = lambda numInst => Num._*_ numInst;
+_/_ = lambda numInst => Num._/_ numInst;
+
+IntNum : Num Int;
+IntNum = Num # Int_+ Int_- Int_* Int_/;
+
+IntegerNum : Num Integer;
+IntegerNum = Num # Integer_+ Integer_- Integer_* Integer_/;
+
+FloatNum : Num Float;
+FloatNum = Num # Float_+ Float_- Float_* Float_/;
+
+record (FromInt (α : Type)) (fromInt : Int -> α);
+
+typeclass FromInt;
+
+fromInt = lambda fromIntInst => FromInt.fromInt fromIntInst;
+
+IntFromInt : FromInt Int;
+IntFromInt = FromInt # (lambda x -> x);
+
+IntegerFromInt : FromInt Integer;
+IntegerFromInt = FromInt # Int->Integer;
=====================================
src/REPL.ml
=====================================
@@ -135,8 +135,11 @@ let ierase_type (lexps: (ldecl list list * lexpr list)) =
let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) =
     let pdecls, pexprs = pexps in
-    let ldecls, lctx = Elab.lexp_p_decls pdecls lctx in
+    (* FIXME We take the parsed input here but we should take the
+       unparsed tokens directly instead *)
+    let ldecls, lctx = Elab.lexp_p_decls pdecls [] lctx in
     let lexprs = Elab.lexp_parse_all pexprs lctx in
+    List.iter Elab.resolve_instances lexprs;
     List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp))
               lexprs;
     (ldecls, lexprs), lctx
@@ -164,8 +167,7 @@ let ieval f str ectx rctx =
 let raw_eval f str ectx rctx =
     let pres = (f str) in
     let sxps = lex default_stt pres in
-    let nods = sexp_parse_all_to_list (ectx_to_grm ectx) sxps (Some ";") in
-    let lxps, ectx = Elab.lexp_p_decls nods ectx in
+    let lxps, ectx = Elab.lexp_p_decls [] sxps ectx in
     let elxps = List.map OL.clean_decls lxps in
     (* At this point, `elxps` is a `(vname * elexp) list list`, where:
      * - each `(vname * elexp)` is a definition
=====================================
src/builtin.ml
=====================================
@@ -99,19 +99,6 @@ let dloc    = DB.dloc
 let op_binary t = mkArrow (Anormal, (dloc, None), t, dloc,
                            mkArrow (Anormal, (dloc, None), t, dloc, t))
-let type_eq =
-  let lv = (dloc, Some "l") in
-  let tv = (dloc, Some "t") in
-  mkArrow (Aerasable, lv,
-           DB.type_level, dloc,
-           mkArrow (Aerasable, tv,
-                    mkSort (dloc, Stype (mkVar (lv, 0))), dloc,
-                    mkArrow (Anormal, (dloc, None),
-                             mkVar (tv, 0), dloc,
-                             mkArrow (Anormal, (dloc, None),
-                                      mkVar (tv, 1), dloc,
-                                      mkSort (dloc, Stype (mkVar (lv, 3)))))))
-
 let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx
(* Typer list as seen during runtime.  *)
@@ -161,7 +148,9 @@ let register_builtin_csts () =
   add_builtin_cst "Integer" DB.type_integer;
   add_builtin_cst "Float" DB.type_float;
   add_builtin_cst "String" DB.type_string;
-  add_builtin_cst "Elab_Context" DB.type_elabctx
+  add_builtin_cst "Elab_Context" DB.type_elabctx;
+  add_builtin_cst "Eq" DB.type_eq;
+  add_builtin_cst "Eq.refl" DB.eq_refl
let register_builtin_types () =
   let _ = new_builtin_type "Sexp" DB.type0 in
@@ -175,7 +164,6 @@ let register_builtin_types () =
             "Array" (mkArrow (Anormal, (dloc, None),
                             DB.type0, dloc, DB.type0)) in
   let _ = new_builtin_type "FileHandle" DB.type0 in
-  let _ = new_builtin_type "Eq" type_eq in
   ()
let _ = register_builtin_csts ();
=====================================
src/debruijn.ml
=====================================
@@ -94,6 +94,37 @@ let type_integer = mkBuiltin ((dloc, "Integer"), type0, None)
 let type_float = mkBuiltin ((dloc, "Float"), type0, None)
 let type_string = mkBuiltin ((dloc, "String"), type0, None)
 let type_elabctx = mkBuiltin ((dloc, "Elab_Context"), type0, None)
+let type_eq_type =
+  let lv = (dloc, Some "l") in
+  let tv = (dloc, Some "t") in
+  mkArrow (Aerasable, lv,
+           type_level, dloc,
+           mkArrow (Aerasable, tv,
+                    mkSort (dloc, Stype (mkVar (lv, 0))), dloc,
+                    mkArrow (Anormal, (dloc, None),
+                             mkVar (tv, 0), dloc,
+                             mkArrow (Anormal, (dloc, None),
+                                      mkVar (tv, 1), dloc,
+                                      mkSort (dloc, Stype (mkVar (lv, 3)))))))
+let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type, None)
+let eq_refl =
+  let lv = (dloc, Some "l") in
+  let tv = (dloc, Some "t") in
+  let xv = (dloc, Some "x") in
+  mkBuiltin ((dloc, "Eq.refl"),
+             mkArrow (Aerasable, lv,
+                      type_level, dloc,
+                      mkArrow (Aerasable, tv,
+                               mkSort (dloc, Stype (mkVar (lv, 0))), dloc,
+                               mkArrow (Aerasable, xv,
+                                        mkVar (tv, 0), dloc,
+                                        mkCall (type_eq,
+                                                [Aerasable, mkVar (lv, 2);
+                                                 Aerasable, mkVar (tv, 1);
+                                                 Anormal, mkVar (xv, 0);
+                                                 Anormal, mkVar (xv, 0)])))),
+             None)
+
(* easier to debug with type annotations *)
 type env_elem = (vname * varbind * ltype)
@@ -112,26 +143,29 @@ type meta_scope
     * lctx_length     (* Length of ctx when the scope is added.  *)
     * (meta_id SMap.t ref) (* Metavars already known in this scope.  *)
+type typeclass_ctx
+  = (ltype * lctx_length) list (* FIXME make it a set of lexps ? *)
+
 (* This is the *elaboration context* (i.e. a context that holds
  * a lexp context plus some side info.  *)
 type elab_context
-  = Grammar.grammar * senv_type * lexp_context * meta_scope
+  = Grammar.grammar * senv_type * lexp_context * meta_scope * typeclass_ctx
let get_size (ctx : elab_context)
-  = let (_, (n, _), lctx, _) = ctx in
+  = let (_, (n, _), lctx, _, _) = ctx in
     assert (n = M.length lctx); n
let ectx_to_grm (ectx : elab_context) : Grammar.grammar =
-  let (grm,_, _, _) = ectx in grm
+  let (grm,_, _, _, _) = ectx in grm
(* Extract the lexp context from the context used during elaboration.  *)
 let ectx_to_lctx (ectx : elab_context) : lexp_context =
-  let (_,_, lctx, _) = ectx in lctx
+  let (_,_, lctx, _, _) = ectx in lctx
-let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level
+let ectx_to_scope_level ((_, _, _, (sl, _, _), _) : elab_context) : scope_level
   = sl
-let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int
+let ectx_local_scope_size ((_, (n, _), _, (_, slen, _), _) as ectx) : int
   = get_size ectx - slen
(*  Public methods: DO USE
@@ -142,7 +176,7 @@ let empty_lctx = M.nil
let empty_elab_context : elab_context
   = (Grammar.default_grammar, empty_senv, empty_lctx,
-     (0, 0, ref SMap.empty))
+     (0, 0, ref SMap.empty), [])
(* senv_lookup caller were using Not_found exception *)
 exception Senv_Lookup_Fail of (string list)
@@ -150,7 +184,7 @@ let senv_lookup_fail relateds = raise (Senv_Lookup_Fail relateds)
(* Return its current DeBruijn index.  *)
 let senv_lookup (name: string) (ctx: elab_context): int =
-  let (_, (n, map), _, _) = ctx in
+  let (_, (n, map), _, _, _) = ctx in
   try n - (SMap.find name map) - 1
   with Not_found
        -> let get_related_names (n : db_ridx) name map =
@@ -189,11 +223,11 @@ let lctx_extend (ctx : lexp_context) (def: vname) (v: varbind) (t: lexp) =
let env_extend_rec (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) =
   let (loc, oname) = def in
-  let (grm, (n, map), env, sl) = ctx in
+  let (grm, (n, map), env, sl, tcctx) = ctx in
   let nmap = match oname with None -> map | Some name -> SMap.add name n map in
   (grm, (n + 1, nmap),
    lexp_ctx_cons env def v t,
-   sl)
+   sl, tcctx)
let ectx_extend (ctx: elab_context) (def: vname) (v: varbind) (t: lexp) = env_extend_rec ctx def v t
@@ -207,28 +241,33 @@ let lctx_extend_rec (ctx : lexp_context) (defs: (vname * lexp * ltype) list) =
   ctx
let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) =
-  let (grm, (n, senv), lctx, sl) = ctx in
+  let (grm, (n, senv), lctx, sl, tcctx) = ctx in
   let senv', _ = List.fold_left
                    (fun (senv, i) ((_, oname), _, _) ->
                      (match oname with None -> senv
                                      | Some name -> SMap.add name i senv),
                      i + 1)
                    (senv, n) defs in
-  (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl)
+  (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl, tcctx)
let ectx_new_scope (ectx : elab_context) : elab_context =
-  let (grm, senv, lctx, (scope, _, rmmap)) = ectx in
-  (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)))
+  let (grm, senv, lctx, (scope, _, rmmap), tcctx) = ectx in
+  (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)), tcctx)
let ectx_get_scope (ectx : elab_context) : meta_scope =
-  let (_, _, _, sl) = ectx in sl
+  let (_, _, _, sl, _) = ectx in sl
let ectx_get_grammar (ectx : elab_context) : Grammar.grammar =
-  let (grm, _, _, _) = ectx in grm
+  let (grm, _, _, _, _) = ectx in grm
let env_lookup_by_index index (ctx: lexp_context): env_elem =
   Myers.nth index ctx
+let env_add_typeclass (ectx : elab_context) (t : ltype) : elab_context =
+  let (grm, senv, lctx, sl, tcctx) = ectx in
+  let ntcctx = ((t, get_size ectx) :: tcctx) in
+  (grm, senv, lctx, sl, ntcctx)
+
 (*  Print context  *)
 let print_lexp_ctx_n (ctx : lexp_context) start =
     let n = (M.length ctx) - 1 in
=====================================
src/debug_util.ml
=====================================
@@ -138,8 +138,6 @@ let arg_defs = [
         Arg.Unit (add_p_option "pretok"), " Print pretok debug info");
     ("-tok",
         Arg.Unit (add_p_option "tok"), " Print tok debug info");
-    ("-sexp",
-        Arg.Unit (add_p_option "sexp"), " Print sexp debug info");
     ("-pexp",
         Arg.Unit (add_p_option "pexp"), " Print pexp debug info");
     ("-lexp",
@@ -152,7 +150,6 @@ let arg_defs = [
         Arg.Unit (fun () ->
             add_p_option "pretok" ();
             add_p_option "tok" ();
-            add_p_option "sexp" ();
             add_p_option "pexp" ();
             add_p_option "lexp" ();
             add_p_option "lctx" ();
@@ -165,7 +162,6 @@ let parse_args () =
let make_default () =
     arg_print_options := SMap.empty;
-    add_p_option "sexp" ();
     add_p_option "pexp" ();
     add_p_option "lexp" ()
@@ -176,10 +172,8 @@ let format_source () =
     let filename = List.hd (!arg_files) in
     let pretoks = prelex_file filename in
     let toks = lex default_stt pretoks in
-    let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx)
-                                       toks (Some ";") in
     let ctx = Elab.default_ectx in
-    let lexps, _ = Elab.lexp_p_decls nodes ctx in
+    let lexps, _ = Elab.lexp_p_decls [] toks ctx in
print_string (make_sep '-'); print_string "\n";
@@ -235,26 +229,12 @@ let main () =
             print_string (make_title " Base Sexp");
             debug_sexp_print_all toks; print_string "\n"));
-        (* get node sexp  *)
-        print_string yellow;
-        let nodes = sexp_parse_all_to_list (ectx_to_grm Elab.default_ectx)
-                                           toks (Some ";") in
-        print_string reset;
-
-        (if (get_p_option "sexp") then(
-            print_string (make_title " Node Sexp ");
-            debug_sexp_print_all nodes; print_string "\n"));
-
-        (* Parse All Declaration *)
-        print_string yellow;
-        print_string reset;
-
         (* get lexp *)
         let octx = Elab.default_ectx in
(* debug lexp parsing once merged *)
         print_string yellow;
-        let lexps, nctx = try Elab.lexp_p_decls nodes octx
+        let lexps, nctx = try Elab.lexp_p_decls [] toks octx
           with e ->
             print_string reset;
             raise e in
=====================================
src/elab.ml
=====================================
@@ -57,6 +57,7 @@ open Grammar
 module BI = Builtin
module Unif = Unification
+module Inst = Instances
module OL = Opslexp
 module EL = Elexp
@@ -238,9 +239,9 @@ let ctx_define_rec (ctx: elab_context) decls =
  * infer the types and perform macro-expansion.
  *
  * More specifically, we do it with 2 mutually recursive functions:
- * - `check` takes a Pexp along with its expected type and returns an Lexp
+ * - `check` takes an Sexp along with its expected type and returns an Lexp
  *   of that type (hopefully)
- * - `infer` takes a Pexp and infers its type (which it returns along with
+ * - `infer` takes an Sexp and infers its type (which it returns along with
  *   the Lexp).
  * This is the idea of "bidirectional type checking", which minimizes
  * the amount of "guessing" and/or annotations.  Since we infer types anyway
@@ -257,6 +258,13 @@ let newMetavar (ctx : lexp_context) sl name t =
   let meta = Unif.create_metavar ctx sl t in
   mkMetavar (meta, S.identity, name)
+let newInstanceMetavar (ctx : elab_context) name t =
+  let lctx = ectx_to_lctx ctx in
+  let sl = ectx_to_scope_level ctx in
+  let meta = Unif.create_metavar lctx sl t in
+  Inst.add_instance_metavar meta ctx (fst name);
+  mkMetavar (meta, S.identity, name)
+
 let newMetalevel (ctx : lexp_context) sl loc =
   newMetavar ctx sl (loc, Some "ℓ") type_level
@@ -280,8 +288,8 @@ let sdform_define_operator (ctx : elab_context) loc sargs _ot : elab_context =
         | Symbol (_, "") -> None
         | Integer (_, n) -> Some n
         | _ -> sexp_error (sexp_location s) "Expecting an integer or ()"; None in
-      let (grm, a, b, c) = ctx in
-      (SMap.add name (level l, level r) grm, a, b, c)
+      let (grm, a, b, c, d) = ctx in
+      (SMap.add name (level l, level r) grm, a, b, c, d)
   | [o; _; _]
     -> sexp_error (sexp_location o) "Expecting a string"; ctx
   | _
@@ -466,11 +474,11 @@ let rec meta_to_var ids (e : lexp) =
       -> let ncases
           = SMap.map
               (fun (l, fields, e)
-               -> (l, fields, loop (o + List.length fields) e))
+               -> (l, fields, loop (o + List.length fields + 1) e))
               cases in
         mkCase (l, loop o e, loop o t, ncases,
                 match default with None -> None
-                                 | Some (v, e) -> Some (v, loop (1 + o) e))
+                                 | Some (v, e) -> Some (v, loop (2 + o) e))
     | Metavar (id, s, name)
       -> if IMap.mem id ids then
           mkVar (name, o + count - IMap.find id ids)
@@ -625,12 +633,83 @@ and get_implicit_arg ctx loc oname t =
 and instantiate_implicit e t ctx =
   let rec instantiate t args =
     match OL.lexp_whnf t (ectx_to_lctx ctx) with
+    | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) when Inst.is_typeclass ctx t1
+      -> let arg = newInstanceMetavar ctx (lexp_location e, v) t1 in
+         instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args)
     | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2)
       -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in
         instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args)
     | _ -> (mkCall (e, List.rev args), t)
   in instantiate t []
+and myers_filter_map_index (f : int -> 'a -> 'b option) (m : 'a M.myers)
+    : ('b M.myers)
+  = snd (M.fold_right
+           (fun x (i, l') ->
+             match (f i x) with
+             | Some y -> (i - 1, M.cons y l')
+             | None -> (i - 1, l'))
+           m (M.length m - 1, M.nil))
+
+and search_instance (ctx : elab_context) (loc : location) (t : ltype) : lexp option =
+  Log.log_debug ~loc ("Searching for t = `" ^ (lexp_string t) ^ "`");
+  let ctx = ectx_new_scope ctx in
+  let lctx = (ectx_to_lctx ctx) in
+  let sl = (ectx_to_scope_level ctx) in
+  let env_elem_match (i : int) (elem : DB.env_elem) : (int * DB.env_elem * lexp * ltype) option =
+    let ((_, namopt), _, t') = elem in
+    let var = mkVar ((loc,namopt), i) in
+    let t' = mkSusp t' (S.shift (i + 1)) in
+    let (e, t') = instantiate_implicit var t' ctx in
+    (* All candidates should have a type that is a typeclass *)
+    if not (Inst.is_typeclass ctx t') then None else
+      match Inst.check_typeclass_match t t' lctx sl with
+      | (Impossible | Possible) -> None
+      (* | Possible -> None *)
+      | (Match) -> Some (i, elem, e, t') in
+  let candidates =
+    myers_filter_map_index env_elem_match lctx in
+  Log.log_debug ("Candidates for instance of type `" ^ lexp_string t ^ "`:")
+    ~print_action:(fun () ->
+      M.iter (fun (i, ((_, so),_,t'),_, _) ->
+          lalign_print_int i 4;
+          lalign_print_string (match so with | Some s -> s | None -> "<none>") 10;
+          print_endline (lexp_string t')) candidates);
+  match M.safe_car candidates with
+  | None  -> None
+  | Some (i, (vname, _, t'),e,t) ->
+     let t' = mkSusp t' (S.shift (i + 1)) in
+     Log.log_debug ~loc
+       ("Found candidate at index " ^ (string_of_int i) ^ ": `" ^
+          (lexp_string (Var (vname, i))) ^ " : " ^ (lexp_string t') ^ "`");
+     Some e
+
+and resolve_instances e =
+  let (_, (fv_map, _)) = OL.fv e in
+  U.IMap.iter (fun i (sl, t, cl, vn) ->
+      match Inst.instance_metavar_lookup i with
+      | Some (ctx, loc) ->
+         (match search_instance ctx loc t with
+          | Some e -> Unif.associate i e; resolve_instances e
+          | None ->
+             error ~loc ("No instance found for type `" ^ (lexp_string t) ^ "`")
+         )
+      | None -> ()
+    ) fv_map
+
+
+and resolve_instances_and_generalize ctx e =
+  resolve_instances e;
+  generalize ctx e
+
+and sdform_typeclass (ctx : elab_context) loc sargs _ot : elab_context =
+  match sargs with
+  | [se] ->
+     let (t, _) = infer se ctx in
+     Inst.add_typeclass ctx t
+  | _
+    -> sexp_error loc "typeclass expects 1 argument"; ctx
+
 and infer_type pexp ectx var =
   (* We could also use lexp_check with an argument of the form
    * Sort (?s), but in most cases the metavar would be allocated
@@ -707,7 +786,8 @@ and check_inferred ctx e inferred_t t =
      -> lexp_error (lexp_location e) e
          ("Type mismatch("
           ^ (match ck with | Unif.CKimpossible -> "impossible"
-                           | Unif.CKresidual -> "residue")
+                           | Unif.CKresidual -> "residue"
+                           | _ -> failwith "impossible" )
           ^ ")!  Context expected:\n    "
           ^ lexp_string t ^ "\nbut expression has type:\n    "
           ^ lexp_string inferred_t ^ "\ncan't unify:\n    "
@@ -738,16 +818,16 @@ and check_case rtype (loc, target, ppatterns) ctx =
     let ltarget = ref tlxp in
let get_cs_as it' lctor =
+      let unify_ind expected actual =
+        match Unif.unify actual expected (ectx_to_lctx ctx) with
+        | (_::_)
+          -> lexp_error loc lctor
+               ("Expected pattern of type `" ^ lexp_string expected
+                ^ "` but got `" ^ lexp_string actual ^ "`")
+        | [] -> () in
       match !it_cs_as with
       | Some (it, cs, args)
-        -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with
-            | (_::_)
-              -> lexp_error loc lctor
-                  ("Expected pattern of type `"
-                   ^ lexp_string it ^ "` but got `"
-                   ^ lexp_string it' ^ "`")
-            | [] -> () in
-          (cs, args)
+        -> unify_ind it it'; (cs, args)
       | None
         -> match OL.lexp_whnf it' (ectx_to_lctx ctx) with
           | Inductive (_, _, fargs, constructors)
@@ -768,6 +848,7 @@ and check_case rtype (loc, target, ppatterns) ctx =
                   with | Call (f, args) -> (f, args)
                        | _ -> (e,[]) in
                 let (it, targs) = call_split tltp in
+                unify_ind it it';
                 let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with
                   | Inductive (_, _, fargs, constructors)
                     -> assert (List.length fargs = List.length targs);
@@ -776,14 +857,42 @@ and check_case rtype (loc, target, ppatterns) ctx =
                           ("Can't `case` on objects of this type: "
                            ^ lexp_string tltp);
                         SMap.empty in
+                it_cs_as := Some (it, constructors, targs);
                 (constructors, targs) in
(*  Read patterns one by one *)
     let fold_fun (lbranches, dflt) (pat, pexp) =
+      let shift_to_extended_ctx nctx lexp =
+        mkSusp lexp (S.shift (M.length (ectx_to_lctx nctx)
+                              - M.length (ectx_to_lctx ctx))) in
+
+      let ctx_extend_with_eq nctx head_lexp =
+        (* Add a proof of equality between the target and the branch
+           head to the context *)
+        let tlxp' = shift_to_extended_ctx nctx tlxp in
+        let tltp' = shift_to_extended_ctx nctx tltp in
+        let tkind = OL.get_type (ectx_to_lctx nctx) tltp' in
+        let tlevel = (match OL.lexp_whnf tkind (ectx_to_lctx nctx) with
+                      | Sort (_, Stype l) -> l
+                      | _ -> error "HMMM"; DB.level0) in
+        let head_lexp_type = OL.get_type (ectx_to_lctx nctx) head_lexp in
+        (match Unif.unify tltp' head_lexp_type (ectx_to_lctx nctx) with
+         | [] -> ()
+         | constraints -> Log.log_error "Unification failed for case Eq");
+        let eqty = mkCall (DB.type_eq,
+                           [(Aerasable, tlevel);   (* Typelevel *)
+                            (Aerasable, tltp');    (* Inductive type *)
+                            (Anormal, tlxp');      (* Target lexp *)
+                            (Anormal, head_lexp)]) (* Lexp of the branch head *)
+        in ctx_extend nctx (loc, None) Variable eqty
+      in
+
       let add_default v =
         (if dflt != None then uniqueness_warn pat);
         let nctx = ctx_extend ctx v Variable tltp in
+        let head_lexp = mkVar (v, 0) in
+        let nctx = ctx_extend_with_eq nctx head_lexp in
         let rtype' = mkSusp rtype (S.shift (M.length (ectx_to_lctx nctx)
                                             - M.length (ectx_to_lctx ctx))) in
         let lexp = check pexp rtype' nctx in
@@ -864,6 +973,15 @@ and check_case rtype (loc, target, ppatterns) ctx =
                   make_nctx nctx (ssink var s) pargs cargs pe
                             ((ak, var)::acc) in
             let nctx, fargs = make_nctx ctx subst pargs cargs SMap.empty [] in
+            let head_lexp_ctor =
+              shift_to_extended_ctx nctx
+                (mkCall (lctor, List.map (fun (_, a) -> (Aerasable, a)) targs)) in
+            let head_lexp_args =
+              List.mapi (fun i (ak, vname) ->
+                  (* This is not pretty :( *)
+                  (ak, mkVar (vname, List.length fargs - i - 1))) fargs in
+            let head_lexp = mkCall (head_lexp_ctor, head_lexp_args) in
+            let nctx = ctx_extend_with_eq nctx head_lexp in
             let rtype' = mkSusp rtype
                                 (S.shift (M.length (ectx_to_lctx nctx)
                                           - M.length (ectx_to_lctx ctx))) in
@@ -946,11 +1064,13 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =
          (* Don't instantiate after the last explicit arg: the rest is done,
           * when needed in infer_and_check (via instantiate_implicit).  *)
          when not (sargs = [] && SMap.is_empty pending)
-      -> let larg = get_implicit_arg
-                     ctx (match sargs with
-                          | [] -> loc
-                          | sarg::_ -> sexp_location sarg)
-                     v arg_type in
+      -> let larg = if Inst.is_typeclass ctx arg_type
+                    then newInstanceMetavar ctx (loc, v) arg_type
+                    else get_implicit_arg
+                           ctx (match sargs with
+                                | [] -> loc
+                                | sarg::_ -> sexp_location sarg)
+                           v arg_type in
         handle_fun_args ((ak, larg) :: largs) sargs pending
                         (L.mkSusp ret_type (S.substitute larg))
     | [], _
@@ -996,7 +1116,7 @@ and lexp_parse_inductive ctors ctx =
                                 (fun (ak, n, t) aa
                                  -> Arrow (ak, n, t, dummy_location, aa))
                                 acc impossible in
-                 let g = generalize nctx altacc in
+                 let g = resolve_instances_and_generalize nctx altacc in
                  let altacc' = g (fun _ne vname t l e
                                   -> Arrow (Aerasable, vname, t, l, e))
                                  altacc in
@@ -1110,9 +1230,9 @@ and lexp_check_decls (ectx : elab_context) (* External context.  *)
   (* FIXME: Generalize when/where possible, so things like `map` can be
      defined without type annotations!  *)
   (* Preserve the new operators added to nctx.  *)
-  let ectx = let (_,   a, b, c) = ectx in
-             let (grm, _, _, _) = nctx in
-             (grm, a, b, c) in
+  let ectx = let (_,   a, b, c, _) = ectx in
+             let (grm, _, _, _, tcctx) = nctx in
+             (grm, a, b, c, tcctx) in
   let (declmap, nctx)
     = List.fold_right
                   (fun ((l, vname), pexp) (map, nctx) ->
@@ -1122,10 +1242,11 @@ and lexp_check_decls (ectx : elab_context) (* External context.  *)
                     | (v', ForwardRef, t)
                       -> let adjusted_t = push_susp t (S.shift (i + 1)) in
                         let e = check pexp adjusted_t nctx in
-                        let (grm, ec, lc, sl) = nctx in
+                        resolve_instances e;
+                        let (grm, ec, lc, sl, tcctx) = nctx in
                         let d = (v', LetDef (i + 1, e), t) in
                         (IMap.add i ((l, Some vname), e, t) map,
-                         (grm, ec, Myers.set_nth i d lc, sl))
+                         (grm, ec, Myers.set_nth i d lc, sl, tcctx))
                     | _ -> Log.internal_error "Defining same slot!")
                   defs (IMap.empty, nctx) in
   let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in
@@ -1161,7 +1282,7 @@ and infer_and_generalize_type (ctx : elab_context) se name =
     | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2)
     | Sort _ | Metavar _ -> type0 (* Abritrary closed constant.  *)
     | _ -> t in
-  let g = generalize nctx (strip_rettype t) in
+  let g = resolve_instances_and_generalize nctx (strip_rettype t) in
   g (fun _ne name t l e
      -> mkArrow (Aerasable, name, t, l, e))
     t
@@ -1169,7 +1290,7 @@ and infer_and_generalize_type (ctx : elab_context) se name =
 and infer_and_generalize_def (ctx : elab_context) se =
   let nctx = ectx_new_scope ctx in
   let (e,t) = infer se nctx in
-  let g = generalize nctx e in
+  let g = resolve_instances_and_generalize nctx e in
   let e' = g (fun ne vname t l e
               -> mkLambda ((if ne then Aimplicit else Aerasable),
                           vname, t, e))
@@ -1181,142 +1302,164 @@ and infer_and_generalize_def (ctx : elab_context) se =
   (e', t')
and lexp_decls_1
-      (sdecls : sexp list)
+      (sdecls : sexp list)                        (* What's already parsed *)
+      (tokens : token list)                       (* Rest of input *)
       (ectx : elab_context)                       (* External ctx.  *)
       (nctx : elab_context)                       (* New context.  *)
       (pending_decls : location SMap.t)           (* Pending type decls. *)
       (pending_defs : (symbol * sexp) list)       (* Pending definitions. *)
-    : (vname * lexp * ltype) list * sexp list * elab_context =
-
-  let rec lexp_decls_1 sdecls ectx nctx pending_decls pending_defs =
-  match sdecls with
-  | [] -> (if not (SMap.is_empty pending_decls) then
-            let (s, loc) = SMap.choose pending_decls in
-              error ~loc ("Variable `" ^ s ^ "` declared but not defined!")
-          else
-            assert (pending_defs == []));
-         [], [], nctx
-
-  | Symbol (_, "") :: sdecls
-    -> lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
-
-  | Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls') :: sdecls
-    -> lexp_decls_1 (List.append sdecls' sdecls)
-                   ectx nctx pending_decls pending_defs
-
-  | Node (Symbol (loc, "_:_"), args) :: sdecls
-    (* FIXME: Move this to a "special form"!  *)
-    -> (match args with
-       | [Symbol (loc, vname); stp]
-         -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in
-           if SMap.mem vname pending_decls then
-             (* Don't burp: take'em all and unify!  *)
-             let pt_idx = senv_lookup vname nctx in
-             (* Take the previous type annotation.  *)
-             let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with
-               | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1))
-               | _ -> Log.internal_error "Var not found at its index!" in
-             (* Unify it with the new one.  *)
-             let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with
-              | (_::_)
-                -> lexp_error loc ltp
-                             ("New type annotation `"
-                              ^ lexp_string ltp ^ "` incompatible with previous `"
-                              ^ lexp_string pt ^ "`")
-              | [] -> () in
-             lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
-           else if List.exists (fun ((_, vname'), _) -> vname = vname')
-                               pending_defs then
-             (error ~loc ("Variable `" ^ vname ^ "` already defined!");
-              lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
-           else lexp_decls_1 sdecls ectx
-                             (ectx_extend nctx (loc, Some vname) ForwardRef ltp)
-                             (SMap.add vname loc pending_decls)
-                             pending_defs
-       | _ -> error ~loc "Invalid type declaration syntax";
-             lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
-
-  | Node (Symbol (l, "_=_") as head, args) :: sdecls
-    (* FIXME: Move this to a "special form"!  *)
-    -> (match args with
-      | [Symbol ((l, vname)); sexp]
-           when SMap.is_empty pending_decls
-        -> assert (pending_defs == []);
-          (* Used to be true before we added define-operator.  *)
-          (* assert (ectx == nctx); *)
-          let (lexp, ltp) = infer_and_generalize_def nctx sexp in
-          let var = (l, Some vname) in
-          (* Lexp decls are always recursive, so we have to shift by 1 to
-           * account for the extra var (ourselves).  *)
-          [(var, mkSusp lexp (S.shift 1), ltp)], sdecls,
-          ctx_define nctx var lexp ltp
-
-      | [Symbol (l, vname); sexp]
-        -> if SMap.mem vname pending_decls then
-            let decl_loc = SMap.find vname pending_decls in
-            let v = ({file = l.file;
-                      line = l.line;
-                      column = l.column;
-                      docstr = String.concat "\n" [decl_loc.docstr; l.docstr]},
-                     vname) in
-            let pending_decls = SMap.remove vname pending_decls in
-            let pending_defs = ((v, sexp) :: pending_defs) in
-            if SMap.is_empty pending_decls then
-              let nctx = ectx_new_scope nctx in
-              let decls, nctx = lexp_check_decls ectx nctx pending_defs in
-              decls, sdecls, nctx
-            else
-              lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
-
-          else
-            (error ~loc:l ("`" ^ vname ^ "` defined but not declared!");
-             lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
-
-      | [Node (Symbol s, args) as d; body]
-        -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)!  *)
-         lexp_decls_1 ((Node (head,
-                              [Symbol s;
-                               Node (Symbol (sexp_location d, "lambda_->_"),
-                                     [sexp_u_list args; body])]))
-                       :: sdecls)
-                      ectx nctx pending_decls pending_defs
-
-      | _ -> error ~loc:l "Invalid definition syntax";
-            lexp_decls_1 sdecls ectx nctx pending_decls pending_defs)
-
-  | Node (Symbol (l, "define-operator"), args) :: sdecls
-    (* FIXME: Move this to a "special form"!  *)
-    -> lexp_decls_1 sdecls ectx (sdform_define_operator nctx l args None)
-                   pending_decls pending_defs
-
-  | Node (Symbol ((l, _) as v), sargs) :: sdecls
-    -> (* expand macro and get the generated declarations *)
-     let sdecl' = lexp_decls_macro v sargs nctx in
-     lexp_decls_1 (sdecl' :: sdecls) ectx nctx
-                  pending_decls pending_defs
-
-  | sexp :: sdecls
-    -> error ~loc:(sexp_location sexp) "Invalid declaration syntax";
-      lexp_decls_1 sdecls ectx nctx pending_decls pending_defs
+    : (vname * lexp * ltype) list * sexp list * token list * elab_context =
+
+  let rec lexp_decls_1 sdecls tokens nctx pending_decls pending_defs =
+    let sdecl, sdecls, toks =
+      match (sdecls, tokens) with
+      | (s :: sdecls, _) -> Some s, sdecls, tokens
+      | ([], []) -> None, [], []
+      | ([], _) ->
+         let (s, toks) = sexp_parse_all (ectx_get_grammar nctx)
+                           tokens (Some ";") in
+         Some s, [], toks in
+    let recur prepend_sdecls nctx pending_decls pending_defs =
+      lexp_decls_1 (List.append prepend_sdecls sdecls)
+        toks nctx pending_decls pending_defs in
+    match sdecl with
+    | None -> (if not (SMap.is_empty pending_decls) then
+                 let (s, loc) = SMap.choose pending_decls in
+                 error ~loc ("Variable `" ^ s ^ "` declared but not defined!")
+               else
+                 assert (pending_defs == []));
+              [], [], [],  nctx
+
+    | Some (Symbol (_, ""))
+      -> recur [] nctx pending_decls pending_defs
+
+    | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls'))
+      -> recur sdecls' nctx pending_decls pending_defs
+
+    | Some (Node (Symbol (loc, "_:_"), args) as thesexp)
+      (* FIXME: Move this to a "special form"!  *)
+      -> (match args with
+          | [Symbol (loc, vname); stp]
+            -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in
+               if SMap.mem vname pending_decls then
+                 (* Don't burp: take'em all and unify!  *)
+                 let pt_idx = senv_lookup vname nctx in
+                 (* Take the previous type annotation.  *)
+                 let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with
+                   | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1))
+                   | _ -> Log.internal_error "Var not found at its index!" in
+                 (* Unify it with the new one.  *)
+                 let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with
+                   | (_::_)
+                     -> lexp_error loc ltp
+                          ("New type annotation `"
+                           ^ lexp_string ltp ^ "` incompatible with previous `"
+                           ^ lexp_string pt ^ "`")
+                   | [] -> () in
+                 recur [] nctx pending_decls pending_defs
+               else if List.exists (fun ((_, vname'), _) -> vname = vname')
+                         pending_defs then
+                 (error ~loc ("Variable `" ^ vname ^ "` already defined!");
+                  recur [] nctx pending_decls pending_defs)
+               else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp)
+                      (SMap.add vname loc pending_decls)
+                      pending_defs
+          | _ -> error ~loc ("Invalid type declaration syntax : `" ^
+                               (sexp_string thesexp) ^ "`");
+                 recur [] nctx pending_decls pending_defs)
+
+    | Some (Node (Symbol (l, "_=_") as head, args) as thesexp)
+      (* FIXME: Move this to a "special form"!  *)
+      -> (match args with
+          | [Symbol ((l, vname)); sexp]
+               when SMap.is_empty pending_decls
+            -> assert (pending_defs == []);
+               (* Used to be true before we added define-operator.  *)
+               (* assert (ectx == nctx); *)
+               let (lexp, ltp) = infer_and_generalize_def nctx sexp in
+               let var = (l, Some vname) in
+               (* Lexp decls are always recursive, so we have to shift by 1 to
+                * account for the extra var (ourselves).  *)
+               [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks,
+               ctx_define nctx var lexp ltp
+
+          | [Symbol (l, vname); sexp]
+            -> if SMap.mem vname pending_decls then
+                 let decl_loc = SMap.find vname pending_decls in
+                 let v = ({file = l.file;
+                           line = l.line;
+                           column = l.column;
+                           docstr = String.concat "\n" [decl_loc.docstr;
+                                                        l.docstr]},
+                          vname) in
+                 let pending_decls = SMap.remove vname pending_decls in
+                 let pending_defs = ((v, sexp) :: pending_defs) in
+                 if SMap.is_empty pending_decls then
+                   let nctx = ectx_new_scope nctx in
+                   let decls, nctx = lexp_check_decls ectx nctx pending_defs in
+                   decls, sdecls, toks, nctx
+                 else
+                   recur [] nctx pending_decls pending_defs
+
+               else
+                 (error ~loc:l ("`" ^ vname ^ "` defined but not declared!");
+                  recur [] nctx pending_decls pending_defs)
+
+          | [Node (Symbol s, args) as d; body]
+            -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)!  *)
+             recur [Node (head,
+                          [Symbol s;
+                           Node (Symbol (sexp_location d, "lambda_->_"),
+                                 [sexp_u_list args; body])])]
+               nctx pending_decls pending_defs
+
+          | _ -> error ~loc:l ("Invalid definition syntax : `" ^
+                                 (sexp_string thesexp) ^ "`");
+                 recur [] nctx pending_decls pending_defs)
+
+    | Some (Node (Symbol (l, "define-operator"), args))
+      (* FIXME: Move this to a "special form"!  *)
+      -> recur [] (sdform_define_operator nctx l args None)
+           pending_decls pending_defs
+
+    | Some (Node (Symbol (l, "typeclass"), args))
+      -> recur [] (sdform_typeclass nctx l args None)
+           pending_decls pending_defs
+
+    | Some (Node (Symbol ((l, _) as v), sargs))
+      -> (* expand macro and get the generated declarations *)
+       let sdecl' = lexp_decls_macro v sargs nctx in
+       recur [sdecl'] nctx pending_decls pending_defs
+
+    | Some sexp
+      -> error ~loc:(sexp_location sexp) "Invalid declaration syntax";
+         recur [] nctx pending_decls pending_defs
in (EV.set_getenv nctx;
-      let res = lexp_decls_1 sdecls ectx nctx pending_decls pending_defs in
+      let res = lexp_decls_1 sdecls tokens nctx
+                  pending_decls pending_defs in
         (Log.stop_on_error (); res))
-and lexp_p_decls (sdecls : sexp list) (ctx : elab_context)
+and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context)
     : ((vname * lexp * ltype) list list * elab_context) =
-  let impl sdecls ctx = match sdecls with
-    | [] -> [], ectx_new_scope ctx
-    | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in
-      let declss, nnctx = lexp_p_decls sdecls nctx in
-      decls :: declss, nnctx in
-  let res = impl sdecls ctx in (Log.stop_on_error (); res)
+  let rec impl sdecls tokens ctx =
+    match (sdecls, tokens) with
+    | ([], []) -> [], ectx_new_scope ctx
+    | _ ->
+       let decls, sdecls, tokens, nctx =
+         lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in
+       Log.stop_on_error ();
+       let declss, nnctx = impl sdecls tokens nctx in
+       decls :: declss, nnctx in
+  impl sdecls tokens ctx
and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list =
+  Eval.set_getenv ctx;
   let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in
     (Log.stop_on_error (); res)
and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp =
+  Eval.set_getenv ctx;
   let e, _ = infer e ctx in (Log.stop_on_error (); e)
(* --------------------------------------------------------------------------
@@ -1641,10 +1784,21 @@ let rec sform_lambda kind ctx loc sargs ot =
               -> (match olt1 with
                  | None -> ()
                  | Some lt1'
-                   -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1')
-                     then lexp_error (lexp_location lt1') lt1'
-                                     ("Type mismatch!  Context expected `"
-                                      ^ lexp_string lt1 ^ "`"));
+                   ->   (match Unif.unify lt1' lt1 (ectx_to_lctx ctx) with
+                         | ((ck, _ctx, t1, t2)::_)
+                           -> lexp_error (lexp_location lt1') lt1'
+                                ("Type mismatch("
+                                 ^ (match ck with | Unif.CKimpossible -> "impossible"
+                                                  | Unif.CKresidual -> "residue"
+                                                  | _ -> failwith "impossible")
+                                 ^ ")!  Context expected:\n    "
+                                 ^ lexp_string lt1 ^ "\nbut parameter has type:\n    "
+                                 ^ lexp_string lt1' ^ "\ncan't unify:\n    "
+                                 ^ lexp_string t1
+                                 ^ "\nwith:\n    "
+                                 ^ lexp_string t2);
+                              assert (not (OL.conv_p (ectx_to_lctx ctx) lt1' lt1))
+                         | [] -> ()));
                 mklam lt1 (Some lt2)
| Arrow (ak2, v, lt1, _, lt2) when kind = Anormal
@@ -1695,7 +1849,7 @@ let rec sform_case ctx loc sargs ot = match sargs with
let sform_letin ctx loc sargs ot = match sargs with
   | [sdecls; sbody]
-    -> let declss, nctx = lexp_p_decls [sdecls] ctx in
+    -> let declss, nctx = lexp_p_decls [sdecls] [] ctx in
       (* FIXME: Use `elaborate`.  *)
       let bdy, ltp = infer sbody (ectx_new_scope nctx) in
       let s = List.fold_left (OL.lexp_defs_subst loc) S.identity declss in
@@ -1772,9 +1926,7 @@ let sform_load usr_elctx loc sargs ot =
   let read_file file_name elctx =
     let pres = prelex_file file_name in
     let sxps = lex default_stt pres in
-    let nods = sexp_parse_all_to_list (ectx_get_grammar elctx)
-                                      sxps (Some ";") in
-    let _, elctx = lexp_p_decls nods elctx
+    let _, elctx = lexp_p_decls [] sxps elctx
     in elctx in
(* read file as elab_context *)
@@ -1810,6 +1962,22 @@ let sform_load usr_elctx loc sargs ot =
(tuple',Lazy)
+(**
+   Draft of a special form "instance" that gets refers to a variable
+   of the requested type in the context.
+ **)
+let sform_instance ctx loc sargs ot =
+  match sargs, ot with
+  | ([se; _], _) -> (* Dummy param to trigger the special form *)
+     let t = infer_type se ctx (loc, None) in
+     let mv = newInstanceMetavar ctx (loc, Some "instance") t in
+     (mv, Inferred t)
+  | ([_], Some t) -> (* Dummy param to trigger the special form *)
+     let mv = newInstanceMetavar ctx (loc, Some "instance") t in
+     (mv, Checked)
+  | _ -> (sexp_error loc "##instance expects a type argument if not checked";
+          sform_dummy_ret ctx loc)
+
 (* Register special forms.  *)
 let register_special_forms () =
   List.iter add_special_form
@@ -1839,6 +2007,7 @@ let register_special_forms () =
               (* FIXME: These should be functions!  *)
               ("decltype",      sform_decltype);
               ("declexpr",      sform_declexpr);
+              ("instance",      sform_instance);
             ]
(*      Default context with builtin types
@@ -1860,9 +2029,7 @@ let default_ectx
     let read_file file_name elctx =
       let pres = prelex_file file_name in
       let sxps = lex default_stt pres in
-      let nods = sexp_parse_all_to_list (ectx_get_grammar elctx)
-                                        sxps (Some ";") in
-      let _, lctx = lexp_p_decls nods elctx
+      let _, lctx = lexp_p_decls [] sxps elctx
       in lctx in
(* Register predef *)
@@ -1922,10 +2089,8 @@ let lexp_expr_str str ctx =
let lexp_decl_str str ctx =
   try let tenv = default_stt in
-      let grm = ectx_get_grammar ctx in
-      let limit = Some ";" in
-      let sdecls = sexp_parse_str str tenv grm limit in
-      lexp_p_decls sdecls ctx
+      let tokens = lex_str str tenv in
+      lexp_p_decls [] tokens ctx
   with Log.Stop_Compilation s -> ([],ctx)
=====================================
src/env.ml
=====================================
@@ -167,6 +167,41 @@ let make_runtime_ctx = M.nil
let get_rte_size (ctx: runtime_env): int = M.length ctx
+let print_myers_list l print_fun start =
+    let n = (M.length l) - 1 in
+    print_string (make_title " ENVIRONMENT ");
+    make_rheader [(None, "INDEX");
+        (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")];
+    print_string (make_sep '-');
+
+    for i = start to n do
+    print_string "    | ";
+        ralign_print_int (n - i) 5;
+        print_string " | ";
+        print_fun (M.nth (n - i) l);
+    done;
+    print_string (make_sep '=')
+
+let print_rte_ctx_n (ctx: runtime_env) start =
+  print_myers_list
+    ctx
+    (fun (n, vref) ->
+      let g = !vref in
+      let _ =
+        match n with
+        | (_, Some m) -> lalign_print_string m 12; print_string "  |  "
+        | _ -> print_string (make_line ' ' 12); print_string "  |  " in
+
+      value_print g; print_string "\n") start
+
+(* Only print user defined variables *)
+let print_rte_ctx ctx =
+  print_rte_ctx_n ctx (!L.builtin_size)
+
+(* Dump the whole context *)
+let dump_rte_ctx ctx =
+  print_rte_ctx_n ctx 0
+
 let get_rte_variable (name: vname) (idx: int)
                      (ctx: runtime_env): value_type =
     try (
@@ -177,7 +212,7 @@ let get_rte_variable (name: vname) (idx: int)
             if n1 = n2 then
                 x
             else (
-            fatal
+            fatal ~print_action:(fun () -> dump_rte_ctx ctx)
                 ("Variable lookup failure. Expected: "" ^
                 n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))
@@ -212,37 +247,3 @@ let nfirst_rte_var n ctx =
             List.rev acc in
     loop 0 []
-let print_myers_list l print_fun start =
-    let n = (M.length l) - 1 in
-    print_string (make_title " ENVIRONMENT ");
-    make_rheader [(None, "INDEX");
-        (None, "VARIABLE NAME"); (Some ('l', 48), "VALUE")];
-    print_string (make_sep '-');
-
-    for i = start to n do
-    print_string "    | ";
-        ralign_print_int (n - i) 5;
-        print_string " | ";
-        print_fun (M.nth (n - i) l);
-    done;
-    print_string (make_sep '=')
-
-let print_rte_ctx_n (ctx: runtime_env) start =
-  print_myers_list
-    ctx
-    (fun (n, vref) ->
-      let g = !vref in
-      let _ =
-        match n with
-        | (_, Some m) -> lalign_print_string m 12; print_string "  |  "
-        | _ -> print_string (make_line ' ' 12); print_string "  |  " in
-
-      value_print g; print_string "\n") start
-
-(* Only print user defined variables *)
-let print_rte_ctx ctx =
-  print_rte_ctx_n ctx (!L.builtin_size)
-
-(* Dump the whole context *)
-let dump_rte_ctx ctx =
-  print_rte_ctx_n ctx 0
=====================================
src/eval.ml
=====================================
@@ -744,6 +744,14 @@ let constructor_p name ectx =
       | _ -> false
   with Senv_Lookup_Fail _ -> false
+let inductive_p name ectx =
+  try let idx = senv_lookup name ectx in
+      match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx))
+              (ectx_to_lctx ectx) with
+      | Inductive _ -> true
+      | _ -> false
+  with Senv_Lookup_Fail _ -> false
+
 let erasable_p name nth ectx =
   let is_erasable ctors = match (smap_find_opt name ctors) with
                             | (Some args) ->
@@ -821,10 +829,43 @@ let ctor_arg_pos name arg ectx =
       | _ -> (-1)
   with Senv_Lookup_Fail _ -> (-1)
+let ind_ctor_arg_pos indname ctorname arg ectx =
+  let rec find_opt xs n = match xs with
+    | [] -> None
+    | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1)
+    | _::xs -> find_opt xs (n + 1) in
+  try let idx = senv_lookup indname ectx in
+    match OL.lexp_whnf (mkVar ((dummy_location, Some indname), idx))
+            (ectx_to_lctx ectx) with
+    | Inductive (_, _, _, ctors) ->
+       (match smap_find_opt ctorname ctors with
+        | (Some args) ->
+           (match (find_opt args 0) with
+            | None -> (-1)
+            | Some n -> n)
+        | _ -> (-1))
+    | _ -> (-1)
+  with Senv_Lookup_Fail _ -> (-1)
+
+let count_ctor_args indname ctorname ectx =
+  try let idx = senv_lookup indname ectx in
+      match OL.lexp_whnf (mkVar ((dummy_location, Some indname), idx))
+              (ectx_to_lctx ectx) with
+      | Inductive (_,_,_,ctors) ->
+         (match smap_find_opt ctorname ctors with
+          | Some args -> List.length args
+          | None -> (-1))
+      | _ -> (-1)
+  with Senv_Lookup_Fail _ -> (-1)
+
 let is_constructor loc depth args_val = match args_val with
   | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx)
   | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments"
+let is_inductive loc depth args_val = match args_val with
+  | [Vstring name; Velabctx ectx] -> o2v_bool (inductive_p name ectx)
+  | _ -> error loc "Elab.isinductive takes a String and an Elab_Context as arguments"
+
 let is_nth_erasable loc depth args_val = match args_val with
   | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx)
   | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments"
@@ -841,6 +882,14 @@ let arg_pos loc depth args_val = match args_val with
   | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx)
   | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments"
+let ind_ctor_arg_pos loc depth args_val = match args_val with
+  | [Vstring ind; Vstring ctor; Vstring field; Velabctx ectx] -> Vint (ind_ctor_arg_pos ind ctor field ectx)
+  | _ -> error loc "Elab.ind-ctor-arg-pos takes three String and an Elab_Context as arguments"
+
+let count_ctor_args loc depth args_val = match args_val with
+  | [Vstring ind; Vstring ctor; Velabctx ectx] -> Vint (count_ctor_args ind ctor ectx)
+  | _ -> error loc "Elab.count-ctor-args takes two String and an Elab_Context as arguments"
+
 let array_append loc depth args_val = match args_val with
   | [v; Varray a] ->
     Varray (Array.append (Array.map (fun v -> v) a) (Array.make 1 v))
@@ -996,10 +1045,13 @@ let register_builtin_functions () =
               ("Elab.debug-doc", debug_doc, 2);
               ("Elab.isbound"  , is_bound, 2);
               ("Elab.isconstructor", is_constructor, 2);
+              ("Elab.isinductive", is_inductive, 2);
               ("Elab.is-nth-erasable", is_nth_erasable, 3);
               ("Elab.is-arg-erasable", is_arg_erasable, 3);
               ("Elab.nth-arg"  , nth_arg, 3);
               ("Elab.arg-pos"  , arg_pos, 3);
+              ("Elab.ind-ctor-arg-pos", ind_ctor_arg_pos, 4);
+              ("Elab.count-ctor-args", count_ctor_args, 3);
               ("Array.append"  , array_append,2);
               ("Array.create"  , array_create,2);
               ("Array.length"  , array_length,1);
=====================================
src/instances.ml
=====================================
@@ -0,0 +1,52 @@
+module Unif = Unification
+module U = Util
+module DB = Debruijn
+module L = Lexp
+module S = Subst
+module OL = Opslexp
+
+(* FIXME Is it possible to have multiple references to the same
+   instance metavar? It would break the following code *)         
+let instance_metavar_table = ref (U.IMap.empty : (DB.elab_context * U.location) U.IMap.t)
+let instance_metavar_lookup (id : L.meta_id) : (DB.elab_context * U.location) option
+  = U.IMap.find_opt id (!instance_metavar_table)
+let add_instance_metavar (id : L.meta_id) (ctx : DB.elab_context) (loc : U.location) : unit
+  = instance_metavar_table := U.IMap.add id (ctx, loc) !instance_metavar_table
+
+let env_is_typeclass (ectx : DB.elab_context) (t : L.ltype) : bool =
+  let (_, _, _, _, tcctx) = ectx in
+  let cl = DB.get_size ectx in
+  List.exists (fun (t', cl') ->
+      let i = cl - cl' in
+      let t' = L.mkSusp t' (S.shift i) in
+      OL.conv_p (DB.ectx_to_lctx ectx) t t'
+    (*(Unif.unify ~checking:(max_int (* FIXME *)) t t' (DB.ectx_to_lctx ectx)) = []*)
+    ) tcctx
+
+
+let get_head (lctx : DB.lexp_context) (t : L.ltype) : L.ltype =
+  match OL.lexp_whnf t lctx with
+  | L.Call (head, _) -> head
+  | head -> head
+
+
+let is_typeclass (ctx : DB.elab_context) (t : L.ltype) =
+  let lctx = DB.ectx_to_lctx ctx in
+  let head = get_head lctx t in
+  env_is_typeclass ctx head
+
+let add_typeclass (ctx : DB.elab_context) (t : L.ltype) : DB.elab_context =
+  let lctx = DB.ectx_to_lctx ctx in
+  let head = get_head lctx t in
+  DB.env_add_typeclass ctx head
+
+type match_res = Impossible | Possible | Match
+
+let check_typeclass_match t1 t2 lctx sl =
+  match Unif.unify ~checking:sl t1 t2 lctx with
+  | [] -> Match
+  | constraints when List.exists (function | (Unif.CKimpossible,_,_,_) -> true
+                                           | _ -> false)
+                       constraints -> Impossible
+  | _ -> Possible
+
=====================================
src/inverse_subst.ml
=====================================
@@ -300,11 +300,12 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with
                         -> let s' = L.fold_left
                                      (fun s (_,ov) -> ssink ov s)
                                      s cargs in
-                          (l, cargs, apply_inv_subst e s'))
+                           let s'' = ssink (l, None) s' in
+                           (l, cargs, apply_inv_subst e s''))
                        cases,
               match default with
               | None -> default
-              | Some (v,e) -> Some (v, apply_inv_subst e (ssink v s)))
+              | Some (v,e) -> Some (v, apply_inv_subst e (ssink (l, None) (ssink v s))))
   | Metavar (id, s', name)
     -> match metavar_lookup id with
       | MVal e -> apply_inv_subst (push_susp e s') s
=====================================
src/lexp.ml
=====================================
@@ -150,7 +150,7 @@ type metavar_info =
   | MVal of lexp            (* Exp to which the var is instantiated.  *)
   | MVar of scope_level     (* Outermost scope in which the var appears.  *)
             * ltype         (* Expected type.  *)
-            (* We'd like to keep the lexp_content in which the type is to be
+            (* We'd like to keep the lexp_context in which the type is to be
              * understood, but lexp_context is not yet defined here,
              * so we just keep the length of the lexp_context.  *)
             * ctx_length
@@ -274,7 +274,7 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000
 let rec mkSusp e s =
   if S.identity_p s then e else
     (* We apply the substitution eagerly to some terms.
-     * There's no deep technical rason for that:
+     * There's no deep technical reason for that:
      * it just seemed like a good idea to do it eagerly when it's easy.  *)
     match e with
     | Imm _ -> e
@@ -313,7 +313,7 @@ let rec sunshift n =
 let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))
(* The quick test below seemed to indicate that about 50% of the "sink"s
- * are applied on top of another "sink" and hence cound be combined into
+ * are applied on top of another "sink" and hence could be combined into
  * a single "Lift^n" constructor.  Doesn't seem high enough to justify
  * the complexity of adding a `Lift` to `subst`.
  *)
@@ -409,11 +409,11 @@ let rec push_susp e s =            (* Push a suspension one level down.  *)
                         -> let s' = L.fold_left
                                      (fun s (_,ov) -> ssink ov s)
                                      s cargs in
-                          (l, cargs, mkSusp e s'))
+                          (l, cargs, mkSusp e (ssink (l, None) s')))
                        cases,
               match default with
               | None -> default
-              | Some (v,e) -> Some (v, mkSusp e (ssink v s)))
+              | Some (v,e) -> Some (v, mkSusp e (ssink (l, None) (ssink v s))))
   (* Susp should never appear around Var/Susp/Metavar because mkSusp
    * pushes the subst into them eagerly.  IOW if there's a Susp(Var..)
    * or Susp(Metavar..) it's because some chunk of code should use mkSusp
@@ -475,11 +475,12 @@ let clean e =
                           -> let s' = L.fold_left
                                        (fun s (_,ov) -> ssink ov s)
                                        s cargs in
-                            (l, cargs, clean s' e))
+                             let s'' = ssink (l, None) s' in
+                             (l, cargs, clean s'' e))
                          cases,
                 match default with
                 | None -> default
-                | Some (v,e) -> Some (v, clean (ssink v s) e))
+                | Some (v,e) -> Some (v, clean (ssink (l, None) (ssink v s)) e))
     | Susp (e, s') -> clean (scompose s' s) e
     | Var _ -> if S.identity_p s then e
               else clean S.identity (mkSusp e s)
@@ -805,7 +806,7 @@ and lexp_str ctx (exp : lexp) : string =
         | Metavar (idx, subst, (loc, name))
           (* print metavar result if any *)
           -> (match metavar_lookup idx with
-             | MVal e -> lexp_str ctx e
+             | MVal e -> lexp_str ctx (push_susp e subst)
              | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))
| Let (_, decls, body)   ->
@@ -992,8 +993,18 @@ let rec eq e1 e2 =
         && (match (def1, def2) with
           | (Some (_, e1), Some (_, e2)) -> eq e1 e2
           | _ -> def1 = def2)
-    | (Metavar (i1, s1, _), Metavar (i2, s2, _))
-      -> i1 = i2 && subst_eq s1 s2
+    | (Metavar (i1, s1, _), Metavar (i2, s2, _)) when i1 == i2
+      -> subst_eq s1 s2
+    | (Metavar (i1, s1, _), _) when
+           (match metavar_lookup i1 with MVal _ -> true | _ -> false)
+      -> (match metavar_lookup i1 with
+          | MVal l ->  eq (push_susp l s1) e2
+          | _ -> Log.internal_error "impossible")
+    | (_, Metavar (i2, s2, _)) when
+           (match metavar_lookup i2 with MVal _ -> true | _ -> false)
+      -> (match metavar_lookup i2 with
+          | MVal l ->  eq e1 (push_susp l s2)
+          | _ -> Log.internal_error "impossible")
     | _ -> false
and subst_eq s1 s2 =
=====================================
src/log.ml
=====================================
@@ -133,11 +133,13 @@ let print_entry entry =
 let log_entry (entry : log_entry) =
   if (entry.level <= typer_log_config.level)
   then (
-    log_push entry;
-    if (typer_log_config.print_at_log)
+    if (typer_log_config.print_at_log ||
+          entry.level >= Debug)
     then
       (print_entry entry;
        flush stdout)
+    else
+      log_push entry
   )
let count_msgs (lvlp : log_level -> bool) =
=====================================
src/myers.ml
=====================================
@@ -54,11 +54,21 @@ let car l =
   | Mnil -> raise Not_found
   | Mcons (x, _, _, _) -> x
+let safe_car l =
+  match l with
+  | Mnil -> None
+  | Mcons (x, _, _, _) -> Some x
+
 let cdr l =
   match l with
   | Mnil -> Mnil
   | Mcons (_, l, _, _) -> l
+let safe_cdr l =
+  match l with
+  | Mnil -> None
+  | Mcons (_, l, _, _) -> Some l
+
 let case l n c =
   match l with
   | Mnil -> n ()
@@ -136,3 +146,6 @@ let rec fold_right f l i = match l with
 let map f l = fold_right (fun x l' -> cons (f x) l') l nil
let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l
+
+let iter (f : 'a -> unit) (l : 'a myers) : unit
+  = fold_left (fun _ x -> f x; ()) () l
=====================================
src/opslexp.ml
=====================================
@@ -38,6 +38,22 @@ module S = Subst
 (* module L = List *)
 module DB = Debruijn
+type set_plexp = (lexp * lexp) list
+type sort_compose_result
+  = SortResult of ltype
+  | SortInvalid
+  | SortK1NotType
+  | SortK2NotType
+type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t
+              (* Metavars that appear in non-erasable positions.  *)
+              * unit IMap.t
+
+module LMap
+  (* Memoization table.  FIXME: Ideally the keys should be "weak", but
+   * I haven't found any such functionality in OCaml's libs.  *)
+  = Hashtbl.Make
+      (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end)
+
 let error_tc = Log.log_error ~section:"TC"
 let warning_tc = Log.log_warning ~section:"TC"
@@ -132,7 +148,7 @@ let lexp_close lctx e =
  * but only on *types*.  If you must use it on code, be sure to use its
  * return value as little as possible since WHNF will inherently introduce
  * call-by-name behavior.  *)
-let lexp_whnf e (ctx : DB.lexp_context) : lexp =
+let rec lexp_whnf e (ctx : DB.lexp_context) : lexp =
   let rec lexp_whnf e (ctx : DB.lexp_context) : lexp =
   match e with
   | Var v -> (match lookup_value ctx v with
@@ -156,21 +172,28 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp =
       | _ -> e)                 (* Keep `e`, assuming it's more readable!  *)
   | Case (l, e, rt, branches, default) ->
      let e' = lexp_whnf e ctx in
+     let get_refl e =
+       let etype = get_type ctx e in (* FIXME we should not need get_type here *)
+       let elevel = match lexp_whnf (get_type ctx etype) ctx with
+         | Sort (_, Stype l) -> l
+         | _ -> Log.internal_error "" in
+       mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in
      let reduce name aargs =
        try
          let (_, _, branch) = SMap.find name branches in
-         let (subst, _)
+         let subst
            = List.fold_left
-               (fun (s,d) (_, arg) ->
-                 (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s,
-                  d + 1))
-               (S.identity, 0)
+               (fun (s) (_, arg) -> S.cons (lexp_whnf arg ctx) s)
+               S.identity
                aargs in
+         (* Substitute case Eq variable by the proof (Eq.refl l t e') *)
+         let subst = S.cons (get_refl e') subst in
          lexp_whnf (push_susp branch subst) ctx
        with Not_found
             -> match default
               with | Some (v,default)
-                     -> lexp_whnf (push_susp default (S.substitute e')) ctx
+                     -> let subst = S.cons (get_refl e') (S.substitute e') in
+                        lexp_whnf (push_susp default subst) ctx
                    | _ -> Log.log_error ~section:"WHNF" ~loc:l
                                      ("Unhandled constructor " ^
                                         name ^ "in case expression");
@@ -198,9 +221,8 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp =
(** A very naive implementation of sets of pairs of lexps.  *)
-type set_plexp = (lexp * lexp) list
-let set_empty : set_plexp = []
-let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool
+and set_empty : set_plexp = []
+and set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool
   = assert (e1 == Lexp.hc e1);
     assert (e2 == Lexp.hc e2);
     try let _ = List.find (fun (e1', e2')
@@ -208,14 +230,14 @@ let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool
                           s
         in true
      with Not_found -> false
-let set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp
+and set_add (s : set_plexp) (e1 : lexp) (e2 : lexp) : set_plexp
   = (* assert (not (set_member_p s e1 e2)); *)
     ((e1, e2) :: s)
-let set_shift_n (s : set_plexp) (n : U.db_offset)
+and set_shift_n (s : set_plexp) (n : U.db_offset)
   = List.map (let s = S.shift n in
               fun (e1, e2) -> (Lexp.push_susp e1 s, Lexp.push_susp e2 s))
              s
-let set_shift s : set_plexp = set_shift_n s 1
+and set_shift s : set_plexp = set_shift_n s 1
(********* Testing if two types are "convertible" aka "equivalent"  *********)
@@ -225,7 +247,7 @@ let set_shift s : set_plexp = set_shift_n s 1
  * `c` is the maximum "constant" level that occurs in `e`
  * and `m` maps variable indices to the maxmimum depth at which they were
  * found.  *)
-let level_canon e =
+and level_canon e =
   let add_var_depth v d ((c,m) as acc) =
     let o = try IMap.find v m with Not_found -> -1 in
     if o < d then (c, IMap.add v d m) else acc in
@@ -244,18 +266,21 @@ let level_canon e =
     | _ -> (max_int, m)
   in canon e 0 (0,IMap.empty)
-let level_leq (c1, m1) (c2, m2) =
+and level_leq (c1, m1) (c2, m2) =
   c1 <= c2
   && c1 != max_int
   && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false)
                  m1
(* Returns true if e₁ and e₂ are equal (upto alpha/beta/...).  *)
-let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
+and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
   let e1' = lexp_whnf e1 ctx in
   let e2' = lexp_whnf e2 ctx in
+  Log.log_debug ("conv_p : e1' = `" ^ (lexp_string e1')
+                 ^ "`; e2' = `" ^ (lexp_string e2') ^ "`");
   e1' == e2' ||
     let changed = not (e1 == e1' && e2 == e2') in
+    Log.log_debug ("changed : " ^ string_of_bool changed);
     if changed && set_member_p vs e1' e2' then true else
     let vs' = if changed then set_add vs e1' e2' else vs in
     let conv_p = conv_p' ctx vs' in
@@ -319,19 +344,119 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
           | _,_ -> false in
         l1 == l2 && conv_args ctx vs' args1 args2
     | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2
-    (* I'm not sure to understand how to compare two Metavar  *
-     * Should I do a `lookup`? Or is it that simple:          *)
-    (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*)
-    (* FIXME: Various missing cases, such as Case.  *)
-    | (_, _) -> false
-
-let conv_p (ctx : DB.lexp_context) e1 e2
+    | (Case (_, te1, r1, cases1, def1), Case (_, te2, r2, cases2, def2))
+      -> Log.log_debug ("conv_p of case : e1' = `" ^ (lexp_string e1')
+                        ^ "`; e2' = `" ^ (lexp_string e2') ^ "`");
+         eq e1' e2' ||
+         (Log.log_debug "subexpr"; conv_p te1 te2) &&
+           (Log.log_debug "return"; conv_p r1 r2) && (
+           Log.log_debug "branches";
+           (* Compare the branches *)
+           (* 1. Get the inductive for the field types *)
+           let call_split e = match e with
+             | Call (f, args) -> (f, args)
+             | _ -> (e,[]) in
+           (* We can arbitrarily use te1 since te1 and te2 are convertible *)
+           let etype = lexp_whnf (get_type ctx te1) ctx in
+           let it, aargs = call_split etype in
+           (* 2. Build the substitution for the inductive arguments *)
+           let fargs, ctors =
+             (match lexp_whnf it ctx with
+              | Inductive (_, _, fargs, constructors)
+                -> fargs, constructors
+              | _ -> Log.log_fatal ("Case of non-inductive in conv_p")) in
+           let fargs_subst = List.fold_left2 (fun s _farg (_, aarg) -> S.cons aarg s)
+                               S.identity fargs aargs in
+           (* 3. Compare the branches *)
+           (* The map module doesn't have a function to compare two
+              maps with the key (which is needed to get the field
+              types from the inductive. Instead, we work with the
+              lists of associations. *)
+           (try
+              List.for_all2 (fun (l1, (_, fields1, e1)) (l2, (_, fields2, e2)) ->
+                  l1 = l2 &&
+                    let fieldtypes = SMap.find l1 ctors in
+                    let rec mkctx ctx args s i vdefs1 vdefs2 fieldtypes =
+                      match vdefs1, vdefs2, fieldtypes with
+                      | [], [], [] -> Some (ctx, List.rev args, s)
+                      | (ak1, vdef1)::vdefs1, (ak2, vdef2)::vdefs2,
+                        (ak', vdef', ftype)::fieldtypes
+                        -> if ak1 = ak2 && ak2 = ak' then
+                             (* FIXME Should we compare the variable names ? *)
+                             mkctx
+                               (DB.lexp_ctx_cons ctx vdef1 Variable (mkSusp ftype s))
+                               ((ak1, (mkVar (vdef1, i)))::args)
+                               (ssink vdef1 s)
+                               (i - 1)
+                               vdefs1 vdefs2 fieldtypes
+                           else None
+                      | _,_,_ -> None in
+                    match mkctx ctx [] fargs_subst (List.length fields1)
+                            fields1 fields2 fieldtypes with
+                    | None -> false
+                    | Some (nctx, args, _subst) ->
+                       (* TODO build head lexp the eq type *)
+                       let offset = (List.length fields1) in
+                       let subst = S.shift offset in
+                       Log.log_debug "hlxp time";
+                       let tlxp = mkSusp te1 subst in
+                       Log.log_debug ("tlxp : `" ^ (lexp_string tlxp) ^ "`");
+                       let tltp = mkSusp etype subst in
+                       Log.log_debug ("etype : `" ^ (lexp_string etype) ^ "`");
+                       Log.log_debug ("subst : `" ^ (subst_string subst) ^ "`");
+                       Log.log_debug ("tltp : `" ^ (lexp_string tltp) ^ "`");
+                       let tlev = (match lexp_whnf (get_type nctx tltp) nctx with
+                                   | Sort (_, Stype l) -> l
+                                   | _ -> Log.log_error "HMMM"; DB.level0) in
+                       let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)), aargs)) subst in
+                       Log.log_debug ("ctor : `" ^ (lexp_string ctor) ^ "`");
+                       let hlxp = mkCall (ctor, args) in
+                       Log.log_debug ("hlxp : `" ^ (lexp_string hlxp) ^ "`");
+                       let eqty = mkCall (DB.type_eq,
+                                          [(Aerasable, tlev);     (* Typelevel *)
+                                           (Aerasable, tltp);     (* Inductive type *)
+                                           (Anormal, tlxp);       (* Target lexp *)
+                                           (Anormal, hlxp)])  in  (* Lexp of the branch head *)
+                       let nctx = DB.lexp_ctx_cons nctx (DB.dloc, None) Variable eqty in
+                       conv_p' nctx (set_shift_n vs' (offset + 1)) e1 e2
+                ) (SMap.bindings cases1) (SMap.bindings cases2)
+            with
+            | Invalid_argument _ -> false (* If the lists have different length *)
+           )
+           && (match (def1, def2) with
+               | (Some (v1, e1), Some (v2, e2)) ->
+                  (* FIXME should we compare the variable names ? *)
+                  Log.log_debug "default";
+                  let nctx = DB.lctx_extend ctx v1 Variable etype in
+                  let subst = S.shift 1 in
+                  let tlxp = mkSusp e1 subst in
+                  let tltp = mkSusp etype subst in
+                  let tlev = (match lexp_whnf (get_type nctx tltp) nctx with
+                              | Sort (_, Stype l) -> l
+                              | _ -> Log.log_error "HMMM"; DB.level0) in
+                  let hlxp = mkVar ((DB.dloc, None), 0) in
+                  let eqty = mkCall (DB.type_eq,
+                                     [(Aerasable, tlev);     (* Typelevel *)
+                                      (Aerasable, tltp);     (* Inductive type *)
+                                      (Anormal, tlxp);       (* Target lexp *)
+                                      (Anormal, hlxp)])  in  (* Lexp of the branch head *)
+                  let nctx = DB.lexp_ctx_cons nctx (DB.dloc, None) Variable eqty in
+                  conv_p' nctx (set_shift_n vs' 2) e1 e2
+               | None, None -> true
+               | _, _ -> false))
+         (* I'm not sure to understand how to compare two Metavar  *
+          * Should I do a `lookup`? Or is it that simple:          *)
+         (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*)
+         (* FIXME: Various missing cases, such as Case.  *)
+         | (_, _) -> false
+
+and conv_p (ctx : DB.lexp_context) e1 e2
   = if e1 == e2 then true
     else conv_p' ctx set_empty e1 e2
(********* Testing if a lexp is properly typed  *********)
-let rec mkSLlub ctx e1 e2 =
+and mkSLlub ctx e1 e2 =
   match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with
   | (SortLevel SLz, _) -> e2
   | (_, SortLevel SLz) -> e1
@@ -344,13 +469,7 @@ let rec mkSLlub ctx e1 e2 =
       else if level_leq ce2 ce1 then e1
       else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *)
-type sort_compose_result
-  = SortResult of ltype
-  | SortInvalid
-  | SortK1NotType
-  | SortK2NotType
-
-let sort_compose ctx1 ctx2 l ak k1 k2 =
+and sort_compose ctx1 ctx2 l ak k1 k2 =
   (* BEWARE!  Technically `k2` can refer to `v`, but this should only happen
    * if `v` is a TypeLevel.  *)
   match (lexp_whnf k1 ctx1, lexp_whnf k2 ctx2) with
@@ -388,11 +507,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 =
   | (Sort (_, _), _) -> SortK2NotType
   | (_, _) -> SortK1NotType
-let dbset_push ak erased =
+and dbset_push ak erased =
   let nerased = DB.set_sink 1 erased in
   if ak = P.Aerasable then DB.set_set 0 nerased else nerased
-let nerased_let defs erased =
+and nerased_let defs erased =
   (* Let bindings are not erasable, with the important exception of
    * let-bindings of the form `x = y` where `y` is an erasable var.
    * This exception is designed so that macros like `case` which need to
@@ -418,7 +537,7 @@ let nerased_let defs erased =
       erased es
(* "check ctx e" should return τ when "Δ ⊢ e : τ"  *)
-let rec check'' erased ctx e =
+and check'' erased ctx e =
   let check = check'' in
   let assert_type ctx e t t' =
     if conv_p ctx t t' then ()
@@ -610,24 +729,38 @@ let rec check'' erased ctx e =
           SMap.iter
             (fun name (l, vdefs, branch)
              -> let fieldtypes = SMap.find name constructors in
-               let rec mkctx erased ctx s vdefs fieldtypes =
+               let rec mkctx erased ctx s hlxp vdefs fieldtypes =
                  match vdefs, fieldtypes with
-                 | [], [] -> (erased, ctx)
+                 | [], [] -> (erased, ctx, hlxp)
                  (* FIXME: If ak is Aerasable, make sure the var only
                   * appears in type annotations.  *)
                  | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes
                    -> mkctx (dbset_push ak erased)
                            (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s))
-                           (S.cons (mkVar (vdef, 0))
-                                   (S.mkShift s 1))
+                           (ssink vdef s)
+                           (mkCall (mkSusp hlxp (S.shift 1), [(ak, mkVar (vdef, 0))]))
                            vdefs fieldtypes
                  | _,_ -> (error_tc ~loc:l
                                       "Wrong number of args to constructor!";
-                          (erased, ctx)) in
-               let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in
+                          (erased, ctx, hlxp)) in
+               let hctor = mkCall (mkCons (it, (l, name)), aargs) in
+               let (nerased, nctx, hlxp) =
+                 mkctx erased ctx s hctor vdefs fieldtypes in
+               (* Create Eq type between target and lexp matching the
+                  branch head, and add it (erasable) to the context *)
+               let subst = S.shift (List.length vdefs) in
+               let tlxp = mkSusp e subst in
+               let tltp = mkSusp etype subst in
+               let eqty = mkCall (DB.type_eq,
+                           [(Aerasable, DB.type0); (* Typelevel *)  (* FIXME The real typelevel *)
+                            (Aerasable, tltp);     (* Inductive type *)
+                            (Anormal, tlxp);       (* Target lexp *)
+                            (Anormal, hlxp)])  in  (* Lexp of the branch head *)
+               let nerased = dbset_push Aerasable nerased in (* The eq proof is erasable *)
+               let nctx = DB.lexp_ctx_cons nctx (l, None) Variable eqty in
                assert_type nctx branch
                            (check nerased nctx branch)
-                           (mkSusp ret (S.shift (List.length fieldtypes))))
+                           (mkSusp ret (S.shift ((List.length fieldtypes) + 1))))
             branches;
           let diff = SMap.cardinal constructors - SMap.cardinal branches in
           (match default with
@@ -635,8 +768,21 @@ let rec check'' erased ctx e =
              -> if diff <= 0 then
                  warning_tc ~loc:l "Redundant default clause";
                let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in
-               assert_type nctx d (check (DB.set_sink 1 erased) nctx d)
-                           (mkSusp ret (S.shift 1))
+               let nerased = DB.set_sink 1 erased in
+               let subst = S.shift 1 in
+               (* FIXME DRY this code *)
+               let tlxp = mkSusp e subst in
+               let tltp = mkSusp etype subst in
+               let hlxp = mkVar ((l, None), 0) in
+               let eqty = mkCall (DB.type_eq,
+                           [(Aerasable, DB.type0); (* Typelevel *) (* FIXME The real typelevel *)
+                            (Aerasable, tltp);     (* Inductive type *)
+                            (Anormal, tlxp);       (* Target lexp *)
+                            (Anormal, hlxp)])  in  (* Lexp of the branch head *)
+               let nerased = dbset_push Aerasable nerased in (* The eq proof is erasable *)
+               let nctx = DB.lexp_ctx_cons nctx (l, None) Variable eqty in
+               assert_type nctx d (check nerased nctx d)
+                           (mkSusp ret (S.shift 2))
            | None
              -> if diff > 0 then
                  error_tc ~loc:l ("Non-exhaustive match: "
@@ -682,24 +828,21 @@ let rec check'' erased ctx e =
                   check erased ctx e
        | MVar (_, t, _) -> push_susp t s)
-let check' ctx e =
+and check' ctx e =
   let res = check'' DB.set_empty ctx e in
     (Log.stop_on_error (); res)
-let check = check'
+and check ctx e = check' ctx e
(** Compute the set of free (meta)variables.  **)
-let rec list_union l1 l2 = match l1 with
+and list_union l1 l2 = match l1 with
   | [] -> l2
   | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))
-type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t
-              (* Metavars that appear in non-erasable positions.  *)
-              * unit IMap.t
-let mv_set_empty : mv_set = (IMap.empty, IMap.empty)
-let mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes)
-let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set
+and mv_set_empty : mv_set = (IMap.empty, IMap.empty)
+and mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes)
+and mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set
   = (IMap.merge (fun _m oss1 oss2
                 -> match (oss1, oss2) with
                   | (None, _) -> oss2
@@ -715,23 +858,19 @@ let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set
                       Some ss1)
                 ms1 ms2,
      IMap.merge (fun _m _o1 _o2 -> Some ()) nes1 nes2)
-let mv_set_erase (ms, _nes) = (ms, IMap.empty)
+and mv_set_erase (ms, _nes) = (ms, IMap.empty)
-module LMap
-  (* Memoization table.  FIXME: Ideally the keys should be "weak", but
-   * I haven't found any such functionality in OCaml's libs.  *)
-  = Hashtbl.Make
-      (struct type t = lexp let hash = Hashtbl.hash let equal = (==) end)
-let fv_memo = LMap.create 1000
+and fv_memo = LMap.create 1000
+and fv_flush () = LMap.clear fv_memo
-let fv_empty = (DB.set_empty, mv_set_empty)
-let fv_union (fv1, mv1) (fv2, mv2)
+and fv_empty = (DB.set_empty, mv_set_empty)
+and fv_union (fv1, mv1) (fv2, mv2)
   = (DB.set_union fv1 fv2, mv_set_union mv1 mv2)
-let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs)
-let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs)
-let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)
+and fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs)
+and fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs)
+and fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)
-let rec fv (e : lexp) : (DB.set * mv_set) =
+and fv (e : lexp) : (DB.set * mv_set) =
   let fv' e = match e with
     | Imm _ -> fv_empty
     | SortLevel SLz -> fv_empty
@@ -784,9 +923,9 @@ let rec fv (e : lexp) : (DB.set * mv_set) =
       -> let s = fv_union (fv e) (fv_erase (fv t)) in
         let s = match def with
           | None -> s
-          | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in
+          | Some (_, e) -> fv_union s (fv_hoist 2 (fv e)) in
         SMap.fold (fun _ (_, fields, e) s
-                   -> fv_union s (fv_hoist (List.length fields) (fv e)))
+                   -> fv_union s (fv_hoist (List.length fields + 1) (fv e)))
                   cases s
     | Metavar (id, s, name)
       -> (match metavar_lookup id with
@@ -806,7 +945,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) =
 (** Finding the type of a expression.  **)
 (* This should never signal any warning/error.  *)
-let rec get_type ctx e =
+and get_type ctx e =
   match e with
   | Imm (Float (_, _)) -> DB.type_float
   | Imm (Integer (_, _)) -> DB.type_int
@@ -933,7 +1072,7 @@ let rec erase_type (lxp: L.lexp): E.elexp =
| L.Case(l, target, _, cases, default) ->
             E.Case(l, (erase_type target), (clean_map cases),
-                                         (clean_maybe default))
+                                         (clean_default default))
| L.Susp(l, s)                -> erase_type (L.push_susp l s)
@@ -962,10 +1101,12 @@ and filter_arg_list lst =
 and clean_decls decls =
    List.map (fun (v, lxp, _) -> (v, (erase_type lxp))) decls
-and clean_maybe lxp =
-    match lxp with
-        | Some (v, lxp) -> Some (v, erase_type lxp)
-        | None -> None
+and clean_default lxp =
+  match lxp with
+  | Some (v, lxp) ->
+     Some (v,
+           erase_type (L.push_susp lxp (S.substitute DB.type0)))
+  | None -> None
and clean_map cases =
     let clean_arg_list lst =
@@ -979,7 +1120,8 @@ and clean_map cases =
         clean_arg_list lst [] in
SMap.map (fun (l, args, expr)
-               -> (l, (clean_arg_list args), (erase_type expr)))
+              -> (l, (clean_arg_list args),
+                  erase_type (L.push_susp expr (S.substitute DB.type0))))
               cases
(** Turning a set of declarations into an object.  **)
=====================================
src/sexp.ml
=====================================
@@ -160,13 +160,18 @@ let rec sexp_parse (g : grammar) (rest : sexp list)
                  mk_node ((l,"")::op) largs rargs true),
               rest)
          | (Some ll, None) when ll > level
-           (* A closer without matching opener.
-            * It might simply be a postfix symbol that binds very tightly.
-            * We currently signal an error because it's more common for
-            * it to be a closer with missing opener.  *)
-           -> sexp_error l ("Lonely postfix/closer ""^name^""");
-             sexp_parse rest' level op largs
-                        [mk_node [(l,name);(l,"")] [] rargs true]
+           (* A closer without matching opener or a postfix symbol
+              that binds very tightly. Previously, we signaled an
+              error (assuming the former), but it prevented the use
+              tightly binding postfix operators.
+
+              For example, it signaled spurious errors when parsing
+              expressions with a tightly binding postfix # operator
+              that implemented record construction by taking an
+              inductive as argument and returning the inductive's only
+              constructor. *)
+           -> sexp_parse rest' level op largs
+                [mk_node [(l,name);(l,"")] [] rargs true]
          | (Some ll, Some rl) when ll > level
            (* A new infix which binds more tightly, i.e. does not close
             * the current `op' but takes its `rargs' instead.  *)
=====================================
src/unification.ml
=====================================
@@ -46,6 +46,7 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype)
 type constraint_kind =
   | CKimpossible                (* Unification is simply impossible.  *)
   | CKresidual                  (* We failed to find a unifier.  *)
+  | CKassoc                     (* Couldn't associate because of checking mode *)
 (* FIXME: Each constraint should additionally come with a description of how
    it relates to its "top-level" or some other info which might let us
    fix the problem (e.g. by introducing coercions).  *)
@@ -54,8 +55,9 @@ type constraints  = (constraint_kind * DB.lexp_context * lexp * lexp) list
 type return_type = constraints
(** Alias for VMap.add*)
-let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst
-  = U.IMap.add id (MVal lxp) subst
+let associate (id: meta_id) (lxp: lexp) : unit
+  = metavar_table := U.IMap.add id (MVal lxp) (!metavar_table);
+    OL.fv_flush ()
let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
   | MVal _ -> Log.internal_error
@@ -174,13 +176,15 @@ let rec s_offset s = match s with
The metavar unifier is the end rule, it can't call unify with its parameter (changing their order)
 *)
-let rec unify (e1: lexp) (e2: lexp)
+let rec unify ?checking
+              (e1: lexp) (e2: lexp)
               (ctx : DB.lexp_context)
         : return_type =
-  unify' e1 e2 ctx OL.set_empty
+  unify' e1 e2 ctx OL.set_empty checking
and unify' (e1: lexp) (e2: lexp)
            (ctx : DB.lexp_context) (vs : OL.set_plexp)
+           (c : scope_level option) (* checking mode scope level *)
     : return_type =
   if e1 == e2 then [] else
   let e1' = OL.lexp_whnf e1 ctx in
@@ -190,20 +194,26 @@ and unify' (e1: lexp) (e2: lexp)
   if changed && OL.set_member_p vs e1' e2' then [] else
   let vs' = if changed then OL.set_add vs e1' e2' else vs in
   match (e1', e2') with
-    | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _)
-       | (Var _, Var _))
+    | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _))
       -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)]
-    | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l
-    | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r
-    | (l, (Call _ as r))    -> unify_call     r l ctx vs'
-    (* | (l, (Case _ as r))    -> unify_case     r l subst *)
-    | (Arrow _ as l, r)     -> unify_arrow    l r ctx vs'
-    | (Lambda _ as l, r)    -> unify_lambda   l r ctx vs'
-    | (Call _ as l, r)      -> unify_call     l r ctx vs'
-    (* | (Case _ as l, r)      -> unify_case     l r subst *)
-    (* | (Inductive _ as l, r) -> unify_induct   l r subst *)
-    | (Sort _ as l, r)      -> unify_sort     l r ctx vs'
-    | (SortLevel _ as l, r) -> unify_sortlvl  l r ctx vs'
+    | (l, (Metavar (idx, s, _) as r)) -> unify_metavar c ctx idx s r l
+    | ((Metavar (idx, s, _) as l), r) -> unify_metavar c ctx idx s l r
+    | (l, (Call _ as r))      -> unify_call     c r l ctx vs'
+    | ((Call _ as l), r)      -> unify_call     c l r ctx vs'
+    | (l, (Var _ as r))       -> unify_var        r l ctx vs'
+    | ((Var _ as l), r)       -> unify_var        l r ctx vs'
+    | (l, (Arrow _ as r))     -> unify_arrow    c r l ctx vs'
+    | ((Arrow _ as l), r)     -> unify_arrow    c l r ctx vs'
+    | (l, (Lambda _ as r))    -> unify_lambda   c r l ctx vs'
+    | ((Lambda _ as l), r)    -> unify_lambda   c l r ctx vs'
+    (* | (l, (Case _ as r))      -> unify_case     r l subst *)
+    (* | ((Case _ as l), r)      -> unify_case     l r subst *)
+    (* | (l, (Inductive _ as r)) -> unify_induct   r l subst *)
+    (* | ((Inductive _ as l), r) -> unify_induct   l r subst *)
+    | (l, (Sort _ as r))      -> unify_sort     c r l ctx vs'
+    | ((Sort _ as l), r)      -> unify_sort     c l r ctx vs'
+    | (l, (SortLevel _ as r)) -> unify_sortlvl  c r l ctx vs'
+    | ((SortLevel _ as l), r) -> unify_sortlvl  c l r ctx vs'
     | (Inductive (_loc1, label1, args1, consts1),
        Inductive (_loc2, label2, args2, consts2))
       -> (* print_string ("Unifying inductives "
@@ -211,7 +221,7 @@ and unify' (e1: lexp) (e2: lexp)
          *               ^ " and "
          *               ^ snd label2
          *               ^ "\n"); *)
-        unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2
+        unify_inductive c ctx vs' args1 args2 consts1 consts2 e1 e2
     | _ -> (if OL.conv_p ctx e1' e2' then []
            else ((* print_string "Unification failure on default\n"; *)
              [(CKresidual, ctx, e1, e2)]))
@@ -222,87 +232,77 @@ and unify' (e1: lexp) (e2: lexp)
  - (Arrow, Arrow) -> if var_kind = var_kind
                      then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp))
                      else None
- - (Arrow, Var) -> Constraint
  - (_, _) -> None
 *)
-and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs
+and unify_arrow (checking : scope_level option) (arrow: lexp) (lxp: lexp) ctx vs
   : return_type =
   match (arrow, lxp) with
   | (Arrow (var_kind1, v1, ltype1, _, lexp1),
      Arrow (var_kind2, _, ltype2, _, lexp2))
     -> if var_kind1 = var_kind2
-      then (unify' ltype1 ltype2  ctx vs)
+      then (unify' ltype1 ltype2  ctx vs checking)
            @(unify' lexp1 (srename v1 lexp2)
                (DB.lexp_ctx_cons ctx v1 Variable ltype1)
-               (OL.set_shift vs))
-      else [(CKimpossible, ctx, arrow, lxp)]
-  | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)]
-  | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)])
-  | (Arrow _, _) -> unify' lxp arrow ctx vs
+               (OL.set_shift vs) checking)
+       else [(CKimpossible, ctx, arrow, lxp)]
   | (_, _) -> [(CKimpossible, ctx, arrow, lxp)]
(** Unify a Lambda and a lexp if possible
- - Lamda     , Lambda             -> if var_kind = var_kind
+ - Lambda    , Lambda             -> if var_kind = var_kind
                                      then UNIFY ltype & lxp else ERROR
- - Lambda    , Var                -> CONSTRAINT
- - Lambda    , Call               -> Constraint
- - Lambda    , Let                -> Constraint
- - Lambda    , lexp               -> unify lexp lambda subst
+ - Lambda    , _                  -> Impossible
 *)
-and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
+and unify_lambda (checking : scope_level option) (lambda: lexp) (lxp: lexp) ctx vs : return_type =
   match (lambda, lxp) with
   | (Lambda (var_kind1, v1, ltype1, lexp1),
      Lambda (var_kind2, _, ltype2, lexp2))
     -> if var_kind1 = var_kind2
-      then (unify' ltype1 ltype2  ctx vs)
+      then (unify' ltype1 ltype2  ctx vs checking)
            @(unify' lexp1 lexp2
                (DB.lexp_ctx_cons ctx v1 Variable ltype1)
-               (OL.set_shift vs))
+               (OL.set_shift vs) checking)
       else [(CKimpossible, ctx, lambda, lxp)]
-  | ((Lambda _, Var _)
-     | (Lambda _, Let _)
-     | (Lambda _, Call _))  -> [(CKresidual, ctx, lambda, lxp)]
-  | (Lambda _, Arrow _)
-    | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)]
-  | (Lambda _, _)       -> unify' lxp lambda ctx vs
-  | (_, _)              -> [(CKimpossible, ctx, lambda, lxp)]
+  | (_, _)             -> [(CKimpossible, ctx, lambda, lxp)]
(** Unify a Metavar and a lexp if possible
- - lexp      , {metavar <-> none} -> UNIFY
- - lexp      , {metavar <-> lexp} -> UNFIFY lexp subst[metavar]
- - metavar   , metavar            -> if Metavar = Metavar then OK else ERROR
- - metavar   , lexp               -> OK
+ - metavar   , metavar            -> if Metavar = Metavar then intersect
+ - metavar   , metavar            -> inverse subst (both sides)
+ - metavar   , lexp               -> inverse subst
 *)
-and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
+and unify_metavar (checking : scope_level option) ctx idx s1 (lxp1: lexp) (lxp2: lexp)
     : return_type =
   let unif idx s lxp =
-    let t = match metavar_lookup idx with
+    let t, sl = match metavar_lookup idx with
       | MVal _ -> Log.internal_error
                    "`lexp_whnf` returned an instantiated metavar!!"
-      | MVar (_, t, _) -> push_susp t s in
+      | MVar (_, t, sl) -> push_susp t s, sl in
     match Inverse_subst.apply_inv_subst lxp s with
     | exception Inverse_subst.Not_invertible
-      -> log_info ?loc:None ("Unification of metavar failed:\n  "
-                            ^ "?[" ^ subst_string s ^ "]"
-                            ^ "\nAgainst:\n    "
-                            ^ lexp_string lxp ^ "\n");
+      -> log_info ~loc:(lexp_location lxp)
+           ("Unification of metavar failed:\n  "
+            ^ "?[" ^ subst_string s ^ "]"
+            ^ "\nAgainst:\n    "
+            ^ lexp_string lxp ^ "\n");
         [(CKresidual, ctx, lxp1, lxp2)]
     | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)]
     | lxp'
-      -> metavar_table := associate idx lxp' (!metavar_table);
-        match unify t (OL.get_type ctx lxp) ctx with
-        | [] as r -> r
-        (* FIXME: Let's ignore the error for now.  *)
-        | _
-          -> log_info ?loc:None
-               ("Unification of metavar type failed:\n  "
-                ^ lexp_string t ^ " != "
-                ^ lexp_string (OL.get_type ctx lxp)
-                ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n");
-            [(CKresidual, ctx, lxp1, lxp2)] in
+      -> match checking with
+         | Some l when l >= sl -> [(CKassoc, ctx, lxp1, lxp2)]
+         | _ -> (
+            associate idx lxp';
+           match unify t (OL.get_type ctx lxp) ctx with
+           | [] as r -> r
+           (* FIXME: Let's ignore the error for now.  *)
+           | _
+             -> log_info ?loc:None
+                  ("Unification of metavar type failed:\n  "
+                   ^ lexp_string t ^ " != "
+                   ^ lexp_string (OL.get_type ctx lxp)
+                   ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n");
+                [(CKresidual, ctx, lxp1, lxp2)]) in
   match lxp2 with
   | Metavar (idx2, s2, name)
-    -> if idx = idx2 then
+    -> if idx = idx2 && checking == None then
         match common_subset ctx s1 s2 with
         | S.Identity 0 -> []     (* Optimization!  *)
         (* ¡ s1 != s2 !
@@ -353,7 +353,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
                    *                 ^ "\n  =\n    "
                    *                 ^ subst_string (scompose s s2)
                    *                 ^ "\n"); *)
-                  metavar_table := associate idx lexp (!metavar_table);
+                  associate idx lexp;
                   assert (OL.conv_p ctx lxp1 lxp2);
                   []
       else
@@ -364,18 +364,28 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
          | _ -> unif idx2 s2 lxp1)
   | _ -> unif idx s1 lxp2
+(** Unify a Var (var) and a lexp (lxp)
+ - Var      , Var                -> IF same var THEN ok ELSE constraint
+ - Var      , lexp               -> Constraint
+*)
+and unify_var (var: lexp) (lxp: lexp) ctx vs
+    : return_type =
+  match (var, lxp) with
+  | (Var _, Var _) when OL.conv_p ctx var lxp -> []
+  | (_, _)      -> [(CKresidual, ctx, var, lxp)]
+
 (** Unify a Call (call) and a lexp (lxp)
  - Call      , Call               -> UNIFY
  - Call      , lexp               -> CONSTRAINT
 *)
-and unify_call (call: lexp) (lxp: lexp) ctx vs
+and unify_call (checking : scope_level option) (call: lexp) (lxp: lexp) ctx vs
     : return_type =
   match (call, lxp) with
   | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2))
        when OL.conv_p ctx lxp_left lxp_right
     -> List.fold_left (fun op ((ak1, e1), (ak2, e2))
                       -> if ak1 == ak2 then
-                          (unify' e1 e2 ctx vs)@op
+                          (unify' e1 e2 ctx vs checking)@op
                         else [(CKimpossible, ctx, call, lxp)])
                      []
                      (List.combine lxp_list1 lxp_list2)
@@ -438,31 +448,29 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs
  - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR
  - SortLevel, _         -> ERROR
 *)
-and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type =
+and unify_sortlvl (checking : scope_level option) (sortlvl: lexp) (lxp: lexp) ctx vs : return_type =
   match sortlvl, lxp with
   | (SortLevel s, SortLevel s2) -> (match s, s2 with
       | SLz, SLz -> []
-      | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs
+      | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs checking
       | SLlub (l11, l12), SLlub (l21, l22)
         -> (* FIXME: This SLlub representation needs to be
            * more "canonicalized" otherwise it's too restrictive!  *)
-         (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs)
+         (unify' l11 l21 ctx vs checking)@(unify' l12 l22 ctx vs checking)
       | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)])
   | _, _ -> [(CKresidual, ctx, sortlvl, lxp)]
(** Unify a Sort and a lexp
  - Sort, Sort -> if Sort ~= Sort then OK else ERROR
- - Sort, Var  -> Constraint
  - Sort, lexp -> ERROR
 *)
-and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type =
+and unify_sort (checking : scope_level option) (sort_: lexp) (lxp: lexp) ctx vs : return_type =
   match sort_, lxp with
   | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with
-      | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs
+      | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs checking
       | StypeOmega, StypeOmega -> []
       | StypeLevel, StypeLevel -> []
       | _, _ -> [(CKimpossible, ctx, sort_, lxp)])
-  | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)]
   | _, _          -> [(CKimpossible, ctx, sort_, lxp)]
(************************ Helper function ************************************)
@@ -513,7 +521,7 @@ and is_same arglist arglist2 =
  *        | None -> test e subst)
  *     ) None lst *)
-and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 =
+and unify_inductive (checking : scope_level option) ctx vs args1 args2 consts1 consts2 e1 e2 =
   let unif_formals ctx vs args1 args2
     = if not (List.length args1 == List.length args2) then
         (ctx, vs, [(CKimpossible, ctx, e1, e2)])
@@ -522,7 +530,7 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 =
                         -> (DB.lexp_ctx_cons ctx v1 Variable t1,
                            OL.set_shift vs,
                            if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)]
-                           else (unify' t1 t2 ctx vs) @ residue))
+                           else (unify' t1 t2 ctx vs checking) @ residue))
           (ctx, vs, [])
           (List.combine args1 args2) in
   let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in
=====================================
tests/unify_test.ml
=====================================
@@ -199,6 +199,7 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res =
       else (Unification, res, lxp1, lxp2)
   | (CKresidual, _, _, _)::_      -> (Constraint, res, lxp1, lxp2)
   | (CKimpossible, _, _, _)::_    -> (Nothing, res, lxp1, lxp2)
+  | _ -> failwith "impossible"
let check (lxp1: lexp) (lxp2: lexp) (res: result): bool =
   let r, _, _, _ = test_input lxp1 lxp2
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2f5e0deb9f057a3a1232e4fc282692f9f...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/2f5e0deb9f057a3a1232e4fc282692f9f...
You're receiving this email because of your account on gitlab.com.





    

2024

2023

2022

2021

2020

2019

2018

2017

2016

[Typer] [Git][monnier/typer][ja-barszcz] 30 commits: * btl/builtins.typer (Eq_comm): Update FIXME