Disable Universe Check

Stream: general

[finegeometer]

Hi,

How do I disable Lean's universe check, analogous to Agda's {-# OPTIONS --type-in-type #-}? I'm happy to label everything unsafe.

I tried simply using unsafe structure for the relevant definition, but the universe error persisted.

Thanks!

[Aaron Liu]

what structure are you trying to make?

[Aaron Liu]

can you give the example

[finegeometer]

Generally, I want to be able to write something of the following form.

unsafe structure Foo : Type where
    X : Type
    -- ... lots of fields that refer to X

If the solution is a sufficiently intensive restructuring that more information is needed, it's probably easier for me to simply switch to Agda.

[finegeometer]

In more detail:

Several times, I've tried to use Lean as a programming language, rather than a proof assistant. When I do so, it's because I'm doing something I don't quite understand, so I want the safety of dependent types to check my work. But this tends to mean I'm working on something that causes a lot of cognitive load, so "nitpicky" issues like the universe check serve only to prevent me from doing anything at all. In this situation, I can't afford complicated, problem-specific solutions; it's either disable the check or discontinue the project. And I can't find a way to disable the check.

[finegeometer]

What I'd really like is a way to disable the universe check, and maybe other similar checks, throughout an entire file, or an entire project. Just like Agda's {-# OPTIONS --type-in-type #-}.

[Henrik Böving]

The easiest solution would just be to leave : Type out of your structure declaration because lean is perfectly capable of inferring universes in most situations.

But no you can not just generally disable it

[finegeometer]

Good to know. I will use Agda then.

[Aaron Liu]

finegeometer said:

Generally, I want to be able to write something of the following form.

unsafe structure Foo : Type where
    X : Type
    -- ... lots of fields that refer to X

If the solution is a sufficiently intensive restructuring that more information is needed, it's probably easier for me to simply switch to Agda.

this is really troubling me because I totally thought this would be possible

[Aaron Liu]

with unsafe

[Eric Wieser]

Isn't there some unsafe inverse to ULift that pulls something down to a different universe?

[Eric Wieser]

Certainly you can implement one with unsafeCast

[Aaron Liu]

Eric Wieser said:

Isn't there some unsafe inverse to ULift that pulls something down to a different universe?

But why would that exist

[Aaron Liu]

I can't think of any use cases

[Eric Wieser]

Working with big types in IO where the monad only allows Type 0

[Aaron Liu]

sure but then the question is why do you have big types

[Eric Wieser]

Polymorphism with vtables a la C++ gives you such types

[Eric Wieser]

Indeed, that thread also prototypes the usquashI'm thinking of

[François G. Dorais]

finegeometer said:

Good to know. I will use Agda then.

Probably too late to correct the misunderstanding but better late than never...

Henrik was not suggesting that you should leave. Instead, he was suggesting to leave out : Type from your structure declarations.

[François G. Dorais]

In other words, you should not worry about universe levels and just use Type _ everywhere rather than Type. If you run into issues where Lean can't figure out a solution to the universe unification problem on its own, discussing the specific issue here is probably the right way to solve the problem.

However, as Henrik pointed out, Lean does not provide a blanket solution to ignore these issues. After all, Type : Type is well-known to be inconsistent. By design, Lean doesn't try to make it easy to get into an inconsistent situation.

[Weiyi Wang]

Probably too late to correct the misunderstanding but better late than never...

Henrik was not suggesting that you should leave. Instead, he was suggesting to leave out : Type from your structure declarations.

My phone inserted a line break between : and Type and that message read so wrong until you pointed out...