Janno (Nov 30 2020 at 12:48): Janno (Nov 30 2020 at 12:48):How can I test that a certain universe relation is valid without adding it to the global graph? I want to assert "a < b could be a valid constraint". I tried modules, functors, monomorphic sections in modules/functors, module types,.. All of these add the constraint to the global graph even before the module/functor is imported or even instantiated.
Janno (Nov 30 2020 at 12:51):I suppose I have to move the test into its own file, don't I?
Gaëtan Gilbert (Nov 30 2020 at 12:51):Section Tmp. Polymorphic Constraint a < b. End Tmp.
Janno (Nov 30 2020 at 12:52):Oh, I see.. I am not even sure now why I wanted a module around it. Thanks!
Gaëtan Gilbert (Nov 30 2020 at 12:52):something with Fail Constraint may also be possible, I haven't fully thought it through
Janno (Nov 30 2020 at 12:52):Fail Constraint will not be equivalent if the universes are currently unrelated, I think.
Gaëtan Gilbert (Nov 30 2020 at 12:53):you could also Fail Fail Constraint
Janno (Nov 30 2020 at 12:53):Ah, good old double negation! I'll try that :)
Gaëtan Gilbert (Nov 30 2020 at 12:54):I think Polymorphic Constraint has better errors (Fail Fail will say "command has not failed" or some such thing)
Janno (Nov 30 2020 at 12:56):Indeed. I just tried it and that error message is all I get. Polymorphic Constraint it is, then. Thanks again!
Last updated: Oct 05 2023 at 02:01 UTC