jon.recoil.org

Source file mtype.ml

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
(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*             Xavier Leroy, projet Cristal, INRIA Rocquencourt           *)
(*                                                                        *)
(*   Copyright 1996 Institut National de Recherche en Informatique et     *)
(*     en Automatique.                                                    *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU Lesser General Public License version 2.1, with the          *)
(*   special exception on linking described in the file LICENSE.          *)
(*                                                                        *)
(**************************************************************************)

(* Operations on module types *)

open Asttypes
open Path
open Types

let freshen ~scope mty =
  Subst.modtype (Rescope scope) Subst.identity mty

(* Strengthen a type as far as possible without unfolding abbreviations,
  pushing strengthening into signatures and functors. Return None if we
  couldn't push it inwards (or eliminate it) and an Mty_strengthen node
  needs to be constructed instead.

  Generally, strengthening with a module M is *aliasable* M is guaranteed
  to be a "real" module (and thus can appear in Mty_alias) and is not
  aliasable if M can be a functor argument. Aliasable strengthening is
  shallow in the sense that we simply replace the types of any submodule
  N by `Mty_alias M.N`. Non-aliasable strengthening is deep since we can't
  form aliases to M or its submodules. Instead, we have to unfold the entire
  module type and strengthen all type definition which is expensive.

  The decision whether a particular strengthening operation is aliasable is
  made when we first introduce it (in Typemod). Strengthening with a functor
  argument remains non-aliasable even if we later substitute a "real" module
  for it. This ensures that strengthening commutes with substitution and
  that it is irrelevant when exactly a strengthening node is expanded.  *)
let rec reduce_strengthen_lazy ~aliasable mty p =
  let open Subst.Lazy in
  match mty with
    Mty_signature sg ->
      Some (Mty_signature(strengthen_lazy_sig ~aliasable sg p))

  | Mty_functor(Named (Some param, arg, marg), res, mres)
    when !Clflags.applicative_functors ->
      Some (Mty_functor(Named (Some param, arg, marg),
        strengthen_lazy ~aliasable:false res (Papply(p, Pident param)), mres))
  | Mty_functor(Named (None, arg, marg), res, mres)
    when !Clflags.applicative_functors ->
      let param = Ident.create_scoped ~scope:(Path.scope p) "Arg" in
      Some (Mty_functor(Named (Some param, arg, marg),
        strengthen_lazy ~aliasable:false res (Papply(p, Pident param)), mres))

  | Mty_strengthen (mty,q,Not_aliasable) when aliasable ->
      (* Normally, we have S/M/N = S/M. However, if the inner strengthening is
        not aliasable and the outer is, we have to strengthen types in S with M
        and modules with N as per the semantics of strengthening.  *)
      begin match reduce_strengthen_lazy ~aliasable:false mty q with
      | Some mty -> reduce_strengthen_lazy ~aliasable:true mty p
      | None -> None
      end
  | Mty_alias _ | Mty_functor _ | Mty_strengthen _ ->
      (* Strengthening aliases, generative functors and already strengthened
        types is a no-op. *)
      Some mty
  | Mty_ident _ | Mty_for_hole -> None

(* Strengthen a type by pushing strengthening inward and/or constructing
    appropriate Mty_strengthen nodes. *)
and strengthen_lazy ~aliasable mty p =
  match reduce_strengthen_lazy ~aliasable mty p with
  | Some mty -> mty
  | None ->
      Subst.Lazy.Mty_strengthen (mty, p, Aliasability.aliasable aliasable)

