Simplify types in lean

Stream: general

[Konstantin Weitz]

I often have complex looking types that are actually really easy if you evaluate them. Is there a way for Lean to simplify types before printing them.

A simple example:

def x : Fin (4 + 2) := Fin.mk 5 sorry

#check x

I'd like the type of x to be shown as Fin 6, but it shows as Fin (4 + 2) instead. How can this be done? I tried set_option pp.beta true, but it doesn't work.

(I previously asked this on stackoverflow but felt like I didn't get a good answer: https://stackoverflow.com/questions/79279223/simplify-types-in-lean)

[Aaron Liu]

why do you want this?

[Aaron Liu]

Can you give an example of some of the complex types you have and why you want to simplify them?

[Eric Wieser]

#check cast (by conv => norm_num) x is one option here

[Konstantin Weitz]

I have a library like this:

def ExecutionType (recipe:Recipe) : Type :=
  match recipe with
  | .concat => String -> String -> String
  -- ...

def execute (recipe:Recipe) : ExecutionType recipe :=
  -- ...

execute Recipe.concat "hello" 5

Right now, users of my library get an error like:

execute is passed String and Nat but is expected ExecutionType Recipe.concat. This is really hard to understand what's going on. It would be much nicer if it said: execute has type String -> String -> String but you passed String -> Nat -> X or something like that.

[Aaron Liu]

oh this is tricky

[Aaron Liu]

I'm aware of time formatting in Std which has something like this

[Aaron Liu]

I think in this case you should get a "type mismatch" error which tells you everything you need to know

[Aaron Liu]

or a "cannot synthesize OfNat String 5" maybe

[Eric Wieser]

Here I think you should just make ExecutionType an abbrev

[Konstantin Weitz]

@Eric Wieser I just tried, but it doesn't seem to do anything. At least If you pass the wrong arguments, you still get a very hard to understand type error message. That said, my actual definition of ExecutionType is also recursive, so maybe that's why it doesn't work.

[Eric Wieser]

Can you share the actual definition?