Cleaner quantifiers for type classes, breaks clrewrite for the moment but implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 196 insertions, 123 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index e6ea17b47..b1d08f5d2 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -25,6 +25,7 @@ open Typeclasses_errors
 open Termops
 open Decl_kinds
 open Entries
+open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
 
@@ -78,11 +79,27 @@ let type_ctx_instance isevars env ctx inst subst =
 	(na, c) :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
+let type_class_instance_params isevars env id n ctx inst subst =
+  List.fold_left2
+    (fun (subst, instctx) (na, _, t) ce ->
+      let t' = replace_vars subst t in
+      let c = 
+(* 	if ce = CHole (dummy_loc) then *)
+(* 	  (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
+(* 	     in instance search. *\) *)
+(* 	  Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
+(* 	else *)
+	  interp_casted_constr_evars isevars env ce t' 
+      in
+      let d = na, Some c, t' in
+	(na, c) :: subst, d :: instctx)
+    (subst, []) (List.rev ctx) inst
+
 let substitution_of_constrs ctx cstrs =
   List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
 
-let new_instance sup  (instid, bk, cl) props =
-  let id, par = Implicit_quantifiers.destClassApp cl in
+let new_instance sup (instid, bk, cl) props =
+  let id, par = Implicit_quantifiers.destClassAppExpl cl in
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let avoid = Termops.ids_of_context env in
@@ -97,7 +114,7 @@ let new_instance sup  (instid, bk, cl) props =
       let g l = not (List.exists (fun ((_, y), _, _) -> y = Name x) l) in
 	f gen_ctx && g sup
     in
-    let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) par in
+    let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) (List.map fst par) in
     let parbinders' = List.filter is_free parbinders in
       gen_ctx @ parbinders'
   in
@@ -105,28 +122,35 @@ let new_instance sup  (instid, bk, cl) props =
   let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in
 
   let subst =
+    let cl_context = List.map snd k.cl_context in
     match bk with
       | Explicit ->
-	  if List.length par <> List.length k.cl_context + List.length k.cl_params then 
-	    Classes.mismatched_params env par (k.cl_params @ k.cl_context);
-	  let len = List.length k.cl_context in
-	  let ctx, par = Util.list_chop len par in
-	  let subst, _ = type_ctx_instance isevars env' k.cl_context ctx [] in
-	  let subst = Typeclasses.substitution_of_named_context isevars env' k.cl_name len subst 
-	    k.cl_super
-	  in
-	  let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst
+	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
+	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
+	    if needlen <> applen then 
+	      Classes.mismatched_params env (List.map fst par) cl_context;
+	    let pars, _ = Implicit_quantifiers.combine_params Idset.empty (* need no avoid *)
+	      (fun avoid (clname, (id, _, t)) -> 
+		match clname with 
+		    Some _ -> CHole (Util.dummy_loc), avoid
+		  | None -> failwith ("new instance: under-applied typeclass"))
+	      par (List.rev k.cl_context)
+	    in
+	    let subst, _ = type_class_instance_params isevars env' (snd id) 0 cl_context pars [] in
+	      subst
 
       | Implicit ->
-	  let t' = interp_type_evars isevars env' (Topconstr.mkAppC (CRef (Ident id), par)) in
+	  let t' = interp_type_evars isevars env' (Topconstr.CApp (Util.dummy_loc, (None, CRef (Ident id)), par)) in
 	    match kind_of_term t' with 
 		App (c, args) -> 
-		  substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context) 
+		  substitution_of_constrs cl_context
 		    (List.rev (Array.to_list args))
 	      | _ -> assert false
   in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
+  isevars := resolve_typeclasses ~check:false env sigma !isevars;
+  let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
   let subst, _propsctx = 
     let props = 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 4799eb7b3..162591872 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -94,19 +94,36 @@ let ids_of_named_context_avoiding avoid l =
     let id' = next_ident_away_from id avoid in id' :: ids, Idset.add id' avoid) 
     ([], avoid) (Termops.ids_of_named_context l)
     