and strengthen_lazy_sig' ~aliasable sg p =
  let open Subst.Lazy in
  match sg with
    [] -> []
  | (Sig_value(_, _, _) as sigelt) :: rem ->
      sigelt :: strengthen_lazy_sig' ~aliasable rem p
  | Sig_type(id, {type_kind=Type_abstract _}, _, _) :: rem
    when Btype.is_row_name (Ident.name id) ->
      strengthen_lazy_sig' ~aliasable rem p
  | Sig_type(id, decl, rs, vis) :: rem ->
      let strengthen_decl path decl =
        match decl.type_manifest, decl.type_private, decl.type_kind with
          Some _, Public, _ -> decl
        | Some _, Private, (Type_record _ | Type_record_unboxed_product _
                            | Type_variant _) ->
          decl
        | _ ->
            let manif =
              Some(Btype.newgenty(Tconstr(path,
                                          decl.type_params, ref Mnil))) in
            if Btype.type_kind_is_abstract decl then begin
              { decl with
                type_private = Public;
                type_manifest = manif;
                type_ikind =
                  Types.ikinds_todo
                    (Format_doc.asprintf "strengthen abstract path=%a"
                       Path.print path)
              }
            end else begin
              { decl with
                type_manifest = manif;
                type_ikind =
                  Types.ikinds_todo
                    (Format_doc.asprintf "strengthen manifest path=%a"
                       Path.print path)
              }
            end
      in
      let path = Pdot(p, Ident.name id) in
      let new_unboxed_version =
        Option.map (strengthen_decl (Path.unboxed_version path))
          decl.type_unboxed_version
      in
      let newdecl =
        strengthen_decl path
          {decl with type_unboxed_version = new_unboxed_version}
      in
      Sig_type(id, newdecl, rs, vis) ::
        strengthen_lazy_sig' ~aliasable rem p
  | (Sig_typext _ as sigelt) :: rem ->
      sigelt :: strengthen_lazy_sig' ~aliasable rem p
  | Sig_module(id, pres, md, rs, vis) :: rem ->
      let str =
        strengthen_lazy_decl ~aliasable md (Pdot(p, Ident.name id))
      in
      Sig_module(id, pres, str, rs, vis)
      :: strengthen_lazy_sig' ~aliasable rem p
  | Sig_modtype(id, decl, vis) :: rem ->
      let newdecl =
        match decl.mtd_type with
        | Some _ when not aliasable ->
            (* [not alisable] condition needed because of recursive modules.
               See [Typemod.check_recmodule_inclusion]. *)
            decl
        | _ ->
            {decl with mtd_type = Some(Mty_ident(Pdot(p,Ident.name id)))}
      in
      Sig_modtype(id, newdecl, vis) ::
      strengthen_lazy_sig' ~aliasable rem p
  | (Sig_class _ as sigelt) :: rem ->
      sigelt :: strengthen_lazy_sig' ~aliasable rem p
  | (Sig_class_type _ as sigelt) :: rem ->
      sigelt :: strengthen_lazy_sig' ~aliasable rem p
  | Sig_jkind(id, decl, vis) as sigelt :: rem ->
      let sigelt =
        match decl.jkind_manifest with
        | Some _ -> sigelt
        | None ->
          let manif =
            Some (Jkind.Const.of_path (Pdot(p, Ident.name id)))
          in
          let newdecl = { decl with jkind_manifest = manif } in
          Sig_jkind (id, newdecl, vis)
      in
      sigelt :: strengthen_lazy_sig' ~aliasable rem p

and strengthen_lazy_sig ~aliasable sg p =
  let sg = Subst.Lazy.force_signature_once sg in
  let sg = strengthen_lazy_sig' ~aliasable sg p in
  Subst.Lazy.of_value sg

and strengthen_lazy_decl ~aliasable md p =
  let open Subst.Lazy in
  match md.md_type with
  | Mty_alias _ -> md
  | _ when aliasable -> {md with md_type = Mty_alias p}
  | mty -> {md with md_type = strengthen_lazy ~aliasable mty p}

let strengthen ~aliasable mty p =
  let mty = strengthen_lazy ~aliasable (Subst.Lazy.of_modtype mty) p in
  Subst.Lazy.force_modtype mty

let strengthen_decl ~aliasable md p =
  let md = strengthen_lazy_decl ~aliasable (Subst.Lazy.of_module_decl md) p in
  Subst.Lazy.force_module_decl md

(* Perform one reduction on a module type, returning None is it couldn't be
  reduced. Possible reductions are unfolding type abbreviations, pushing
  strengthening inwards and, if aliases is true, resolving module aliases. *)
let rec reduce_lazy ~aliases env mty =
  let open Subst.Lazy in
  match mty with
    Mty_ident p ->
      begin try
        Some (Env.find_modtype_expansion_lazy p env)
      with Not_found ->
        None
      end
  | Mty_alias path when aliases ->
        begin try
          let mty = (Env.find_module_lazy path env).md_type in
          let normal_path = Env.normalize_instance_names_in_module_path path in
          let mty = strengthen_lazy ~aliasable:true mty normal_path in
          Some mty
        with Not_found ->
          (*Location.prerr_warning Location.none
            (Warnings.No_cmi_file (Path.name path));*)
          None
        end
  | Mty_strengthen (mty,p,a) ->
      let aliasable = Aliasability.is_aliasable a in
      begin match reduce_strengthen_lazy ~aliasable mty p with
      | Some mty -> Some mty
      | None ->
        begin match reduce_lazy ~aliases env mty with
        | Some mty -> Some (strengthen_lazy ~aliasable mty p)
        | None -> None
        end
      end
  | Mty_signature _ | Mty_functor _ | Mty_alias _ | Mty_for_hole -> None

