Inner-types a la Coscoy now correctly generated even for atoms.

[helm.git] / helm / gTopLevel / doubleTypeInference.ml

diff --git a/helm/gTopLevel/doubleTypeInference.ml b/helm/gTopLevel/doubleTypeInference.ml
index 024f49ebf6732ca6bf4ad6e82d5011007c1012b7..f58c554fb0990a005f4f790c9691c305ce19cfa9 100644 (file)
--- a/helm/gTopLevel/doubleTypeInference.ml
+++ b/helm/gTopLevel/doubleTypeInference.ml
@@ -308,19 +308,24 @@ let rec type_of_aux' subterms_to_types metasenv context t expectedty =
          (* Checks suppressed *)
          C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t None)
      | C.Appl (he::tl) when List.length tl > 0 ->
-        let hetype = type_of_aux context he None in
-        let tlbody_and_type =
-         let rec aux =
-          function
-             _,[] -> []
-           | C.Prod (n,s,t),he::tl ->
-              (he, type_of_aux context he (Some (head_beta_reduce s)))::
-               (aux (R.whd context (S.subst he t), tl))
-           | _ -> assert false
-         in
-          aux (R.whd context hetype, tl)
+        let expected_hetype =
+         (* Inefficient, the head is computed twice. But I know *)
+         (* of no other solution.                               *)
+         R.whd context (CicTypeChecker.type_of_aux' metasenv context he)
         in
-         eat_prods context hetype tlbody_and_type
+         let hetype = type_of_aux context he (Some expected_hetype) in
+         let tlbody_and_type =
+          let rec aux =
+           function
+              _,[] -> []
+            | C.Prod (n,s,t),he::tl ->
+               (he, type_of_aux context he (Some (head_beta_reduce s)))::
+                (aux (R.whd context (S.subst he t), tl))
+            | _ -> assert false
+          in
+           aux (expected_hetype, tl)
+         in
+          eat_prods context hetype tlbody_and_type
      | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
      | C.Const (uri,cookingsno) ->
         cooked_type_of_constant uri cookingsno