better error messages. sorts are compared using whd

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 2dce2a4a70f0dad2de5ce0738c7f13b339043f41..05862d9dab7f63ed4616119766f456f2660a3b97 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -60,7 +60,7 @@ let force_to_sort metasenv subst context t =
        else metasenv, subst, i
      in
      metasenv, subst, C.Meta (newmeta,(0,C.Irl 0))
-  | C.Sort _ -> metasenv, subst, t 
+  | C.Sort _ as t -> metasenv, subst, t 
   | _ -> assert false
 ;;
 
@@ -327,7 +327,8 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
             typeof ~localise metasenv subst context arg (Some s) in
           let t = NCicSubstitution.subst ~avoid_beta_redexes:true arg t in
           aux metasenv subst (arg :: args_so_far) t tl
-      | t ->
+      | C.Meta _
+      | C.Appl (C.Meta _ :: _) as t ->
           let metasenv, subst, arg, ty_arg = 
             typeof ~localise metasenv subst context arg None in
           let metasenv, meta, _ = 
@@ -343,13 +344,28 @@ and eat_prods localise metasenv subst context orig_he he ty_he args =
           let metasenv, subst = 
              try NCicUnification.unify metasenv subst context t flex_prod 
              with exc -> raise (wrap_exc (lazy (localise orig_he, Printf.sprintf
-              ("The term %s is here applied to %d arguments but expects " ^^
-              "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
-              (List.length args) (List.length args_so_far))) exc)
+              ("The term %s has an inferred type %s, but is applied to the" ^^
+               " argument %s of type %s")
+              (NCicPp.ppterm ~metasenv ~subst ~context he)
+              (NCicPp.ppterm ~metasenv ~subst ~context t)
+              (NCicPp.ppterm ~metasenv ~subst ~context arg)
+              (NCicPp.ppterm ~metasenv ~subst ~context ty_arg))) exc)
               (* XXX coerce to funclass *)
           in
           let meta = NCicSubstitution.subst ~avoid_beta_redexes:true arg meta in
           aux metasenv subst (arg :: args_so_far) meta tl
+      | C.Match (_,_,C.Meta _,_) 
+      | C.Match (_,_,C.Appl (C.Meta _ :: _),_) 
+      | C.Appl (C.Const (NReference.Ref (_, NReference.Fix _)) :: _) ->
+          raise (Uncertain (lazy (localise orig_he, Printf.sprintf
+            ("The term %s is here applied to %d arguments but expects " ^^
+            "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+            (List.length args) (List.length args_so_far))))
+      | _ ->
+          raise (RefineFailure (lazy (localise orig_he, Printf.sprintf
+            ("The term %s is here applied to %d arguments but expects " ^^
+            "only %d arguments") (NCicPp.ppterm ~metasenv ~subst ~context he)
+            (List.length args) (List.length args_so_far))))
   in
    aux metasenv subst [] ty_he args
   (*D*)in outside(); rc with exc -> outside (); raise exc