fixing #213

examples/bug-reports/bug213.fst

@@ -1,19 +1,12 @@
 module Bug213
 
-open Constructive
-
 type intPair =
-  | IP : f:int -> s:int -> intPair
+  | IP : f:int -> intPair
 
-(* This does not work *)
-val foo : cexists (fun p -> ceq (IP.f p) (IP.s p)) -> Tot unit
-let foo h =
-  let ExIntro (IP p1 p2) hp = h in
-  ()
+type cexists : a:Type -> (a -> Type) -> Type =
+  | ExIntro : #a:Type -> #p:(a -> Type) -> x:a -> p x -> cexists a p
 
-(* This works *)
-val foo' : cexists (fun p -> ceq (IP.f p) (IP.s p)) -> Tot unit
-let foo' h =
-  let ExIntro p hp = h in
-  let IP p1 p2 = p in
+val foo : cexists intPair (fun (p:intPair) -> unit) -> Tot unit
+let foo h =
+  let ExIntro (IP p) hp = h in
   ()

examples/metatheory/f-omega.fst

@@ -1,3 +1,8 @@
+(*--build-config
+    options:--max_fuel 1 --max_ifuel 1 --initial_fuel 1 --initial_ifuel 1;
+    variables:LIB=../../lib;
+    other-files:$LIB/constr.fst $LIB/classical.fst $LIB/ext.fst
+ --*)
 (*
    Copyright 2008-2015 Catalin Hritcu (Inria), Aseem Rastogi (UMD), and
    Nikhil Swamy (Microsoft Research)
@@ -14,7 +19,7 @@
    limitations under the License.
 *)
 
-module LambdaOmega
+module FOmega
 
 open Constructive
 open Classical
