typing: resolve record projections from the record type

Field projections (e.`f) were resolved by looking up the field name as
an operator, which requires the projection operator -- and hence the
theory declaring the record type -- to be in scope. As a result, a
projection through a type from a non-imported theory failed.

When the record type is known, resolve the projector directly from the
type: the projection operator lives in the theory declaring the type and
is reachable by its qualified name even when that theory is not imported.
This also disambiguates same-named fields of unrelated records by type.
Fall back to the name-based search only when the type is not yet known.

Author: strub

src/ecTyping.ml

@@ -447,8 +447,30 @@ let select_form_op env mode ~forcepv opsc name ue tvi psig =
 (* -------------------------------------------------------------------- *)
 let select_proj env opsc name ue tvi recty =
   let filter = (fun _ op -> EcDecl.is_proj op) in
-  let ops = EcUnify.select_op ~filter tvi env name ue ([recty], None) in
-  let ops = List.map (fun (p, ty, ue, _) -> (p, ty, ue)) ops in
+  let do_select name =
+    let ops = EcUnify.select_op ~filter tvi env name ue ([recty], None) in
+    List.map (fun (p, ty, ue, _) -> (p, ty, ue)) ops in
+
+  (* When the record type is known, resolve the projector from the type so it
+     need not be in scope by name; fall back to a name-based search otherwise. *)
+  let ty = ty_subst (Tuni.subst (UE.assubst ue)) recty in
+  let ops =
+    match (EcEnv.ty_hnorm ty env).ty_node with
+    | Tconstr (tp, _) -> begin
+        let projp = EcPath.pqoname (EcPath.prefix tp) (snd name) in
+        match EcEnv.Op.by_path_opt projp env with
+        | Some op when EcDecl.is_proj op
+                    && EcPath.p_equal tp (proj3_1 (EcDecl.operator_as_proj op)) ->
+            let subue = EcUnify.UniEnv.copy ue in
+            let top, tvs =
+              EcUnify.UniEnv.openty subue op.op_tparams tvi op.op_ty in
+            (try  EcUnify.unify env subue top (EcUnify.tfun_expected subue [recty])
+             with EcUnify.UnificationFailure _ -> assert false);
+            [((projp, tvs), top, subue)]
+        | _ -> do_select name
+      end
+    | _ -> do_select name
+  in
 
   match ops, opsc with
   | _ :: _ :: _, Some opsc ->

tests/record-proj-unimported.ec

@@ -0,0 +1,31 @@
+(* Record field projections must resolve from the record type alone, even when
+   the theory declaring the type (and hence the projection operator) is not
+   imported in the current scope. See issue #1011. *)
+
+theory T.
+  type t = { f : unit }.
+  op e : t.
+end T.
+
+(* `T` is not imported: `f` is not in scope by its bare name, but the
+   projection is determined by the type of `T.e`. *)
+op test = T.e.`f.
+
+(* Same field name in two unrelated records: the known type disambiguates. *)
+theory A. type t = { g : int  }. op e : t. end A.
+theory B. type t = { g : bool }. op e : t. end B.
+
+op ta : int  = A.e.`g.
+op tb : bool = B.e.`g.
+
+(* Projection through a clone that inlines the record type. *)
+theory U.
+  type u.
+  op e : u.
+end U.
+
+type u' = { h : int }.
+
+clone U as U' with type u <- u'.
+
+op tc : int = U'.e.`h.