let rec scrape_lazy ~aliases env mty =
  match reduce_lazy ~aliases env mty with
  | Some mty -> scrape_lazy ~aliases env mty
  | None -> mty

let reduce_alias_lazy env mty = reduce_lazy ~aliases:true env mty

let reduce_lazy env mty = reduce_lazy ~aliases:false env mty

let reduce env mty =
  Subst.Lazy.of_modtype mty
  |> reduce_lazy env
  |> Option.map Subst.Lazy.force_modtype

(* Expand delayed strengthening *)

let rec expand_lazy env mty =
  let open Subst.Lazy in
  match mty with
  | Mty_strengthen _ ->
    begin match reduce_lazy env mty with
    | Some mty -> expand_lazy env mty
    | None -> mty
    end
  | _ -> mty

let expand env mty =
  Subst.Lazy.of_modtype mty
  |> expand_lazy env
  |> Subst.Lazy.force_modtype

(* Expand delayed strengthening up to the given paths. Note that if M.N is in
    paths then M must be in paths, too. This is guaranteed by expand_to below. *)

let rec expand_paths_lazy paths env =
  let open Subst.Lazy in
  function
    Mty_signature sg ->
      Mty_signature (expand_paths_lazy_sig paths env sg)
  | Mty_functor (param,res,mres) ->
      let param, env = match param with
        Unit -> Unit, env
      | Named (name,mty,mm) ->
          let mty = expand_paths_lazy paths env mty in
          let mode = Mode.(alloc_as_value mm |> Value.disallow_right) in
          let env = match name with
            | Some param when !Clflags.applicative_functors ->
                Env.add_module_lazy ~update_summary:false param Mp_present mty
                  ~mode env
            | Some _ | None -> env
          in
          Named (name, mty, mm), env
      in
      let res = expand_paths_lazy paths env res in
      Mty_functor (param,res,mres)
  | Mty_strengthen (_,p,_) as mty when Path.Set.mem p paths ->
      (* If the path we're strengthening with is in paths then we need to
          unfold the node. *)
      begin match reduce_lazy env mty with
      | Some mty -> expand_paths_lazy paths env mty
      | None -> assert false
          (* This shouldn't be able to happen because for
            `with module M.N := X`, `paths` will only contain M but not M.N
            and M's type can't be abstract. *)
      end
  | Mty_strengthen (mty,p,a) ->
      (* If the path we're strengthening with isn't in paths then we can
          can just unfold the strengthened type but keep the Mty_strengthen
          node. *)
      let mty = expand_paths_lazy paths env mty in
      Mty_strengthen (mty,p,a)
  | Mty_ident _ | Mty_alias _ | Mty_for_hole as mty ->
      mty

and expand_paths_lazy_sig paths env sg =
  let open Subst.Lazy in
  force_signature_once sg
  |> expand_paths_lazy_sig_items paths env
  |> of_value

and expand_paths_lazy_sig_items paths env sg =
  let open Subst.Lazy in
  let expand_item env = function
    | Sig_module (id,pres,md,rs,vis) ->
        let md = { md with md_type = expand_paths_lazy paths env md.md_type }
        in
        let env =
          Env.add_module_declaration_lazy ~update_summary:false id pres md env
        in
        env, Sig_module (id,pres,md,rs,vis)
      | Sig_modtype (id,mtd,vis) ->
          let mt = Option.map (expand_paths_lazy paths env) mtd.mtd_type in
          let mtd = { mtd with mtd_type = mt } in
          let env = Env.add_modtype_lazy ~update_summary:false id mtd env in
          env, Sig_modtype (id,mtd,vis)
      | Sig_value _ | Sig_type _ | Sig_typext _ | Sig_class _
      | Sig_class_type _ | Sig_jkind _ as item ->
          env, item
  in
  List.fold_left_map expand_item env sg |> snd

let expand_to env sg paths =
  let rec add_paths paths = function
    | Pdot (p,_) -> add_paths (Path.Set.add p paths) p
    | _ -> paths
  in
  let paths = List.fold_left add_paths Path.Set.empty paths in
  Subst.Lazy.of_signature sg
  |> expand_paths_lazy_sig paths env
  |> Subst.Lazy.force_signature

