Jesper Cockx

@nad is this finished? I am assuming it is, if not please reopen.

See also the discussion on #4908: we should split up `--safe` into a set of flags that can be enabled/disabled individually (and make `--safe` an alias for this set).

I do not think the issue tracker is the best place to discuss novel research ideas. If you have a concrete proposal of what should be implemented, feel free to...

I applaud the initiative to make Cubical Agda more user-friendly, and the proposal makes sense to me from the implementation perspective. However, I am not an expert on the implementation...

A more lightweight alternative might be to use difference lists? (e.g. https://hackage.haskell.org/package/dlist-1.0/docs/Data-DList.html)

I am very much in favour of this proposal! I'm already looking forward to the last day I have to type out `Relation.Binary.PropositionalEquality` in full :)

Does anyone know why the Travis build is timing out on GHC 8.0 (and only 8.0)?

When I run it on my own PC (using GHC 8.0.2), agda runs out of heap: ``` Checking Data.Vec.Relation.Unary.Any.Properties (/home/jesper/agda/std-lib/src/Data/Vec/Relation/Unary/Any/Properties.agda). agda: Heap exhausted; agda: Current maximum heap size is 1610612736...

I'm trying again to run on Travis with 2GB heap for the standard library (instead of 1.5GB), just to see if it makes a difference.

It fixes the problem on my own PC but not on Travis: the build simply times out on ``` with-stdlib AllStdLib: ```