aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
blob: 88ea08c84063011a9738d289ac1c881a95851686 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open CErrors
open Util
open Names
open Term
open Vars
open CClosure
open Reduction
open Reductionops
open Termops
open Environ
open Recordops
open Evarutil
open Evardefine
open Evarsolve
open Globnames
open Evd
open Pretype_errors
open Sigma.Notations
open Context.Named.Declaration

module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration

type unify_fun = transparent_state ->
  env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result

let debug_unification = ref (false)
let _ = Goptions.declare_bool_option {
  Goptions.optsync = true; Goptions.optdepr = false;
  Goptions.optname =
    "Print states sent to Evarconv unification";
  Goptions.optkey = ["Debug";"Unification"];
  Goptions.optread = (fun () -> !debug_unification);
  Goptions.optwrite = (fun a -> debug_unification:=a);
}

let unfold_projection env evd ts p c =
  let cst = Projection.constant p in
    if is_transparent_constant ts cst then
      Some (mkProj (Projection.make cst true, c))
    else None
      
let eval_flexible_term ts env evd c =
  match kind_of_term c with
  | Const (c,u as cu) ->
      if is_transparent_constant ts c
      then constant_opt_value_in env cu
      else None
  | Rel n ->
      (try match lookup_rel n env with
           | RelDecl.LocalAssum _ -> None
           | RelDecl.LocalDef (_,v,_) -> Some (lift n v)
       with Not_found -> None)
  | Var id ->
      (try
	 if is_transparent_variable ts id then
	   env |> lookup_named id |> NamedDecl.get_value
	 else None
       with Not_found -> None)
  | LetIn (_,b,_,c) -> Some (subst1 b c)
  | Lambda _ -> Some c
  | Proj (p, c) -> 
    if Projection.unfolded p then assert false
    else unfold_projection env evd ts p c
  | _ -> assert false

type flex_kind_of_term =
  | Rigid
  | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *)
  | Flexible of existential

let flex_kind_of_term ts env evd c sk =
  match kind_of_term c with
    | LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
      Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c)
    | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c
    | Evar ev -> Flexible ev
    | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid
    | Meta _ -> Rigid
    | Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
    | Cast _ | App _ | Case _ -> assert false

let apprec_nohdbeta ts env evd c =
  let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
  if Stack.not_purely_applicative sk
  then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
		   ts env evd Cst_stack.empty appr))
  else c

let position_problem l2r = function
  | CONV -> None
  | CUMUL -> Some l2r

let occur_rigidly (evk,_ as ev) evd t =
  let rec aux t =
    match kind_of_term (whd_evar evd t) with
    | App (f, c) -> if aux f then Array.exists aux c else false
    | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
    | Proj (p, c) -> not (aux c)
    | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
    | Cast (p, _, _) -> aux p
    | Lambda _ | LetIn _ -> false
    | Const _ -> false
    | Prod (_, b, t) -> ignore(aux b || aux t); true
    | Rel _ | Var _ -> false
    | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false
  in try ignore(aux t); false with Occur -> true

(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose 
   the problem (t1 stack1) = (t2 stack2) into a problem

     stack1 = params1@[c1]@extra_args1
     stack2 = us2@extra_args2
     t1 params1 c1 = proji params (c xs)
     t2 us2 = head us
     extra_args1 = extra_args2

   by finding a record R and an object c := [xs:bs](Build_R params v1..vn)
   with vi = (head us), for which we know that the i-th projection proji
   satisfies

      proji params (c xs) = head us

   Rem: such objects, usable for conversion, are defined in the objdef
   table; practically, it amounts to "canonically" equip t2 into a
   object c in structure R (since, if c1 were not an evar, the
   projection would have been reduced) *)

let check_conv_record env sigma (t1,sk1) (t2,sk2) =
  let (proji, u), arg = Universes.global_app_of_constr t1 in
  let canon_s,sk2_effective =
    try
      match kind_of_term t2 with
	Prod (_,a,b) -> (* assert (l2=[]); *)
	  let _, a, b = destProd (Evarutil.nf_evar sigma t2) in
      	  if dependent (mkRel 1) b then raise Not_found
	  else lookup_canonical_conversion (proji, Prod_cs),
	    (Stack.append_app [|a;pop b|] Stack.empty)
      | Sort s ->
	lookup_canonical_conversion
	  (proji, Sort_cs (family_of_sort s)),[]
      | _ ->
	let c2 = global_of_constr t2 in
	  lookup_canonical_conversion (proji, Const_cs c2),sk2
    with Not_found ->
      let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in 
	(c,cs),[]
  in
  let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
        o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in
  let params1, c1, extra_args1 =
    match arg with
    | Some c -> (* A primitive projection applied to c *)
      let ty = Retyping.get_type_of ~lax:true env sigma c in
      let (i,u), ind_args = 
	try Inductiveops.find_mrectype env sigma ty 
	with _ -> raise Not_found
      in Stack.append_app_list ind_args Stack.empty, c, sk1
    | None ->
      match Stack.strip_n_app nparams sk1 with
      | Some (params1, c1, extra_args1) -> params1, c1, extra_args1
      | _ -> raise Not_found in
  let us2,extra_args2 =
    let l_us = List.length us in
      if Int.equal l_us 0 then Stack.empty,sk2_effective
      else match (Stack.strip_n_app (l_us-1) sk2_effective) with
      | None -> raise Not_found
      | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
  let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
  let c' = subst_univs_level_constr subst c in
  let t' = subst_univs_level_constr subst t' in
  let bs' = List.map (subst_univs_level_constr subst) bs in
  let h, _ = decompose_app_vect t' in
    ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
    (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
    (n,Stack.zip(t2,sk2))

(* Precondition: one of the terms of the pb is an uninstantiated evar,
 * possibly applied to arguments. *)

let rec ise_try evd = function
    [] -> assert false
  | [f] -> f evd
  | f1::l ->
      match f1 evd with
      | Success _ as x -> x
      | UnifFailure _ -> ise_try evd l

let ise_and evd l =
  let rec ise_and i = function
      [] -> assert false
    | [f] -> f i
    | f1::l ->
        match f1 i with
	| Success i' -> ise_and i' l
	| UnifFailure _ as x -> x in
  ise_and evd l

let ise_exact ise x1 x2 =
  match ise x1 x2 with
  | None, out -> out
  | _, (UnifFailure _ as out) -> out
  | Some _, Success i -> UnifFailure (i,NotSameArgSize)

let ise_array2 evd f v1 v2 =
  let rec allrec i = function
    | -1 -> Success i
    | n ->
        match f i v1.(n) v2.(n) with
	| Success i' -> allrec i' (n-1)
	| UnifFailure _ as x -> x in
  let lv1 = Array.length v1 in
  if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
  else UnifFailure (evd,NotSameArgSize)

(* Applicative node of stack are read from the outermost to the innermost
   but are unified the other way. *)
let rec ise_app_stack2 env f evd sk1 sk2 =
  match sk1,sk2 with
  | Stack.App node1 :: q1, Stack.App node2 :: q2 ->
     let (t1,l1) = Stack.decomp_node_last node1 q1 in
     let (t2,l2) = Stack.decomp_node_last node2 q2 in
     begin match ise_app_stack2 env f evd l1 l2 with
	   |(_,UnifFailure _) as x -> x
	   |x,Success i' -> x,f env i' CONV t1 t2
     end
  | _, _ -> (sk1,sk2), Success evd

(* This function tries to unify 2 stacks element by element. It works
   from the end to the beginning. If it unifies a non empty suffix of
   stacks but not the entire stacks, the first part of the answer is
   Some(the remaining prefixes to tackle)) *)
