[Git][monnier/typer][there-can-be-only-one-inductive] Remove arguments to inductive types. - Typer

9 Déc 2020


      Simon Génier pushed to branch there-can-be-only-one-inductive at Stefan / Typer
Commits:
71f83760 by Simon Génier at 2020-12-09T18:26:34-05:00
Remove arguments to inductive types.
There used to be two ways to express indexed types: one could either add
parameters directly on the type or put the type behind a lambda. These two are
semantically equivalent, so we unify them into the latter in this patch.
- - - - -
10 changed files:
- btl/builtins.typer
- btl/pervasive.typer
- src/elab.ml
- src/eval.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/opslexp.ml
- src/pexp.ml
- src/unification.ml
- + tests/opslexp_test.ml
Changes:
=====================================
btl/builtins.typer
=====================================
@@ -191,14 +191,14 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp;
 %%       List
 %% -----------------------------------------------------
-%% FIXME: "List : ?" should be sufficient but triggers
-List : Type_ ?ℓ -> Type_ ?ℓ;
-%% List a = typecons List (nil) (cons a (List a));
-%% nil = lambda a ≡> datacons (List a) nil;
-%% cons = lambda a ≡> datacons (List a) cons;
-List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a));
-nil = datacons List nil;
-cons = datacons List cons;
+List : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ;
+List = lambda ℓ ≡> lambda α -> typecons List (nil) (cons α (List (ℓ := ℓ) α));
+
+nil : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> List (ℓ := ℓ) α;
+nil = lambda ℓ ≡> lambda α ≡> datacons (List (ℓ := ℓ) α) nil;
+
+cons : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> α -> List (ℓ := ℓ) α -> List (ℓ := ℓ) α;
+cons = lambda ℓ ≡> lambda α ≡> datacons (List (ℓ := ℓ) α) cons;
%%%% Macro-related definitions
=====================================
btl/pervasive.typer
=====================================
@@ -32,659 +32,664 @@
%%%% `Option` type
-Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a);
-some = datacons Option some;
-none = datacons Option none;
+Option : Type_ ?ℓ -> Type_ ?ℓ;
+Option = lambda α -> typecons Option (none) (some α);
-%%%% List functions
-
-List_length : List ?a -> Int;   % Recursive defs aren't generalized :-(
-List_length xs = case xs
-  | nil => 0
-  | cons hd tl =>
-      (1 + (List_length tl));
-
-%% ML's typical `head` function is not total, so can't be defined
-%% as-is in Typer.  There are several workarounds:
-%% - Provide a default value : `a -> List a -> a`;
-%% - Disallow problem case   : `(l : List a) -> (l != nil) -> a`;
-%% - Return an Option/Error
-List_head1 xs = case xs
-  | nil => none
-  | cons hd tl => some hd;
-
-List_head x = lambda xs -> case xs
-  | cons x _ => x
-  | nil => x;
-
-List_tail xs = case xs
-  | nil => nil
-  | cons hd tl => tl;
-
-List_map : (?a -> ?b) -> List ?a -> List ?b;
-List_map f = lambda xs -> case xs
-  | nil => nil
-  | cons x xs => cons (f x) (List_map f xs);
-
-List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a;
-List_foldr f = lambda xs -> lambda i -> case xs
-  | nil => i
-  | cons x xs => f x (List_foldr f xs i);
-
-List_find : (?a -> Bool) -> List ?a -> Option ?a;
-List_find f = lambda xs -> case xs
-  | nil => none
-  | cons x xs => case f x | true => some x | false => List_find f xs;
-
-List_nth : Int -> List ?a -> ?a -> ?a;
-List_nth = lambda n -> lambda xs -> lambda d -> case xs
-  | nil => d
-  | cons x xs
-    => case Int_<= n 0
-       | true => x
-       | false => List_nth (n - 1) xs d;
-
-%%%% A more flexible `lambda`
-
-%% An `Sexp` which we use to represents an *error*.
-Sexp_error = Sexp_symbol "<error>";
-
-%% Sexp_to_list : Sexp -> List Sexp -> List Sexp;
-Sexp_to_list s = lambda exceptions ->
-  let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"!
-  Sexp_dispatch
-      s
-      (node := lambda head -> lambda tail
-        -> case List_find (Sexp_eq head) exceptions
-        | some _ => singleton ()
-        | none => cons head tail)
-      (symbol := lambda s
-        -> case String_eq "" s
-        | true => nil
-        | false => singleton ())
-      singleton singleton singleton singleton;
-
-multiarg_lambda =
-  %% This macro lets `lambda_->_` (and siblings) accept multiple arguments.
-  %% TODO: We could additionally turn
-  %%     lambda (x :: t) y -> e
-  %% into
-  %%     lambda (x : t) => lambda y -> e`
-  %% thus providing an alternate syntax for lambdas which don't use
-  %% => and ≡>.
-  let exceptions = List_map Sexp_symbol
-                            (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in
-  lambda name ->
-  let sym = (Sexp_symbol name);
-      mklambda = lambda arg -> lambda body ->
-        Sexp_node sym (cons arg (cons body nil)) in
-  lambda (margs : List Sexp)
-  -> IO_return
-         case margs
-         | nil => Sexp_error
-         | cons fargs margstail
-           => case margstail
-              | nil => Sexp_error
-              | cons body bodytail
-                => case bodytail
-                   | cons _ _ => Sexp_error
-                   | nil => List_foldr mklambda
-                                       (Sexp_to_list fargs exceptions)
-                                       body;
-
-lambda_->_ = macro (multiarg_lambda "##lambda_->_");
-lambda_=>_ = macro (multiarg_lambda "##lambda_=>_");
-lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_");
-
-%%%% More list functions
-
-List_reverse : List ?a -> List ?a -> List ?a;
-List_reverse l t = case l
-  | nil => t
-  | cons hd tl => List_reverse tl (cons hd t);
-
-List_concat l t = List_reverse (List_reverse l nil) t;
-
-List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a;
-List_foldl f i xs = case xs
-  | nil => i
-  | cons x xs => List_foldl f (f i x) xs;
-
-List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b;
-List_mapi f xs = let
-  helper : (a -> Int -> b) -> Int -> List a -> List b;
-  helper f i xs = case xs
-    | nil => nil
-    | cons x xs => cons (f x i) (helper f (i + 1) xs);
-in helper f 0 xs;
-
-List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c;
-List_map2 f xs ys = case xs
-  | nil => nil
-  | cons x xs => case ys
-    | nil => nil % error
-    | cons y ys => cons (f x y) (List_map2 f xs ys);
-
-%% Fold 2 List as long as both List are non-empty
-List_fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> List ?b -> List ?c -> ?a;
-List_fold2 f o xs ys = case xs
-  | cons x xs => ( case ys
-    | cons y ys => List_fold2 f (f o x y) xs ys
-    | nil => o ) % may be an error
-  | nil => o; % may or may not be an error
-
-%% Is argument List empty?
-List_empty : List ?a -> Bool;
-List_empty xs = Int_eq (List_length xs) 0;
-
-%%% Good 'ol combinators
-
-I x = x;
-
-%% Use explicit erasable annotations since with an annotation like
-%%     K : ?a -> ?b -> ?a;
-%% Typer generalizes to
-%%     K : (a : Type) ≡> (b : Type) ≡> a -> b -> a;
-%% Which is less general.
-%% FIXME: Change the generalizer to insert the `(b : Type) ≡>`
-%% more lazily (i.e. after the `a` argument).
-K : ?a -> (b : Type) ≡> b -> ?a;
-K x y = x;
-
-%%%% Quasi-Quote macro
-
-%%   f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"])
-%%
-%%   f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil))
-%%
-%%     =>       x
-
-%% Takes an Sexp `x` as argument and return an Sexp which represents code
-%% which will construct an Sexp equivalent to `x` at run-time.
-%% This is basically *cross stage persistence* for Sexp.
-quote1 : Sexp -> Sexp;
-quote1 x = let
-               qlist : List Sexp -> Sexp;
-               qlist xs = case xs
-                 | nil => Sexp_symbol "nil"
-                 | cons x xs => Sexp_node (Sexp_symbol "cons")
-                                          (cons (quote1 x)
-                                                (cons (qlist xs) nil));
-               make_app str sexp =
-                 Sexp_node (Sexp_symbol str) (cons sexp nil);
-
-               node op y = case (Sexp_eq op (Sexp_symbol "uquote"))
-                 | true  => List_head Sexp_error y
-                 | false => Sexp_node (Sexp_symbol "##Sexp.node")
-                                      (cons (quote1 op)
-                                            (cons (qlist y) nil));
-               symbol s = make_app "##Sexp.symbol" (Sexp_string s);
-               string s = make_app "##Sexp.string" (Sexp_string s);
-               integer i = make_app "##Sexp.integer"
-                                    (make_app "##Int->Integer" (Sexp_integer i));
-               float f = make_app "##Sexp.float" (Sexp_float f);
-               block sxp =
-                  %% FIXME ##Sexp.block takes a string (and prelexes
-                  %% it) but we have a sexp, what should we do?
-                  Sexp_symbol "<error FIXME block quoting>";
-           in Sexp_dispatch x node symbol string integer float block;
-
-%% quote definition
-quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x)));
-
-%%%% The `type` declaration macro
-
-%% Build a declaration:
-%%     var-name = value-expr;
-make-decl : Sexp -> Sexp -> Sexp;
-make-decl var-name value-expr =
-  Sexp_node (Sexp_symbol "_=_")
-            (cons var-name
-                  (cons value-expr nil));
-
-chain-decl : Sexp -> Sexp -> Sexp;
-chain-decl a b =
-  Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil));
-
-chain-decl3 : Sexp -> Sexp -> Sexp -> Sexp;
-chain-decl3 a b c =
-  Sexp_node (Sexp_symbol "_;_") (cons a (cons b (cons c nil)));
-
-%% Build datacons:
-%%     ctor-name = datacons type-name ctor-name;
-make-cons : Sexp -> Sexp -> Sexp;
-make-cons ctor-name type-name =
-  make-decl ctor-name
-            (Sexp_node (Sexp_symbol "datacons")
-                       (cons type-name
-                             (cons ctor-name nil)));
-
-%% Build type annotation:
-%%     var-name : type-expr;
-make-ann : Sexp -> Sexp -> Sexp;
-make-ann var-name type-expr =
-  Sexp_node (Sexp_symbol "_:_")
-            (cons var-name
-                  (cons type-expr nil));
-
-type-impl = lambda (x : List Sexp) ->
-  %% `x` follow the mask ->
-  %%                  (_|_ Nat zero (succ Nat))
-  %%       Type name  --^    ^------^ constructors
-
-  %% Return a list contained inside a node sexp.
-  let knil = K nil;
-      kerr = K Sexp_error;
-
-      get-list : Sexp -> List Sexp;
-      get-list node = Sexp_dispatch node
-                                     (lambda op lst -> lst) % Nodes
-                                     knil      % Symbol
-                                     knil      % String
-                                     knil      % Integer
-                                     knil      % Float
-                                     knil;     % List of Sexp
-
-      %% Get a name (symbol) from a sexp
-      %%   - (name t) -> name
-      %%   - name -> name
-      get-name : Sexp -> Sexp;
-      get-name sxp =
-        Sexp_dispatch sxp
-                       (lambda op _ -> get-name op) % Nodes
-                       (lambda _    -> sxp) % Symbol
-                       kerr  % String
-                       kerr  % Integer
-                       kerr  % Float
-                       kerr; % List of Sexp
-
-      get-args : Sexp -> List Sexp;
-      get-args sxp =
-        Sexp_dispatch sxp
-                       (lambda _ args -> args)            % Nodes
-                       (lambda _    -> (nil : List Sexp)) % Symbol
-                       (lambda _ -> (nil : List Sexp))    % String
-                       (lambda _ -> (nil : List Sexp))    % Integer
-                       (lambda _ -> (nil : List Sexp))    % Float
-                       (lambda _ -> (nil : List Sexp));   % List of Sexp
-
-      get-type : Sexp -> Sexp;
-      get-type sxp =
-        Sexp_dispatch sxp
-                      (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_"))
-                        | true  => List_nth 1 ss Sexp_error
-                        | false => sxp)
-                      (lambda _ -> sxp)
-                      (lambda _ -> Sexp_error)
-                      (lambda _ -> Sexp_error)
-                      (lambda _ -> Sexp_error)
-                      (lambda _ -> Sexp_error);
-
-      get-head = List_head Sexp_error;
-
-      %% Get expression.
-      expr = get-head x;
-
-      %% Expression is  Sexp_node (Sexp_symbol "|") (list)
-      %% we only care about the list bit
-      lst = get-list expr;
-
-      %% head is (Sexp_node type-name (arg list))
-      name = get-head lst;
-      ctor = List_tail lst;
-
-      type-name = get-name name;
-
-      %% Create the inductive type definition.
-      inductive = Sexp_node (Sexp_symbol "typecons")
-                            (cons name ctor);
-
-      %% Declare the inductive type as a function
-      %% Useful for recursive type
-      type-decl = quote ((uquote (get-name name)) : (uquote (
-        (List_foldl (lambda args arg ->
-          Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil)))
-            %% FIXME: Don't hardcode TypeLevel.z!
-            (Sexp_symbol "Type") (List_reverse (get-args name) nil))
-      )));
-
-      decl  = make-decl type-name inductive;
-
-      %% Add constructors.
-      ctors = let for-each : List Sexp -> Sexp -> Sexp;
-                  for-each ctr acc = case ctr
-                    | cons hd tl =>
-                        let acc2 = chain-decl (make-cons (get-name hd)
-                                                         type-name)
-                                              acc
-                        in for-each tl acc2
-                    | nil => acc
-              in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
-
-                            %% return decls
-  in IO_return (chain-decl3 type-decl % type as a function declaration
-                            decl      % inductive type declaration
-                            ctors);   % constructor declarations
-
-type_ = macro type-impl;
-
-%%%% An inductive type to wrap Sexp
-
-type Sexp_wrapper
-  | node Sexp (List Sexp)
-  | symbol String
-  | string String
-  | integer Integer
-  | float Float
-  | block Sexp;
-
-Sexp_wrap s = Sexp_dispatch s node symbol string integer float block;
-
-%%%% Tuples
-
-%% Sample tuple: a module holding Bool and its constructors.
-BoolMod = (##datacons
-             %% We need the `?` metavars to be lexically outside of the
-             %% `typecons` expression, otherwise they end up generalized, so
-             %% we end up with a type constructor like
-             %%
-             %%     typecons _ (cons (τ₁ : Type) (t : τ₁)
-             %%                      (τ₂ : Type) (true : τ₂)
-             %%                      (τ₃ : Type) (false : τ₃))
-             %%
-             %% And it's actually even worse because it tries to generalize
-             %% over the level of those `Type`s, so we end up with an invalid
-             %% inductive type.
-             ((lambda t1 t2 t3
-               -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3)))
-                  ? ? ?)
-             cons)
-              (_ := Bool) (_ := true) (_ := false);
-
-Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
-pair = datacons Pair pair;
-
-__.__ =
-  let mksel o f =
-        let constructor = Sexp_node (Sexp_symbol "##datacons")
-                                    (cons (Sexp_symbol "?")
-                                          (cons (Sexp_symbol "cons")
-                                                nil));
-            pattern = Sexp_node constructor
-                                (cons (Sexp_node (Sexp_symbol "_:=_")
-                                                 (cons f (cons (Sexp_symbol "v")
-                                                               nil)))
-                                      nil);
-            branch = Sexp_node (Sexp_symbol "_=>_")
-                               (cons pattern (cons (Sexp_symbol "v") nil));
-        in Sexp_node (Sexp_symbol "case_")
-                     (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);
-
-%% Triplet (tuple with 3 values)
-type Triplet (a : Type) (b : Type) (c : Type)
-  | triplet (x : a) (y : b) (z : c);
-
-%%%% List with tuple
-
-%% Merge two List to a List of Pair
-%% Both List must be of same length
-List_merge : List ?a -> List ?b -> List (Pair ?a ?b);
-List_merge xs ys = case xs
-  | cons x xs => ( case ys
-    | cons y ys => cons (pair x y) (List_merge xs ys)
-    | nil => nil ) % error
-  | nil => nil;
-
-%% `Unmerge` a List of Pair
-%% The two functions name said it all
-List_map-fst xs = let
-  mf p = case p | pair x _ => x;
-in List_map mf xs;
-
-List_map-snd xs = let
-  mf p = case p | pair _ y => y;
-in List_map mf xs;
-
-%%%% Logic
-
-%% `False` should be one of the many empty types.
-%% Other popular choices are False = ∀a.a and True = ∃a.a.
-False = Void;
-True = Unit;
-
-Not prop = prop -> False;
-
-%% Like Bool, except that it additionally carries the meaning of its value.
-%% 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_ ?ℓ))
-                     (true (p ::: prop)) (false (p ::: Not prop));
-
-%% Testing generalization in inductive type constructors.
-LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient!
-type LList (a : Type) (n : Int)
-  | vnil (p ::: Eq n 0)
-  | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound!
-
-%%%% If
-
-define-operator "if" () 2;
-define-operator "then" 2 1;
-define-operator "else" 1 66;
-
-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 uquote e1
-                                | true => uquote e2
-                                | false => uquote e3)));
-
-%%%% More boolean
-
-%% FIXME: Type annotations should not be needed below.
-not : Bool -> Bool;
-%% FIXME: We use braces here to delay parsing, otherwise the if/then/else
-%% part of the grammar declared above is not yet taken into account.
-not x = { if x then false else true };
-
-or : Bool -> Bool -> Bool;
-or x y = { if x then x else y };
-
-and : Bool -> Bool -> Bool;
-and x y = { if x then y else x };
-
-xor : Bool -> Bool -> Bool;
-xor x y = { if x then (not y) else y };
-
-%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic,
-%% which we don't support in `load` yet.
-fold : Bool -> (a : Type) ≡> a -> a -> a;
-fold x t e = { if x then t else e};
-
-%%%% Test
-test1 : ?;
-test2 : Option Int;
-test3 : Option Int;
-test1 = test2;
-%% In earlier versions of Typer, we could use `?` in declarations
-%% to mean "fill this for me by unifying with later type information",
-%% but this is incompatible with the use of generalization to introduce
-%% implicit arguments.
-%%     test4 : Option ?;
-test2 = none;
-test4 : Option Int;
-test4 = test1 : Option ?;
-test3 = test4;
-
-%%%% Rewrite of some builtins to use `Option`
-
-%%
-%% If `Elab_nth-arg'` returns "_" it means:
-%%   A- The constructor isn't defined, or
-%%   B- The constructor has no n'th argument
-%%
-%% So in those case this function returns `none`
-%%
-Elab_nth-arg a b c = let
-  r = Elab_nth-arg' a b c;
-in case (String_eq r "_")
-     | true  => (none)
-     | false => (some r);
-
-%%
-%% If `Elab_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_arg-pos a b c = let
-  r = Elab_arg-pos' a b c;
-in case (Int_eq r (-1))
-     | true  => (none)
-     | false => (some r);
-
-%%%%
-%%%% Common library
-%%%%
-
-%%
-%% `<-` operator used in macro `do` and for tuple assignment
-%%
+none : (α : Type_ ?ℓ) ≡> Option (ℓ := ?ℓ) α;
+none = lambda ℓ ≡> lambda α ≡> datacons (Option α) none;
-define-operator "<-" 80 96;
+some : (α : Type_ ?ℓ) ≡> α -> Option (ℓ := ?ℓ) α;
+some = lambda ℓ ≡> lambda α ≡> datacons (Option α) some;
-%%
-%% `List` is the type and `list` is the module
-%%
-list = load "btl/list.typer";
-
-%%
-%% Macro `do` for easier series of IO operation
-%%
-%% e.g.:
-%%     do { IO_return true; };
-%%
-do = let lib = load "btl/do.typer" in lib.do;
-
-%%
-%% Module containing various macros for tuple
-%% Used by `case_`
-%%
-tuple-lib = load "btl/tuple.typer";
-
-%%
-%% Get the nth element of a tuple
-%%
-%% e.g.:
-%%     tuple-nth tup 0;
-%%
-tuple-nth = tuple-lib.tuple-nth;
-
-%%
-%% Affectation of tuple
-%%
-%% e.g.:
-%%     (x,y,z) <- tup;
-%%
-_<-_ = tuple-lib.assign-tuple;
-
-%%
-%% Instantiate a tuple from expressions
-%%
-%% e.g.:
-%%     tup = (x,y,z);
-%%
-_,_ = tuple-lib.make-tuple;
-
-Tuple = tuple-lib.tuple-type;
-
-%%
-%% Macro `case` for a some more complex pattern matching
-%%
-case_ = let lib = load "btl/case.typer" in lib.case-macro;
-
-%%
-%% plain-let
-%% Not recursive and not sequential
-%%
-%% e.g.:
-%%     plain-let x = 1; in x;
-%%
-
-define-operator "plain-let" () 3;
-
-%%
-%% Already defined:
-%%     define-operator "in" 3 67;
-%%
-
-plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro;
-
-%%
-%% `case` at function level
-%%
-%% e.g.:
-%%     my-fun (x : Bool)
-%%       | true  => false
-%%       | false => true;
-%%
-_|_ = let lib = load "btl/polyfun.typer" in lib._|_;
-
-%%
-%% case_as_return_, case_return_
-%% A `case` for dependent elimination
-%%
-
-define-operator "as" 42 42;
-define-operator "return" 42 42;
-depelim = load "btl/depelim.typer";
-case_as_return_ = depelim.case_as_return_;
-case_return_ = depelim.case_return_;
-
-%%%% Unit tests function for doing file
-
-%% It's hard to do a primitive which execute test file
-%% because of circular dependency...
+%%%% List functions
-%%
-%% A macro using `load` for unit testing purpose
-%%
-%% Takes a file name (String) as argument
-%% Returns variable named `exec-test` from the loaded file
-%%
-%% `exec-test` should be a command doing unit tests
-%% for other purpose than that just use `load` directly!
-%%
-Test_file = macro (lambda args -> let
-
-  %% return an empty command on error
-  ret = Sexp_node
-    (Sexp_symbol "IO_return")
-    (cons (Sexp_symbol "unit") nil);
-
-%% Expecting a String and nothing else
-in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error)
-    (lambda _ _ -> ret)
-    (lambda _ -> ret)
-    %% `load` is a special form and takes a Sexp rather than a real `String`
-    (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test))
-    (lambda _ -> ret)
-    (lambda _ -> ret)
-    (lambda _ -> ret))
-);
-
-%%% pervasive.typer ends here.
+% Recursive defs aren't generalized :-(
+List_length : (ℓ : TypeLevel) ≡> (α : Type_ ℓ) ≡> List (ℓ := ℓ) α -> Int;
+List_length = lambda ℓ ≡> lambda α ≡> lambda xs -> case xs
+  | nil => 0
+  | cons hd tl => 1 + List_length (ℓ := ℓ) (α := α) tl;
+
+% %% ML's typical `head` function is not total, so can't be defined
+% %% as-is in Typer.  There are several workarounds:
+% %% - Provide a default value : `a -> List a -> a`;
+% %% - Disallow problem case   : `(l : List a) -> (l != nil) -> a`;
+% %% - Return an Option/Error
+% List_head1 xs = case xs
+%   | nil => none
+%   | cons hd tl => some hd;
+
+% List_head x = lambda xs -> case xs
+%   | cons x _ => x
+%   | nil => x;
+
+% List_tail xs = case xs
+%   | nil => nil
+%   | cons hd tl => tl;
+
+% List_map : (?a -> ?b) -> List ?a -> List ?b;
+% List_map f = lambda xs -> case xs
+%   | nil => nil
+%   | cons x xs => cons (f x) (List_map f xs);
+
+% List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a;
+% List_foldr f = lambda xs -> lambda i -> case xs
+%   | nil => i
+%   | cons x xs => f x (List_foldr f xs i);
+
+% List_find : (?a -> Bool) -> List ?a -> Option ?a;
+% List_find f = lambda xs -> case xs
+%   | nil => none
+%   | cons x xs => case f x | true => some x | false => List_find f xs;
+
+% List_nth : Int -> List ?a -> ?a -> ?a;
+% List_nth = lambda n -> lambda xs -> lambda d -> case xs
+%   | nil => d
+%   | cons x xs
+%     => case Int_<= n 0
+%        | true => x
+%        | false => List_nth (n - 1) xs d;
+
+% %%%% A more flexible `lambda`
+
+% %% An `Sexp` which we use to represents an *error*.
+% Sexp_error = Sexp_symbol "<error>";
+
+% %% Sexp_to_list : Sexp -> List Sexp -> List Sexp;
+% Sexp_to_list s = lambda exceptions ->
+%   let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"!
+%   Sexp_dispatch
+%       s
+%       (node := lambda head -> lambda tail
+%         -> case List_find (Sexp_eq head) exceptions
+%         | some _ => singleton ()
+%         | none => cons head tail)
+%       (symbol := lambda s
+%         -> case String_eq "" s
+%         | true => nil
+%         | false => singleton ())
+%       singleton singleton singleton singleton;
+
+% multiarg_lambda =
+%   %% This macro lets `lambda_->_` (and siblings) accept multiple arguments.
+%   %% TODO: We could additionally turn
+%   %%     lambda (x :: t) y -> e
+%   %% into
+%   %%     lambda (x : t) => lambda y -> e`
+%   %% thus providing an alternate syntax for lambdas which don't use
+%   %% => and ≡>.
+%   let exceptions = List_map Sexp_symbol
+%                             (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in
+%   lambda name ->
+%   let sym = (Sexp_symbol name);
+%       mklambda = lambda arg -> lambda body ->
+%         Sexp_node sym (cons arg (cons body nil)) in
+%   lambda (margs : List Sexp)
+%   -> IO_return
+%          case margs
+%          | nil => Sexp_error
+%          | cons fargs margstail
+%            => case margstail
+%               | nil => Sexp_error
+%               | cons body bodytail
+%                 => case bodytail
+%                    | cons _ _ => Sexp_error
+%                    | nil => List_foldr mklambda
+%                                        (Sexp_to_list fargs exceptions)
+%                                        body;
+
+% lambda_->_ = macro (multiarg_lambda "##lambda_->_");
+% lambda_=>_ = macro (multiarg_lambda "##lambda_=>_");
+% lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_");
+
+% %%%% More list functions
+
+% List_reverse : List ?a -> List ?a -> List ?a;
+% List_reverse l t = case l
+%   | nil => t
+%   | cons hd tl => List_reverse tl (cons hd t);
+
+% List_concat l t = List_reverse (List_reverse l nil) t;
+
+% List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a;
+% List_foldl f i xs = case xs
+%   | nil => i
+%   | cons x xs => List_foldl f (f i x) xs;
+
+% List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b;
+% List_mapi f xs = let
+%   helper : (a -> Int -> b) -> Int -> List a -> List b;
+%   helper f i xs = case xs
+%     | nil => nil
+%     | cons x xs => cons (f x i) (helper f (i + 1) xs);
+% in helper f 0 xs;
+
+% List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c;
+% List_map2 f xs ys = case xs
+%   | nil => nil
+%   | cons x xs => case ys
+%     | nil => nil % error
+%     | cons y ys => cons (f x y) (List_map2 f xs ys);
+
+% %% Fold 2 List as long as both List are non-empty
+% List_fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> List ?b -> List ?c -> ?a;
+% List_fold2 f o xs ys = case xs
+%   | cons x xs => ( case ys
+%     | cons y ys => List_fold2 f (f o x y) xs ys
+%     | nil => o ) % may be an error
+%   | nil => o; % may or may not be an error
+
+% %% Is argument List empty?
+% List_empty : List ?a -> Bool;
+% List_empty xs = Int_eq (List_length xs) 0;
+
+% %%% Good 'ol combinators
+
+% I x = x;
+
+% %% Use explicit erasable annotations since with an annotation like
+% %%     K : ?a -> ?b -> ?a;
+% %% Typer generalizes to
+% %%     K : (a : Type) ≡> (b : Type) ≡> a -> b -> a;
+% %% Which is less general.
+% %% FIXME: Change the generalizer to insert the `(b : Type) ≡>`
+% %% more lazily (i.e. after the `a` argument).
+% K : ?a -> (b : Type) ≡> b -> ?a;
+% K x y = x;
+
+% %%%% Quasi-Quote macro
+
+% %%   f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"])
+% %%
+% %%   f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil))
+% %%
+% %%     =>       x
+
+% %% Takes an Sexp `x` as argument and return an Sexp which represents code
+% %% which will construct an Sexp equivalent to `x` at run-time.
+% %% This is basically *cross stage persistence* for Sexp.
+% quote1 : Sexp -> Sexp;
+% quote1 x = let
+%                qlist : List Sexp -> Sexp;
+%                qlist xs = case xs
+%                  | nil => Sexp_symbol "nil"
+%                  | cons x xs => Sexp_node (Sexp_symbol "cons")
+%                                           (cons (quote1 x)
+%                                                 (cons (qlist xs) nil));
+%                make_app str sexp =
+%                  Sexp_node (Sexp_symbol str) (cons sexp nil);
+
+%                node op y = case (Sexp_eq op (Sexp_symbol "uquote"))
+%                  | true  => List_head Sexp_error y
+%                  | false => Sexp_node (Sexp_symbol "##Sexp.node")
+%                                       (cons (quote1 op)
+%                                             (cons (qlist y) nil));
+%                symbol s = make_app "##Sexp.symbol" (Sexp_string s);
+%                string s = make_app "##Sexp.string" (Sexp_string s);
+%                integer i = make_app "##Sexp.integer"
+%                                     (make_app "##Int->Integer" (Sexp_integer i));
+%                float f = make_app "##Sexp.float" (Sexp_float f);
+%                block sxp =
+%                   %% FIXME ##Sexp.block takes a string (and prelexes
+%                   %% it) but we have a sexp, what should we do?
+%                   Sexp_symbol "<error FIXME block quoting>";
+%            in Sexp_dispatch x node symbol string integer float block;
+
+% %% quote definition
+% quote = macro (lambda x -> IO_return (quote1 (List_head Sexp_error x)));
+
+% %%%% The `type` declaration macro
+
+% %% Build a declaration:
+% %%     var-name = value-expr;
+% make-decl : Sexp -> Sexp -> Sexp;
+% make-decl var-name value-expr =
+%   Sexp_node (Sexp_symbol "_=_")
+%             (cons var-name
+%                   (cons value-expr nil));
+
+% chain-decl : Sexp -> Sexp -> Sexp;
+% chain-decl a b =
+%   Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil));
+
+% chain-decl3 : Sexp -> Sexp -> Sexp -> Sexp;
+% chain-decl3 a b c =
+%   Sexp_node (Sexp_symbol "_;_") (cons a (cons b (cons c nil)));
+
+% %% Build datacons:
+% %%     ctor-name = datacons type-name ctor-name;
+% make-cons : Sexp -> Sexp -> Sexp;
+% make-cons ctor-name type-name =
+%   make-decl ctor-name
+%             (Sexp_node (Sexp_symbol "datacons")
+%                        (cons type-name
+%                              (cons ctor-name nil)));
+
+% %% Build type annotation:
+% %%     var-name : type-expr;
+% make-ann : Sexp -> Sexp -> Sexp;
+% make-ann var-name type-expr =
+%   Sexp_node (Sexp_symbol "_:_")
+%             (cons var-name
+%                   (cons type-expr nil));
+
+% type-impl = lambda (x : List Sexp) ->
+%   %% `x` follow the mask ->
+%   %%                  (_|_ Nat zero (succ Nat))
+%   %%       Type name  --^    ^------^ constructors
+
+%   %% Return a list contained inside a node sexp.
+%   let knil = K nil;
+%       kerr = K Sexp_error;
+
+%       get-list : Sexp -> List Sexp;
+%       get-list node = Sexp_dispatch node
+%                                      (lambda op lst -> lst) % Nodes
+%                                      knil      % Symbol
+%                                      knil      % String
+%                                      knil      % Integer
+%                                      knil      % Float
+%                                      knil;     % List of Sexp
+
+%       %% Get a name (symbol) from a sexp
+%       %%   - (name t) -> name
+%       %%   - name -> name
+%       get-name : Sexp -> Sexp;
+%       get-name sxp =
+%         Sexp_dispatch sxp
+%                        (lambda op _ -> get-name op) % Nodes
+%                        (lambda _    -> sxp) % Symbol
+%                        kerr  % String
+%                        kerr  % Integer
+%                        kerr  % Float
+%                        kerr; % List of Sexp
+
+%       get-args : Sexp -> List Sexp;
+%       get-args sxp =
+%         Sexp_dispatch sxp
+%                        (lambda _ args -> args)            % Nodes
+%                        (lambda _    -> (nil : List Sexp)) % Symbol
+%                        (lambda _ -> (nil : List Sexp))    % String
+%                        (lambda _ -> (nil : List Sexp))    % Integer
+%                        (lambda _ -> (nil : List Sexp))    % Float
+%                        (lambda _ -> (nil : List Sexp));   % List of Sexp
+
+%       get-type : Sexp -> Sexp;
+%       get-type sxp =
+%         Sexp_dispatch sxp
+%                       (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_"))
+%                         | true  => List_nth 1 ss Sexp_error
+%                         | false => sxp)
+%                       (lambda _ -> sxp)
+%                       (lambda _ -> Sexp_error)
+%                       (lambda _ -> Sexp_error)
+%                       (lambda _ -> Sexp_error)
+%                       (lambda _ -> Sexp_error);
+
+%       get-head = List_head Sexp_error;
+
+%       %% Get expression.
+%       expr = get-head x;
+
+%       %% Expression is  Sexp_node (Sexp_symbol "|") (list)
+%       %% we only care about the list bit
+%       lst = get-list expr;
+
+%       %% head is (Sexp_node type-name (arg list))
+%       name = get-head lst;
+%       ctor = List_tail lst;
+
+%       type-name = get-name name;
+
+%       %% Create the inductive type definition.
+%       inductive = Sexp_node (Sexp_symbol "typecons")
+%                             (cons name ctor);
+
+%       %% Declare the inductive type as a function
+%       %% Useful for recursive type
+%       type-decl = quote ((uquote (get-name name)) : (uquote (
+%         (List_foldl (lambda args arg ->
+%           Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil)))
+%             %% FIXME: Don't hardcode TypeLevel.z!
+%             (Sexp_symbol "Type") (List_reverse (get-args name) nil))
+%       )));
+
+%       decl  = make-decl type-name inductive;
+
+%       %% Add constructors.
+%       ctors = let for-each : List Sexp -> Sexp -> Sexp;
+%                   for-each ctr acc = case ctr
+%                     | cons hd tl =>
+%                         let acc2 = chain-decl (make-cons (get-name hd)
+%                                                          type-name)
+%                                               acc
+%                         in for-each tl acc2
+%                     | nil => acc
+%               in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
+
+%                             %% return decls
+%   in IO_return (chain-decl3 type-decl % type as a function declaration
+%                             decl      % inductive type declaration
+%                             ctors);   % constructor declarations
+
+% type_ = macro type-impl;
+
+% %%%% An inductive type to wrap Sexp
+
+% type Sexp_wrapper
+%   | node Sexp (List Sexp)
+%   | symbol String
+%   | string String
+%   | integer Integer
+%   | float Float
+%   | block Sexp;
+
+% Sexp_wrap s = Sexp_dispatch s node symbol string integer float block;
+
+% %%%% Tuples
+
+% %% Sample tuple: a module holding Bool and its constructors.
+% BoolMod = (##datacons
+%              %% We need the `?` metavars to be lexically outside of the
+%              %% `typecons` expression, otherwise they end up generalized, so
+%              %% we end up with a type constructor like
+%              %%
+%              %%     typecons _ (cons (τ₁ : Type) (t : τ₁)
+%              %%                      (τ₂ : Type) (true : τ₂)
+%              %%                      (τ₃ : Type) (false : τ₃))
+%              %%
+%              %% And it's actually even worse because it tries to generalize
+%              %% over the level of those `Type`s, so we end up with an invalid
+%              %% inductive type.
+%              ((lambda t1 t2 t3
+%                -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3)))
+%                   ? ? ?)
+%              cons)
+%               (_ := Bool) (_ := true) (_ := false);
+
+% Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
+% pair = datacons Pair pair;
+
+% __.__ =
+%   let mksel o f =
+%         let constructor = Sexp_node (Sexp_symbol "##datacons")
+%                                     (cons (Sexp_symbol "?")
+%                                           (cons (Sexp_symbol "cons")
+%                                                 nil));
+%             pattern = Sexp_node constructor
+%                                 (cons (Sexp_node (Sexp_symbol "_:=_")
+%                                                  (cons f (cons (Sexp_symbol "v")
+%                                                                nil)))
+%                                       nil);
+%             branch = Sexp_node (Sexp_symbol "_=>_")
+%                                (cons pattern (cons (Sexp_symbol "v") nil));
+%         in Sexp_node (Sexp_symbol "case_")
+%                      (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);
+
+% %% Triplet (tuple with 3 values)
+% type Triplet (a : Type) (b : Type) (c : Type)
+%   | triplet (x : a) (y : b) (z : c);
+
+% %%%% List with tuple
+
+% %% Merge two List to a List of Pair
+% %% Both List must be of same length
+% List_merge : List ?a -> List ?b -> List (Pair ?a ?b);
+% List_merge xs ys = case xs
+%   | cons x xs => ( case ys
+%     | cons y ys => cons (pair x y) (List_merge xs ys)
+%     | nil => nil ) % error
+%   | nil => nil;
+
+% %% `Unmerge` a List of Pair
+% %% The two functions name said it all
+% List_map-fst xs = let
+%   mf p = case p | pair x _ => x;
+% in List_map mf xs;
+
+% List_map-snd xs = let
+%   mf p = case p | pair _ y => y;
+% in List_map mf xs;
+
+% %%%% Logic
+
+% %% `False` should be one of the many empty types.
+% %% Other popular choices are False = ∀a.a and True = ∃a.a.
+% False = Void;
+% True = Unit;
+
+% Not prop = prop -> False;
+
+% %% Like Bool, except that it additionally carries the meaning of its value.
+% %% 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_ ?ℓ))
+%                      (true (p ::: prop)) (false (p ::: Not prop));
+
+% %% Testing generalization in inductive type constructors.
+% LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient!
+% type LList (a : Type) (n : Int)
+%   | vnil (p ::: Eq n 0)
+%   | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound!
+
+% %%%% If
+
+% define-operator "if" () 2;
+% define-operator "then" 2 1;
+% define-operator "else" 1 66;
+
+% 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 uquote e1
+%                                 | true => uquote e2
+%                                 | false => uquote e3)));
+
+% %%%% More boolean
+
+% %% FIXME: Type annotations should not be needed below.
+% not : Bool -> Bool;
+% %% FIXME: We use braces here to delay parsing, otherwise the if/then/else
+% %% part of the grammar declared above is not yet taken into account.
+% not x = { if x then false else true };
+
+% or : Bool -> Bool -> Bool;
+% or x y = { if x then x else y };
+
+% and : Bool -> Bool -> Bool;
+% and x y = { if x then y else x };
+
+% xor : Bool -> Bool -> Bool;
+% xor x y = { if x then (not y) else y };
+
+% %% FIXME: Can't use ?a because that is generalized to be universe-polymorphic,
+% %% which we don't support in `load` yet.
+% fold : Bool -> (a : Type) ≡> a -> a -> a;
+% fold x t e = { if x then t else e};
+
+% %%%% Test
+% test1 : ?;
+% test2 : Option Int;
+% test3 : Option Int;
+% test1 = test2;
+% %% In earlier versions of Typer, we could use `?` in declarations
+% %% to mean "fill this for me by unifying with later type information",
+% %% but this is incompatible with the use of generalization to introduce
+% %% implicit arguments.
+% %%     test4 : Option ?;
+% test2 = none;
+% test4 : Option Int;
+% test4 = test1 : Option ?;
+% test3 = test4;
+
+% %%%% Rewrite of some builtins to use `Option`
+
+% %%
+% %% If `Elab_nth-arg'` returns "_" it means:
+% %%   A- The constructor isn't defined, or
+% %%   B- The constructor has no n'th argument
+% %%
+% %% So in those case this function returns `none`
+% %%
+% Elab_nth-arg a b c = let
+%   r = Elab_nth-arg' a b c;
+% in case (String_eq r "_")
+%      | true  => (none)
+%      | false => (some r);
+
+% %%
+% %% If `Elab_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_arg-pos a b c = let
+%   r = Elab_arg-pos' a b c;
+% in case (Int_eq r (-1))
+%      | true  => (none)
+%      | false => (some r);
+
+% %%%%
+% %%%% Common library
+% %%%%
+
+% %%
+% %% `<-` operator used in macro `do` and for tuple assignment
+% %%
+
+% define-operator "<-" 80 96;
+
+% %%
+% %% `List` is the type and `list` is the module
+% %%
+% list = load "btl/list.typer";
+
+% %%
+% %% Macro `do` for easier series of IO operation
+% %%
+% %% e.g.:
+% %%     do { IO_return true; };
+% %%
+% do = let lib = load "btl/do.typer" in lib.do;
+
+% %%
+% %% Module containing various macros for tuple
+% %% Used by `case_`
+% %%
+% tuple-lib = load "btl/tuple.typer";
+
+% %%
+% %% Get the nth element of a tuple
+% %%
+% %% e.g.:
+% %%     tuple-nth tup 0;
+% %%
+% tuple-nth = tuple-lib.tuple-nth;
+
+% %%
+% %% Affectation of tuple
+% %%
+% %% e.g.:
+% %%     (x,y,z) <- tup;
+% %%
+% _<-_ = tuple-lib.assign-tuple;
+
+% %%
+% %% Instantiate a tuple from expressions
+% %%
+% %% e.g.:
+% %%     tup = (x,y,z);
+% %%
+% _,_ = tuple-lib.make-tuple;
+
+% Tuple = tuple-lib.tuple-type;
+
+% %%
+% %% Macro `case` for a some more complex pattern matching
+% %%
+% case_ = let lib = load "btl/case.typer" in lib.case-macro;
+
+% %%
+% %% plain-let
+% %% Not recursive and not sequential
+% %%
+% %% e.g.:
+% %%     plain-let x = 1; in x;
+% %%
+
+% define-operator "plain-let" () 3;
+
+% %%
+% %% Already defined:
+% %%     define-operator "in" 3 67;
+% %%
+
+% plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro;
+
+% %%
+% %% `case` at function level
+% %%
+% %% e.g.:
+% %%     my-fun (x : Bool)
+% %%       | true  => false
+% %%       | false => true;
+% %%
+% _|_ = let lib = load "btl/polyfun.typer" in lib._|_;
+
+% %%
+% %% case_as_return_, case_return_
+% %% A `case` for dependent elimination
+% %%
+
+% define-operator "as" 42 42;
+% define-operator "return" 42 42;
+% depelim = load "btl/depelim.typer";
+% case_as_return_ = depelim.case_as_return_;
+% case_return_ = depelim.case_return_;
+
+% %%%% Unit tests function for doing file
+
+% %% It's hard to do a primitive which execute test file
+% %% because of circular dependency...
+
+% %%
+% %% A macro using `load` for unit testing purpose
+% %%
+% %% Takes a file name (String) as argument
+% %% Returns variable named `exec-test` from the loaded file
+% %%
+% %% `exec-test` should be a command doing unit tests
+% %% for other purpose than that just use `load` directly!
+% %%
+% Test_file = macro (lambda args -> let
+
+%   %% return an empty command on error
+%   ret = Sexp_node
+%     (Sexp_symbol "IO_return")
+%     (cons (Sexp_symbol "unit") nil);
+
+% %% Expecting a String and nothing else
+% in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error)
+%     (lambda _ _ -> ret)
+%     (lambda _ -> ret)
+%     %% `load` is a special form and takes a Sexp rather than a real `String`
+%     (lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test))
+%     (lambda _ -> ret)
+%     (lambda _ -> ret)
+%     (lambda _ -> ret))
+% );
+
+% %%% pervasive.typer ends here.
=====================================
src/elab.ml
=====================================
@@ -443,28 +443,17 @@ let rec meta_to_var ids (e : lexp) =
       -> mkLambda (ak, v, loop o t, loop (1 + o) e)
     | Call (f, args)
       -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o e)) args)
-    | Inductive (l, label, args, cases)
-      -> let alen = List.length args in
-        let (_, nargs)
-          = List.fold_right (fun (ak, v, t) (o', args)
-                             -> let o' = o' - 1 in
-                               (o', (ak, v, loop (o' + o) t)
-                                    :: args))
-                            args (alen, []) in
-        let ncases
-          = SMap.map
-              (fun fields
-               -> let flen = List.length fields in
-                 let (_, nfields)
-                   = List.fold_right
-                       (fun (ak, v, t) (o', fields)
-                        -> let o' = o' - 1 in
-                          (o', (ak, v, loop (o' + o) t)
-                               :: fields))
-                       fields (flen + alen, []) in
-                 nfields)
-              cases in
-        mkInductive (l, label, nargs, ncases)
+    | Inductive (l, ((_, name) as label), cases)
+      -> let unmeta_field (ak, v, t) (o', fields) =
+           let o' = o' - 1 in
+           o', (ak, v, loop (o' + o) t) :: fields
+         in
+         let unmeta_constructor fields =
+           let flen = List.length fields in
+           let (_, nfields) = List.fold_right unmeta_field fields (flen, []) in
+           nfields
+         in
+         mkInductive (l, label, SMap.map unmeta_constructor cases)
     | Cons (t, l) -> mkCons (loop o t, l)
     | Case (l, e, t, cases, default)
       -> let ncases
@@ -689,7 +678,12 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp =
         check_inferred ctx e inferred_t t
and unify_or_error lctx lxp ?lxp_name expect actual =
-  match Unif.unify expect actual lctx with
+  print_endline ("[unify_or_error] lexp = " ^ lexp_string lxp);
+  print_endline ("[unify_or_error] expect = " ^ lexp_string expect);
+  print_endline ("[unify_or_error] actual = " ^ lexp_string actual);
+  let res = Unif.unify expect actual lctx in
+  print_endline ("[unify_or_error] unify done");
+  match res with
    | ((ck, _ctx, t1, t2)::_)
      -> lexp_error (lexp_location lxp) lxp
          ("Type mismatch"
@@ -709,11 +703,17 @@ and unify_or_error lctx lxp ?lxp_name expect actual =
  * we use is to instantiate implicit arguments when needed, but we could/should
  * do lots of other things.  *)
 and check_inferred ctx e inferred_t t =
+  print_endline ("[check_inferred] e = " ^ lexp_string e);
+  print_endline ("[check_inferred] inferred_t = " ^ lexp_string inferred_t);
+  print_endline ("[check_inferred] t = " ^ lexp_string t);
   let (e, inferred_t) =
-  match OL.lexp'_whnf t (ectx_to_lctx ctx) with
+    match OL.lexp'_whnf t (ectx_to_lctx ctx) with
     | Arrow ((Aerasable | Aimplicit), _, _, _, _)
       -> (e, inferred_t)
-    | _ -> instantiate_implicit e inferred_t ctx in
+    | _ -> instantiate_implicit e inferred_t ctx
+  in
+  print_endline ("[check_inferred] e = " ^ lexp_string e);
+  print_endline ("[check_inferred] inferred_t = " ^ lexp_string inferred_t);
   unify_or_error (ectx_to_lctx ctx) e t inferred_t;
   e
@@ -721,168 +721,176 @@ and check_inferred ctx e inferred_t t =
 and check_case rtype (loc, target, ppatterns) ctx =
   (* Helpers *)
+  print_endline ("[check_case] rtype = " ^ lexp_string rtype);
+  print_endline ("[check_case] target = " ^ sexp_string target);
+
   let pat_string p = sexp_string (pexp_u_pat p) in
-    let uniqueness_warn pat =
-      warning ~loc:(pexp_pat_location pat)
-              ("Pattern " ^ pat_string pat
-               ^ " is a duplicate.  It will override previous pattern.") in
-
-    let check_uniqueness pat name map =
-      if SMap.mem name map then uniqueness_warn pat in
-
-    (* get target and its type *)
-    let tlxp, tltp = infer target ctx in
-    let tknd = OL.get_type (ectx_to_lctx ctx) tltp in
-    let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with
-      | Sort (_, Stype l) -> l
-      | _ -> fatal "Target lexp's kind is not a sort" in
-    let it_cs_as = ref None in
-    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)
-        -> unify_ind it it'; (cs, args)
-      | None
-        -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with
-          | Inductive (_, _, fargs, constructors)
-            -> let (s, targs) = List.fold_left
-                                 (fun (s, targs) (ak, name, t)
-                                  -> let arg = newMetavar
-                                                (ectx_to_lctx ctx)
-                                                (ectx_to_scope_level ctx)
-                                                name (mkSusp t s) in
-                                    (S.cons arg s, (ak, arg) :: targs))
-                                 (S.identity, [])
-                                 fargs in
-              let (cs, args) = (constructors, List.rev targs) in
-              ltarget := check_inferred ctx tlxp tltp (mkCall (it', args));
-              it_cs_as := Some (it', cs, args);
-              (cs, args)
-          | _ -> let call_split e =
-                      match OL.lexp'_whnf e (ectx_to_lctx ctx) with
-                       | Call (f, args) -> (f, args)
-                       | _ -> (e,[]) in
+  let uniqueness_warn pat =
+    warning ~loc:(pexp_pat_location pat)
+            ("Pattern " ^ pat_string pat
+             ^ " is a duplicate.  It will override previous pattern.") in
+
+  let check_uniqueness pat name map =
+    if SMap.mem name map then uniqueness_warn pat in
+
+  (* get target and its type *)
+  let tlxp, tltp = infer target ctx in
+  print_endline ("[check_case] tlxp = " ^ lexp_string tlxp);
+  print_endline ("[check_case] ltlp = " ^ lexp_string tltp);
+
+  let tknd = OL.get_type (ectx_to_lctx ctx) tltp in
+  print_endline ("[check_case] tknd = " ^ lexp_string tknd);
+
+  let tlvl = match OL.lexp'_whnf tknd (ectx_to_lctx ctx) with
+    | Sort (_, Stype l) -> l
+    | _ -> fatal "Target lexp's kind is not a sort" in
+  print_endline ("[check_case] tlvl = " ^ lexp_string tlvl);
+
+  let it_cs_as = ref None in
+  let ltarget = ref tlxp in
+
+  let get_cs_as it' lctor =
+    print_endline ("[get_cs_as] it' = " ^ lexp_string it');
+    print_endline ("[get_cs_as] lctor = " ^ lexp_string 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)
+      -> print_endline "unify";
+         unify_ind it it'; (cs, args)
+    | None
+      -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with
+         | Inductive (_, _, constructors)
+           -> print_endline "checking with inductive";
+              ltarget := check_inferred ctx tlxp tltp (mkCall (it', []));
+              print_endline ("[get_cs_as] ltarget = " ^ lexp_string !ltarget);
+              it_cs_as := Some (it', constructors, []);
+              (constructors, [])
+         | _ -> let call_split e =
+                  match OL.lexp'_whnf e (ectx_to_lctx 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);
-                      constructors
+                  | Inductive (_, _, constructors)
+                    -> assert (List.length targs == 0);
+                       constructors
                   | _ -> lexp_error (sexp_location target) tlxp
-                          ("Can't `case` on objects of this type: "
-                           ^ lexp_string tltp);
-                        SMap.empty in
+                                    ("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) =
+  (*  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 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
+    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 tlvl' = shift_to_extended_ctx nctx tlvl in
-        let eqty = mkCall (DB.type_eq,
-                           [(Aerasable, tlvl');    (* Typelevel *)
-                            (Aerasable, tltp');    (* Inductive type *)
-                            (Anormal, head_lexp);  (* Lexp of the branch head *)
-                            (Anormal, tlxp')])     (* Target lexp *)
-        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' = shift_to_extended_ctx nctx rtype in
-        let lexp = check pexp rtype' nctx in
-        lbranches, Some (v, lexp) in
-
-      let add_branch pctor pargs =
-        let loc = sexp_location pctor in
-        let lctor, ct = infer pctor ctx in
-        let rec inst_args ctx e =
+      let tlxp' = shift_to_extended_ctx nctx tlxp in
+      let tltp' = shift_to_extended_ctx nctx tltp in
+      let tlvl' = shift_to_extended_ctx nctx tlvl in
+      let eqty = mkCall (DB.type_eq,
+                         [(Aerasable, tlvl');    (* Typelevel *)
+                          (Aerasable, tltp');    (* Inductive type *)
+                          (Anormal, head_lexp);  (* Lexp of the branch head *)
+                          (Anormal, tlxp')])     (* Target lexp *)
+      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' = shift_to_extended_ctx nctx rtype in
+      let lexp = check pexp rtype' nctx in
+      lbranches, Some (v, lexp) in
+
+    let add_branch pctor pargs =
+      let loc = sexp_location pctor in
+      let lctor, ct = infer pctor ctx in
+      let rec inst_args ctx e =
         let lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in
-         match lexp_lexp' lxp with
-          | Lambda (Aerasable, v, t, body)
-            -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx)
-                          v t in
-              let nctx = ctx_extend ctx v Variable t in
-              let body = inst_args nctx body in
-              mkSusp body (S.substitute arg)
-          | e -> lxp in
-        match lexp_lexp' (nosusp (inst_args ctx lctor)) with
-        | Cons (it', (_, cons_name))
-          -> let _ = check_uniqueness pat cons_name lbranches in
-            let (constructors, targs) = get_cs_as it' lctor in
-            let cargs
-              = try SMap.find cons_name constructors
-                with Not_found
-                     -> lexp_error loc lctor
+        match lexp_lexp' lxp with
+        | Lambda (Aerasable, v, t, body)
+          -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx)
+                                  v t in
+             let nctx = ctx_extend ctx v Variable t in
+             let body = inst_args nctx body in
+             mkSusp body (S.substitute arg)
+        | e -> lxp in
+      match lexp_lexp' (nosusp (inst_args ctx lctor)) with
+      | Cons (it', (_, cons_name))
+        -> let _ = check_uniqueness pat cons_name lbranches in
+           let (constructors, targs) = get_cs_as it' lctor in
+           let cargs
+             = try SMap.find cons_name constructors
+               with Not_found
+                    -> lexp_error loc lctor
                                   ("`" ^ (lexp_string it')
                                    ^ "` does not have a `"
                                    ^ cons_name ^ "` constructor");
                        [] in