let rec sig_make_manifest sg =
  match sg with
    [] -> []
  | (Sig_value _ | Sig_class _ | Sig_class_type _) as t :: rem ->
    t :: sig_make_manifest rem
  | Sig_type (id,decl,rs,vis) :: rem ->
    let decl_make_manifest path decl =
      match decl.type_manifest, decl.type_private, decl.type_kind with
        Some _, Public, _ -> decl
      | Some _, Private,
        (Type_record _ | Type_record_unboxed_product _ | Type_variant _) -> decl
      | _ ->
        let manif =
          Some (Btype.newgenty(Tconstr(path, decl.type_params, ref Mnil)))
        in
        match decl.type_kind with
        | Type_abstract _ ->
          { decl with type_private = Public; type_manifest = manif }
        | (Type_record _ | Type_record_unboxed_product _ | Type_variant _
          | Type_open) ->
          { decl with type_manifest = manif }
    in
    let path = Pident id in
    let new_unboxed_version =
      Option.map (decl_make_manifest (Path.unboxed_version path))
        decl.type_unboxed_version
    in
    let newdecl =
      decl_make_manifest path
        {decl with type_unboxed_version = new_unboxed_version}
    in
    Sig_type(Ident.rename id, newdecl, rs, vis) :: sig_make_manifest rem
  | Sig_typext _ as sigelt :: rem ->
    sigelt :: sig_make_manifest rem
  | Sig_module(id, pres, md, rs, vis) :: rem ->
    let md =
      match md.md_type with
      | Mty_alias _ -> md
      | _ -> {md with md_type = Mty_alias (Pident id)}
    in
    Sig_module(Ident.rename id, pres, md, rs, vis) :: sig_make_manifest rem
  | Sig_modtype(id, decl, vis) :: rem ->
    let newdecl =
      {decl with mtd_type =
                   match decl.mtd_type with
                   | None -> Some (Mty_ident (Pident id))
                   | Some _ -> decl.mtd_type }
    in
    Sig_modtype(Ident.rename id, newdecl, vis) :: sig_make_manifest rem
  | Sig_jkind (id, decl, vis) as sigelt :: rem ->
    let sigelt =
      match decl.jkind_manifest with
      | Some _ -> sigelt
      | None ->
        let manifest = Jkind.Const.of_path (Pident id) in
        let newdecl = { decl with jkind_manifest = Some manifest } in
        Sig_jkind (Ident.rename id, newdecl, vis)
    in
    sigelt :: sig_make_manifest rem

let rec make_aliases_absent ~aliased pres mty =
  (* aliased=true means that mty is subject to aliasable strengthening
    and thus any module we encounter in it will be an alias (we don't need to
    know of what) and thus absent. This is purely an optimisation over
    expanding Mty_strengthen nodes. *)
  match mty with
  | Mty_alias _ -> Mp_absent, mty
  | Mty_signature sg ->
      let make_item = function
        | Sig_module(id, pres, md, rs, priv) ->
          let pres, md = if aliased
            then Mp_absent, md
            else
              let pres, md_type =
                make_aliases_absent ~aliased:false pres md.md_type
              in
              pres, { md with md_type }
          in
          Sig_module(id, pres, md, rs, priv)
        | Sig_value _ | Sig_type _ | Sig_typext _ | Sig_modtype _
        | Sig_class _ | Sig_class_type _ | Sig_jkind _ as item ->
          item
      in
      pres, Mty_signature(List.map make_item sg)
  | Mty_functor(arg, res, mres) ->
      let _, res = make_aliases_absent ~aliased:false Mp_present res in
      pres, Mty_functor(arg, res, mres)
  | Mty_ident _ | Mty_for_hole ->
      pres, mty
  | Mty_strengthen (mty,p,a) ->
      let aliased = aliased || Aliasability.is_aliasable a in
      let pres, res = make_aliases_absent ~aliased pres mty in
      pres, Mty_strengthen (res,p,a)

let scrape_for_type_of env pres mty =
  let rec loop env outer = function
    | Mty_alias path -> begin
        try
          let md = Env.find_module path env in
          let mty = strengthen ~aliasable:false md.md_type path in
          loop env mty mty
        with Not_found -> outer
      end
    | Mty_strengthen (inner,_,_) -> loop env outer inner
    | Mty_ident _ | Mty_signature _ | Mty_functor _ | Mty_for_hole -> outer
  in
  make_aliases_absent ~aliased:false pres (loop env mty mty)

(* Expand manifest module type names at the top of the given module type *)

let scrape_alias_lazy env mty = scrape_lazy ~aliases:true env mty

(* Non-lazy version of scrape_alias *)
let scrape_alias env mty =
  Subst.Lazy.of_modtype mty
  |> scrape_alias_lazy env
  |> Subst.Lazy.force_modtype