let ise_stack2 no_app env evd f sk1 sk2 =
  let rec ise_stack2 deep i sk1 sk2 =
    let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i
      else None, x in
    match sk1, sk2 with
    | [], [] -> None, Success i
    | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
      (match f env i CONV t1 t2 with
      | Success i' ->
	(match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
	| Success i'' -> ise_stack2 true i'' q1 q2
        | UnifFailure _ as x -> fail x)
      | UnifFailure _ as x -> fail x)
    | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
       if eq_constant (Projection.constant p1) (Projection.constant p2)
       then ise_stack2 true i q1 q2
       else fail (UnifFailure (i, NotSameHead))
    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
      if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
        match ise_and i [
	  (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
	  (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
	  (fun i -> ise_exact (ise_stack2 false i) a1 a2)] with
        | Success i' -> ise_stack2 true i' q1 q2
        | UnifFailure _ as x -> fail x
      else fail (UnifFailure (i,NotSameHead))
    | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
    | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
    | Stack.App _ :: _, Stack.App _ :: _ ->
       if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else
	 begin match ise_app_stack2 env f i sk1 sk2 with
	       |_,(UnifFailure _ as x) -> fail x
	       |(l1, l2), Success i' -> ise_stack2 true i' l1 l2
	 end
    |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead))
  in ise_stack2 false evd (List.rev sk1) (List.rev sk2)

