Motive issue when creating a dependent structure instance

Stream: new members

[Vláďa Sedláček]

import Mathlib.Data.List.Perm

def foo (a b : List α) := True

structure bar (a : List α) where
  b : List α
  baz : foo a b

def perm_bar {a b : List α} (A : bar a) (perm: a ~ b) : bar b := by
  induction perm with
  | nil => sorry
  | cons => sorry
  | swap => sorry
  | trans => sorry

In the above example, induction fails with the following error:

type mismatch when assigning motive
  fun {a b} perm => bar a → bar b
has type
  {a b : List α} → a ~ b → Type ?u.391 : Type (?u.391 + 1)
but is expected to have type
  (a a_1 : List α) → a ~ a_1 → Prop : Type ?u.391

and the same goes for cases (match fails with tag not found, which might be unrelated).
What would be the proper way to instantiate bar b, while making use of the inductively defined perm?

[Kyle Miller]

It looks like what it's indirectly letting you know is that docs#List.Perm is a Prop, so you can't induct on it to create data.

[Kyle Miller]

You could prove Nonempty (bar b) inductively for example, since this is a proposition.

[Kyle Miller]

The hint in the motive type is that the computed motive has that Type ?u.391 in it, but the expected type of the motive (as controlled by List.Perm) has Prop in its place.