let scrape_lazy env mty = scrape_lazy ~aliases:false env mty

let scrape env mty =
  match mty with
    Mty_ident _ | Mty_strengthen _ ->
      Subst.Lazy.force_modtype (scrape_lazy env (Subst.Lazy.of_modtype mty))
  | _ -> mty

let () =
  Printtyp.expand_module_type := expand ;
  Env.scrape_alias := scrape_alias_lazy ;
  Env.scrape_lazy := scrape_lazy

let find_type_of_module ~strengthen ~aliasable env path =
  if strengthen then
    let md = Env.find_module_lazy path env in
    let mty = strengthen_lazy ~aliasable md.md_type path in
    Subst.Lazy.force_modtype mty
  else
    (Env.find_module path env).md_type

(* In nondep_supertype, env is only used for the type it assigns to id.
   Hence there is no need to keep env up-to-date by adding the bindings
   traversed. *)

type variance = Co | Contra | Strict

let rec nondep_mty_with_presence env va ids pres mty =
  match expand env mty with
    Mty_ident p ->
      begin match Path.find_free_opt ids p with
      | Some id ->
          let expansion =
            try Env.find_modtype_expansion p env
            with Not_found ->
              raise (Ctype.Nondep_cannot_erase id)
          in
          nondep_mty_with_presence env va ids pres expansion
      | None -> pres, mty
      end
  | Mty_alias p ->
      begin match Path.find_free_opt ids p with
      | Some id ->
          let expansion =
            try Env.find_module p env
            with Not_found ->
              raise (Ctype.Nondep_cannot_erase id)
          in
          nondep_mty_with_presence env va ids Mp_present expansion.md_type
      | None -> pres, mty
      end
  | Mty_signature sg ->
      let mty = Mty_signature(nondep_sig env va ids sg) in
      pres, mty
  | Mty_functor(Unit, res, mres) ->
      pres, Mty_functor(Unit, nondep_mty env va ids res, mres)
  | Mty_functor(Named (param, arg, marg), res, mres) ->
      let var_inv =
        match va with Co -> Contra | Contra -> Co | Strict -> Strict in
      let mode = Mode.(alloc_as_value marg |> Value.disallow_right) in
      let res_env =
        match param with
        | None -> env
        | Some param -> Env.add_module ~arg:true param Mp_present arg ~mode env
      in
      let mty =
        Mty_functor(Named (param, nondep_mty env var_inv ids arg, marg),
                    nondep_mty res_env va ids res, mres)
      in
      pres, mty
  | Mty_for_hole as mty_for_hole -> pres, mty_for_hole
  | Mty_strengthen (mty,p,a) ->
      (* If we end up strengthening an abstract type with a dependent module,
        just drop the strengthening. *)
      let pres,mty = nondep_mty_with_presence env va ids pres mty
      in
      let mty =
        if Path.exists_free ids p
          then mty
          else strengthen ~aliasable:(Aliasability.is_aliasable a) mty p
      in
      pres,mty

and nondep_mty env va ids mty =
  snd (nondep_mty_with_presence env va ids Mp_present mty)

and nondep_sig_item env va ids = function
  | Sig_value(id, d, vis) ->
      Sig_value(id,
                {d with val_type = Ctype.nondep_type env ids d.val_type},
                vis)
  | Sig_type(id, d, rs, vis) ->
      Sig_type(id, Ctype.nondep_type_decl env ids (va = Co) d, rs, vis)
  | Sig_typext(id, ext, es, vis) ->
      Sig_typext(id, Ctype.nondep_extension_constructor env ids ext, es, vis)
  | Sig_module(id, pres, md, rs, vis) ->
      let pres, mty = nondep_mty_with_presence env va ids pres md.md_type in
      Sig_module(id, pres, {md with md_type = mty}, rs, vis)
  | Sig_modtype(id, d, vis) ->
      begin try
        Sig_modtype(id, nondep_modtype_decl env ids d, vis)
      with Ctype.Nondep_cannot_erase _ as exn ->
        match va with
          Co -> Sig_modtype(id, {mtd_type=None; mtd_loc=Location.none;
                                 mtd_attributes=[]; mtd_uid = d.mtd_uid}, vis)
        | _  -> raise exn
      end
  | Sig_class(id, d, rs, vis) ->
      Sig_class(id, Ctype.nondep_class_declaration env ids d, rs, vis)
  | Sig_class_type(id, d, rs, vis) ->
      Sig_class_type(id, Ctype.nondep_cltype_declaration env ids d, rs, vis)
  | Sig_jkind (id, d, vis) ->
      Sig_jkind (id, Ctype.nondep_jkind_declaration env ids d, vis)