-            let subst = List.fold_left (fun s (_, t) -> S.cons t s)
-                                        S.identity targs in
-            let rec make_nctx ctx   (* elab context.  *)
-                              s     (* Pending substitution.  *)
-                              pargs (* Pattern arguments.  *)
-                              cargs (* Constructor arguments.  *)
-                              pe    (* Pending explicit pattern args.  *)
-                              acc = (* Accumulated result.  *)
-              match (pargs, cargs) with
-              | (_, []) when not (SMap.is_empty pe)
-                -> let pending = SMap.bindings pe in
+           let subst = List.fold_left (fun s (_, t) -> S.cons t s)
+                                      S.identity targs in
+           let rec make_nctx ctx   (* elab context.  *)
+                             s     (* Pending substitution.  *)
+                             pargs (* Pattern arguments.  *)
+                             cargs (* Constructor arguments.  *)
+                             pe    (* Pending explicit pattern args.  *)
+                             acc = (* Accumulated result.  *)
+             match (pargs, cargs) with
+             | (_, []) when not (SMap.is_empty pe)
+               -> let pending = SMap.bindings pe in
                   sexp_error loc
                              ("Explicit pattern args `"
                               ^ String.concat ", " (List.map (fun (l, _) -> l)
                                                              pending)
                               ^ "` have no matching fields");
                   make_nctx ctx s pargs cargs SMap.empty acc
