Checking `isType` with max in level parameters

Stream: lean4

[Adam Topaz]

Consider the following example:

import Lean

open Lean

elab "foo%" t:term : term => do
  let t ← Elab.Term.elabTerm t none
  let tp ← Meta.inferType t
  unless tp.isType do throwError "ERROR"
  return t

#check foo% (Nat × Nat)

This results in ERROR, I think because the match in isType asks for .sort (.succ _), but in this case it has the form .sort (.max (.succ _) (.succ _)). Is there a more robust way to check whether something is a type that allows for max in the level parameters?

[Alex J. Best]

I'm sure I've had to deal with this somewhere I just can't remember the short solution.
You can use docs#Lean.Level.isNeverZero I think, but maybe there is a function somewhere doing exactly what you want.

[Marcus Rossel]

import Lean
open Lean

elab "foo%" t:term : term => do
  let t ← Elab.Term.elabTerm t none
  let tp ← Meta.inferType t
  let tp' ← instantiateMVars tp
  unless tp'.isType do throwError "ERROR"
  return t

#check foo% (Nat × Nat)

[Adam Topaz]

Aha, great, yeah I thought it may have something to do with the level mvars. Thanks!

[Alex J. Best]

#3682 is what I was remembering

[Adam Topaz]

@Marcus Rossel that works for Nat, but I think what Alex points out is still an issue:

import Lean

open Lean

elab "foo%" t:term : term => do
  let t ← Elab.Term.elabTerm t none
  let tp ← Meta.inferType t
  let tp ← instantiateMVars tp
  unless tp.isType do throwError "ERROR"
  return t

universe u v

#check foo% (ULift.{u} Nat × ULift.{v} Nat) -- ERROR

[Adam Topaz]

I think I'll introduce

/-- If an `Expr` has the form `Type u`, then return `some u`, otherwise `none`. -/
def type? : Expr → Option Level
  | .sort u => u.dec
  | _ => none

thoughts?

[Alex J. Best]

LGTM yes