(* Make sure that the matching suffix is the all stack *)
let exact_ise_stack2 env evd f sk1 sk2 =
  let rec ise_stack2 i sk1 sk2 =
    match sk1, sk2 with
    | [], [] -> Success i
    | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 ->
      ise_and i [
      (fun i -> ise_stack2 i q1 q2);
      (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2);
      (fun i -> f env i CONV t1 t2)]
    | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1,
      Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
      if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
	ise_and i [
	  (fun i -> ise_stack2 i q1 q2);
	  (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
	  (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
	  (fun i -> ise_stack2 i a1 a2)]
      else UnifFailure (i,NotSameHead)
    | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 ->
       if eq_constant (Projection.constant p1) (Projection.constant p2)
       then ise_stack2 i q1 q2
       else (UnifFailure (i, NotSameHead))
    | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _
    | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false
    | Stack.App _ :: _, Stack.App _ :: _ ->
	 begin match ise_app_stack2 env f i sk1 sk2 with
	       |_,(UnifFailure _ as x) -> x
	       |(l1, l2), Success i' -> ise_stack2 i' l1 l2
	 end
    |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead)
  in
  if Reductionops.Stack.compare_shape sk1 sk2 then
    ise_stack2 evd (List.rev sk1) (List.rev sk2)
  else UnifFailure (evd, (* Dummy *) NotSameHead)

let rec evar_conv_x ts env evd pbty term1 term2 =
  let term1 = whd_head_evar evd term1 in
  let term2 = whd_head_evar evd term2 in
  (* Maybe convertible but since reducing can erase evars which [evar_apprec]
     could have found, we do it only if the terms are free of evar.
     Note: incomplete heuristic... *)
  let ground_test =
    if is_ground_term evd term1 && is_ground_term evd term2 then (
      let e =
	try
	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
	    env evd term1 term2 
	  in
	    if b then Success evd
	    else UnifFailure (evd, ConversionFailed (env,term1,term2))
	with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
      in
	match e with
	| UnifFailure (evd, e) when not (is_ground_env evd env) -> None
	| _ -> Some e)
    else None
  in
  match ground_test with
    | Some result -> result
    | None ->
	(* Until pattern-unification is used consistently, use nohdbeta to not
	   destroy beta-redexes that can be used for 1st-order unification *)
        let term1 = apprec_nohdbeta (fst ts) env evd term1 in
        let term2 = apprec_nohdbeta (fst ts) env evd term2 in
	let default () = 
          evar_eqappr_x ts env evd pbty
            (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty)
            (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty)
	in
          begin match kind_of_term term1, kind_of_term term2 with
          | Evar ev, _ when Evd.is_undefined evd (fst ev) ->
            (match solve_simple_eqn (evar_conv_x ts) env evd
              (position_problem true pbty,ev,term2) with
	      | UnifFailure (_,OccurCheck _) -> 
		(* Eta-expansion might apply *) default ()
	      | x -> x)
          | _, Evar ev when Evd.is_undefined evd (fst ev) ->
            (match solve_simple_eqn (evar_conv_x ts) env evd
              (position_problem false pbty,ev,term1) with
	      | UnifFailure (_, OccurCheck _) ->
		(* Eta-expansion might apply *) default () 
	      | x -> x)
          | _ -> default ()
        end

and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
    ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
  let quick_fail i = (* not costly, loses info *)
    UnifFailure (i, NotSameHead)
  in
  let miller_pfenning on_left fallback ev lF tM evd =
    match is_unification_pattern_evar env evd ev lF tM with
      | None -> fallback ()
      | Some l1' -> (* Miller-Pfenning's patterns unification *)
	let t2 = nf_evar evd tM in
	let t2 = solve_pattern_eqn env l1' t2 in
	  solve_simple_eqn (evar_conv_x ts) env evd
	    (position_problem on_left pbty,ev,t2) 
  in
  let consume_stack on_left (termF,skF) (termO,skO) evd =
    let switch f a b = if on_left then f a b else f b a in
    let not_only_app = Stack.not_purely_applicative skO in
    match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
      |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
      |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
      |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
      |_, (UnifFailure _ as x) -> x
      |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
  let eta env evd onleft sk term sk' term' =
    assert (match sk with [] -> true | _ -> false);
    let (na,c1,c'1) = destLambda term in
    let c = nf_evar evd c1 in
    let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
    let out1 = whd_betaiota_deltazeta_for_iota_state
      (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
    let out2 = whd_nored_state evd
      (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), 
      Cst_stack.empty in
    if onleft then evar_eqappr_x ts env' evd CONV out1 out2
    else evar_eqappr_x ts env' evd CONV out2 out1
  in
  let rigids env evd sk term sk' term' =
    let univs = Universes.eq_constr_universes term term' in
    match univs with
    | Some univs ->
       ise_and evd [(fun i ->
         let cstrs = Universes.to_constraints (Evd.universes i) univs in
           try Success (Evd.add_constraints i cstrs)
           with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
                  (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')]
    | None ->
      UnifFailure (evd,NotSameHead)
  in
  let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM =
    let switch f a b = if on_left then f a b else f b a in
    let not_only_app = Stack.not_purely_applicative skM in
    let f1 i =
      match Stack.list_of_app_stack skF with
      | None -> quick_fail evd
      | Some lF -> 
        let tM = Stack.zip apprM in
	  miller_pfenning on_left
	    (fun () -> if not_only_app then (* Postpone the use of an heuristic *)
	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
	    else quick_fail i)
	  ev lF tM i
    and consume (termF,skF as apprF) (termM,skM as apprM) i = 
      if not (Stack.is_empty skF && Stack.is_empty skM) then
        consume_stack on_left apprF apprM i
      else quick_fail i
    and delta i =
      switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
	     (whd_betaiota_deltazeta_for_iota_state
  	        (fst ts) env i cstsM (vM,skM))
    in    
    let default i = ise_try i [f1; consume apprF apprM; delta]
    in
      match kind_of_term termM with
      | Proj (p, c) when not (Stack.is_empty skF) ->
	(* Might be ?X args = p.c args', and we have to eta-expand the 
	   primitive projection if |args| >= |args'|+1. *)
	let nargsF = Stack.args_size skF and nargsM = Stack.args_size skM in
	  begin
	    (* ?X argsF' ~= (p.c ..) argsM' -> ?X ~= (p.c ..), no need to expand *)
	    if nargsF <= nargsM then default evd
	    else 
	      let f =
		try 
		  let termM' = Retyping.expand_projection env evd p c [] in
		  let apprM', cstsM' = 
		    whd_betaiota_deltazeta_for_iota_state
		      (fst ts) env evd cstsM (termM',skM)
		  in
		  let delta' i = 
		    switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') 
		  in
		    fun i -> ise_try i [f1; consume apprF apprM'; delta']
		with Retyping.RetypeError _ ->
		(* Happens thanks to w_unify building ill-typed terms *) 
		  default
	      in f evd
	  end
      | _ -> default evd
  in
  let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
    let switch f a b = if on_left then f a b else f b a in
    let eta evd =
      match kind_of_term termR with
      | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
         eta env evd false skR termR skF termF
      | Construct u -> eta_constructor ts env evd skR u skF termF
      | _ -> UnifFailure (evd,NotSameHead)
    in
    match Stack.list_of_app_stack skF with
    | None ->
        ise_try evd [consume_stack on_left apprF apprR; eta]
    | Some lF ->
        let tR = Stack.zip apprR in
	  miller_pfenning on_left
	    (fun () ->
	      ise_try evd 
	        [eta;(* Postpone the use of an heuristic *)
		 (fun i -> 
		   if not (occur_rigidly ev i tR) then
                     let i,tF =
                       if isRel tR || isVar tR then
                         (* Optimization so as to generate candidates *)
                         let i,ev = evar_absorb_arguments env i ev lF in
                         i,mkEvar ev
                       else
                         i,Stack.zip apprF in
		     switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
	               tF tR
		   else
                     UnifFailure (evd,OccurCheck (fst ev,tR)))])
	    ev lF tR evd
  in
  let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
  (* Evar must be undefined since we have flushed evars *)
  let () = if !debug_unification then
	     let open Pp in
	     Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in
  match (flex_kind_of_term (fst ts) env evd term1 sk1, 
	 flex_kind_of_term (fst ts) env evd term2 sk2) with
    | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
        (* sk1[?ev1] =? sk2[?ev2] *)
	let f1 i =
          (* Try first-order unification *)
	  match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
	  | None, Success i' ->
            (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
            (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
	    let ev1' = whd_evar i' (mkEvar ev1) in
	      if isEvar ev1' then
		solve_simple_eqn (evar_conv_x ts) env i'
		  (position_problem true pbty,destEvar ev1',term2)
	      else 
		evar_eqappr_x ts env evd pbty 
		  ((ev1', sk1), csts1) ((term2, sk2), csts2)
	  | Some (r,[]), Success i' ->
            (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
            (* we now unify r[?ev1] and ?ev2 *)
	    let ev2' = whd_evar i' (mkEvar ev2) in
	      if isEvar ev2' then
		solve_simple_eqn (evar_conv_x ts) env i'
		  (position_problem false pbty,destEvar ev2',Stack.zip(term1,r))
	      else 
		evar_eqappr_x ts env evd pbty 
		  ((ev2', sk1), csts1) ((term2, sk2), csts2)
	  | Some ([],r), Success i' ->
            (* Symmetrically *)
            (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
            (* we now unify ?ev1 and r[?ev2] *)
	    let ev1' = whd_evar i' (mkEvar ev1) in
	      if isEvar ev1' then
		solve_simple_eqn (evar_conv_x ts) env i'
	          (position_problem true pbty,destEvar ev1',Stack.zip(term2,r))
	      else evar_eqappr_x ts env evd pbty 
		((ev1', sk1), csts1) ((term2, sk2), csts2)
	  | None, (UnifFailure _ as x) ->
             (* sk1 and sk2 have no common outer part *)
             if Stack.not_purely_applicative sk2 then
               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
               flex_rigid true ev1 appr1 appr2
             else
             if Stack.not_purely_applicative sk1 then
               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
               flex_rigid false ev2 appr2 appr1
             else
               (* We could instead try Miller unification, then
                  postpone to see if other equations help, as in:
                  [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *)
               x
	  | Some _, Success _ ->
             (* sk1 and sk2 have a common outer part *)
             if Stack.not_purely_applicative sk2 then
               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
               flex_rigid true ev1 appr1 appr2
             else
             if Stack.not_purely_applicative sk1 then
               (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
               flex_rigid false ev2 appr2 appr1
             else
               (* We could instead try Miller unification, then
                  postpone to see if other equations help, as in:
                  [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
               UnifFailure (i,NotSameArgSize)
          | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")

	and f2 i =
          if Evar.equal sp1 sp2 then
	    match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
	    |None, Success i' ->
              Success (solve_refl (fun env i pbty a1 a2 ->
                is_success (evar_conv_x ts env i pbty a1 a2))
                env i' (position_problem true pbty) sp1 al1 al2)
	    |_, (UnifFailure _ as x) -> x
            |Some _, _ -> UnifFailure (i,NotSameArgSize)
          else UnifFailure (i,NotSameHead)
	in
	ise_try evd [f1; f2]

    | Flexible ev1, MaybeFlexible v2 ->
      flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2

    | MaybeFlexible v1, Flexible ev2 -> 
      flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1

    | MaybeFlexible v1, MaybeFlexible v2 -> begin
        match kind_of_term term1, kind_of_term term2 with
        | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
        let f1 i = (* FO *)
          ise_and i
            [(fun i -> ise_try i
               [(fun i -> evar_conv_x ts env i CUMUL t1 t2);
                (fun i -> evar_conv_x ts env i CUMUL t2 t1)]);
             (fun i -> evar_conv_x ts env i CONV b1 b2);
	     (fun i ->
	       let b = nf_evar i b1 in
	       let t = nf_evar i t1 in
               let na = Nameops.name_max na1 na2 in
	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
	and f2 i =
          let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
          and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
	  in evar_eqappr_x ts env i pbty out1 out2
	in
	ise_try evd [f1; f2]

	| Proj (p, c), Proj (p', c') 
	  when Constant.equal (Projection.constant p) (Projection.constant p') ->
	  let f1 i = 
	    ise_and i 
	    [(fun i -> evar_conv_x ts env i CONV c c');
	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
	  and f2 i =
            let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
            and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2)
	    in evar_eqappr_x ts env i pbty out1 out2
	  in
	    ise_try evd [f1; f2]
	      
	(* Catch the p.c ~= p c' cases *)
	| Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' ->
	  let res = 
	    try Some (destApp (Retyping.expand_projection env evd p c []))
	    with Retyping.RetypeError _ -> None
	  in
	    (match res with 
	    | Some (f1,args1) -> 
	      evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) 
		(appr2,csts2)
	    | None -> UnifFailure (evd,NotSameHead))
	      
	| Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') ->
	  let res = 
	    try Some (destApp (Retyping.expand_projection env evd p' c' []))
	    with Retyping.RetypeError _ -> None
	  in 
	    (match res with
	    | Some (f2,args2) ->
	      evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2)
	    | None -> UnifFailure (evd,NotSameHead))
	      
	| _, _ ->
	let f1 i = 
	  (* Gather the universe constraints that would make term1 and term2 equal.
	     If these only involve unifications of flexible universes to other universes,
	     allow this identification (first-order unification of universes). Otherwise
	     fallback to unfolding.
	  *)
	  let univs = Universes.eq_constr_universes term1 term2 in
          match univs with
          | Some univs ->
	      ise_and i [(fun i -> 
		try Success (Evd.add_universe_constraints i univs)
		with UniversesDiffer -> UnifFailure (i,NotSameHead)
		| Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p));
			 (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
          | None ->
            UnifFailure (i,NotSameHead)
	and f2 i =
	  (try 
	     if not (snd ts) then raise Not_found
	     else conv_record ts env i
               (try check_conv_record env i appr1 appr2
		with Not_found -> check_conv_record env i appr2 appr1)
           with Not_found -> UnifFailure (i,NoCanonicalStructure))
	and f3 i =
          (* heuristic: unfold second argument first, exception made
             if the first argument is a beta-redex (expand a constant
             only if necessary) or the second argument is potentially
             usable as a canonical projection or canonical value *)
          let rec is_unnamed (hd, args) = match kind_of_term hd with
            | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) ->
	      Stack.not_purely_applicative args
            | (CoFix _|Meta _|Rel _)-> true
            | Evar _ -> Stack.not_purely_applicative args
	    (* false (* immediate solution without Canon Struct *)*)
            | Lambda _ -> assert (match args with [] -> true | _ -> false); true
            | LetIn (_,b,_,c) -> is_unnamed
	     (fst (whd_betaiota_deltazeta_for_iota_state
		      (fst ts) env i Cst_stack.empty (subst1 b c, args)))
	    | Fix _ -> true (* Partially applied fix can be the result of a whd call *)
	    | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args
            | Case _ | App _| Cast _ -> assert false in
          let rhs_is_stuck_and_unnamed () =
	    let applicative_stack = fst (Stack.strip_app sk2) in
	    is_unnamed
	      (fst (whd_betaiota_deltazeta_for_iota_state
		      (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in
          let rhs_is_already_stuck =
            rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in

	  if (isLambda term1 || rhs_is_already_stuck)
	    && (not (Stack.not_purely_applicative sk1)) then
	    evar_eqappr_x ~rhs_is_already_stuck ts env i pbty
	      (whd_betaiota_deltazeta_for_iota_state
		 (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
	      (appr2,csts2)
	  else
	    evar_eqappr_x ts env i pbty (appr1,csts1)
	      (whd_betaiota_deltazeta_for_iota_state
		 (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
	in
	ise_try evd [f1; f2; f3]
    end

    | Rigid, Rigid when isLambda term1 && isLambda term2 ->
        let (na1,c1,c'1) = destLambda term1 in
        let (na2,c2,c'2) = destLambda term2 in
        assert app_empty;
        ise_and evd
          [(fun i -> evar_conv_x ts env i CONV c1 c2);
           (fun i ->
	     let c = nf_evar i c1 in
             let na = Nameops.name_max na1 na2 in
	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]

    | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
    | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1

    | MaybeFlexible v1, Rigid ->
	let f3 i =
	  (try 
	     if not (snd ts) then raise Not_found
	     else conv_record ts env i (check_conv_record env i appr1 appr2)
           with Not_found -> UnifFailure (i,NoCanonicalStructure))
	and f4 i =
	  evar_eqappr_x ts env i pbty
	    (whd_betaiota_deltazeta_for_iota_state
	       (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1))
	    (appr2,csts2)
	in
	  ise_try evd [f3; f4]

    | Rigid, MaybeFlexible v2 ->
	let f3 i =
	  (try
	     if not (snd ts) then raise Not_found
	     else conv_record ts env i (check_conv_record env i appr2 appr1)
           with Not_found -> UnifFailure (i,NoCanonicalStructure))
	and f4 i =
	  evar_eqappr_x ts env i pbty (appr1,csts1)
	    (whd_betaiota_deltazeta_for_iota_state
	       (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2))
	in
	  ise_try evd [f3; f4]

    (* Eta-expansion *)
    | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
        eta env evd true sk1 term1 sk2 term2

    | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
        eta env evd false sk2 term2 sk1 term1

    | Rigid, Rigid -> begin
        match kind_of_term term1, kind_of_term term2 with

	| Sort s1, Sort s2 when app_empty ->
	    (try
	       let evd' =
		 if pbty == CONV
		 then Evd.set_eq_sort env evd s1 s2
		 else Evd.set_leq_sort env evd s1 s2
	       in Success evd'
	     with Univ.UniverseInconsistency p ->
               UnifFailure (evd,UnifUnivInconsistency p)
	     | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead))

	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
            ise_and evd
              [(fun i -> evar_conv_x ts env i CONV c1 c2);
               (fun i ->
 	         let c = nf_evar i c1 in
                 let na = Nameops.name_max n1 n2 in
	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]

	| Rel x1, Rel x2 ->
	    if Int.equal x1 x2 then
              exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
            else UnifFailure (evd,NotSameHead)

	| Var var1, Var var2 ->
	    if Id.equal var1 var2 then
              exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
            else UnifFailure (evd,NotSameHead)

	| Const _, Const _
	| Ind _, Ind _ 
	| Construct _, Construct _ ->
	  rigids env evd sk1 term1 sk2 term2

	| Construct u, _ ->
	  eta_constructor ts env evd sk1 u sk2 term2
	    
	| _, Construct u ->
	  eta_constructor ts env evd sk2 u sk1 term1

	| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
	  if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
            ise_and evd [
	      (fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2);
	      (fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2);
	      (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
	  else UnifFailure (evd, NotSameHead)

	| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
            if Int.equal i1 i2  then
              ise_and evd
                [(fun i -> ise_array2 i
                    (fun i -> evar_conv_x ts env i CONV) tys1 tys2);
                 (fun i -> ise_array2 i
		     (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV)
		     bds1 bds2);
                 (fun i -> exact_ise_stack2 env i
                     (evar_conv_x ts) sk1 sk2)]
            else UnifFailure (evd,NotSameHead)

	| (Meta _, _) | (_, Meta _) ->
	  begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
	  |_, (UnifFailure _ as x) -> x
	  |None, Success i' -> evar_conv_x ts env i' CONV term1 term2
	  |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2'))
	  end

	| (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ ->
	  UnifFailure (evd,NotSameHead)
	| _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) ->
	  UnifFailure (evd,NotSameHead)

	| (App _ | Cast _ | Case _ | Proj _), _ -> assert false
	| (LetIn _| Evar _), _ -> assert false
	| (Lambda _), _ -> assert false

      end

and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) =
  (* Tries to unify the states

        (proji params1 c1 | sk1)   =   (proji params2 (c (?xs:bs)) | sk2)

     and the terms

        h us  =  h2 us2

     where

     c = the constant for the canonical structure (i.e. some term of the form
         fun (xs:bs) => Build_R params v1 .. vi-1 (h us) vi+1 .. vn)
     bs = the types of the parameters of the canonical structure
     c1 = the main argument of the canonical projection
     sk1, sk2 = the surrounding stacks of the conversion problem
     params1, params2 = the params of the projection (empty if a primitive proj)

     knowing that

       (proji params1 c1 | sk1)   =   (h2 us2 | sk2)

     had to be initially resolved
  *)
  let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
  if Reductionops.Stack.compare_shape sk1 sk2 then
    let (evd',ks,_,test) =
      List.fold_left
	(fun (i,ks,m,test) b ->
	  if match n with Some n -> Int.equal m n | None -> false then
	    let ty = Retyping.get_type_of env i t2 in
	    let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in
	      (i,t2::ks, m-1, test)
	  else
	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
	    let i = Sigma.Unsafe.of_evar_map i in
            let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
            let i' = Sigma.to_evar_map i' in
	    (i', ev :: ks, m - 1,test))
	(evd,[],List.length bs,fun i -> Success i) bs
    in
    let app = mkApp (c, Array.rev_of_list ks) in
    ise_and evd'
      [(fun i ->
	exact_ise_stack2 env i
          (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x))
          params1 params);
       (fun i ->
	 exact_ise_stack2 env i
           (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u))
           us2 us);
       (fun i -> evar_conv_x trs env i CONV c1 app);
       (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2);
       test;
       (fun i -> evar_conv_x trs env i CONV h2
	 (fst (decompose_app_vect (substl ks h))))]
  else UnifFailure(evd,(*dummy*)NotSameHead)

and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
  let mib = lookup_mind (fst ind) env in
    match mib.Declarations.mind_record with
    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
      let pars = mib.Declarations.mind_nparams in
	(try 
	   let l1' = Stack.tail pars sk1 in
	   let l2' = 
	     let term = Stack.zip (term2,sk2) in 
	       List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs)
	   in
	     exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' 
	       (Stack.append_app_list l2' Stack.empty)
	 with 
	 | Invalid_argument _ ->
	   (* Stack.tail: partially applied constructor *)
	   UnifFailure(evd,NotSameHead))
    | _ -> UnifFailure (evd,NotSameHead)

let evar_conv_x ts = evar_conv_x (ts, true)

(* Profiling *)
let evar_conv_x =
  if Flags.profile then
    let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in
      Profile.profile6 evar_conv_xkey evar_conv_x
  else evar_conv_x

let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()

let evar_conv_x ts = Hook.get evar_conv_hook_get ts

let set_evar_conv f = Hook.set evar_conv_hook_set f


(* We assume here |l1| <= |l2| *)

let first_order_unification ts env evd (ev1,l1) (term2,l2) =
  let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in
  ise_and evd
    (* First compare extra args for better failure message *)
    [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1);
    (fun i ->
      (* Then instantiate evar unless already done by unifying args *)
      let t2 = mkApp(term2,deb2) in
      if is_defined i (fst ev1) then
	evar_conv_x ts env i CONV t2 (mkEvar ev1)
      else
	solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))]

let choose_less_dependent_instance evk evd term args =
  let evi = Evd.find_undefined evd evk in
  let subst = make_pure_subst evi args in
  let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in
  match subst' with
  | [] -> None
  | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)

let apply_on_subterm env evdref f c t =
  let rec applyrec (env,(k,c) as acc) t =
    (* By using eq_constr, we make an approximation, for instance, we *)
    (* could also be interested in finding a term u convertible to t *)
    (* such that c occurs in u *)
    if e_eq_constr_univs evdref c t then f k
    else
      match kind_of_term t with
      | Evar (evk,args) when Evd.is_undefined !evdref evk ->
          let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in
          let g decl a = if is_local_assum decl then applyrec acc a else a in
          mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args)))
      | _ ->
        map_constr_with_binders_left_to_right
	  (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
	  applyrec acc t
  in
  applyrec (env,(0,c)) t

let filter_possible_projections c ty ctxt args =
  (* Since args in the types will be replaced by holes, we count the
     fv of args to have a well-typed filter; don't know how necessary
     it is however to have a well-typed filter here *)
  let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in
  let fv2 = collect_vars (mkApp (c,args)) in
  let len = Array.length args in
  let tyvars = collect_vars ty in
  List.map_i (fun i decl ->
    let () = assert (i < len) in
    let a = Array.unsafe_get args i in
    (match decl with
     | NamedDecl.LocalAssum _ -> false
     | NamedDecl.LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
    a == c ||
    (* Here we make an approximation, for instance, we could also be *)
    (* interested in finding a term u convertible to c such that a occurs *)
    (* in u *)
    isRel a && Int.Set.mem (destRel a) fv1 ||
    isVar a && Id.Set.mem (destVar a) fv2 ||
    Id.Set.mem (NamedDecl.get_id decl) tyvars)
    0 ctxt

let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
let set_solve_evars f = solve_evars := f

(* We solve the problem env_rhs |- ?e[u1..un] = rhs knowing
 * x1:T1 .. xn:Tn |- ev : ty
 * by looking for a maximal well-typed abtraction over u1..un in rhs
 *
 * We first build C[e11..e1p1,..,en1..enpn] obtained from rhs by replacing
 * all occurrences of u1..un by evars eij of type Ti' where itself Ti' has
 * been obtained from the type of ui by also replacing all occurrences of
 * u1..ui-1 by evars.
 *
 * Then, we use typing to infer the relations between the different
 * occurrences. If some occurrence is still unconstrained after typing,
 * we instantiate successively the unresolved occurrences of un by xn,
 * of un-1 by xn-1, etc [the idea comes from Chung-Kil Hur, that he
 * used for his Heq plugin; extensions to several arguments based on a
 * proposition from Dan Grayson]
 *)

exception TypingFailed of evar_map

let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
  try
  let evi = Evd.find_undefined evd evk in
  let env_evar = evar_filtered_env evi in
  let sign = named_context_val env_evar in
  let ctxt = evar_filtered_context evi in
  let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in

  let rec make_subst = function
  | decl'::ctxt', c::l, occs::occsl when isVarId (NamedDecl.get_id decl') c ->
      begin match occs with
      | Some _ ->
        error "Cannot force abstraction on identity instance."
      | None ->
        make_subst (ctxt',l,occsl)
      end
  | decl'::ctxt', c::l, occs::occsl ->
      let id = NamedDecl.get_id decl' in
      let t = NamedDecl.get_type decl' in
      let evs = ref [] in
      let ty = Retyping.get_type_of env_rhs evd c in
      let filter' = filter_possible_projections c ty ctxt args in
      (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl)
  | _, _, [] -> []
  | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in

  let rec set_holes evdref rhs = function
  | (id,_,c,cty,evsref,filter,occs)::subst ->
      let set_var k =
        match occs with
        | Some Locus.AllOccurrences -> mkVar id
        | Some _ -> error "Selection of specific occurrences not supported"
        | None ->
        let evty = set_holes evdref cty subst in
        let instance = Filter.filter_list filter instance in
        let evd = Sigma.Unsafe.of_evar_map !evdref in
        let Sigma (ev, evd, _) = new_evar_instance sign evd evty ~filter instance in
        let evd = Sigma.to_evar_map evd in
        evdref := evd;
        evsref := (fst (destEvar ev),evty)::!evsref;
        ev in
      set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst
  | [] -> rhs in

  let subst = make_subst (ctxt,Array.to_list args,argoccs) in

  let evdref = ref evd in
  let rhs = set_holes evdref rhs subst in
  let evd = !evdref in

  (* We instantiate the evars of which the value is forced by typing *)
  let evd,rhs =
    let evdref = ref evd in
    try let c = !solve_evars env_evar evdref rhs in !evdref,c
    with e when Pretype_errors.precatchable_exception e ->
      (* Could not revert all subterms *)
      raise (TypingFailed !evdref) in

  let rec abstract_free_holes evd = function
  | (id,idty,c,_,evsref,_,_)::l ->
      let rec force_instantiation evd = function
      | (evk,evty)::evs ->
          let evd =
            if is_undefined evd evk then
              (* We force abstraction over this unconstrained occurrence *)
              (* and we use typing to propagate this instantiation *)
              (* This is an arbitrary choice *)
              let evd = Evd.define evk (mkVar id) evd in
              match evar_conv_x ts env_evar evd CUMUL idty evty with
              | UnifFailure _ -> error "Cannot find an instance"
              | Success evd ->
              match reconsider_unif_constraints (evar_conv_x ts) evd with
              | UnifFailure _ -> error "Cannot find an instance"
              | Success evd ->
              evd
            else
              evd
          in
          force_instantiation evd evs
      | [] ->
          abstract_free_holes evd l
      in
      force_instantiation evd !evsref
  | [] ->
    let evd = 
      try Evarsolve.check_evar_instance evd evk rhs 
	    (evar_conv_x full_transparent_state)
      with IllTypedInstance _ -> raise (TypingFailed evd)
    in
      Evd.define evk rhs evd 
  in
  abstract_free_holes evd subst, true
  with TypingFailed evd -> evd, false

let second_order_matching_with_args ts env evd pbty ev l t =
(*
  let evd,ev = evar_absorb_arguments env evd ev l in
  let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
  let evd, b = second_order_matching ts env evd ev argoccs t in
  if b then Success evd
  else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
  if b then Success evd else
 *)
  let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
  UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))

let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
  let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
  let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
  let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in
  let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in
  let () = if !debug_unification then
	     let open Pp in
	     Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1
                                       ++ cut () ++ print_constr t2 ++ cut ())) in
  let app_empty = Array.is_empty l1 && Array.is_empty l2 in
  match kind_of_term term1, kind_of_term term2 with
  | Evar (evk1,args1), (Rel _|Var _) when app_empty
      && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a)
        (remove_instance_local_defs evd evk1 args1) ->
      (* The typical kind of constraint coming from pattern-matching return
         type inference *)
      (match choose_less_dependent_instance evk1 evd term2 args1 with
      | Some evd -> Success evd
      | None ->
         let reason = ProblemBeyondCapabilities in
         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
  | (Rel _|Var _), Evar (evk2,args2) when app_empty
      && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
        (remove_instance_local_defs evd evk2 args2) ->
      (* The typical kind of constraint coming from pattern-matching return
         type inference *)
      (match choose_less_dependent_instance evk2 evd term1 args2 with
      | Some evd -> Success evd
      | None ->
         let reason = ProblemBeyondCapabilities in
         UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
  | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
      let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
      Success (solve_refl ~can_drop:true f env evd
                 (position_problem true pbty) evk1 args1 args2)
  | Evar ev1, Evar ev2 when app_empty ->
      Success (solve_evar_evar ~force:true
        (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
        (position_problem true pbty) ev1 ev2)
  | Evar ev1,_ when Array.length l1 <= Array.length l2 ->
      (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
      (* and otherwise second-order matching *)
      ise_try evd
        [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2);
         (fun evd ->
           second_order_matching_with_args ts env evd pbty ev1 l1 t2)]
  | _,Evar ev2 when Array.length l2 <= Array.length l1 ->
      (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
      (* and otherwise second-order matching *)
      ise_try evd
        [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1);
         (fun evd ->
           second_order_matching_with_args ts env evd pbty ev2 l2 t1)]
  | Evar ev1,_ ->
      (* Try second-order pattern-matching *)
      second_order_matching_with_args ts env evd pbty ev1 l1 t2
  | _,Evar ev2 ->
      (* Try second-order pattern-matching *)
      second_order_matching_with_args ts env evd pbty ev2 l2 t1
  | _ ->
      (* Some head evar have been instantiated, or unknown kind of problem *)
      evar_conv_x ts env evd pbty t1 t2

let error_cannot_unify env evd pb ?reason t1 t2 =
  Pretype_errors.error_cannot_unify
    ~loc:(loc_of_conv_pb evd pb) env
    evd ?reason (t1, t2)

let check_problems_are_solved env evd =
  match snd (extract_all_conv_pbs evd) with
  | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
  | _ -> ()

let max_undefined_with_candidates evd =
  (* If evar were ordered with highest index first, fold_undefined
     would be going decreasingly and we could use fold_undefined to
     find the undefined evar of maximum index (alternatively,
     max_bindings from ocaml 3.12 could be used); instead we traverse
     the whole map *)
  let l = Evd.fold_undefined
    (fun evk ev_info evars ->
        match ev_info.evar_candidates with
        | None -> evars
        | Some l -> (evk,ev_info,l)::evars) evd [] in
  match l with
  | [] -> None
  | a::l -> Some (List.last (a::l))

let rec solve_unconstrained_evars_with_candidates ts evd =
  (* max_undefined is supposed to return the most recent, hence
     possibly most dependent evar *)
  match max_undefined_with_candidates evd with
  | None -> evd
  | Some (evk,ev_info,l) ->
      let rec aux = function
      | [] -> error "Unsolvable existential variables."
      | a::l ->
          try
            let conv_algo = evar_conv_x ts in
            let evd = check_evar_instance evd evk a conv_algo in
            let evd = Evd.define evk a evd in
            match reconsider_unif_constraints conv_algo evd with
            | Success evd -> solve_unconstrained_evars_with_candidates ts evd
            | UnifFailure _ -> aux l
          with
          | IllTypedInstance _ -> aux l
          | e when Pretype_errors.precatchable_exception e -> aux l in
      (* List.rev is there to favor most dependent solutions *)
      (* and favor progress when used with the refine tactics *)
      let evd = aux (List.rev l) in
      solve_unconstrained_evars_with_candidates ts evd

let solve_unconstrained_impossible_cases env evd =
  Evd.fold_undefined (fun evk ev_info evd' ->
    match ev_info.evar_source with
    | loc,Evar_kinds.ImpossibleCase ->
      let j, ctx = coq_unit_judge () in
      let evd' = Evd.merge_context_set Evd.univ_flexible_alg ~loc evd' ctx in
      let ty = j_type j in
      let conv_algo = evar_conv_x full_transparent_state in
      let evd' = check_evar_instance evd' evk ty conv_algo in
	Evd.define evk ty evd' 
    | _ -> evd') evd evd

let solve_unif_constraints_with_heuristics env
    ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd =
  let evd = solve_unconstrained_evars_with_candidates ts evd in
  let rec aux evd pbs progress stuck =
    match pbs with
    | (pbty,env,t1,t2 as pb) :: pbs ->
        (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
	| Success evd' ->
	    let (evd', rest) = extract_all_conv_pbs evd' in
            begin match rest with
            | [] -> aux evd' pbs true stuck
            | _ -> (* Unification got actually stuck, postpone *)
	      aux evd pbs progress (pb :: stuck)
            end
        | UnifFailure (evd,reason) ->
           error_cannot_unify env evd pb ~reason t1 t2)
    | _ -> 
	if progress then aux evd stuck false []
	else 
	  match stuck with
	  | [] -> (* We're finished *) evd
	  | (pbty,env,t1,t2 as pb) :: _ ->
	     (* There remains stuck problems *)
             error_cannot_unify env evd pb t1 t2
  in
  let (evd,pbs) = extract_all_conv_pbs evd in
  let heuristic_solved_evd = aux evd pbs false [] in
  check_problems_are_solved env heuristic_solved_evd;
  solve_unconstrained_impossible_cases env heuristic_solved_evd

let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics

(* Main entry points *)

exception UnableToUnify of evar_map * unification_error

let default_transparent_state env = full_transparent_state
(* Conv_oracle.get_transp_state (Environ.oracle env) *)

let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
  match evar_conv_x ts env evd CONV  t1 t2 with
  | Success evd' -> evd'
  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))

let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
  match evar_conv_x ts env evd CUMUL t1 t2 with
  | Success evd' -> evd'
  | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))

let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
  match evar_conv_x ts env !evdref CONV t1 t2 with
  | Success evd' -> evdref := evd'; true
  | _ -> false

let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 =
  match evar_conv_x ts env !evdref CUMUL t1 t2 with
  | Success evd' -> evdref := evd'; true
  | _ -> false