Potential vm bug

Stream: general

[Keeley Hoek]

The following code typechecks:

meta def oopsie : list string → tactic (option string)
| [] := none                          -- I'm being naughty on this line
| (a :: rest) := oopsie rest

#eval oopsie ["a"]

I don't understand why it should. If I inspect the output of the #eval, I see the output "failed". Have I found a bug in the VM?

[Edward Ayers]

There is a coercion from option to tactic in tactic.lean:

meta instance opt_to_tac : has_coe (option α) (tactic α) :=
⟨returnopt⟩

[Edward Ayers]

So your tactic will throw if you give it an empty list

[Keeley Hoek]

Ah, cheers!

[Edward Ayers]

I only spotted this because I happen to be reading tactic.lean currently. Does anyone know if there is a way to discover what coercions are occurring in a given expression? Or a #command which will tell me coercions to a particular type?

[Edward Ayers]

I can't figure out how to use
set_option pp.coercions true

[Simon Hudon]

I only spotted this because I happen to be reading tactic.lean currently.

Good read! Don't spoil the ending though!

[Simon Hudon]

Does anyone know if there is a way to discover what coercions are occurring in a given expression?

#print instances has_coe