-              | [], [] -> ctx, List.rev acc
-              | (_, pat)::_, []
-                -> lexp_error loc lctor
+             | [], [] -> ctx, List.rev acc
+             | (_, pat)::_, []
+               -> lexp_error loc lctor
                              "Too many pattern args to the constructor";
                   make_nctx ctx s [] [] pe acc
-              | (_, (ak, (_, Some fname), fty)::cargs)
-                   when SMap.mem fname pe
-                -> let var = SMap.find fname pe in
+             | (_, (ak, (_, Some fname), fty)::cargs)
+                  when SMap.mem fname pe
+               -> let var = SMap.find fname pe in
                   let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
                   make_nctx nctx (ssink var s) pargs cargs
                             (SMap.remove fname pe)
                             ((ak, var)::acc)
-              | ((ef, var)::pargs, (ak, _, fty)::cargs)
-                   when (match (ef, ak) with
-                         | (Some (_, "_"), _) | (None, Anormal) -> true
-                         | _ -> false)
-                -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
+             | ((ef, var)::pargs, (ak, _, fty)::cargs)
+                  when (match (ef, ak) with
+                        | (Some (_, "_"), _) | (None, Anormal) -> true
+                        | _ -> false)
+               -> let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
                   make_nctx nctx (ssink var s) pargs cargs pe
                             ((ak, var)::acc)
