diff options
Diffstat (limited to 'test-suite/failure')
-rw-r--r-- | test-suite/failure/circular_subtyping1.v | 7 | ||||
-rw-r--r-- | test-suite/failure/circular_subtyping2.v | 20 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/failure/circular_subtyping1.v b/test-suite/failure/circular_subtyping1.v new file mode 100644 index 000000000..cfd91a2eb --- /dev/null +++ b/test-suite/failure/circular_subtyping1.v @@ -0,0 +1,7 @@ +(* Circular substitution check in subtyping verification *) +Module Type S. End S. +Module Type T. Declare Module M:S. End T. + +Module N:S. End N. +Module NN <: T. Module M:=N. End NN. +Module P <: T with Module M:=NN := NN. diff --git a/test-suite/failure/circular_subtyping2.v b/test-suite/failure/circular_subtyping2.v new file mode 100644 index 000000000..75b27bce9 --- /dev/null +++ b/test-suite/failure/circular_subtyping2.v @@ -0,0 +1,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. +*) +*) |