<commit_before>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Util
open Names
open Nameops
open Namegen
open Term
open Termops
open Indtypes
open Environ
open Pretype_errors
open Type_errors
open Typeclasses_errors
open Indrec
open Cases
open Logic
open Printer
open Evd

(* This simplifies the typing context of Cases clauses *)
(* hope it does not disturb other typing contexts *)
let contract env lc =
  let l = ref [] in
  let contract_context (na,c,t) env =
    match c with
      | Some c' when isRel c' ->
          l := (Vars.substl !l c') :: !l;
          env
      | _ ->
          let t' = Vars.substl !l t in
          let c' = Option.map (Vars.substl !l) c in
          let na' = named_hd env t' na in
          l := (mkRel 1) :: List.map (Vars.lift 1) !l;
          push_rel (na',c',t') env in
  let env = process_rel_context contract_context env in
  (env, List.map (Vars.substl !l) lc)

let contract2 env a b = match contract env [a;b] with
  | env, [a;b] -> env,a,b | _ -> assert false

let contract3 env a b c = match contract env [a;b;c] with
  | env, [a;b;c] -> env,a,b,c | _ -> assert false

let contract4 env a b c d = match contract env [a;b;c;d] with
  | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false

let contract1_vect env a v =
  match contract env (a :: Array.to_list v) with
  | env, a::l -> env,a,Array.of_list l
  | _ -> assert false

let contract3' env a b c = function
  | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
  | NotClean ((evk,args),env',d) ->
      let env',d,args = contract1_vect env' d args in
      contract3 env a b c,NotClean((evk,args),env',d)
  | ConversionFailed (env',t1,t2) ->
      let (env',t1,t2) = contract2 env' t1 t2 in
      contract3 env a b c, ConversionFailed (env',t1,t2)
  | NotSameArgSize | NotSameHead | NoCanonicalStructure
  | MetaOccurInBody _ | InstanceNotSameType _
  | UnifUnivInconsistency _ as x -> contract3 env a b c, x

(** Printers *)

let pr_lconstr c = quote (pr_lconstr c)
let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)

(** A canonisation procedure for constr such that comparing there
    externalisation catches more equalities *)
let canonize_constr c =
  (* replaces all the names in binders by [dn] ("default name"),
     ensures that [alpha]-equivalent terms will have the same
     externalisation. *)
  let dn = Name.Anonymous in
  let rec canonize_binders c =
    match Term.kind_of_term c with
    | Prod (_,t,b) -> mkProd(dn,t,b)
    | Lambda (_,t,b) -> mkLambda(dn,t,b)
    | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b)
    | _ -> Term.map_constr canonize_binders c
  in
  canonize_binders c

(** Tries to realize when the two terms, albeit different are printed the same. *)
let display_eq ~flags env sigma t1 t2 =
  (* terms are canonized, then their externalisation is compared syntactically *)
  let open Constrextern in
  let t1 = canonize_constr t1 in
  let t2 = canonize_constr t2 in
  let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in
  let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in
  Constrexpr_ops.constr_expr_eq ct1 ct2

(** This function adds some explicit printing flags if the two arguments are
    printed alike. *)
let rec pr_explicit_aux env sigma t1 t2 = function
| [] ->
  (** no specified flags: default. *)
  (quote (Printer.pr_lconstr_env env sigma t1), quote (Printer.pr_lconstr_env env sigma t2))
| flags :: rem ->
  let equal = display_eq ~flags env sigma t1 t2 in
  if equal then
    (** The two terms are the same from the user point of view *)
    pr_explicit_aux env sigma t1 t2 rem
  else
    let open Constrextern in
    let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) ()
    in
    let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
    in
    quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2)

let explicit_flags =
  let open Constrextern in
  [ []; (** First, try with the current flags *)
    [print_implicits]; (** Then with implicit *)
    [print_universes]; (** Then with universes *)
    [print_universes; print_implicits]; (** With universes AND implicits *)
    [print_implicits; print_coercions; print_no_symbol]; (** Then more! *)
    [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]

let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags

let pr_db env i =
  try
    match lookup_rel i env with
        Name id, _, _ -> pr_id id
      | Anonymous, _, _ -> str "<>"
  with Not_found -> str "UNBOUND_REL_" ++ int i

let explain_unbound_rel env sigma n =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  str "Unbound reference: " ++ pe ++
  str "The reference " ++ int n ++ str " is free."

let explain_unbound_var env v =
  let var = pr_id v in
  str "No such section variable or assumption: " ++ var ++ str "."

let explain_not_type env sigma j =
  let j = Evarutil.j_nf_evar sigma j in
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc,pt = pr_ljudge_env env sigma j in
  pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
  str "has type" ++ spc () ++ pt ++ spc () ++
  str "which should be Set, Prop or Type."

let explain_bad_assumption env sigma j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc,pt = pr_ljudge_env env sigma j in
  pe ++ str "Cannot declare a variable or hypothesis over the term" ++
  brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
  str "because this term is not a type."

let explain_reference_variables id c =
  (* c is intended to be a global reference *)
  let pc = pr_global (Globnames.global_of_constr c) in
  pc ++ strbrk " depends on the variable " ++ pr_id id ++
  strbrk " which is not declared in the context."

let rec pr_disjunction pr = function
  | [a] -> pr  a
  | [a;b] -> pr a ++ str " or" ++ spc () ++ pr b
  | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
  | [] -> assert false

let pr_puniverses f env (c,u) = 
  f env c ++ 
  (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
    str"(*" ++ Univ.Instance.pr u ++ str"*)"
  else mt())

let explain_elim_arity env sigma ind sorts c pj okinds =
  let env = make_all_name_different env in
  let pi = pr_inductive env (fst ind) in
  let pc = pr_lconstr_env env sigma c in
  let msg = match okinds with
  | Some(kp,ki,explanation) ->
      let pki = pr_sort_family ki in
      let pkp = pr_sort_family kp in
      let explanation =	match explanation with
	| NonInformativeToInformative ->
          "proofs can be eliminated only to build proofs"
	| StrongEliminationOnNonSmallType ->
          "strong elimination on non-small inductive types leads to paradoxes"
	| WrongArity ->
	  "wrong arity" in
      let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
      let ppt = pr_lconstr_env env sigma ((strip_prod_assum pj.uj_type)) in
      hov 0
	(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
	 str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
      fnl () ++
      hov 0
	(str "Elimination of an inductive object of sort " ++
	 pki ++ brk(1,0) ++
         str "is not allowed on a predicate in sort " ++ pkp ++ fnl () ++
         str "because" ++ spc () ++ str explanation ++ str ".")
  | None ->
      str "ill-formed elimination predicate."
  in
  hov 0 (
    str "Incorrect elimination of" ++ spc () ++ pc ++ spc () ++
    str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++
  fnl () ++ msg

let explain_case_not_inductive env sigma cj =
  let cj = Evarutil.j_nf_evar sigma cj in
  let env = make_all_name_different env in
  let pc = pr_lconstr_env env sigma cj.uj_val in
  let pct = pr_lconstr_env env sigma cj.uj_type in
    match kind_of_term cj.uj_type with
      | Evar _ ->
	  str "Cannot infer a type for this expression."
      | _ ->
	  str "The term" ++ brk(1,1) ++ pc ++ spc () ++
	  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
	  str "which is not a (co-)inductive type."

let explain_number_branches env sigma cj expn =
  let cj = Evarutil.j_nf_evar sigma cj in
  let env = make_all_name_different env in
  let pc = pr_lconstr_env env sigma cj.uj_val in
  let pct = pr_lconstr_env env sigma cj.uj_type in
  str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
  str "of type" ++ brk(1,1) ++ pct ++ spc () ++
  str "expects " ++  int expn ++ str " branches."

let explain_ill_formed_branch env sigma c ci actty expty =
  let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
  let c = Evarutil.nf_evar sigma c in
  let env = make_all_name_different env in
  let pc = pr_lconstr_env env sigma c in
  let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
  strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
  spc () ++ strbrk "the branch for constructor" ++ spc () ++
  quote (pr_puniverses pr_constructor env ci) ++
  spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
  str "which should be" ++ brk(1,1) ++ pe ++ str "."

let explain_generalization env sigma (name,var) j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pv = pr_ltype_env env sigma var in
  let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in
  pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
  str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
  str "it has type" ++ spc () ++ pt ++
  spc () ++ str "which should be Set, Prop or Type."

let explain_unification_error env sigma p1 p2 = function
  | None -> mt()
  | Some e ->
    match e with
    | OccurCheck (evk,rhs) ->
        let rhs = Evarutil.nf_evar sigma rhs in
        spc () ++ str "(cannot define " ++ quote (pr_existential_key sigma evk) ++
	strbrk " with term " ++ pr_lconstr_env env sigma rhs ++
        strbrk " that would depend on itself)"
    | NotClean ((evk,args),env,c) ->
        let c = Evarutil.nf_evar sigma c in
        let args = Array.map (Evarutil.nf_evar sigma) args in
        spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key sigma evk)
        ++ strbrk " because " ++ pr_lconstr_env env sigma c ++
	strbrk " is not in its scope" ++
        (if Array.is_empty args then mt() else
         strbrk ": available arguments are " ++
         pr_sequence (pr_lconstr_env env sigma) (List.rev (Array.to_list args))) ++
        str ")"
    | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
        (* Error speaks from itself *) mt ()
    | ConversionFailed (env,t1,t2) ->
        if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then mt () else
        let env = make_all_name_different env in
        let t1 = Evarutil.nf_evar sigma t1 in
        let t2 = Evarutil.nf_evar sigma t2 in
        if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then
          let t1, t2 = pr_explicit env sigma t1 t2 in
          spc () ++ str "(cannot unify " ++ t1 ++ strbrk " and " ++
            t2 ++ str ")"
        else mt ()
    | MetaOccurInBody evk ->
        spc () ++ str "(instance for " ++ quote (pr_existential_key sigma evk) ++
	strbrk " refers to a metavariable - please report your example)"
    | InstanceNotSameType (evk,env,t,u) ->
        let t, u = pr_explicit env sigma t u in
        spc () ++ str "(unable to find a well-typed instantiation for " ++
        quote (pr_existential_key sigma evk) ++ strbrk ": cannot unify " ++
        t ++ strbrk " and " ++ u ++ str ")"
    | UnifUnivInconsistency p ->
        if !Constrextern.print_universes then
	  spc () ++ str "(Universe inconsistency: " ++ 
	    Univ.explain_universe_inconsistency p ++ str")"
	else
          spc () ++ str "(Universe inconsistency)"

let explain_actual_type env sigma j t reason =
  let env = make_all_name_different env in<commit_msg>Slight improving of a unification error message.<commit_after>(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Util
open Names
open Nameops
open Namegen
open Term
open Termops
open Indtypes
open Environ
open Pretype_errors
open Type_errors
open Typeclasses_errors
open Indrec
open Cases
open Logic
open Printer
open Evd

(* This simplifies the typing context of Cases clauses *)
(* hope it does not disturb other typing contexts *)
let contract env lc =
  let l = ref [] in
  let contract_context (na,c,t) env =
    match c with
      | Some c' when isRel c' ->
          l := (Vars.substl !l c') :: !l;
          env
      | _ ->
          let t' = Vars.substl !l t in
          let c' = Option.map (Vars.substl !l) c in
          let na' = named_hd env t' na in
          l := (mkRel 1) :: List.map (Vars.lift 1) !l;
          push_rel (na',c',t') env in
  let env = process_rel_context contract_context env in
  (env, List.map (Vars.substl !l) lc)

let contract2 env a b = match contract env [a;b] with
  | env, [a;b] -> env,a,b | _ -> assert false

let contract3 env a b c = match contract env [a;b;c] with
  | env, [a;b;c] -> env,a,b,c | _ -> assert false

let contract4 env a b c d = match contract env [a;b;c;d] with
  | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false

let contract1_vect env a v =
  match contract env (a :: Array.to_list v) with
  | env, a::l -> env,a,Array.of_list l
  | _ -> assert false

let contract3' env a b c = function
  | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
  | NotClean ((evk,args),env',d) ->
      let env',d,args = contract1_vect env' d args in
      contract3 env a b c,NotClean((evk,args),env',d)
  | ConversionFailed (env',t1,t2) ->
      let (env',t1,t2) = contract2 env' t1 t2 in
      contract3 env a b c, ConversionFailed (env',t1,t2)
  | NotSameArgSize | NotSameHead | NoCanonicalStructure
  | MetaOccurInBody _ | InstanceNotSameType _
  | UnifUnivInconsistency _ as x -> contract3 env a b c, x

(** Printers *)

let pr_lconstr c = quote (pr_lconstr c)
let pr_lconstr_env e s c = quote (pr_lconstr_env e s c)
let pr_ljudge_env e s c = let v,t = pr_ljudge_env e s c in (quote v,quote t)

(** A canonisation procedure for constr such that comparing there
    externalisation catches more equalities *)
let canonize_constr c =
  (* replaces all the names in binders by [dn] ("default name"),
     ensures that [alpha]-equivalent terms will have the same
     externalisation. *)
  let dn = Name.Anonymous in
  let rec canonize_binders c =
    match Term.kind_of_term c with
    | Prod (_,t,b) -> mkProd(dn,t,b)
    | Lambda (_,t,b) -> mkLambda(dn,t,b)
    | LetIn (_,u,t,b) -> mkLetIn(dn,u,t,b)
    | _ -> Term.map_constr canonize_binders c
  in
  canonize_binders c

(** Tries to realize when the two terms, albeit different are printed the same. *)
let display_eq ~flags env sigma t1 t2 =
  (* terms are canonized, then their externalisation is compared syntactically *)
  let open Constrextern in
  let t1 = canonize_constr t1 in
  let t2 = canonize_constr t2 in
  let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) () in
  let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) () in
  Constrexpr_ops.constr_expr_eq ct1 ct2

(** This function adds some explicit printing flags if the two arguments are
    printed alike. *)
let rec pr_explicit_aux env sigma t1 t2 = function
| [] ->
  (** no specified flags: default. *)
  (quote (Printer.pr_lconstr_env env sigma t1), quote (Printer.pr_lconstr_env env sigma t2))
| flags :: rem ->
  let equal = display_eq ~flags env sigma t1 t2 in
  if equal then
    (** The two terms are the same from the user point of view *)
    pr_explicit_aux env sigma t1 t2 rem
  else
    let open Constrextern in
    let ct1 = Flags.with_options flags (fun () -> extern_constr false env sigma t1) ()
    in
    let ct2 = Flags.with_options flags (fun () -> extern_constr false env sigma t2) ()
    in
    quote (Ppconstr.pr_lconstr_expr ct1), quote (Ppconstr.pr_lconstr_expr ct2)

let explicit_flags =
  let open Constrextern in
  [ []; (** First, try with the current flags *)
    [print_implicits]; (** Then with implicit *)
    [print_universes]; (** Then with universes *)
    [print_universes; print_implicits]; (** With universes AND implicits *)
    [print_implicits; print_coercions; print_no_symbol]; (** Then more! *)
    [print_universes; print_implicits; print_coercions; print_no_symbol] (** and more! *) ]

let pr_explicit env sigma t1 t2 = pr_explicit_aux env sigma t1 t2 explicit_flags

let pr_db env i =
  try
    match lookup_rel i env with
        Name id, _, _ -> pr_id id
      | Anonymous, _, _ -> str "<>"
  with Not_found -> str "UNBOUND_REL_" ++ int i

let explain_unbound_rel env sigma n =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  str "Unbound reference: " ++ pe ++
  str "The reference " ++ int n ++ str " is free."

let explain_unbound_var env v =
  let var = pr_id v in
  str "No such section variable or assumption: " ++ var ++ str "."

let explain_not_type env sigma j =
  let j = Evarutil.j_nf_evar sigma j in
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc,pt = pr_ljudge_env env sigma j in
  pe ++ str "The term" ++ brk(1,1) ++ pc ++ spc () ++
  str "has type" ++ spc () ++ pt ++ spc () ++
  str "which should be Set, Prop or Type."

let explain_bad_assumption env sigma j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pc,pt = pr_ljudge_env env sigma j in
  pe ++ str "Cannot declare a variable or hypothesis over the term" ++
  brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
  str "because this term is not a type."

let explain_reference_variables id c =
  (* c is intended to be a global reference *)
  let pc = pr_global (Globnames.global_of_constr c) in
  pc ++ strbrk " depends on the variable " ++ pr_id id ++
  strbrk " which is not declared in the context."

let rec pr_disjunction pr = function
  | [a] -> pr  a
  | [a;b] -> pr a ++ str " or" ++ spc () ++ pr b
  | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
  | [] -> assert false

let pr_puniverses f env (c,u) = 
  f env c ++ 
  (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
    str"(*" ++ Univ.Instance.pr u ++ str"*)"
  else mt())

let explain_elim_arity env sigma ind sorts c pj okinds =
  let env = make_all_name_different env in
  let pi = pr_inductive env (fst ind) in
  let pc = pr_lconstr_env env sigma c in
  let msg = match okinds with
  | Some(kp,ki,explanation) ->
      let pki = pr_sort_family ki in
      let pkp = pr_sort_family kp in
      let explanation =	match explanation with
	| NonInformativeToInformative ->
          "proofs can be eliminated only to build proofs"
	| StrongEliminationOnNonSmallType ->
          "strong elimination on non-small inductive types leads to paradoxes"
	| WrongArity ->
	  "wrong arity" in
      let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) sorts in
      let ppt = pr_lconstr_env env sigma ((strip_prod_assum pj.uj_type)) in
      hov 0
	(str "the return type has sort" ++ spc () ++ ppt ++ spc () ++
	 str "while it" ++ spc () ++ str "should be " ++ ppar ++ str ".") ++
      fnl () ++
      hov 0
	(str "Elimination of an inductive object of sort " ++
	 pki ++ brk(1,0) ++
         str "is not allowed on a predicate in sort " ++ pkp ++ fnl () ++
         str "because" ++ spc () ++ str explanation ++ str ".")
  | None ->
      str "ill-formed elimination predicate."
  in
  hov 0 (
    str "Incorrect elimination of" ++ spc () ++ pc ++ spc () ++
    str "in the inductive type" ++ spc () ++ quote pi ++ str ":") ++
  fnl () ++ msg

let explain_case_not_inductive env sigma cj =
  let cj = Evarutil.j_nf_evar sigma cj in
  let env = make_all_name_different env in
  let pc = pr_lconstr_env env sigma cj.uj_val in
  let pct = pr_lconstr_env env sigma cj.uj_type in
    match kind_of_term cj.uj_type with
      | Evar _ ->
	  str "Cannot infer a type for this expression."
      | _ ->
	  str "The term" ++ brk(1,1) ++ pc ++ spc () ++
	  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
	  str "which is not a (co-)inductive type."

let explain_number_branches env sigma cj expn =
  let cj = Evarutil.j_nf_evar sigma cj in
  let env = make_all_name_different env in
  let pc = pr_lconstr_env env sigma cj.uj_val in
  let pct = pr_lconstr_env env sigma cj.uj_type in
  str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
  str "of type" ++ brk(1,1) ++ pct ++ spc () ++
  str "expects " ++  int expn ++ str " branches."

let explain_ill_formed_branch env sigma c ci actty expty =
  let simp t = Reduction.nf_betaiota env (Evarutil.nf_evar sigma t) in
  let c = Evarutil.nf_evar sigma c in
  let env = make_all_name_different env in
  let pc = pr_lconstr_env env sigma c in
  let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
  strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
  spc () ++ strbrk "the branch for constructor" ++ spc () ++
  quote (pr_puniverses pr_constructor env ci) ++
  spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
  str "which should be" ++ brk(1,1) ++ pe ++ str "."

let explain_generalization env sigma (name,var) j =
  let pe = pr_ne_context_of (str "In environment") env sigma in
  let pv = pr_ltype_env env sigma var in
  let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) env) sigma j in
  pe ++ str "Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
  str "over" ++ brk(1,1) ++ pc ++ str "," ++ spc () ++
  str "it has type" ++ spc () ++ pt ++
  spc () ++ str "which should be Set, Prop or Type."

let explain_unification_error env sigma p1 p2 = function
  | None -> mt()
  | Some e ->
    match e with
    | OccurCheck (evk,rhs) ->
        let rhs = Evarutil.nf_evar sigma rhs in
        spc () ++ str "(cannot define " ++ quote (pr_existential_key sigma evk) ++
	strbrk " with term " ++ pr_lconstr_env env sigma rhs ++
        strbrk " that would depend on itself)"
    | NotClean ((evk,args),env,c) ->
        let c = Evarutil.nf_evar sigma c in
        let args = Array.map (Evarutil.nf_evar sigma) args in
        spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key sigma evk)
        ++ strbrk " because " ++ pr_lconstr_env env sigma c ++
	strbrk " is not in its scope" ++
        (if Array.is_empty args then mt() else
         strbrk ": available arguments are " ++
         pr_sequence (pr_lconstr_env env sigma) (List.rev (Array.to_list args))) ++
        str ")"
    | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
        (* Error speaks from itself *) mt ()
    | ConversionFailed (env,t1,t2) ->
        if Term.eq_constr t1 p1 && Term.eq_constr t2 p2 then mt () else
        let env = make_all_name_different env in
        let t1 = Evarutil.nf_evar sigma t1 in
        let t2 = Evarutil.nf_evar sigma t2 in
        if not (Term.eq_constr t1 p1) || not (Term.eq_constr t2 p2) then
          let t1, t2 = pr_explicit env sigma t1 t2 in
          spc () ++ str "(cannot unify " ++ t1 ++ strbrk " and " ++
            t2 ++ str ")"
        else mt ()
    | MetaOccurInBody evk ->
        spc () ++ str "(instance for " ++ quote (pr_existential_key sigma evk) ++
	strbrk " refers to a metavariable - please report your example)"
    | InstanceNotSameType (evk,env,t,u) ->
        let t, u = pr_explicit env sigma t u in
        spc () ++ str "(unable to find a well-typed instantiation for " ++
        quote (pr_existential_key sigma evk) ++
        strbrk ": cannot ensure that " ++
        t ++ strbrk " is a subtype of " ++ u ++ str ")"
    | UnifUnivInconsistency p ->
        if !Constrextern.print_universes then
	  spc () ++ str "(Universe inconsistency: " ++ 
	    Univ.explain_universe_inconsistency p ++ str")"
	else
          spc () ++ str "(Universe inconsistency)"

let explain_actual_type env sigma j t reason =
  let env = make_all_name_different env in
{'fraction_non_alphanumeric': 0.1310583779863825, 'fraction_numerical': 0.008863462390717537, 'mean_word_length': 3.0009671179883948, 'pattern_counts': {'":': 6, '<': 7, '<?xml version=': 0, '>': 101, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2310938', 'n_tokens_mistral': 8869, 'n_tokens_neox': 8533, 'n_words': 3015}