and nondep_sig env va ids sg =
  let scope = Ctype.create_scope () in
  let sg, env = Env.enter_signature ~scope sg env in
  List.map (nondep_sig_item env va ids) sg

and nondep_modtype_decl env ids mtd =
  {mtd with mtd_type = Option.map (nondep_mty env Strict ids) mtd.mtd_type}

let nondep_supertype env ids = nondep_mty env Co ids
let nondep_sig env ids = nondep_sig env Co ids
let nondep_sig_item env ids = nondep_sig_item env Co ids

let enrich_typedecl env p id decl =
  match decl.type_manifest with
    Some _ -> decl
  | None ->
    match Env.find_type p env with
    | exception Not_found -> decl
        (* Type which was not present in the signature, so we don't have
           anything to do. *)
    | orig_decl ->
        if decl.type_arity <> orig_decl.type_arity then
          decl
        else begin
          let orig_ty =
            Ctype.reify_univars env
              (Btype.newgenty(Tconstr(p, orig_decl.type_params, ref Mnil)))
          in
          let new_ty =
            Ctype.reify_univars env
              (Btype.newgenty(Tconstr(Pident id, decl.type_params, ref Mnil)))
          in
          let env = Env.add_type ~check:false id decl env in
          match Ctype.mcomp env orig_ty new_ty with
          | exception Ctype.Incompatible -> decl
              (* The current declaration is not compatible with the one we got
                 from the signature. We should just fail now, but then, we could
                 also have failed if the arities of the two decls were
                 different, which we didn't. *)
          | () ->
              let orig_ty =
                Btype.newgenty(Tconstr(p, decl.type_params, ref Mnil))
              in
              let type_unboxed_version =
                Option.map
                  (fun d ->
                    let orig_ty_unboxed =
                      Btype.newgenty
                        (Tconstr
                           (Path.unboxed_version p, decl.type_params, ref Mnil))
                    in
                    { d with
                      type_manifest = Some orig_ty_unboxed;
                      type_ikind =
                        Types.ikinds_todo
                          (Format_doc.asprintf "enrich unboxed path=%a"
                             Path.print (Path.unboxed_version p))
                    })
                  decl.type_unboxed_version
              in
              { decl with
                type_manifest = Some orig_ty;
                type_unboxed_version;
                type_ikind =
                  Types.ikinds_todo
                    (Format_doc.asprintf "enrich manifest path=%a" Path.print p)
              }
        end

let rec enrich_modtype env p mty =
  match expand env mty with
    Mty_signature sg ->
      Mty_signature(List.map (enrich_item env p) sg)
  | _ ->
      mty

and enrich_item env p = function
    Sig_type(id, decl, rs, priv) ->
      Sig_type(id,
                enrich_typedecl env (Pdot(p, Ident.name id)) id decl, rs, priv)
  | Sig_module(id, pres, md, rs, priv) ->
      Sig_module(id, pres,
                  {md with
                   md_type = enrich_modtype env
                       (Pdot(p, Ident.name id)) md.md_type},
                 rs,
                 priv)
  | item -> item

(* Merlin-only: The compiler uses a labeled tuple instead of this record type. Once Merlin
   is upgraded to 5.4, we should delete this and bring ourselves back in line with the
   compiler. *)
type type_and_jkind_paths =
  { types : Path.t list
  ; jkinds : Path.t list
  }

let rec type_and_jkind_paths env p mty =
  match scrape env mty with
  | Mty_ident _ | Mty_alias _ | Mty_functor _ | Mty_strengthen _ | Mty_for_hole ->
    { types = []; jkinds = [] }
  | Mty_signature sg -> type_and_jkind_paths_sig env p sg

and type_and_jkind_paths_sig env p sg =
  match sg with
  | [] -> { types = []; jkinds = [] }
  | Sig_type(id, _decl, _, _) :: rem ->
    let { types; jkinds } = type_and_jkind_paths_sig env p rem in
    { types = (Pdot(p, Ident.name id) :: types); jkinds }
  | Sig_jkind(id, _decl, _) :: rem ->
    let { types; jkinds } = type_and_jkind_paths_sig env p rem in
    { types; jkinds = (Pdot(p, Ident.name id) :: jkinds) }
  | Sig_module(id, pres, md, _, _) :: rem ->
    let { types = nested_types; jkinds = nested_jkinds } =
      type_and_jkind_paths env (Pdot(p, Ident.name id)) md.md_type
    in
    let env =
      Env.add_module_declaration ~check:false id pres md env
    in
    let { types = rem_types; jkinds = rem_jkinds } =
      type_and_jkind_paths_sig env p rem
    in
    { types = (nested_types @ rem_types); jkinds = (nested_jkinds @ rem_jkinds) }
  | Sig_modtype(id, decl, _) :: rem ->
    type_and_jkind_paths_sig (Env.add_modtype id decl env) p rem
  | (Sig_value _ | Sig_typext _ | Sig_class _ | Sig_class_type _) :: rem ->
    type_and_jkind_paths_sig env p rem

let rec no_code_needed_mod env pres mty =
  match pres with
  | Mp_absent -> true
  | Mp_present -> begin
      match scrape env mty with
        Mty_ident _ -> false
      | Mty_signature sg -> no_code_needed_sig env sg
      | Mty_functor _ -> false
      | Mty_alias _ -> false
      | Mty_for_hole -> true
      | Mty_strengthen _ -> false
    end

and no_code_needed_sig env sg =
  match sg with
    [] -> true
  | Sig_value(_id, decl, _) :: rem ->
      begin match decl.val_kind with
      | Val_prim _ -> no_code_needed_sig env rem
      | _ -> false
      end
  | Sig_module(id, pres, md, _, _) :: rem ->
      no_code_needed_mod env pres md.md_type &&
      no_code_needed_sig
        (Env.add_module_declaration ~check:false id pres md env) rem
  | (Sig_type _ | Sig_modtype _ | Sig_class_type _ | Sig_jkind _) :: rem ->
      no_code_needed_sig env rem
  | (Sig_typext _ | Sig_class _) :: _ ->
      false

let no_code_needed env mty = no_code_needed_mod env Mp_present mty

(* Check whether a module type may return types *)

module Contains_type_or_jkind = struct
  type t = Type | Jkind

  let to_string_plural = function
    | Type -> "types"
    | Jkind -> "kinds"

  exception Contains of t

  let rec contains_type_or_jkind env mty =
    match scrape env mty with
      Mty_ident _ -> raise (Contains Type) (* PR#6427 *)
    | Mty_signature sg ->
        contains_type_or_jkind_sig env sg
    | Mty_functor (_, body, _) ->
        contains_type_or_jkind env body
    | Mty_alias _
    | Mty_for_hole ->
        ()
    | Mty_strengthen _ -> raise (Contains Type)

  and contains_type_or_jkind_sig env =
    List.iter (contains_type_or_jkind_item env)

  and contains_type_or_jkind_item env = function
      Sig_type (_,({type_manifest = None} |
                   {type_kind = Type_abstract _; type_private = Private}),_, _)
    | Sig_modtype _
    | Sig_typext (_, {ext_args = Cstr_record _}, _, _) ->
        (* We consider that extension constructors with an inlined
           record create a type (the inlined record), even though
           it would be technically safe to ignore that considering
           the current constraints which guarantee that this type
           is kept local to expressions.  *)
        raise (Contains Type)
    | Sig_jkind (_, {jkind_manifest = None; _}, _) ->
        raise (Contains Jkind)
    | Sig_module (_, _, {md_type = mty}, _, _) ->
        contains_type_or_jkind env mty
    | Sig_value _
    | Sig_type _
    | Sig_typext _
    | Sig_class _
    | Sig_class_type _
    | Sig_jkind _ ->
        ()

  let check env mty =
    try contains_type_or_jkind env mty; None with Contains tj -> Some tj
end


(* Remove module aliases from a signature *)

let rec get_prefixes = function
  | Pident _ -> Path.Set.empty
  | Pdot (p, _) | Papply (p, _) | Pextra_ty (p, _)
    -> Path.Set.add p (get_prefixes p)

let rec get_arg_paths = function
  | Pident _ -> Path.Set.empty
  | Pdot (p, _) | Pextra_ty (p, _) -> get_arg_paths p
  | Papply (p1, p2) ->
      Path.Set.add p2
        (Path.Set.union (get_prefixes p2)
           (Path.Set.union (get_arg_paths p1) (get_arg_paths p2)))

let rec rollback_path subst p =
  try Pident (Path.Map.find p subst)
  with Not_found ->
    match p with
      Pident _ | Papply _ -> p
    | Pdot (p1, s) ->
        let p1' = rollback_path subst p1 in
        if Path.same p1 p1' then p else rollback_path subst (Pdot (p1', s))
    | Pextra_ty (p1, extra) ->
        let p1' = rollback_path subst p1 in
        if Path.same p1 p1' then p
        else rollback_path subst (Pextra_ty (p1', extra))

let rec collect_ids subst bindings p =
    begin match rollback_path subst p with
      Pident id ->
        let ids =
          try collect_ids subst bindings (Ident.find_same id bindings)
          with Not_found -> Ident.Set.empty
        in
        Ident.Set.add id ids
    | _ -> Ident.Set.empty
    end

let collect_arg_paths mty =
  let open Btype in
  let paths = ref Path.Set.empty
  and subst = ref Path.Map.empty
  and bindings = ref Ident.empty in
  (* let rt = Ident.create "Root" in
     and prefix = ref (Path.Pident rt) in *)
  with_type_mark begin fun mark ->
    let super = type_iterators mark in
    let it_path p = paths := Path.Set.union (get_arg_paths p) !paths
    and it_signature_item it si =
      super.it_signature_item it si;
      match si with
      | Sig_module (id, _, {md_type=Mty_alias p}, _, _) ->
          bindings := Ident.add id p !bindings
      | Sig_module (id, _, {md_type=Mty_signature sg}, _, _) ->
          List.iter
            (function Sig_module (id', _, _, _, _) ->
                subst :=
                  Path.Map.add (Pdot (Pident id, Ident.name id')) id' !subst
              | _ -> ())
            sg
      | _ -> ()
    in
    let it = {super with it_path; it_signature_item} in
    it.it_module_type it mty;
    Path.Set.fold (fun p -> Ident.Set.union (collect_ids !subst !bindings p))
      !paths Ident.Set.empty
  end

type remove_alias_from =
  | Alias of Ident.t
  | Strengthening
type remove_alias_args =
    { mutable modified: bool;
      exclude: remove_alias_from -> Path.t -> bool;
      scrape: Env.t -> module_type -> module_type }

let rec remove_aliases_mty env args pres mty =
  let args' = {args with modified = false} in
  let res =
    match args.scrape env mty with
      Mty_signature sg ->
        Mp_present, Mty_signature (remove_aliases_sig env args' sg)
    | Mty_alias _ ->
        let mty' = scrape_alias env mty in
        if mty' = mty then begin
          pres, mty
        end else begin
          args'.modified <- true;
          remove_aliases_mty env args' Mp_present mty'
        end
    | Mty_strengthen (mty,p,Aliasable) when not (args.exclude Strengthening p) ->
        let mty = strengthen ~aliasable:false mty p in
        args'.modified <- true;
        Mp_present, mty
    | mty ->
        Mp_present, mty
  in
  if args'.modified then begin
    args.modified <- true;
    res
  end else begin
    pres, mty
  end

and remove_aliases_sig env args sg =
  match sg with
    [] -> []
  | Sig_module(id, pres, md, rs, priv) :: rem  ->
      let pres, mty =
        match md.md_type with
          Mty_alias p when args.exclude (Alias id) p ->
            pres, md.md_type
        | mty ->
            remove_aliases_mty env args pres mty
      in
      Sig_module(id, pres, {md with md_type = mty} , rs, priv) ::
      remove_aliases_sig (Env.add_module id pres mty env) args rem
  | Sig_modtype(id, mtd, priv) :: rem ->
      Sig_modtype(id, mtd, priv) ::
      remove_aliases_sig (Env.add_modtype id mtd env) args rem
  | it :: rem ->
      it :: remove_aliases_sig env args rem

let scrape_for_functor_arg env mty =
  let exclude _id p =
    try ignore (Env.find_module p env); true with Not_found -> false
  in
  let _, mty =
    remove_aliases_mty env {modified=false; exclude; scrape} Mp_present mty
  in
  mty

let scrape_for_type_of ~remove_aliases env mty =
  if remove_aliases then begin
    let excl = collect_arg_paths mty in
    let exclude id _p = match id with
      | Alias id -> Ident.Set.mem id excl
      | Strengthening -> false
    in
    let scrape _ mty = mty in
    let _, mty =
      remove_aliases_mty env {modified=false; exclude; scrape} Mp_present mty
    in
    mty
  end else begin
    let _, mty = scrape_for_type_of env Mp_present mty in
    mty
  end

(* Lower non-generalizable type variables *)

let lower_nongen nglev mty =
  let open Btype in
  with_type_mark begin fun mark ->
    let super = type_iterators mark in
    let it_do_type_expr it ty =
      match get_desc ty with
        Tvar _ ->
          let level = get_level ty in
          if level < generic_level && level > nglev then set_level ty nglev
      | _ ->
          super.it_do_type_expr it ty
    in
    let it = {super with it_do_type_expr} in
    it.it_module_type it mty
  end