-              | ((Some (l, fname), var)::pargs, cargs)
-                -> if SMap.mem fname pe then
+             | ((Some (l, fname), var)::pargs, cargs)
+               -> if SMap.mem fname pe then
                     sexp_error l ("Duplicate explicit field `" ^ fname ^ "`");
                   make_nctx ctx s pargs cargs (SMap.add fname var pe) acc
-              | pargs, (ak, fname, fty)::cargs
-                -> let var = (loc, None) in
+             | pargs, (ak, fname, fty)::cargs
+               -> let var = (loc, None) in
                   let nctx = ctx_extend ctx var Variable (mkSusp fty s) in
                   if ak = Anormal then
                     sexp_error loc
@@ -891,37 +899,37 @@ 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) ->
-                  (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' = shift_to_extended_ctx nctx rtype in
-            let lexp = check pexp rtype' nctx in
-            SMap.add cons_name (loc, fargs, lexp) lbranches,
-            dflt
-        (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it
-         * and try again with the result.  *)
-        | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt
-      in
-
-      match pat with
-      | Ppatsym ((_, None) as var) -> add_default var
-      | Ppatsym ((l, Some name) as var)
-        -> if Eval.constructor_p name ctx then
-            add_branch (Symbol (l, name)) []
-          else add_default var (* A named default branch.  *)
-
-      | Ppatcons (pctor, pargs) -> add_branch pctor pargs in
-
-    let (lpattern, dflt) =
-        List.fold_left fold_fun (SMap.empty, None) ppatterns in
-
-    mkCase (loc, tlxp, rtype, lpattern, dflt)
+           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) ->
+                 (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' = shift_to_extended_ctx nctx rtype in
+           let lexp = check pexp rtype' nctx in
+           SMap.add cons_name (loc, fargs, lexp) lbranches,
+           dflt
+      (* FIXME: If `ct` is Special-Form or Macro, pass pargs to it
+       * and try again with the result.  *)
+      | _ -> lexp_error loc lctor "Not a constructor"; lbranches, dflt
+    in
+
+    match pat with
+    | Ppatsym ((_, None) as var) -> add_default var
+    | Ppatsym ((l, Some name) as var)
+      -> if Eval.constructor_p name ctx then
+           add_branch (Symbol (l, name)) []
+         else add_default var (* A named default branch.  *)
+
+    | Ppatcons (pctor, pargs) -> add_branch pctor pargs in
+
+  let (lpattern, dflt) =
+    List.fold_left fold_fun (SMap.empty, None) ppatterns in
+
+  mkCase (loc, tlxp, rtype, lpattern, dflt)
and elab_macro_call ctx func args ot =
   let t
@@ -1156,11 +1164,11 @@ and lexp_check_decls (ectx : elab_context) (* External context.  *)
                     match Myers.nth i (ectx_to_lctx nctx) with
                     | (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
-                        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))
+                         let e = check pexp adjusted_t nctx in
+                         let (grm, ec, lc, sl) = 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))
                     | _ -> Log.internal_error "Defining same slot!")
                   defs (IMap.empty, nctx) in
   let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in
