Picking a `case` with mutually inductive types

Stream: general

[Wojciech Nawrocki]

I think there might be something wrong with naming scopes with mutually inductive types - it seems impossible to pick one of its constructors as a case in the type's own namespace:

mutual inductive foo, bar
with foo: Type
| FooA: foo
| FooB: foo → foo
with bar: Type
| Bar: bar

namespace foo

#check FooB -- FooB : foo → foo
#check foo.FooB -- FooB : foo → foo

example (f: foo)
  : f = f := begin -- nevermind I'm proving f=f by cases, it's just an example
  cases f,

  case FooB { sorry },
  /- invalid `case`, there is no goal tagged with prefix [FooB]
     state:
     2 goals
     case foo.FooA
     ⊢ FooA = FooA

     case foo.FooB
     f : foo
     ⊢ FooB f = FooB f -/

  case foo.FooB { sorry },
  /- 'foo.FooB' is not a constructor
     state:
     2 goals
     case foo.FooA
     ⊢ FooA = FooA

     case foo.FooB
     f : foo
     ⊢ FooB f = FooB f -/
end

[Mario Carneiro]

I think the "foo.fooB is not a constructor" message is not very forward thinking

[Mario Carneiro]

probably requires a patch to lean though

[Wojciech Nawrocki]

Yeah I think it's definitely broken. If I introduce a notation ``FOOB`` := foo.FooB before namespace Foo and then use it inside in a function fn within the namespace, unfold fn stops working. I can't reproduce this so possibly I made a mistake somewhere.