Running `evalConst` in `Type 1`

Stream: lean4

[Anand Rao Tadipatri]

I have a definition that lives in Type 1

import Lean

open Lean Elab Meta Command

structure Test where
  map : Type → Type

#check Test -- Type 1

def instTestList : Test where
  map := List


#check show MetaM _ from do
  evalConst Test ``instTestList
/- ERROR
application type mismatch
  evalConst Test
argument
  Test
has type
  Type 1 : Type 2
but is expected to have type
  Type : Type 1
-/

This makes it difficult to use it in conjunction with evalConst and MetaM, which expect a term of type Type. Is there a way around this?

[Eric Wieser]

Can you give a more complex example? There's nothing to evaluate in this one

[Kyle Miller]

evalConst would only work with computationally relevant values. Type has no runtime representation.

[Anand Rao Tadipatri]

Apologies for the delay, I've updated my example.

[Kyle Miller]

If you wanting to evaluate Test at runtime, this has problems because Type -> Type has no runtime representation.

Is this a toy example for what you actually want to do?

[Anand Rao Tadipatri]

Thanks. Yes, it's a toy example for the actual situation I would like to use it in.

[Kyle Miller]

Ok, I see. Unfortunately Lean.evalConst has that universe constraint, but if you use docs#Lean.Environment.evalConst directly you can evaluate it.

[Eric Wieser]

What's the Intended difference between that and docs#Lean.evalConst ?

[Eric Wieser]

Oh, I guess the latter uses the monad stack for convenience, but is stuck in Type as a result