@@ -1408,11 +1416,11 @@ let sform_built_in ctx loc sargs ot =
           * performance of type-inference (at least until we have proper
           * memoization of push_susp and/or whnf).  *)
          -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in
-           let bi = mkBuiltin ((loc, name), ltp') in
-           if not (SMap.mem name (!EV.builtin_functions)) then
-             sexp_error loc ("Unknown built-in `" ^ name ^ "`");
-           BI.add_builtin_cst name bi;
-           (bi, Checked)
+            let bi = mkBuiltin ((loc, name), ltp') in
+            if not (SMap.mem name (!EV.builtin_functions)) then
+              sexp_error loc ("Unknown built-in `" ^ name ^ "`");
+            BI.add_builtin_cst name bi;
+            (bi, Checked)
        | None -> error ~loc "Built-in's type not provided by context!";
                 sform_dummy_ret ctx loc)
@@ -1445,62 +1453,40 @@ let elab_datacons_arg s = match s with
     -> (elab_colon_to_ak k, elab_p_id s, t)
   | _ -> (Anormal, (sexp_location s, None), s)
-let elab_typecons_arg arg : (arg_kind * vname * sexp option) =
-  match arg with
-  | Node (Symbol (_, (("_:::_" | "_::_" | "_:_") as k)), [Symbol (l,name); e])
-    -> (elab_colon_to_ak k,
-       (l, Some name), Some e)
-  | Symbol (l, name) -> (Anormal, (l, Some name), None)
-  | _ -> sexp_error ~print_action:(fun _ -> sexp_print arg; print_newline ())
-           (sexp_location arg)
-           "Unrecognized formal arg";
-         (Anormal, (sexp_location arg, None), None)
-
 let sform_typecons ctx loc sargs ot =
   match sargs with
   | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy)
-  | formals :: constrs
-    -> let (label, formals) = match formals with
-        | Node (label, formals) -> (label, formals)
-        | _ -> (formals, []) in
-      let label = match label with
+  | label :: constrs
+    -> let (_, name) as label =
+        match label with
         | Symbol label -> label
-        | _ -> let loc = sexp_location label in
-              sexp_error loc "Unrecognized inductive type name";
-              (loc, "<error>") in
-
-      let rec parse_formals sformals rformals ctx = match sformals with
-        | [] -> (List.rev rformals, ctx)
-        | sformal :: sformals
-          -> let (kind, var, opxp) = elab_typecons_arg sformal in
-            let ltp = match opxp with
-              | Some pxp -> let (l,_) = infer pxp ctx in l
-              | None -> let (l,_) = var in
-                       newMetatype (ectx_to_lctx ctx)
-                                   (ectx_to_scope_level ctx) l in
-
-            parse_formals sformals ((kind, var, ltp) :: rformals)
-                          (ectx_extend ctx var Variable ltp) in
-
-      let (formals, nctx) = parse_formals formals [] ctx in
-
-      let ctors
-        = List.fold_right
-          (fun case pcases
-           -> match case with
-             (* read Constructor name + args => Type ((Symbol * args) list) *)
-             | Node (Symbol s, cases)
-               -> (s, List.map elab_datacons_arg cases)::pcases
-             (* This is a constructor with no args *)
-             | Symbol s -> (s, [])::pcases
-
-             | _ -> sexp_error (sexp_location case)
-                              "Unrecognized constructor declaration";
-                   pcases)
-          constrs [] in
-
-      let map_ctor = lexp_parse_inductive ctors nctx in
-      (mkInductive (loc, label, formals, map_ctor), Lazy)
+        | _
+          -> let loc = sexp_location label in
+             let message =
+               "Expected the inductive type name to be a symbol, but got "
+               ^ sexp_string label
+             in
+             sexp_error loc message;
+             (loc, "<error>")
+       in
+
+       let ctors
+         = List.fold_right
+             (fun case pcases
+              -> match case with
+                 (* read Constructor name + args => Type ((Symbol * args) list) *)
+                 | Node (Symbol s, cases)
+                   -> (s, List.map elab_datacons_arg cases)::pcases
+                 (* This is a constructor with no args *)
+                 | Symbol s -> (s, [])::pcases
+
+                 | _ -> sexp_error (sexp_location case)
+                                   "Unrecognized constructor declaration";
+                        pcases)
+             constrs [] in
+
+       let map_ctor = lexp_parse_inductive ctors ctx in
+       mkInductive (loc, label, map_ctor), Lazy
let sform_hastype ctx loc sargs ot =
   match sargs with
@@ -1689,17 +1675,22 @@ let rec sform_lambda kind ctx loc sargs ot =
 let rec sform_case ctx loc sargs ot = match sargs with
   | [Node (Symbol (_, "_|_"), se :: scases)]
     -> let parse_case branch = match branch with
-        | Node (Symbol (_, "_=>_"), [pat; code])
-          -> (pexp_p_pat pat, code)
-        | _ -> let l = (sexp_location branch) in
-              sexp_error l "Unrecognized simple case branch";
-              (Ppatsym (l, None), Symbol (l, "?")) in
-      let pcases = List.map parse_case scases in
-      let t = match ot with
-        | Some t -> t
-        | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in
-      let le = check_case t (loc, se, pcases) ctx in
-      (le, match ot with Some _ -> Checked | None -> Inferred t)
+         | Node (Symbol (_, "_=>_"), [pat; code])
+           -> (pexp_p_pat pat, code)
+         | _ -> let l = (sexp_location branch) in
+                sexp_error l "Unrecognized simple case branch";
+                (Ppatsym (l, None), Symbol (l, "?"))
+       in
+       let pcases = List.map parse_case scases in
+
+       let t = match ot with
+         | Some t -> t
+         | None -> newMetatype (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc in
+       print_endline ("[sform_case] t = " ^ lexp_string t);
+       print_endline ("[sform_case] se = " ^ sexp_string se);
+       let le = check_case t (loc, se, pcases) ctx in
+       print_endline ("[sform_case] le = " ^ lexp_string le);
+       (le, match ot with Some _ -> Checked | None -> Inferred t)
(* In case there are no branches, pretend there was a | anyway.  *)
   | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot
=====================================
src/eval.ml
=====================================
@@ -812,14 +812,18 @@ let erasable_p name nth ectx =
                                     | (k, _, _) -> k = Aerasable )
                               else false
                             | _ -> false in
-  try let idx = senv_lookup name ectx in
-    match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with
-      | Cons (e, _) when is_var e
-        -> (match (env_lookup_expr ectx (get_var e)) with
-            | Some i when is_inductive i
-              -> is_erasable (get_inductive_ctor (get_inductive i))
-            | _ -> false)
-      | _ -> false
+  try
+    let idx = senv_lookup name ectx in
+    match
+      OL.lexp'_whnf
+        (mkVar ((dummy_location, Some name), idx))
+        (ectx_to_lctx ectx)
+    with
+    | Cons (e, _) when is_var e
+      -> (match (env_lookup_expr ectx (get_var e)) with
+          | Some (Inductive (_, _, constructors), _) -> is_erasable constructors
+          | _ -> false)
+    | _ -> false
   with Senv_Lookup_Fail _ -> false
let erasable_p2 t name ectx =
@@ -833,14 +837,18 @@ let erasable_p2 t name ectx =
              | _ -> false)
           args)
     | _ -> false in
-  try let idx = senv_lookup t ectx in
-    match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with
-      | Cons (e, _) when is_var e
-        -> (match (env_lookup_expr ectx (get_var e)) with
-            | Some i when is_inductive i
-              -> is_erasable (get_inductive_ctor (get_inductive i))
-            | _ -> false)
-      | _ -> false
+  try
+    let idx = senv_lookup t ectx in
+    match
+      OL.lexp'_whnf
+        (mkVar ((dummy_location, Some t), idx))
+        (ectx_to_lctx ectx)
+    with
+    | Cons (e, _) when is_var e
+      -> (match env_lookup_expr ectx (get_var e) with
+          | Some (Inductive (_, _, constructors), _) -> is_erasable constructors
+          | _ -> false)
+    | _ -> false
   with Senv_Lookup_Fail _ -> false
let nth_ctor_arg name nth ectx =
@@ -851,14 +859,18 @@ let nth_ctor_arg name nth ectx =
         | _ -> "_"
         | exception (Failure _) -> "_" )
     | _ -> "_" in
-  try let idx = senv_lookup name ectx in
-  match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with
-      | Cons (e, _) when is_var e
-        -> (match (env_lookup_expr ectx (get_var e)) with
-            | Some i when is_inductive i
-              -> find_nth (get_inductive_ctor (get_inductive i))
-            | _ -> "_")
-      | _ -> "_"
+  try
+    let idx = senv_lookup name ectx in
+    match
+      OL.lexp'_whnf
+        (mkVar ((dummy_location, Some name), idx))
+        (ectx_to_lctx ectx)
+    with
+    | Cons (e, _) when is_var e
+      -> (match (env_lookup_expr ectx (get_var e)) with
+          | Some (Inductive (_, _, constructors), _) -> find_nth constructors
+          | _ -> "_")
+    | _ -> "_"
   with Senv_Lookup_Fail _ -> "_"
let ctor_arg_pos name arg ectx =
@@ -872,14 +884,18 @@ let ctor_arg_pos name arg ectx =
                                   | None -> (-1)
                                   | Some n -> n )
                             | _ -> (-1) in
