Can't display a number whose type is wrapped in a structure

Stream: new members

[Mike Shulman]

Eric Wieser said:

This feels like an #xy problem

What do you think my X is?

[Mike Shulman]

Or maybe I should say, what makes you think what I'm asking about isn't my X? Isn't it reasonable to want to display things?

[Mike Shulman]

Alex J. Best said:

What do you mean by instance of wrap (instance is a keyword) are you varying wrapN or the class?

I mean different elements of wrap in which t is different.

[Eric Wieser]

I have no idea what your X is, but I'm very skeptical that structure wrap := (t : Type) is something you want to go anywhere near

[Johan Commelin]

Well, we have newtypes like that in mathlib in several places.

[Eric Wieser]

Do we? Can you give an example?

[Eric Wieser]

Category theory is maybe the only place I can think of

[Johan Commelin]

But usually they are very much on a one-off basis, and so reimplementing a couple of typeclasses is not a problem.

[Johan Commelin]

For example, we have something like

structure real :=
(cauchy : @cau_seq.completion.Cauchy ℚ _ _ _ abs _)

[Johan Commelin]

Which is a similar pattern.

[Eric Wieser]

Johan, I think you're misreading structure wrap := (t : Type) for structure wrap := (val : some_type) where some_type : Type

[Johan Commelin]

Fair enough.

[Mike Shulman]

Well, the actual example has more fields of course:

structure group :=
  (t : Type)
  (op : t → t → t)
  -- etc.

[Adam Topaz]

You could probably @[derive has_repr] and save a few characters

[Adam Topaz]

(In the Nat case, that is)

[Adam Topaz]

What behaviour do you expect from eval in the group case?

[Mike Shulman]

group is the analogue of the general wrap. I would only want to display elements of particular groups, like a groupN.

[Mike Shulman]

Where do I put @[derive has_repr]?

[Adam Topaz]

hmmm derive doesn't quite work. sorry!

[Mario Carneiro]

wasn't the solution already shown?

instance : has_repr wrapN.t := nat.has_repr

[Adam Topaz]

yeah that works

[Mario Carneiro]

you can also do

instance : has_repr wrapN.t := by dunfold wrapN; apply_instance

if you don't know the instance name

[Mike Shulman]

Okay, this works for ℕ, but not for ℝ. When I try it with ℝ I get

kernel failed to type check declaration 't.has_repr' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  has_repr Rvsp.t
elaborated value:
  id real.has_repr
nested exception message:
invalid definition, it uses untrusted declaration 'real.has_repr'

[Eric Wieser]

You need the word meta for real

[Eric Wieser]

Note that if you use my @[reducible] suggestion I made in the third post you don't have to deal with any of this

[Mike Shulman]

Where does the word meta go?

[Adam Topaz]

In the form meta instance ... should work

[Mike Shulman]

Thanks. What does meta mean?

[Adam Topaz]

It's a tag that's used for defs at the metaprogramming level

[Adam Topaz]

(In Lean3. Lean4 doesn't have meta.)

[Mike Shulman]

And why does the instance for real need to be at the metaprogramming level, but not the one for nat?

[Adam Topaz]

src#real.has_repr (just so I can take a look ;))

[Mario Carneiro]

I was wondering if you were going to ask that... :) It's the same issue I highlighted before: the implementation has to cheat using unsafe code to get at the representation behind the quotient

[Mario Carneiro]

The ultimate source of this unsafe hackery is src#quot.unquot

[Mario Carneiro]

As you yourself said @Mike Shulman there are no computable functions definable in the logic which can distinguish real numbers by a continuity argument, but clearly a function that turns a real into a string would have to do just that

[Mario Carneiro]

meta means "I don't care if this introduces type unsafety or unsoundness" and enables access to stuff like unchecked type casting, unguarded recursion and C++ FFI. The lean 4 equivalent is unsafe and luckily it is much less necessary than it was in lean 3. meta declarations don't exist as far as the kernel is concerned, they are only for the VM/compiler.

[Mike Shulman]

Thanks. I think the error message could have been more helpful in indicating that this was the problem...

[Mario Carneiro]

do you have a mwe?

[Mario Carneiro]

it is true that the error message is pretty bad, it looks like something made it past the first line of defense and you are getting the backup error message

[Mike Shulman]

import data.real.basic
structure wrap := (t : Type)
def wrapR : wrap := {t := ℝ}
instance : has_repr wrapR.t := by dunfold wrapR; apply_instance

[Mario Carneiro]

Huh, I guess that's always what you get when you use a meta declaration in a non-meta one.

meta def bar : ℕ := 0
def foo : ℕ := bar
-- kernel failed to type check declaration 'foo' this is usually due to a buggy tactic or a bug in the builtin elaborator
-- elaborated type:
--   ℕ
-- elaborated value:
--   bar
-- nested exception message:
-- invalid definition, it uses untrusted declaration 'bar'

The error for missing noncomputable is much better:

noncomputable! def bar : ℕ := 0
def foo : ℕ := bar
-- missing 'noncomputable' modifier, definition 'foo' depends on 'bar'

[Mike Shulman]

The last line "invalid definition, it uses untrusted declaration 'bar'" would be fairly informative if it were on its own.

[Johan Commelin]

Is this related to bundled?