Replace -type-in-type with Export Unset Universe Checking in UniMath.Foundations.Init

[peterlefanulumsdaine]

This addresses #1696 : it replaces the use of the -type-in-type flag (in the Makefile, emacs local variables file, etc) with the command Export Unset Universe Checking in UniMath.Foundations.Init.

As discussed in detail in #1696 , these should be entirely equivalent in their current effect within UniMath; the two effective differences are:

• The new setting will be more “infectious” downstream — projects importing UniMath will get universe checking unset, unless they specifically re-enable it with Set Universe Checking after importing UniMath.
• This makes it easier in future to reduce our reliance on type-in-type, by setting/unsetting universe checking on a file-by-file basis.

Compared to f917518 in #1671 , I’ve used Export rather than Global — according to the guidance in the Coq Reference Manual here and here, that seems to me like the correct one.

[benediktahrens]

@peterlefanulumsdaine thanks a lot for preparing this. There is a warning about deprecated "Export Set" - should we address this before merging?

[m-lindgren]

I think we should be very careful about merging this. This will effectively enable -type-in-type in every project that use UniMath, without them knowing it. It is my opinion that it's not very good practice for a library to export a setting that collapses the entire universe hierarchy for the user, even if UniMath internally relies on it.

In particular since we have no way of informing projects that rely on UniMath that we are making this change in their projects. We do not know every user of UniMath, and any problems related to this will only cause headaches for them, not us unfortunately. (Imagine spending hours trying to figure out why your project suddenly has a flat universe hierarchy, despite you being sure that you don't have -type-in-type in your Makefile. Recloning/cleaning the project, reinstalling/upgrading/downgrading Coq, clearing caches, reading Coq documentation, filing Coq issues ...)

I like the idea of taking steps towards removing type-in-type but this looks to me like a step in the opposite direction since it makes more code overall compile with universe checking disabled, not less, and the effort saved seems to amount only to the effort required to add Export Unset Universe Checking to one file, so I don't really see how this helps.

[JasonGross]

@peterlefanulumsdaine thanks a lot for preparing this. There is a warning about deprecated "Export Set" - should we address this before merging?

This warming is easy to address, btw, just use #[export] Set instead of Export Set

[JasonGross]

Why not add #[local] Unset Universe Checking just to the minimal set of files that need it? (Just run make and add the setting to whatever files fail, and do this in a loop)

[peterlefanulumsdaine]

@m-lindgren I feel fairly mixed about this. I agree with your reservations to some extent, but two counter-points:

• (pragmatic) If a downstream importer notices their universe hierarchy has collapsed, I see how the trouble-shooting would take long: stepping through their files and seeing where it first collapses would immediately show that it’s coming from importing UniMath; then googling why UniMath does that should quickly bring up these discussions.

• (principled) I think it’s probably (if anything) slightly better that type-in-type is propagated downstream by default, since (as I mentioned in Should we replace -type-in-type with Unset Universe Checking in some way? #1696 ) working with universe checking but importing un-checked objects seems theoretically pretty unclear. In particular, it certainly doesn’t re-gain consistency — the main thing people might hope it does — so I think it gives a false sense of security, unless a development is very conscious and careful about restricting which objects it imports from us.

These are why in the long-term, I don’t think the change is negative. In the short-term I fully agree it’s not great to affect downstream users without notification — but I’m not sure how we can notify them, other than trying this out.

So I’d lean to merging this (if others agree) but thinking of it as provisional for a while (at least a month, say), and being willing to roll it back if downstream users report any problems. As long as we don’t merge #1671 (which is blocked anyway if we don’t merge this), I don’t think anything else is likely to interact with this and make it difficult to roll back.

[nmvdw]

Why not add #[local] Unset Universe Checking just to the minimal set of files that need it? (Just run make and add the setting to whatever files fail, and do this in a loop)

I really like this solution. I think it addresses Michael’s comments and it properly indicates where type-in-type is used, which is useful for removing the dependency on type-in-type.

[peterlefanulumsdaine]

Why not add #[local] Unset Universe Checking just to the minimal set of files that need it? (Just run make and add the setting to whatever files fail, and do this in a loop)

I didn’t have time to carry this through (I tried something similar just far enough yesterday to see it would definitely take more time than I had), but I agree this would be ideal, as long as the number of files that need it isn’t too large.

[JasonGross]

What about something like (assuming no spaces in names):

debug=1 # change to debug="" to disable waiting on user input
while ! make -k >log 2>&1; do
  files="$(grep -B1 "^Error" log | grep -o '^File "[^"]*' | sed 's/^File "//g')"
  echo "Errors in $files"
  if [ ! -z "$debug" ]; then echo "Press enter to continue, ctrl+c to break..."; read dummyvar; fi
  for f in $files; do
    echo "editing $f"
    if grep -q '#.local. Unset Universe Checking' "$f"; then
      echo "File $f requires manual intervention"
      exit 1
    fi
    cp -f "$f" "$f.tmp"
    { echo "#[local] Unset Universe Checking."; cat "$f.tmp"; } > "$f"
  done
done

or as a one-liner:

debug=1; while ! make -k >log 2>&1; do files="$(grep -B1 "^Error" log | grep -o '^File "[^"]*' | sed 's/^File "//g')"; echo "Errors in $files"; if [ ! -z "$debug" ]; then echo "Press enter to continue, ctrl+c to break..."; read dummyvar; fi; for f in $files; do echo "editing $f"; if grep -q '#.local. Unset Universe Checking' "$f"; then; echo "File $f requires manual intervention"; exit 1; fi; cp -f "$f" "$f.tmp"; ( ( echo "#[local] Unset Universe Checking."; cat "$f.tmp") > "$f"); done; done

Once you set debug="", then you should be able to just let this run in the background while you do other tasks
(Note: I wrote this on my phone and haven't tested manually, so there might be some syntax errors or other minor issues, let me know if it fails in some way)

[peterlefanulumsdaine]

@JasonGross Thanks very much for the script — it came through just as I was starting to scratch my head over putting together such a script myself. Works like a charm, no syntax errors.

I’m trying it out in a branch localise-type-in-type-per-file. Under this naïve approach, it’s needed in a lot of files.