-  try let idx = senv_lookup name ectx in
-  match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with
-      | Cons (e, _) when is_var e
-        -> (match (env_lookup_expr ectx (get_var e)) with
-            | Some i when is_inductive i
-              -> find_arg (get_inductive_ctor (get_inductive i))
-            | _ -> (-1))
-      | _ -> (-1)
+  try
+    let idx = senv_lookup name ectx in
+    match
+      OL.lexp'_whnf
+        (mkVar ((dummy_location, Some name), idx))
+        (ectx_to_lctx ectx)
+    with
+    | Cons (e, _) when is_var e
+      -> (match (env_lookup_expr ectx (get_var e)) with
+          | Some (Inductive (_, _, constructors), _) -> find_arg constructors
+          | _ -> (-1))
+    | _ -> (-1)
   with Senv_Lookup_Fail _ -> (-1)
let is_constructor loc depth args_val = match args_val with
=====================================
src/inverse_subst.ml
=====================================
@@ -197,9 +197,10 @@ let rec lookup_inv_subst (i : db_index) (s : subst) : db_index
   | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible
   | S.Identity o -> i - o
   | S.Cons (e, s, o) when pred_var e (fun e -> get_var_db_index e = i - o)
-    -> (try let i'' = lookup_inv_subst (get_var_db_index (get_var e)) s in
-           assert (i'' != 0);
-           raise Ambiguous
+    -> (try
+          let i'' = lookup_inv_subst (get_var_db_index (get_var e)) s in
+          assert (i'' != 0);
+          raise Ambiguous
        with Not_invertible -> 0)
   | S.Cons (e, s, o)
     -> assert (match lexp_lexp' e with Var _ -> true | _ -> e = impossible);
@@ -281,22 +282,18 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp =
   | Call (f, args)
     -> mkCall (apply_inv_subst f s,
               L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args)
-  | Inductive (l, label, args, cases)
-    -> let (s, nargs)
-        = L.fold_left (fun (s, nargs) (ak, v, t)
-                       -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs))
-                      (s, []) args in
-      let nargs = List.rev nargs in
-      let ncases = SMap.map (fun args
-                             -> let (_, ncase)
-                                 = L.fold_left (fun (s, nargs) (ak, v, t)
-                                                -> (ssink v s,
-                                                   (ak, v, apply_inv_subst t s)
-                                                   :: nargs))
-                                               (s, []) args in
-                               L.rev ncase)
-                            cases in
-      mkInductive (l, label, nargs, ncases)
+  | Inductive (l, label, cases)
+    -> let inv_subst_case args =
+         let (_, ncase) =
+           L.fold_left (fun (s, nargs) (ak, v, t)
+                          -> (ssink v s,
+                              (ak, v, apply_inv_subst t s)
+                              :: nargs))
+                         (s, []) args
+         in
+         L.rev ncase
+       in
+       mkInductive (l, label, SMap.map inv_subst_case cases)
   | Cons (it, name) -> mkCons (apply_inv_subst it s, name)
   | Case (l, e, ret, cases, default)
     -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s,
=====================================
src/lexp.ml
=====================================
@@ -37,7 +37,7 @@ module S = Subst
 type vname = U.vname
 type vref = U.vref
 type meta_id = int             (* Identifier of a meta variable.  *)
-
+type location = U.location
 type label = symbol
(*************** Elaboration to Lexp *********************)
@@ -55,9 +55,11 @@ type label = symbol
  * And the type of the 3rd binding is defined in the scope of the
  * surrounded context extended with the first and the second bindings.  *)
+
 type ltype = lexp
  and subst = lexp S.subst
 (* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *)
+ and inductive = location * label * ((arg_kind * vname * ltype) list) SMap.t
  and lexp = lexp' * int
  and lexp' =
    | Imm of sexp                        (* Used for strings, ...  *)
@@ -71,9 +73,7 @@ type ltype = lexp
    | Arrow of arg_kind * vname * ltype * U.location * ltype
    | Lambda of arg_kind * vname * ltype * lexp
    | Call of lexp * (arg_kind * lexp) list (* Curried call.  *)
-   | Inductive of U.location * label
-                  * ((arg_kind * vname * ltype) list) (* formal Args *)
-                  * ((arg_kind * vname * ltype) list) SMap.t
+   | Inductive of inductive
    | Cons of lexp * symbol (* = Type info * ctor_name  *)
    | Case of U.location * lexp
              * ltype (* The type of the return value of all branches *)
@@ -213,15 +213,10 @@ let lexp'_hash (lp : lexp') =
      -> U.combine_hash 8 (U.combine_hash
           (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v))
           (U.combine_hash (lexp_hash t) (lexp_hash e)))
-   | Inductive (l, n, a, cs)
+   | Inductive (l, n, cs)
      -> U.combine_hash 9 (U.combine_hash
           (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n))
-          (U.combine_hash (U.combine_hashes
-            (List.map (fun e -> let (ak, n, lt) = e in
-              (U.combine_hash (Hashtbl.hash ak)
-                (U.combine_hash (Hashtbl.hash n) (lexp_hash lt))))
-            a))
-          (Hashtbl.hash cs)))
+          (Hashtbl.hash cs))
    | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n))
    | Case (l, e, rt, bs, d)
      -> U.combine_hash 11 (U.combine_hash
@@ -270,11 +265,11 @@ let hc_eq e1 e2 =
       | (Call (e1, as1), Call (e2, as2))
         -> e1 == e2 && List.for_all2
         (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2
-      | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2))
-        -> l1 = l2 && List.for_all2
-        (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2
-          && SMap.equal (List.for_all2
-            (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2
+      | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2))
+        -> let datacons_hc_eq (ak1, _, e1) (ak2, _, e2) =
+             ak1 = ak2 && e1 == e2
+           in
+           l1 = l2 && SMap.equal (List.for_all2 datacons_hc_eq) ctor1 ctor2
       | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2
       | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2))
         -> e1 == e2 && r1 == r2 && SMap.equal
