## Stream: general

### Topic: forall/pi bug

#### Kenny Lau (Jul 26 2020 at 17:53):

#mwe:

constant foo : ∀ {α : Type}, (∀ x : α, true → ∀ y : α, x = x)
#check foo


Error: the forall ∀ is converted to a pi Π in the suggestions.

Minimality: the following changes makes the bug disappear:

• making α into any concrete type (e.g. ℕ)
• removing the dependence of x = x on x (e.g. by changing it to true)
• making the type of y a concrete type
• removing true →
• removing ∀ y : α,

#### Bryan Gin-ge Chen (Jul 26 2020 at 18:01):

Changing the curly braces around α to parentheses also makes the bug disappear.

#### Bryan Gin-ge Chen (Jul 26 2020 at 18:08):

I think this line of shell/completion.cpp is where the completions are returned (if you have ideas about improving the suggestions, this file is also the place to start digging), and that calls "serialize_decl" to format the name and type. I can't look further at the moment, but maybe you can see what the issue is.

#### Scott Viteri (Aug 16 2020 at 17:48):

Is this an instance of the same bug, or something different?

universe u
variable (α : Type u)
inductive pairwise (R : α → α → Prop) : list α → Prop
| nil : pairwise (@list.nil α)
| cons : ∀ {a : α} {l : list α},
(∀ a':α, mem a' l → R a a') → pairwise l → pairwise (list.cons a l)

28:14: type mismatch at application
mem a'
term
a'
has type
α : Type u
but is expected to have type
Type ? : Type (?+1)


#### Mario Carneiro (Aug 16 2020 at 17:49):

what is mem?

#### Scott Viteri (Aug 16 2020 at 17:49):

Where list and mem are explicitly defined in the current namespace

#### Scott Viteri (Aug 16 2020 at 17:49):

def mem : α → list α → Prop
| a  list.nil       := false
| a (list.cons b l) := a = b ∨ mem a l


#mwe

(deleted)

#### Scott Viteri (Aug 16 2020 at 17:50):

alright, my bad will create mwe

#### Mario Carneiro (Aug 16 2020 at 17:50):

What is the type of mem

#### Mario Carneiro (Aug 16 2020 at 17:50):

#print mem -- ???

#### Kevin Buzzard (Aug 16 2020 at 17:50):

there is something wrong with your mem a' and it looks like you've just fed it a bad term but it's hard to tell if you don't post working code. As Mario said, if you look at the type of mem it will probably tell you what you did wrong.

#### Scott Viteri (Aug 16 2020 at 17:50):

α → list α → Prop

#### Mario Carneiro (Aug 16 2020 at 17:51):

that's an open term, I don't believe you

#### Kevin Buzzard (Aug 16 2020 at 17:51):

Is that the actual output of #check @mem?

#### Mario Carneiro (Aug 16 2020 at 17:52):

I notice also that in your post you wrote variable (α : Type u)

yes

#### Kevin Buzzard (Aug 16 2020 at 17:52):

My guess is that mem wants to be fed an explicit type i.e. alpha, and if you look at the actual type you'll see this.

#### Mario Carneiro (Aug 16 2020 at 17:52):

if you defined mem after that then it will pick up this explicit alpha

#### Scott Viteri (Aug 16 2020 at 17:52):

It takes a second to write the output of check since I can't copy paste minibuffer

I'm on it though

#### Mario Carneiro (Aug 16 2020 at 17:52):

there is a copy button

#### Mario Carneiro (Aug 16 2020 at 17:53):

oh you mean emacs

yes

#### Mario Carneiro (Aug 16 2020 at 17:53):

you should be able to copy from the problems panel or sidekick or whatever it's called

#### Scott Viteri (Aug 16 2020 at 17:53):

#check @mem
--mem : Π (α : Type u_1), α → list α → Prop


boom

#### Mario Carneiro (Aug 16 2020 at 17:54):

parentheses means explicit alpha

#### Jannis Limperg (Aug 16 2020 at 17:54):

On Emacs, you can open the buffer Lean Goal or Lean Errors and copy out of that.

#### Mario Carneiro (Aug 16 2020 at 17:54):

so you have to write mem _ a' l

#### Scott Viteri (Aug 16 2020 at 17:54):

Oh I figured out how to copy from minibuffer

#### Mario Carneiro (Aug 16 2020 at 17:54):

or else use variable {α : Type u} at the top of the file

#### Kevin Buzzard (Aug 16 2020 at 17:54):

and probably the same for R

#### Mario Carneiro (Aug 16 2020 at 17:54):

Not in pairwise, I think

#### Mario Carneiro (Aug 16 2020 at 17:55):

you want pairwise R l not pairwise _ l

#### Scott Viteri (Aug 16 2020 at 17:55):

Jannis Limperg said:

On Emacs, you can open the buffer Lean Goal or Lean Errors and copy out of that.

oh yeah that works too, I was just going to messages

#### Scott Viteri (Aug 16 2020 at 17:56):

Mario Carneiro said:

or else use variable {α : Type u} at the top of the file

Why?

#### Kyle Miller (Aug 16 2020 at 17:57):

Scott Viteri said:

Jannis Limperg said:

On Emacs, you can open the buffer Lean Goal or Lean Errors and copy out of that.

oh yeah that works too, I was just going to messages

The Lean Errors buffer (C-c C-n) is also where you can get #print and #lint messages for copy/paste.

#### Scott Viteri (Aug 16 2020 at 17:57):

Ok fixed thx for the super fast responses

#### Scott Viteri (Aug 16 2020 at 17:59):

I didn't realize that the errors buffer also takes output from commands

#### Kyle Miller (Aug 16 2020 at 17:59):

(Also, while you can't copy paste them, you can use C-c C-b to get inline command output.)

#### Scott Viteri (Aug 16 2020 at 18:00):

Yeah that's a nice feature

Last updated: May 11 2021 at 12:15 UTC