aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/circular_subtyping2.v
blob: 75b27bce9751a8f6434223ddf7b667c01894d8d6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(* Circular substitution check at functor application *)
Module Type S. End S.
Module Type T. Declare Module M:S. End T.
Module N:S. End N.

Module F (X:S) (Y:T with Module M:=X). End F.
Module A := F N N.

(* Circular substitution check at with definition *)
(* Should it be implemented?? *)
(*

Module NN:T. Module M:=N. End NN.
Module Type U := T with Module M:=NN.
(*
User error: The construction "with Module M:=..." is about to create
a circular module type. Their resolution is not implemented yet.
If you really need that feature, please report.
*)
*)