-let combine_params avoid applied needed =
+let combine_params avoid fn applied needed =
   let rec aux ids avoid app need =
     match app, need with
 	[], need -> 
-	  let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in
-	    List.rev ids @ (List.rev_map mkIdentC need'), avoid
-      | _, (true, (id, _, _)) :: need -> 
-	  let id' = next_ident_away_from id avoid in
-	    aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need
-      | x :: app, (false, _) :: need -> aux (x :: ids) avoid app need    
+	  let need', avoid = 
+	    List.fold_left (fun (terms, avoid) decl -> 
+	      let t', avoid = fn avoid decl in
+		(t' :: terms, avoid))
+	      ([], avoid) need
+	  in List.rev ids @ (List.rev need'), avoid
+
+      | (x, Some (loc, ExplByName id')) :: app, (Some _, (id, _, _)) :: need when id' = id -> 
+	  aux (x :: ids) avoid app need
+
+      | _, (Some cl, (id, _, _) as d) :: need -> 
+	  let t', avoid' = fn avoid d in
+	    aux (t' :: ids) avoid' app need
+
+      | x :: app, (None, _) :: need -> aux (fst x :: ids) avoid app need    
+
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
   in aux [] avoid applied needed
 
+let combine_params_freevar avoid applied needed =
+  combine_params avoid
+    (fun avoid (_, (id, _, _)) -> 
+      let id' = next_ident_away_from id avoid in
+	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
+    applied needed
+
 let compute_context_vars env l =
   List.fold_left (fun avoid (iid, _, c) -> 
     (match snd iid with Name i -> [i] | Anonymous -> []) @ (free_vars_of_constr_expr c ~bound:env avoid))
@@ -117,6 +134,11 @@ let destClassApp cl =
     | CApp (loc, (None,CRef (Ident f)), l) -> f, List.map fst l
     | _ -> raise Not_found
 
+let destClassAppExpl cl =
+  match cl with
+    | CApp (loc, (None,CRef (Ident f)), l) -> f, l
+    | _ -> raise Not_found
+
 let ids_of_list l = 
   List.fold_right Idset.add l Idset.empty
 
@@ -126,14 +148,10 @@ let full_class_binders env l =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
 	  Explicit -> 
-	    let (id, l) = destClassApp cl in
+	    let (id, l) = destClassAppExpl cl in
 	      (try
 		  let c = class_info (snd id) in
-		  let args, avoid = combine_params avoid l 
-		    (List.rev_map (fun x -> false, x) c.cl_context @ 
-			List.rev_map (fun x -> true, x) c.cl_super @ 
-			List.rev_map (fun x -> false, x) c.cl_params) 
-		  in
+		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
 		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
 		with Not_found -> unbound_class (Global.env ()) id)
 	| Implicit -> (x :: l', avoid))
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d687fe640..3e26b6c72 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -24,6 +24,7 @@ open Typeclasses
 (*i*)
 
 val destClassApp : constr_expr -> identifier located * constr_expr list
+val destClassAppExpl : constr_expr -> identifier located * (constr_expr * explicitation located option) list
 
 val free_vars_of_constr_expr :     Topconstr.constr_expr ->
     ?bound:Idset.t ->
@@ -49,6 +50,13 @@ val nf_named_context : evar_map -> named_context -> named_context
 val nf_rel_context : evar_map -> rel_context -> rel_context
 val nf_env : evar_map -> env -> env
 
+val combine_params : Names.Idset.t ->
+  (Names.Idset.t -> Names.identifier option * (Names.identifier * Term.constr option * Term.types) ->
+    Topconstr.constr_expr * Names.Idset.t) ->
+  (Topconstr.constr_expr * Topconstr.explicitation located option) list ->
+  (Names.identifier option * Term.named_declaration) list ->
+  Topconstr.constr_expr list * Names.Idset.t
+
 
 val ids_of_named_context_avoiding :     Names.Idset.t ->
     Sign.named_context -> Names.Idset.elt list * Names.Idset.t
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index a7d905032..bd6c15ffa 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -102,7 +102,7 @@ let lpar_id_coloneq =
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let typeclass_constraint typeclass_param pattern;
+  binder binder_let binders_let typeclass_constraint pattern;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -359,11 +359,11 @@ GEXTEND Gram
   ;
   typeclass_constraint:
     [ [ id=identref ; cl = LIST1 typeclass_param -> 
-      (loc, Anonymous), Explicit, mkAppC (mkIdentC (snd id), cl)
+      (loc, Anonymous), Explicit, CApp (loc, (None, mkIdentC (snd id)), cl)
     | "?" ; id=identref ; cl = LIST1 typeclass_param -> 
-	(loc, Anonymous), Implicit, mkAppC (mkIdentC (snd id), cl)
+	(loc, Anonymous), Implicit, CApp (loc, (None, mkIdentC (snd id)), cl)
     | iid=identref ; ":" ; id=typeclass_name ; cl = LIST1 typeclass_param -> 
-	(fst iid, Name (snd iid)), (fst id), mkAppC (mkIdentC (snd (snd id)), cl)
+	(fst iid, Name (snd iid)), (fst id), CApp (loc, (None, mkIdentC (snd (snd id))), cl)
     ] ]
   ;
   typeclass_name:
@@ -371,10 +371,14 @@ GEXTEND Gram
     | "?"; id = identref -> (Implicit, id)
     ] ]
   ;
+
   typeclass_param: 
-    [ [ id = identref -> CRef (Libnames.Ident id)
-    | c = sort -> CSort (loc, c)
-    | "("; c = lconstr; ")" -> c ] ]
+    [ [ id = identref -> CRef (Libnames.Ident id), None
+    | c = sort -> CSort (loc, c), None
+    | id = lpar_id_coloneq; c=lconstr; ")" ->
+	(c,Some (loc,ExplByName id))
+    | c=operconstr LEVEL "9" -> c, None
+    ] ]
   ;
   type_cstr:
     [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ee2036167..540d1aac0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -436,7 +436,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)   
 GEXTEND Gram
-  GLOBAL: gallina_ext typeclass_param;
+  GLOBAL: gallina_ext;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -472,9 +472,15 @@ GEXTEND Gram
          t = class_rawexpr ->
 	  VernacCoercion (Global, qid, s, t)
 
+      (* Type classes, new syntax without artificial sup. *)
+      | IDENT "Class"; qid = identref; pars = binders_let;
+	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
+	 props = typeclass_field_types ->
+	   VernacClass (qid, pars, s, [], props)
+
       (* Type classes *)
-      | IDENT "Class"; sup = OPT [ l = typeclass_context; "=>" -> l ];
-	 qid = identref; pars = LIST0 typeclass_param_type;
+      | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ];
+	 qid = identref; pars = binders_let;
 	 s = [ ":"; c = sort -> loc, c | -> (loc,Rawterm.RType None) ];
 	 props = typeclass_field_types ->
 	   VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
@@ -517,10 +523,10 @@ GEXTEND Gram
     | "["; "!"; id = ident; "]" -> (id,true,true) 
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
-  typeclass_param_type:
-    [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t 
-    | id = identref -> id, CHole loc ] ]
-  ;
+(*   typeclass_param_type: *)
+(*     [ [ "(" ; id = identref; ":"; t = lconstr ; ")" -> id, t  *)
+(*     | id = identref -> id, CHole loc ] ] *)
+(*   ; *)
   typeclass_field_type:
     [ [ id = identref; ":"; t = lconstr -> id, t ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 56d547cb5..2430b8863 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -436,7 +436,6 @@ module Constr =
     let binder_let = Gram.Entry.create "constr:binder_let"
     let binders_let = Gram.Entry.create "constr:binders_let"
     let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint"
-    let typeclass_param = Gram.Entry.create "constr:typeclass_param"
   end
 
 module Module =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index eaf298e06..89bdf13eb 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -165,7 +165,6 @@ module Constr :
     val binder_let : local_binder Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
-    val typeclass_param : constr_expr Gram.Entry.e
   end
 
 module Module : 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1470f6902..0b889bf08 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -696,7 +696,8 @@ let rec pr_vernac = function
   | VernacClass (id, par, ar, sup, props) ->
       hov 1 (
 	str"Class" ++ spc () ++ pr_lident id ++
-	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++ 
+(* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *)
+	  pr_and_type_binders_arg par ++
 	  spc () ++ str":" ++ spc() ++ pr_rawsort (snd ar) ++
 	  spc () ++ str"where" ++ spc () ++
 	  prlist_with_sep (fun () -> str";" ++ spc()) (pr_lident_constr (spc () ++ str":" ++ spc())) props )
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 306ef3a19..e253410de 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -29,13 +29,19 @@ type rels = constr list
 
 (* This module defines type-classes *)
 type typeclass = {
-  cl_name : identifier; (* Name of the class *)
-  cl_context : named_context; (* Context in which superclasses and params are typed (usually types) *)
-  cl_super : named_context; (* Superclasses applied to some of the params *)
-  cl_params : named_context; (* Context of the parameters (usually types) *)
-(*   cl_defs : named_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
-  cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
-  cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *)
+  (* Name of the class. FIXME: should not necessarily be globally unique. *)
+  cl_name : identifier;
+
+  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
+  cl_context : (identifier option * named_declaration) list; 
+
+  cl_params: int;
+
+  (* Context of definitions and properties on defs, will not be shared *)
+  cl_props : named_context;
+
+  (* The class implementation: a record parameterized by the context with defs in it. *)
+  cl_impl : inductive; 
 }
 
 type typeclasses = (identifier, typeclass) Gmap.t
@@ -118,11 +124,14 @@ let subst (_,subst,(cl,m,inst)) =
       (na, Option.smartmap do_subst b, do_subst t))
       ctx
   in
+  let do_subst_ctx ctx = 
+    List.map (fun (cl, (na, b, t)) ->
+      (cl, (na, Option.smartmap do_subst b, do_subst t)))
+      ctx
+  in
   let subst_class cl = 
     let cl' = { cl with cl_impl = do_subst_ind cl.cl_impl;
-		cl_context = do_subst_named cl.cl_context;
-		cl_super = do_subst_named cl.cl_super;
-		cl_params = do_subst_named cl.cl_params;
+		cl_context = do_subst_ctx cl.cl_context;
 		cl_props = do_subst_named cl.cl_props; }
     in if cl' = cl then cl else cl'
   in
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f53ea7bea..47cb93a14 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -23,22 +23,25 @@ open Util
 
 (* This module defines type-classes *)
 type typeclass = {
-  cl_name : identifier; (* Name of the class *)
-  cl_context : named_context; (* Context in which superclasses and params are typed (usually types and indirect superclasses) *)
-  cl_super : named_context; (* Direct superclasses applied to some of the params *)
-  cl_params : named_context; (* Context of the real parameters (types and operations) *)
-(*   cl_defs : rel_context; (\* Context of the definitions (usually functions), which may be shared *\) *)
-  cl_props : named_context; (* Context of the properties on defs, in Prop, will not be shared *)
-  cl_impl : inductive; (* The class implementation: a record parameterized by params and defs *)
+  (* Name of the class. FIXME: should not necessarily be globally unique. *)
+  cl_name : identifier;
+
+  (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
+  cl_context : (identifier option * named_declaration) list; 
+
+  cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
+
+  (* Context of definitions and properties on defs, will not be shared *)
+  cl_props : named_context;
+
+  (* The class implementation: a record parameterized by the context with defs in it. *)
+  cl_impl : inductive; 
 }
 
 type instance = {
   is_class: typeclass;
   is_name: identifier; (* Name of the instance *)
-(*   is_params: named_context; (\* Context of the parameters, instanciated *\) *)
-(*   is_super: named_context; (\* The corresponding superclasses *\) *)
   is_impl: constant; 
-(*   is_add_hint : unit -> unit; (\* Hook to add an hint for the instance *\) *)
 }
   
 val instances : Libnames.reference -> instance list
diff --git a/tactics/class_setoid.ml4 b/tactics/class_setoid.ml4
index 9111ba97e..fee38a629 100644
--- a/tactics/class_setoid.ml4
+++ b/tactics/class_setoid.ml4
@@ -112,16 +112,17 @@ let resolve_morphism env sigma direction oldt m args args' =
 	try 
 	  List.iter (fun ((cl, proj), n) ->
 	    evars := Evd.create_evar_defs Evd.empty;
-	    let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] cl.cl_context in
+	    let cl_param, cl_context = match cl.cl_context with hd :: tl -> hd, tl | [] -> assert false in
+	    let ctxevs = substitution_of_named_context evars env cl.cl_name 0 [] (List.map snd cl_context) in
 	    let len = List.length ctxevs in
-	    let superevs = substitution_of_named_context evars env cl.cl_name len ctxevs cl.cl_super in
+(* 	    let superevs = substitution_of_named_context evars env cl.cl_name len ctxevs cl.cl_super in *)
 	    let morphargs, morphobjs = array_chop (Array.length args - n) args in
 	    let morphargs', morphobjs' = array_chop (Array.length args - n) args' in
-	    let args = List.rev_map (fun (_, c) -> c) superevs in
+	    let args = List.rev_map (fun (_, c) -> c) ctxevs in
 	    let appm = mkApp(m, morphargs) in
 	    let appmtype = Typing.type_of env sigma appm in
 	    let app = applistc (mkInd cl.cl_impl) (args @ [appm]) in
-	    let mtype = replace_vars superevs (pi3 (List.hd cl.cl_params)) in
+	    let mtype = replace_vars ctxevs (pi3 (snd cl_param)) in
 	      try 
 		evars := Unification.w_unify true env CONV ~mod_delta:true appmtype mtype !evars;
 		evars := Evarutil.nf_evar_defs !evars;
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index feafd2b3c..000cf70a3 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -209,7 +209,7 @@ Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d e
 Program Instance iff_setoid : Setoid Prop iff :=
   equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
 
-Program Instance not_morphism : Morphism Prop iff Prop iff not.
+(* Program Instance not_morphism : Morphism Prop iff Prop iff not. *)
 
 Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f3db79833..a2eab577d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -85,7 +85,7 @@ let rec unfold n f acc =
 open Topconstr
 
 let declare_implicit_proj c proj imps =
-  let len = List.length c.cl_context + List.length c.cl_super + List.length c.cl_params in
+  let len = List.length c.cl_context in
   let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in
   let expls =
     let rec aux i expls = function
@@ -108,10 +108,14 @@ let declare_implicits impls cl =
 	  | None -> assert(false)
 	  | Some p -> declare_implicit_proj cl p imps)
       projs impls;
+    let len = List.length cl.cl_context in
     let indimps = 
-      list_map_i 
-	(fun i (na, b, t) -> ExplByPos (i, Some na), (false, true))
-	1 (List.rev cl.cl_context)
+      list_fold_left_i 
+	(fun i acc (is, (na, b, t)) -> 
+	  if len - i <= cl.cl_params then acc
+	  else if is = None then (ExplByPos (i, Some na), (false, true)) :: acc
+	  else acc)
+	1 [] (List.rev cl.cl_context)
     in
       Impargs.declare_manual_implicits true (IndRef cl.cl_impl) false indimps
 
@@ -120,6 +124,11 @@ let rel_of_named_context subst l =
     (fun (id, _, t) (ctx, acc) -> (Name id, None, subst_vars acc t) :: ctx, id :: acc)
     l ([], subst)
 
+let ids_of_rel_context subst l = 
+  List.fold_right
+    (fun (id, _, t) acc -> Nameops.out_name id :: acc)
+    l subst
+
 let degenerate_decl (na,b,t) =
   let id = match na with
     | Name id -> id
@@ -156,7 +165,6 @@ let interp_type_evars evdref env ?(impls=([],[])) typ =
   let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
     imps, Pretyping.Default.understand_tcc_evars evdref env Pretyping.IsType typ'
 
-
 let mk_interning_data env na impls typ =
   let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
   in (na, ([], impl, Notation.compute_arguments_scope typ))
@@ -170,30 +178,36 @@ let interp_fields_evars isevars env avoid l =
 	(push_named d env, impl :: uimpls, i :: ids, d::params, ([], data :: snd impls)))
     (env, [], avoid, [], ([], [])) l    
 
+let decompose_typeclass_prod env avoid = 
+  let rec prodec_rec subst env avoid l c =
+    match kind_of_term c with
+    | Prod (x,t,c) ->
+	let name = id_of_name_using_hdchar env c x in
+	let name = Nameops.next_ident_away_from name avoid in
+	let decl = (name,None,substl subst t) in
+	  prodec_rec (mkVar name :: subst) (push_named decl env) (name :: avoid) (add_named_decl decl l) c
+(*     | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c *)
+    | Cast (c,_,_)      -> prodec_rec subst env avoid l c
+    | _               -> l,c
+  in 
+  prodec_rec [] env avoid []
+
+let push_named_context = List.fold_right push_named
+
 let new_class id par ar sup props =
   let env0 = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let avoid = Termops.ids_of_context env0 in
 
-  let env_params, avoid = env0, avoid in
-
-  (* Find the implicitly quantified variables *)
-  let gen_ctx, super = Implicit_quantifiers.resolve_class_binders (vars_of_env env0) sup in
-
-  let env_super_ctx, avoid, ctx_super_ctx = interp_binders_evars isevars env_params avoid gen_ctx in
-    
-  (* Interpret the superclasses constraints *)
-  let env_super, avoid, ctx_super0 = 
-    interp_typeclass_context_evars isevars env_super_ctx avoid super 
-  in
-
-  let env_params, avoid, ctx_params = interp_binders_evars isevars env_super avoid par in
-
   (* Interpret the arity *)
-  let _arity_imps, arity = interp_type_evars isevars env_params (CSort (fst ar, snd ar)) in
+  let arity_imps, fullarity = 
+    let arity = CSort (fst ar, snd ar) in
+    let term = prod_constr_expr (prod_constr_expr arity par) sup in
+      interp_type_evars isevars env0 term      
+  in
+  let ctx_params, arity = decompose_typeclass_prod env0 avoid fullarity in
+  let env_params = push_named_context ctx_params env0 in
     
-  (* let fullarity = it_mkProd_or_LetIn (it_mkProd_or_LetIn arity ctx_defs) ctx_params in*)
-
   (* Interpret the definitions and propositions *)
   let env_props, prop_impls, avoid, ctx_props, _ = 
     interp_fields_evars isevars env_params avoid props 
@@ -202,34 +216,28 @@ let new_class id par ar sup props =
   (* Instantiate evars and check all are resolved *)
   let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in
   let sigma = Evd.evars_of isevars in
-  let ctx_super_ctx = Implicit_quantifiers.nf_named_context sigma ctx_super_ctx in
-  let ctx_super = Implicit_quantifiers.nf_named_context sigma ctx_super0 in
   let ctx_params = Implicit_quantifiers.nf_named_context sigma ctx_params in
   let ctx_props = Implicit_quantifiers.nf_named_context sigma ctx_props in
   let arity = Reductionops.nf_evar sigma arity in
   let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
   let kn = 
     let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
-    let params, subst = rel_of_named_context [] (ctx_params @ ctx_super @ ctx_super_ctx) in
+    let params, subst = rel_of_named_context [] ctx_params (*  @ ctx_super @ ctx_super_ctx) *) in
     let fields, _ = rel_of_named_context subst ctx_props in
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
       declare_structure env0 (snd id) idb params arity fields
   in
-  let ctx_context, ctx_super = 
-    let class_binders, regular_binders = 
-      List.partition (fun (na, b, t) -> 
-	Typeclasses.class_of_constr t <> None)
-	ctx_super_ctx
-    in 
-      if (ctx_super_ctx = class_binders @ regular_binders) then
-	regular_binders, ctx_super @ class_binders
-      else ctx_super_ctx, ctx_super
+  let ctx_context =
+    List.map (fun ((na, b, t) as d) -> 
+      match Typeclasses.class_of_constr t with
+	  None -> (None, d)
+	| Some cl -> (Some cl.cl_name, d))
+      ctx_params
   in
   let k =
     { cl_name = snd id;
+      cl_params = List.length par;
       cl_context = ctx_context;
-      cl_super = ctx_super;
-      cl_params = ctx_params;
       cl_props = ctx_props;
       cl_impl = kn }
   in
@@ -271,8 +279,6 @@ let subst_named inst subst ctx =
       ctx' ([], 0)
   in ctx'
 
-let push_named_context = List.fold_right push_named
-
 let destClass c = 
   match kind_of_term c with
       App (c, args) -> 
@@ -335,24 +341,19 @@ let new_instance sup (instid, bk, cl) props =
   let subst = 
     match bk with
 	Explicit ->
-	  if List.length par <> List.length k.cl_context + List.length k.cl_params then 
-	    mismatched_params env par (k.cl_params @ k.cl_context);
-	  let len = List.length k.cl_context in
+	  if List.length par <> List.length (List.filter (fun (x, y) -> x <> None) k.cl_context) then 
+	    mismatched_params env par (List.map snd k.cl_context);
+	  let cl_context = List.map snd k.cl_context in
+	  let len = List.length cl_context in
 	  let ctx, par = Util.list_chop len par in
-	  let subst, _ = type_ctx_instance isevars env' k.cl_context ctx [] in
-	  let subst = 
-	    Typeclasses.substitution_of_named_context isevars env' k.cl_name len subst 
-	      k.cl_super 
-	  in 
-	    if List.length par <> List.length k.cl_params then 
-	      mismatched_params env par k.cl_params;
-	    let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst
+	  let subst, _ = type_ctx_instance isevars env' cl_context ctx [] in
+	    subst
 
       | Implicit ->
 	  let _imps, t' = interp_type_evars isevars env (Topconstr.mkAppC (CRef (Ident id), par)) in
 	    match kind_of_term t' with 
 		App (c, args) -> 
-		  substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context) 
+		  substitution_of_constrs (List.map snd k.cl_context)
 		    (List.rev (Array.to_list args))
 	      | _ -> assert false
   in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index ec494622c..5855759b2 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -34,9 +34,9 @@ val infer_super_instances : env -> constr list ->
   named_context -> named_context -> types list * identifier list * named_context
 
 val new_class : identifier located ->
-  binder_list ->
+  local_binder list ->
   Vernacexpr.sort_expr located ->
-  typeclass_context ->
+  local_binder list ->
   binder_list -> unit
 
 val new_instance : 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index a5c04a561..02517ae96 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -227,9 +227,9 @@ type vernac_expr =
   (* Type classes *)
   | VernacClass of
       lident * (* name *)
-	(lident * constr_expr) list * (* params *)
+	local_binder list * (* params *)
 	sort_expr located * (* arity *)
-	typeclass_context * (* super *)
+	local_binder list * (* constraints *)
 	(lident * constr_expr) list (* props *)
 	
   | VernacInstance of