generalize hash_kind

we could try to use it in hcons to reduce fragility, not sure if good idea
(we would still need to deal with arrays somehow)

kernel/hConstr.ml

@@ -524,38 +524,38 @@ let push_letin ~body ~typ env =
 
 let hash_array hashf a = Array.fold_left (fun hash x -> Hashset.Combine.combine hash (hashf x)) 0 a
 
-let hash_kind = let open Hashset.Combine in function
+let hash_kind (type a) (hash:a -> int) = let open Hashset.Combine in function
   | Var i -> combinesmall 1 (Id.hash i)
   | Sort s -> combinesmall 2 (Sorts.hash s)
-  | Cast (c,k,t) -> combinesmall 3 (combine3 c.hash (hash_cast_kind k) t.hash)
-  | Prod (na,t,c) -> combinesmall 4 (combine3 (hash_annot na) t.hash c.hash)
-  | Lambda (na,t,c) -> combinesmall 5 (combine3 (hash_annot na) t.hash c.hash)
-  | LetIn (na,b,t,c) -> combinesmall 6 (combine4 (hash_annot na) b.hash t.hash c.hash)
+  | Cast (c,k,t) -> combinesmall 3 (combine3 (hash c) (hash_cast_kind k) (hash t))
+  | Prod (na,t,c) -> combinesmall 4 (combine3 (hash_annot na) (hash t) (hash c))
+  | Lambda (na,t,c) -> combinesmall 5 (combine3 (hash_annot na) (hash t) (hash c))
+  | LetIn (na,b,t,c) -> combinesmall 6 (combine4 (hash_annot na) (hash b) (hash t) (hash c))
   | App (h,args) ->
-    combinesmall 7 (combine (hash_array hash args) h.hash)
+    combinesmall 7 (combine (hash_array hash args) (hash h))
   | Evar _ -> assert false
   | Const (c,u) -> combinesmall 9 (combine (Constant.SyntacticOrd.hash c) (Instance.hash u))
   | Ind (ind,u) -> combinesmall 10 (combine (Ind.SyntacticOrd.hash ind) (Instance.hash u))
   | Construct (c,u) -> combinesmall 11 (combine (Construct.SyntacticOrd.hash c) (Instance.hash u))
   | Case (_,u,pms,(p,_),_,c,bl) ->
     let hash_ctx (bnd,c) =
       let hna = hash_array hash_annot bnd in
-      combine hna c.hash
+      combine hna (hash c)
     in
     let hpms = hash_array hash pms in
     let hbl = hash_array hash_ctx bl in
-    let h = combine5 (Instance.hash u) c.hash hpms (hash_ctx p) hbl in
+    let h = combine5 (Instance.hash u) (hash c) hpms (hash_ctx p) hbl in
     combinesmall 12 h
   | Fix (_,(lna,tl,bl)) ->
     combinesmall 13 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl))
   | CoFix (_,(lna,tl,bl)) ->
     combinesmall 14 (combine3 (hash_array hash_annot lna) (hash_array hash tl) (hash_array hash bl))
   | Meta _ -> assert false
   | Rel n -> combinesmall 16 n
-  | Proj (p,_,c) -> combinesmall 17 (combine (Projection.SyntacticOrd.hash p) c.hash)
+  | Proj (p,_,c) -> combinesmall 17 (combine (Projection.SyntacticOrd.hash p) (hash c))
   | Int i -> combinesmall 18 (Uint63.hash i)
   | Float f -> combinesmall 19 (Float64.hash f)
-  | Array (u,t,def,ty) -> combinesmall 20 (combine4 (Instance.hash u) (hash_array hash t) def.hash ty.hash)
+  | Array (u,t,def,ty) -> combinesmall 20 (combine4 (Instance.hash u) (hash_array hash t) (hash def) (hash ty))
 
 let kind_to_constr = function
   | Rel n -> mkRel n
@@ -590,7 +590,7 @@ let hcons_inplace f a = Array.iteri (fun i x -> Array.unsafe_set a i (f x)) a
 
 let of_kind_nohashcons kind =
   let self = kind_to_constr kind in
-  let hash = hash_kind kind in
+  let hash = hash_kind hash kind in
   let () = match kind with
     | Rel _ -> assert false
     | _ -> ()
@@ -602,7 +602,7 @@ let rec of_constr tbl local_env c =
     let kind = of_constr_aux tbl local_env c in
     let self = kind_to_constr kind in
     let self = if hasheq (Constr.kind self) (Constr.kind c) then c else self in
-    let hash = hash_kind kind in
+    let hash = hash_kind hash kind in
     let isRel, hash = match kind with
       | Rel n ->
         let uid = Range.get local_env.rels (n-1) in