@@ -1614,66 +1619,47 @@ let rec tred_diamond s t u h1 h2 =
     | MkLTup (TrLam k h11) (TrLam _ h12) ->
     (* AR: p only has one constructor Conj,
            but direct pattern matching doesn't work *)
-      let ExIntro t' p = tred_diamond h11 h12 in
-      (match p with
-    	| Conj pa pb -> ExIntro (TLam k t') (Conj (TrLam k pa) (TrLam k pb)))
+      let ExIntro t' (Conj pa pb) = tred_diamond h11 h12 in
+      ExIntro (TLam k t') (Conj (TrLam k pa) (TrLam k pb))
+
     (* if one is TrArr, the other has to be TrArr *)
     | MkLTup (TrArr h11 h12) (TrArr h21 h22) ->
-      let ExIntro v1 p1 = tred_diamond h11 h21 in
-      let ExIntro v2 p2 = tred_diamond h12 h22 in
-
-      (match p1 with
-    	| Conj p1a p1b ->
-    	  (match p2 with
-    	    | Conj p2a p2b ->
-    	      ExIntro (TArr v1 v2) (Conj (TrArr p1a p2a) (TrArr p1b p2b))))
+      let ExIntro v1 (Conj p1a p1b) = tred_diamond h11 h21 in
+      let ExIntro v2 (Conj p2a p2b) = tred_diamond h12 h22 in
+      ExIntro (TArr v1 v2) (Conj (TrArr p1a p2a) (TrArr p1b p2b))
+
     (* both TrApp *)
     | MkLTup (TrApp h11 h12) (TrApp h21 h22) ->
-      let ExIntro v1 p1 = tred_diamond h11 h21 in
-      let ExIntro v2 p2 = tred_diamond h12 h22 in
-
-      (match p1 with
-    	| Conj p1a p1b ->
-    	  (match p2 with
-    	    | Conj p2a p2b ->
-    	      ExIntro (TApp v1 v2) (Conj (TrApp p1a p2a) (TrApp p1b p2b))))
+      let ExIntro v1 (Conj p1a p1b) = tred_diamond h11 h21 in
+      let ExIntro v2 (Conj p2a p2b) = tred_diamond h12 h22 in
+      ExIntro (TApp v1 v2) (Conj (TrApp p1a p2a) (TrApp p1b p2b))
+
     (* both TrBeta *)
     | MkLTup (TrBeta #s1 #s2 #t1' #t2' k h11 h12)
              (TrBeta #s11 #s21 #u1' #u2' k' h21 h22) ->
-      let ExIntro v1 p1 = tred_diamond h11 h21 in
-      let ExIntro v2 p2 = tred_diamond h12 h22 in
-
-      (match p1 with
-    	| Conj p1a p1b ->
-    	  (match p2 with
-    	    | Conj p2a p2b ->
-    	      ExIntro (tsubst_beta_gen 0 v2 v1)
-                      (Conj (subst_of_tred_tred 0 p2a p1a)
-                            (subst_of_tred_tred 0 p2b p1b))))
+      let ExIntro v1 (Conj p1a p1b) = tred_diamond h11 h21 in
+      let ExIntro v2 (Conj p2a p2b) = tred_diamond h12 h22 in
+      ExIntro (tsubst_beta_gen 0 v2 v1)
+              (Conj (subst_of_tred_tred 0 p2a p1a)
+                    (subst_of_tred_tred 0 p2b p1b))
+
     (* one TrBeta and other TrApp *)
     | MkLTup (TrBeta #s1 #s2 #t1' #t2' k h11 h12)
              (TrApp #s1' #s2' #lu1' #u2' h21 h22) ->
     (* AR: does not work without this type annotation *)
       let h21:(tred (TLam.t s1') (TLam.t lu1')) = match h21 with
-    	| TrLam _ h' -> h'
-    	| TrRefl _ -> TrRefl (TLam.t s1')
-      in
+      	| TrLam _ h' -> h'
+      	| TrRefl _ -> TrRefl (TLam.t s1') in
 
-      let ExIntro v1 p1 = tred_diamond h11 h21 in
-      let ExIntro v2 p2 = tred_diamond h12 h22 in
+      let ExIntro v1 (Conj p1a p1b) = tred_diamond h11 h21 in
+      let ExIntro v2 (Conj p2a p2b) = tred_diamond h12 h22 in
+    	let v = tsubst_beta_gen 0 v2 v1 in
+    	ExIntro v (Conj (subst_of_tred_tred 0 p2a p1a) (TrBeta k p1b p2b))
 
-      (match p1 with
-    	| Conj p1a p1b ->
-    	  (match p2 with
-    	    | Conj p2a p2b ->
-    	      let v = tsubst_beta_gen 0 v2 v1 in
-    	      ExIntro v (Conj (subst_of_tred_tred 0 p2a p1a) (TrBeta k p1b p2b))))
     | MkLTup (TrApp #s1' #s2' #lu1' #u2' h21 h22)
              (TrBeta #s1 #s2 #t1' #t2' k h11 h12) ->
-      let ExIntro v1 p = tred_diamond h21 (TrLam k h11) in
-      let Conj (p1:tred lu1' v1) (p2:tred (TLam k t1') v1) = p in
-      let ExIntro v2 p = tred_diamond h22 h12 in
-      let Conj (p3:tred u2' v2) (p4:tred t2' v2) = p in
+      let ExIntro v1 (Conj p1 p2)  = tred_diamond h21 (TrLam k h11) in
+      let ExIntro v2 (Conj p3 p4)  = tred_diamond h22 h12 in
 
       let h_body:(tred (TLam.t lu1') (TLam.t v1)) = match p1 with
     	| TrLam _ h' -> h'
@@ -1690,9 +1676,8 @@ let rec tred_diamond s t u h1 h2 =
     | MkLTup (TrFor k h11) (TrFor _ h12) ->
     (* AR: p only has one constructor Conj,
            but direct pattern matching doesn't work *)
-      let ExIntro t' p = tred_diamond h11 h12 in
-      (match p with
-    	| Conj pa pb -> ExIntro (TFor k t') (Conj (TrFor k pa) (TrFor k pb)))
+      let ExIntro t' (Conj pa pb) = tred_diamond h11 h12 in
+      ExIntro (TFor k t') (Conj (TrFor k pa) (TrFor k pb))
 
 type tred_star: typ -> typ -> Type =
   | TsRefl : t:typ ->

src/tc/rel.fs

@@ -1946,12 +1946,14 @@ and solve_t' (env:Env.env) (problem:problem<typ,exp>) (wl:worklist) : solution =
             | (MisMatch, _) -> //heads definitely do not match
               let head1 = Util.head_and_args t1 |> fst in 
               let head2 = Util.head_and_args t2 |> fst in 
-              begin match head1.n, head2.n with 
-                | Typ_btvar _, _
-                | _, Typ_btvar _ -> (* may match by refinement *) 
-                  solve env (solve_prob orig (Some <| Util.mk_eq_typ t1 t2) [] wl)  
-                | _ -> giveup env "head mismatch" orig        
-              end
+              let may_equate head = match head.n with 
+                | Typ_btvar _  -> true
+                | Typ_const tc -> Env.is_projector env tc.v
+                | _ -> false  in
+              if (may_equate head1 || may_equate head2) && wl.smt_ok
+              then solve env (solve_prob orig (Some <| Util.mk_eq_typ t1 t2) [] wl)  
+              else giveup env "head mismatch" orig        
+
 
             | (_, Some (t1, t2)) -> //heads match after some delta steps
               solve_t env ({problem with lhs=t1; rhs=t2}) wl

src/tc/tcenv.fs

@@ -446,6 +446,13 @@ let lookup_typ_lid env (ftv:lident) : knd =
     | _ ->
       raise (Error(name_not_found ftv, range_of_lid ftv))
 
+let is_projector env (l:lident) : bool = 
+    match lookup_qname env l with 
+        | Some (Inr (Sig_tycon(_, _, _, _, _, quals, _)))
+        | Some (Inr (Sig_val_decl(_, _, quals, _))) -> 
+          Util.for_some (function Projector _ -> true | _ -> false) quals
+        | _ -> false
+
 let try_lookup_effect_lid env (ftv:lident) : option<knd> = 
   match lookup_qname env ftv with
     | Some (Inr (Sig_new_effect(ne, _))) -> 

src/tc/tcenv.fsi

@@ -105,6 +105,7 @@ val lookup_typ_abbrev : env -> lident -> option<typ>
 val lookup_effect_abbrev : env -> lident -> option<(binders * comp)>
 val lookup_btvar : env -> btvar -> knd
 val lookup_typ_lid : env -> lident -> knd
+val is_projector: env -> lident -> bool
 val try_lookup_effect_lid : env -> lident -> option<knd>
 val lookup_effect_lid : env -> lident -> knd
 val lookup_operator : env -> ident -> typ