@@ -300,18 +295,18 @@ let hc_table : WHC.t = WHC.create 1000
 let hc (l : lexp') : lexp =
     WHC.merge hc_table (l, lexp'_hash l)
-let mkImm s                    = hc (Imm s)
-let mkSortLevel l              = hc (SortLevel l)
-let mkSort (l, s)              = hc (Sort (l, s))
-let mkBuiltin (v, t)        = hc (Builtin (v, t))
-let mkVar v                    = hc (Var v)
-let mkLet (l, ds, e)           = hc (Let (l, ds, e))
-let mkArrow (k, v, t1, l, t2)  = hc (Arrow (k, v, t1, l, t2))
-let mkLambda (k, v, t, e)      = hc (Lambda (k, v, t, e))
-let mkInductive (l, n, a, cs)  = hc (Inductive (l, n, a, cs))
-let mkCons (t, n)              = hc (Cons (t, n))
-let mkCase (l, e, rt, bs, d)   = hc (Case (l, e, rt, bs, d))
-let mkMetavar (n, s, v)        = hc (Metavar (n, s, v))
+let mkImm s                   = hc (Imm s)
+let mkSortLevel l             = hc (SortLevel l)
+let mkSort (l, s)             = hc (Sort (l, s))
+let mkBuiltin (v, t)          = hc (Builtin (v, t))
+let mkVar v                   = hc (Var v)
+let mkLet (l, ds, e)          = hc (Let (l, ds, e))
+let mkArrow (k, v, t1, l, t2) = hc (Arrow (k, v, t1, l, t2))
+let mkLambda (k, v, t, e)     = hc (Lambda (k, v, t, e))
+let mkInductive (l, n, cs)    = hc (Inductive (l, n, cs))
+let mkCons (t, n)             = hc (Cons (t, n))
+let mkCase (l, e, rt, bs, d)  = hc (Case (l, e, rt, bs, d))
+let mkMetavar (n, s, v)       = hc (Metavar (n, s, v))
 let mkCall (f, es) =
   match lexp_lexp' f, es with
     | Call (f', es'), _ -> hc (Call (f', es' @ es))
@@ -385,21 +380,16 @@ let get_var_db_index v =
 let get_var_vname v =
   let (n, idx) = v in n
-let pred_inductive l pred =
+let pred_inductive l (pred : inductive -> bool) =
   match lexp_lexp' l with
-    | Inductive (l, n, a, cs) -> pred (l, n, a, cs)
-    | _ -> false
+  | Inductive inductive -> pred inductive
+  | _ -> false
let get_inductive l =
 match lexp_lexp' l with
-  | Inductive (l, n, a, cs) -> (l, n, a, cs)
+  | Inductive (l, n, cs) -> (l, n, cs)
   | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive "
-let get_inductive_ctor i =
-  let (l, n, a, cs) = i in cs
-
-let is_inductive l = pred_inductive l (fun e -> true)
-
 (********* Helper functions to use the Subst operations  *********)
 (* This basically "ties the knot" between Subst and Lexp.
  * Maybe it would be cleaner to just move subst.ml into lexp.ml
@@ -510,7 +500,7 @@ let rec lexp_location e =
   | Arrow (_,_,_,l,_) -> l
   | Lambda (_,(l,_),_,_) -> l
   | Call (f,_) -> lexp_location f
-  | Inductive (l,_,_,_) -> l
+  | Inductive (l,_,_) -> l
   | Cons (_,(l,_)) -> l
   | Case (l,_,_,_,_) -> l
   | Susp (e, _) -> lexp_location e
@@ -547,21 +537,17 @@ let rec push_susp e s =            (* Push a suspension one level down.  *)
   | Lambda (ak, v, t, e) -> mkLambda (ak, v, mkSusp t s, mkSusp e (ssink v s))
   | Call (f, args) -> mkCall (mkSusp f s,
                              L.map (fun (ak, arg) -> (ak, mkSusp arg s)) args)
-  | Inductive (l, label, args, cases)
-    -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t)
-                                    -> (ssink v s, (ak, v, mkSusp t s) :: nargs))
-                                   (s, []) args in
-      let nargs = List.rev nargs in
-      let ncases = SMap.map (fun args
-                             -> let (_, ncase)
-                                 = L.fold_left (fun (s, nargs) (ak, v, t)
+  | Inductive (l, label, cases)
+    -> let ncases = SMap.map (fun args
+                              -> let (_, ncase)
+                                  = L.fold_left (fun (s, nargs) (ak, v, t)
                                                 -> (ssink v s,
-                                                   (ak, v, mkSusp t s)
+                                                    (ak, v, mkSusp t s)
                                                    :: nargs))
                                                (s, []) args in
-                               L.rev ncase)
-                            cases in
-      mkInductive (l, label, nargs, ncases)
+                                L.rev ncase)
+                             cases in
+       mkInductive (l, label, ncases)
   | Cons (it, name) -> mkCons (mkSusp it s, name)
   | Case (l, e, ret, cases, default)
     -> mkCase (l, mkSusp e s, mkSusp ret s,
@@ -614,21 +600,17 @@ let clean e =
     | Lambda (ak, v, t, e) -> mkLambda (ak, v, clean s t, clean (ssink v s) e)
     | Call (f, args) -> mkCall (clean s f,
                                L.map (fun (ak, arg) -> (ak, clean s arg)) args)
-    | Inductive (l, label, args, cases)
-      -> let (s, nargs) = L.fold_left (fun (s, nargs) (ak, v, t)
-                                    -> (ssink v s, (ak, v, clean s t) :: nargs))
-                                   (s, []) args in
-      let nargs = List.rev nargs in
-      let ncases = SMap.map (fun args
-                             -> let (_, ncase)
-                                 = L.fold_left (fun (s, nargs) (ak, v, t)
-                                                -> (ssink v s,
-                                                   (ak, v, clean s t)
-                                                   :: nargs))
-                                               (s, []) args in
-                               L.rev ncase)
-                            cases in
-      mkInductive (l, label, nargs, ncases)
+    | Inductive (l, label, cases)
+      -> let ncases = SMap.map (fun args
+                                -> let (_, ncase)
+                                     = L.fold_left (fun (s, nargs) (ak, v, t)
+                                                    -> (ssink v s,
+                                                        (ak, v, clean s t)
+                                                        :: nargs))
+                                                   (s, []) args in
+                                   L.rev ncase)
+                               cases in
+         mkInductive (l, label, ncases)
     | Cons (it, name) -> mkCons (clean s it, name)
     | Case (l, e, ret, cases, default)
       -> mkCase (l, clean s e, clean s ret,
@@ -689,7 +671,7 @@ let rec lexp_unparse lxp =
       -> (* (vdef * lexp * ltype) list *)
        let sdecls = List.fold_left
                       (fun acc (vdef, lxp, ltp)
-                       -> Node (Symbol (U.dummy_location, "_=_"),
+                       -> Node (Symbol (U.dummy_location, "_:_"),
                                [Symbol (sname vdef); lexp_unparse ltp])
                          :: Node (Symbol (U.dummy_location, "_=_"),
                                   [Symbol (sname vdef); lexp_unparse lxp])
@@ -703,14 +685,9 @@ let rec lexp_unparse lxp =
       let sargs = List.map (fun (kind, elem) -> lexp_unparse elem) largs in
         Node (lexp_unparse lxp, sargs)
-    | Inductive(loc, label, lfargs, ctors) ->
-      (* (arg_kind * vdef * ltype) list *)
-      (* (arg_kind * pvar * pexp option) list *)
-      let pfargs = List.map (fun (kind, vdef, ltp) ->
-        (kind, sname vdef, Some (lexp_unparse ltp))) lfargs in
-
+    | Inductive (loc, label, ctors) ->
       Node (stypecons,
-            Node (Symbol label, List.map pexp_u_formal_arg pfargs)
+            Symbol label
             :: List.map
                  (fun (name, types)
                   -> Node (Symbol (loc, name),
@@ -783,7 +760,7 @@ and lexp_string lxp = sexp_string (lexp_unparse lxp)
and subst_string s = match s with
   | S.Identity o -> "↑" ^ string_of_int o
-  | S.Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s
+  | S.Cons (l, s, 0) -> lexp_string l ^ " · " ^ subst_string s
   | S.Cons (l, s, o)
     -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"
@@ -943,9 +920,6 @@ and lexp_str ctx (exp : lexp) : string =
     let kind_str k = match k with
       | Anormal -> "->" | Aimplicit -> "=>" | Aerasable -> "≡>" in
-    let kindp_str k =  match k with
-      | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in
-
     let get_name fname =
     match lexp_lexp' fname with
       | Builtin ((_, name), _)   -> name,  0
@@ -968,8 +942,8 @@ 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 (push_susp e subst)
-             | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx))
+              | MVal e -> lexp_str ctx (push_susp e subst)
+              | _ -> "?" ^ maybename name ^ " " ^ subst_string subst ^ index idx)
| Let (_, decls, body)   ->
             (* Print first decls without indent *)
@@ -1026,21 +1000,10 @@ and lexp_str ctx (exp : lexp) : string =
             | _ -> let args = List.fold_left print_arg "" args in
                "(" ^ (lexp_str' fname) ^ args ^ ")")
-        | Inductive (_, (_, name), [], ctors) ->
+        | Inductive (_, (_, name), ctors) ->
             (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^
                 (lexp_str_ctor ctx ctors)
-        | Inductive (_, (_, name), args, ctors)
-          -> let args_str
-              = List.fold_left
-                  (fun str (arg_kind, (_, name), ltype)
-                   -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " "
-                     ^ (lexp_str' ltype) ^ ")")
-                  "" args in
-
-            (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^
-              (lexp_str_ctor ctx ctors)
-
         | Case (_, target, _ret, map, dflt) ->(
             let str = (keyword "case ") ^ (lexp_str' target) in
             let arg_str arg
@@ -1138,11 +1101,11 @@ let rec eq e1 e2 =
     | (Call (e1, as1), Call (e2, as2))
       -> eq e1 e2 && List.for_all2
       (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2
-    | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2))
-      -> l1 = l2 && List.for_all2
-      (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) as1 as2
-        && SMap.equal (List.for_all2
-          (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2)) ctor1 ctor2
+    | (Inductive (_, l1, ctor1), Inductive (_, l2, ctor2))
+      -> let datacons_eq (ak1, _, e1) (ak2, _, e2) =
+           ak1 = ak2 && eq e1 e2
+         in
+         l1 = l2 && SMap.equal (List.for_all2 datacons_eq) ctor1 ctor2
     | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2
     | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2))
       -> eq e1 e2 && eq r1 r2 && SMap.equal
=====================================
src/opslexp.ml
=====================================
@@ -26,6 +26,7 @@ module IMap = U.IMap
 (* open Lexer *)
 open Sexp
 module P = Pexp
+open Pexp
 (* open Myers *)
 (* open Grammar *)
 open Lexp
@@ -196,21 +197,17 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp =
          | _ -> Log.internal_error "" in
        mkCall (DB.eq_refl, [Aerasable, elevel; Aerasable, etype; Aerasable, e]) in
      let reduce it name aargs =
-       let targs = match lexp_lexp' (lexp_whnf_aux it ctx) with
-         | Inductive (_,_,fargs,_) -> fargs
-         | _ -> Log.log_error "Case on a non-inductive type in whnf!"; [] in
+       let () = match lexp_lexp' (lexp_whnf_aux it ctx) with
+         | Inductive _ -> ()
+         | _ -> Log.log_error "Case on a non-inductive type in whnf!" in
        try
          let (_, _, branch) = SMap.find name branches in
-         let (subst, _)
-           = List.fold_left
-               (fun (s, targs) (_, arg) ->
-                 match targs with
-                 | [] -> (S.cons (lexp_whnf_aux arg ctx) s, [])
-                 | _targ::targs ->
-                    (* Ignore the type arguments *)
-                    (s, targs))
-               (S.identity, targs)
-               aargs in
+         let subst =
+           List.fold_left
+             (fun s (_, arg) -> S.cons (lexp_whnf_aux 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_aux (push_susp branch subst) ctx
@@ -322,9 +319,8 @@ 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
   e1' == e2' ||
-    let changed = not (e1 == e1' && e2 == e2') in
-    if changed && set_member_p vs e1' e2' then true else
-    let vs' = if changed then set_add vs e1' e2' else vs in
+    if set_member_p vs e1' e2' then true else
+    let vs' = set_add vs e1' e2' in
     let conv_p = conv_p' ctx vs' in
     match (lexp_lexp' e1', lexp_lexp' e2') with
     | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2
@@ -362,29 +358,23 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
                && (conv_erase && ak1 = P.Aerasable || conv_p t1 t2))
             true args1 args2 in
         conv_p f1 f2 && conv_arglist_p args1 args2
-    | (Inductive (_, l1, args1, cases1), Inductive (_, l2, args2, cases2))
+
+    | (Inductive (_, ((_, name_l) as l1), cases1), Inductive (_, ((_, name_r) as l2), cases2))
       -> let rec conv_fields ctx vs fields1 fields2 =
-          match fields1, fields2 with
-          | ([], []) -> true
-          | ((ak1,vd1,t1)::fields1, (ak2,vd2,t2)::fields2)
-            -> ak1 == ak2 && conv_p' ctx vs t1 t2
-              && conv_fields (DB.lexp_ctx_cons ctx vd1 Variable t1)
-                            (set_shift vs)
-                            fields1 fields2
-          | _,_ -> false in
-        let rec conv_args ctx vs args1 args2 =
-          match args1, args2 with
-          | ([], []) ->
-             (* Args checked alright, now go on with the fields,
-              * using the new context.  *)
-             SMap.equal (conv_fields ctx vs) cases1 cases2
-          | ((ak1,l1,t1)::args1, (ak2,l2,t2)::args2)
-            -> ak1 == ak2 && conv_p' ctx vs t1 t2
-              && conv_args (DB.lexp_ctx_cons ctx l1 Variable t1)
-                          (set_shift vs)
-                          args1 args2
-          | _,_ -> false in
-        l1 == l2 && conv_args ctx vs' args1 args2
+           match fields1, fields2 with
+           | [], [] -> true
+           | (ak1, vd1, t1) :: fields1, (ak2, vd2, t2) :: fields2
+             -> ak1 == ak2
+                && conv_p' ctx vs t1 t2
+                && conv_fields
+                     (DB.lexp_ctx_cons ctx vd1 Variable t1)
+                     (set_shift vs)
+                     fields1
+                     fields2
+           | _, _ -> false
+         in
+         l1 == l2 && SMap.equal (conv_fields ctx vs') cases1 cases2
+
     | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2
     | (Case (_, target1, r1, cases1, def1), Case (_, target2, r2, cases2, def2))
       -> (* FIXME The termination of this case conversion is very
@@ -410,13 +400,11 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
             | Call (f, args) -> (f, args)
             | _ -> (etype, []) in
           (* 2. Build the substitution for the inductive arguments *)
-          let fargs, ctors =
+          let ctors =
             (match lexp'_whnf it ctx with
-             | Inductive (_, _, fargs, constructors)
-               -> fargs, constructors
+             | Inductive (_, _, constructors)
+               -> 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 *)
           let ctx_extend_with_eq ctx subst hlxp =
             let tlxp = mkSusp target subst in
@@ -450,7 +438,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool =
                               vdefs1 vdefs2 fieldtypes
                           else None
                      | _,_,_ -> None in
-                   match mkctx ctx [] fargs_subst (List.length fields1)
+                   match mkctx ctx [] Subst.identity (List.length fields1)
                            fields1 fields2 fieldtypes with
                    | None -> false
                    | Some (nctx, args, _subst) ->
@@ -694,53 +682,42 @@ and check'' erased ctx e =
                                ^ lexp_string ft ^ ")!");
                   ft))
         ft args
-  | Inductive (l, label, args, cases)
-    -> let rec arg_loop ctx erased args =
-        match args with
-        | []
-          -> let level
-              = SMap.fold
-                  (fun _ case level ->
-                    let (level, _, _, _) =
-                      List.fold_left
-                        (fun (level, ictx, erased, n) (ak, v, t) ->
-                          ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in
-                            match lexp_lexp' lwhnf with
-                            | Sort (_, Stype _)
-                                 when ak == P.Aerasable && impredicative_erase
-                              -> level
-                            | Sort (_, Stype level')
-                              -> mkSLlub ctx level
-                                  (* We need to unshift because the final type
-                                   * cannot refer to the fields!  *)
-                                  (* FIXME: If it does refer,
-                                   * we get an ugly error! *)
-                                  (mkSusp level' (L.sunshift n))
-                            | tt -> error_tc ~loc:(lexp_location t)
-                                      ~print_action:(fun _ ->
-                                        DB.print_lexp_ctx ictx; print_newline ()
-                                      )
-                                      ("Field type "
-                                       ^ lexp_string t
-                                       ^ " is not a Type! ("
-                                       ^ lexp_string lwhnf ^")");
-                                    level),
-                           DB.lctx_extend ictx v Variable t,
-                           DB.set_sink 1 erased,
-                           n + 1))
-                        (level, ctx, erased, 0)
-                        case in
-                    level)
-                  cases (mkSortLevel SLz) in
-            mkSort (l, Stype level)
-        | (ak, v, t)::args
-          -> let _k = check_type DB.set_empty ctx t in
-            mkArrow (ak, v, t, lexp_location t,
-                     arg_loop (DB.lctx_extend ctx v Variable t)
-                              (dbset_push ak erased)
-                              args) in
-      let tct = arg_loop ctx erased args in
-      tct
+  | Inductive (l, label, cases)
+    -> let level
+         = SMap.fold
+             (fun _ case level ->
+               let (level, _, _, _) =
+                 List.fold_left
+                   (fun (level, ictx, erased, n) (ak, v, t) ->
+                     ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in
+                       match lexp_lexp' lwhnf with
+                       | Sort (_, Stype _)
+                            when ak == P.Aerasable && impredicative_erase
+                         -> level
+                       | Sort (_, Stype level')
+                         -> mkSLlub ctx level
+                                    (* We need to unshift because the final type
+                                     * cannot refer to the fields!  *)
+                                    (* FIXME: If it does refer,
+                                     * we get an ugly error! *)
+                                    (mkSusp level' (L.sunshift n))
+                       | tt -> error_tc ~loc:(lexp_location t)
+                                        ~print_action:(fun _ ->
+                                          DB.print_lexp_ctx ictx; print_newline ()
+                                        )
+                                        ("Field type "
+                                         ^ lexp_string t
+                                         ^ " is not a Type! ("
+                                         ^ lexp_string lwhnf ^")");
+                               level),
+                      DB.lctx_extend ictx v Variable t,
+                      DB.set_sink 1 erased,
+                      n + 1))
+                   (level, ctx, erased, 0)
+                   case in
+               level)
+             cases (mkSortLevel SLz) in
+       mkSort (l, Stype level)
   | Case (l, e, ret, branches, default)
     (* FIXME: Check that the return type isn't TypeLevel.  *)
     -> let call_split e =
@@ -757,17 +734,13 @@ and check'' erased ctx e =
                   "Target lexp's kind is not a sort"; DB.level0 in
       let it, aargs = call_split etype in
       (match lexp'_whnf it ctx, aargs with
-       | Inductive (_, _, fargs, constructors), aargs ->
-          let rec mksubst s fargs aargs =
-            match fargs, aargs with
-            | [], [] -> s
-            | _farg::fargs, (_ak, aarg)::aargs
-              (* We don't check aarg's type, because we assume that `check`
-               * returns a valid type.  *)
-              -> mksubst (S.cons aarg s) fargs aargs
-            | _,_ -> (error_tc ~loc:l
-                                 "Wrong arg number to inductive type!"; s) in
-          let s = mksubst S.identity fargs aargs in
+       | Inductive (_, _, constructors), aargs ->
+          let () = match aargs with
+            | [] -> ()
+            | _
+              -> let message = "Wrong arg number to inductive type!" in
+                 error_tc ~loc:l message
+          in
           let ctx_extend_with_eq ctx subst hlxp nerased =
             let tlxp = mkSusp e subst in
             let tltp = mkSusp etype subst in
@@ -802,7 +775,7 @@ and check'' erased ctx e =
                  mkCall (mkCons (it, (l, name)),
                          List.map (fun (_, a) -> (P.Aerasable, a)) aargs) in
                let (nerased, nctx, hlxp) =
-                 mkctx erased ctx s hctor vdefs fieldtypes in
+                 mkctx erased ctx Subst.identity hctor vdefs fieldtypes in
                let subst = S.shift (List.length vdefs) in
                let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp nerased in
                assert_type nctx branch
@@ -830,29 +803,18 @@ and check'' erased ctx e =
       ret
   | Cons (t, (l, name))
     -> (match lexp'_whnf t ctx with
-        | Inductive (l, _, fargs, constructors)
+        | Inductive (l, _, constructors)
          -> (try
               let fieldtypes = SMap.find name constructors in
-              let rec indtype fargs start_index =
-                match fargs with
-                | [] -> []
-                | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index))
-                                       :: indtype fargs (start_index - 1) in
               let rec fieldargs ftypes =
                 match ftypes with
-                | [] -> let nargs = List.length fieldtypes + List.length fargs in
-                       mkCall (mkSusp t (S.shift nargs),
-                               indtype fargs (nargs - 1))
+                | [] -> let nargs = List.length fieldtypes in
+                       mkCall (mkSusp t (S.shift nargs), [])
                 | (ak, vd, ftype) :: ftypes
                   -> mkArrow (ak, vd, ftype, lexp_location ftype,
-                             fieldargs ftypes) in
-              let rec buildtype fargs =
-                match fargs with
-                | [] -> fieldargs fieldtypes
-                | (ak, ((l,_) as vd), atype) :: fargs
-                  -> mkArrow (P.Aerasable, vd, atype, l,
-                             buildtype fargs) in
-              buildtype fargs
+                             fieldargs ftypes)
+              in
+              fieldargs fieldtypes
             with Not_found
                  -> (error_tc ~loc:l
                                 ("Constructor "" ^ name ^ "" does not exist");
@@ -939,23 +901,19 @@ and fv (e : lexp) : (DB.set * mv_set) =
                                     then fv_erase afvs
                                     else afvs))
                        (fv f) args
-    | Inductive (_, _, args, cases)
-      -> let alen = List.length args in
-        let s
-          = List.fold_left (fun s (_, _, t)
-                            -> fv_sink 1 (fv_union s (fv t)))
-                           fv_empty args in
-        let s
-          = SMap.fold
-              (fun _ fields s
-               -> fv_union
+    | Inductive (_, _, cases)
+      -> let s =
+           SMap.fold
+             (fun _ fields s
+              -> fv_union
                    s
                    (fv_hoist (List.length fields)
                              (List.fold_left (fun s (_, _, t)
                                               -> fv_sink 1 (fv_union s (fv t)))
                                              fv_empty fields)))
-              cases s in
-        fv_hoist alen s
+             cases fv_empty
+         in
+         fv_hoist 0 s
     | Cons (t, _) -> fv_erase (fv t)
     | Case (_, e, t, cases, def)
       -> let s = fv_union (fv e) (fv_erase (fv t)) in
@@ -1020,67 +978,48 @@ and get_type ctx e =
              -> mkSusp t2 (S.substitute arg)
            | _ -> ft)
         ft args
-  | Inductive (l, label, args, cases)
+  | Inductive (l, label, cases)
     (* FIXME: Use `check` here but silencing errors?  *)
-    -> let rec arg_loop args ctx =
-        match args with
-        | []
-          -> let level
-              = SMap.fold
-                  (fun _ case level ->
-                    let (level, _, _) =
-                      List.fold_left
-                        (fun (level, ictx, n) (ak, v, t) ->
-                          ((match lexp'_whnf (get_type ictx t) ictx with
-                            | Sort (_, Stype _)
-                                 when ak == P.Aerasable && impredicative_erase
-                              -> level
-                            | Sort (_, Stype level')
-                              -> mkSLlub ctx level
-                                  (* We need to unshift because the final type
-                                   * cannot refer to the fields!  *)
-                                  (mkSusp level' (L.sunshift n))
-                            | tt -> level),
-                           DB.lctx_extend ictx v Variable t,
-                           n + 1))
-                        (level, ctx, 0)
-                        case in
-                    level)
-                  cases (mkSortLevel SLz) in
-            mkSort (l, Stype level)
-        | (ak, v, t)::args
-          -> mkArrow (ak, v, t, lexp_location t,
-                     arg_loop args (DB.lctx_extend ctx v Variable t)) in
-      let tct = arg_loop args ctx in
-      tct
+    -> let level
+         = SMap.fold
+             (fun _ case level ->
+               let (level, _, _) =
+                 List.fold_left
+                   (fun (level, ictx, n) (ak, v, t) ->
+                     ((match lexp'_whnf (get_type ictx t) ictx with
+                       | Sort (_, Stype _)
+                            when ak == P.Aerasable && impredicative_erase
+                         -> level
+                       | Sort (_, Stype level')
+                         -> mkSLlub ctx level
+                                    (* We need to unshift because the final type
+                                     * cannot refer to the fields!  *)
+                                    (mkSusp level' (L.sunshift n))
+                       | tt -> level),
+                      DB.lctx_extend ictx v Variable t,
+                      n + 1))
+                   (level, ctx, 0)
+                   case in
+               level)
+             cases (mkSortLevel SLz) in
+       mkSort (l, Stype level)
   | Case (l, e, ret, branches, default) -> ret
   | Cons (t, (l, name))
     -> (match lexp'_whnf t ctx with
-       | Inductive (l, _, fargs, constructors)
-         -> (try
-              let fieldtypes = SMap.find name constructors in
-              let rec indtype fargs start_index =
-                match fargs with
-                | [] -> []
-                | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index))
-                                       :: indtype fargs (start_index - 1) in
-              let rec fieldargs ftypes =
-                match ftypes with
-                | [] -> let nargs = List.length fieldtypes + List.length fargs in
-                       mkCall (mkSusp t (S.shift nargs),
-                               indtype fargs (nargs - 1))
-                | (ak, vd, ftype) :: ftypes
-                  -> mkArrow (ak, vd, ftype, lexp_location ftype,
-                             fieldargs ftypes) in
-              let rec buildtype fargs =
-                match fargs with
-                | [] -> fieldargs fieldtypes
-                | (ak, ((l,_) as vd), atype) :: fargs
-                  -> mkArrow (P.Aerasable, vd, atype, l,
-                             buildtype fargs) in
-              buildtype fargs
-            with Not_found -> DB.type_int)
-       | _ -> DB.type_int)
+        | Inductive (l, _, constructors)
+          -> (try
+                let fieldtypes = SMap.find name constructors in
+                let rec fieldargs ftypes =
+                  match ftypes with
+                  | [] -> let nargs = List.length fieldtypes in
+                          mkCall (mkSusp t (S.shift nargs),
+                                  [])
+                  | (ak, vd, ftype) :: ftypes
+                    -> mkArrow (ak, vd, ftype, lexp_location ftype,
+                                fieldargs ftypes) in
+                fieldargs fieldtypes
+              with Not_found -> DB.type_int)
+        | _ -> DB.type_int)
   | Metavar (idx, s, _)
     -> (match metavar_lookup idx with
        | MVal e -> get_type ctx (push_susp e s)
@@ -1122,11 +1061,11 @@ let rec erase_type (lxp: lexp): E.elexp =
         | L.Susp(l, s)                -> erase_type (L.push_susp l s)
(* To be thrown out *)
-        | L.Arrow _                   -> E.Type lxp
-        | L.SortLevel _               -> E.Type lxp
-        | L.Sort _                    -> E.Type lxp
+        | L.Arrow _                 -> E.Type lxp
+        | L.SortLevel _             -> E.Type lxp
+        | L.Sort _                  -> E.Type lxp
         (* Still useful to some extent.  *)
-        | L.Inductive(l, label, _, _) -> E.Type lxp
+        | L.Inductive (l, label, _) -> E.Type lxp
         | L.Metavar (idx, s, _)
           -> (match metavar_lookup idx with
              | MVal e -> erase_type (push_susp e s)
@@ -1207,7 +1146,7 @@ let ctx2tup ctx nctx =
         let types = List.rev types in
         (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*)
-        mkCall (mkCons (mkInductive (loc, type_label, [],
+        mkCall (mkCons (mkInductive (loc, type_label,
                                SMap.add cons_name
                                  (List.map (fun (oname, t)
                                             -> (P.Aimplicit, oname,
=====================================
src/pexp.ml
=====================================
@@ -54,8 +54,10 @@ let pexp_u_formal_arg (arg : arg_kind * pvar * sexp option) =
             [Symbol s; match t with Some e -> e
                                   | None -> Symbol (l, "_")])
-let pexp_p_pat_arg (s : sexp) = match s with
-  | Symbol (l , n) -> (None, (l, match n with "_" -> None | _ -> Some n))
+let pexp_p_pat_arg (s : sexp) =
+  print_endline ("+[pexp_p_pat_arg] s = " ^ sexp_string s);
+  match s with
+  | Symbol (l, n) -> (None, (l, match n with "_" -> None | _ -> Some n))
   | Node (Symbol (_, "_:=_"), [Symbol f; Symbol (l,n)])
     -> (Some f, (l, Some n))
   | _ -> let loc = sexp_location s in
@@ -69,7 +71,9 @@ let pexp_u_pat_arg ((okn, (l, oname)) : symbol option * vname) : sexp =
   | Some ((l,_) as n) ->
      Node (Symbol (l, "_:=_"), [Symbol n; pname])
-let pexp_p_pat (s : sexp) : ppat = match s with
+let pexp_p_pat (s : sexp) : ppat =
+  print_endline ("+[pexp_p_pat] s = " ^ sexp_string s);
+  match s with
   | Symbol (l, n) -> Ppatsym (l, match n with "_" -> None | _ -> Some n)
   | Node (c, args)
     -> Ppatcons (c, List.map pexp_p_pat_arg args)
=====================================
src/unification.ml
=====================================
@@ -79,13 +79,13 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with
         | Lambda (_, _, t, e) -> oi t || oi e
         | Call (f, args)
           -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args
-        | Inductive (_, _, args, cases)
+        | Inductive (_, _, cases)
           -> SMap.fold
               (fun _ fields o
                -> List.fold_left (fun o (_, _, t) -> o || oi t)
                    o fields)
               cases
-              (List.fold_left (fun o (_, _, t) -> o || oi t) false args)
+              false
         | Cons (t, _) -> oi t
         | Case (_, e, t, cases, def)
           -> let o = oi e || oi t in
@@ -203,6 +203,8 @@ and unify' (e1: lexp) (e2: lexp)
   if e1 == e2 then [] else
   let e1' = OL.lexp_whnf e1 ctx in
   let e2' = OL.lexp_whnf e2 ctx in
+  print_endline ("[unify'] e1' = " ^ lexp_string e1');
+  print_endline ("[unify'] e2' = " ^ lexp_string e2');
   if e1' == e2' then [] else
   let changed = true (* not (e1 == e1' && e2 == e2') *) in
   if changed && OL.set_member_p vs e1' e2' then [] else
@@ -296,6 +298,10 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type =
 *)
 and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
     : return_type =
+
+  print_endline ("[unify_metavar] lxp1 = " ^ lexp_string lxp1);
+  print_endline ("[unify_metavar] lxp2 = " ^ lexp_string lxp2);
+
   let unif idx s lxp =
     let t = match metavar_lookup idx with
       | MVal _ -> Log.internal_error
@@ -410,6 +416,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp)
 *)
 and unify_var (var: lexp) (lxp: lexp) ctx vs
     : return_type =
+  print_endline ("[unify_var] var = " ^ lexp_string var);
+  print_endline ("[unify_var] lxp = " ^ lexp_string lxp);
   match (lexp_lexp' var, lexp_lexp' lxp) with
   | (Var _, Var _) when OL.conv_p ctx var lxp -> []
   | (_, _) -> [(CKresidual, ctx, var, lxp)]
@@ -565,12 +573,12 @@ and is_same arglist arglist2 =
and unify_inductive lxp1 lxp2 ctx vs =
   match lexp_lexp' lxp1, lexp_lexp' lxp2 with
-  | (Inductive (_loc1, label1, args1, consts1),
-     Inductive (_loc2, label2, args2, consts2))
-    -> unify_inductive' ctx vs args1 args2 consts1 consts2 lxp1 lxp2
+  | (Inductive (_loc1, label1, consts1),
+     Inductive (_loc2, label2, consts2))
+    -> unify_inductive' ctx vs consts1 consts2 lxp1 lxp2
   | _, _ -> [(CKimpossible, ctx, lxp1, lxp2)]
-and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 =
+and unify_inductive' ctx vs 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)])
@@ -582,7 +590,6 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 =
                            else (unify' t1 t2 ctx vs) @ residue))
           (ctx, vs, [])
           (List.combine args1 args2) in
-  let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in
   if not (SMap.cardinal consts1 == SMap.cardinal consts2) then
     [(CKimpossible, ctx, e1, e2)]
   else
@@ -592,7 +599,7 @@ and unify_inductive' ctx vs args1 args2 consts1 consts2 e1 e2 =
                              = unif_formals ctx vs args1 args2 in
                            residue' @ residue
                  | exception Not_found -> [(CKimpossible, ctx, e1, e2)])
-      consts1 residue
+      consts1 []
(** unify the SMap of list in Inductive *)
 (* and unify_induct_sub_list l1 l2 subst =
=====================================
tests/opslexp_test.ml
=====================================
@@ -0,0 +1,72 @@
+(* Copyright (C) 2020  Free Software Foundation, Inc.
+ *
+ * Author: Simon Génier simon.genier@umontreal.ca
+ * Keywords: languages, lisp, dependent types.
+ *
+ * This file is part of Typer.
+ *
+ * Typer is free software; you can redistribute it and/or modify it under the
+ * terms of the GNU General Public License as published by the Free Software
+ * Foundation, either version 3 of the License, or (at your option) any later
+ * version.
+ *
+ * Typer is distributed in the hope that it will be useful, but WITHOUT ANY
+ * WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
+ * FOR A PARTICULAR PURPOSE.  See the GNU General Public License for more
+ * details.
+ *
+ * You should have received a copy of the GNU General Public License along
+ * with this program.  If not, see http://www.gnu.org/licenses/. *)
+
+open Utest_lib
+open Util
+
+let assert_conv_p
+      (name : string)
+      ?(setup : string option)
+      ?(close : bool = false)
+      (l : string)
+      (r : string)
+    : unit =
+
+  let run () =
+    let ectx = Elab.default_ectx in
+    let ectx =
+      match setup with
+      | Some setup' -> snd (Elab.lexp_decl_str setup' ectx)
+      | None -> ectx
+    in
+    let last_metavar = !Unification.global_last_metavar in
+
+    let ls = Elab.lexp_expr_str l ectx in
+    Unification.global_last_metavar := last_metavar;
+    let rs = Elab.lexp_expr_str r ectx in
+
+    let lctx = Debruijn.ectx_to_lctx ectx in
+    let l' =
+      match ls with
+      | [l'] -> l'
+      | _ -> failwith "expected a single lexp"
+    in
+    let r' =
+      match rs with
+      | [r'] -> if close then Opslexp.lexp_close lctx r' else r'
+      | _ -> failwith "expected a single lexp"
+    in
+
+    if Opslexp.conv_p lctx l' r' then success else failure
+  in
+  add_test "OPSLEXP" name run
+
+let () =
+  assert_conv_p
+    "Inductive type is convertible to its closure."
+    ~setup:{|
+      List* : (ℓ : TypeLevel) ≡> Type_ ℓ -> Type_ ℓ;
+      List* = lambda ℓ ≡> lambda α -> typecons List* (nil*) (cons* α (List* (ℓ := ℓ) α));
+    |}
+    ~close:true
+    "List* Sexp"
+    "List* Sexp";
+
+  run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/71f837603183489fa3d925646634a66271...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/71f837603183489fa3d925646634a66271...
You're receiving this email because of your account on gitlab.com.





    