Non-valid occurrence when abbreving a constructor argument

Stream: lean4

[Valentin Robert]

This is simplified a lot from my actual example, but I'm having an issue with the following:

abbrev Aliased (A : Type a) : Type a := List A
inductive Thing (K : Type k) : Type k where
  | ThingCtor : Aliased (Thing K) → Thing K

inductive ThingInlined (K : Type k) : Type k where
  | ThingCtorInlined : List (Thing K) → Thing K

In my real example, the Aliased thing is more involved (it's something like List (List (Rat × A)), and repeated over many constructors of Thing, so it's annoying to have it inlined everywhere. I tried to pull it out as a def or abbrev, but this gives:

(kernel) arg #2 of 'Thing.ThingCtor' contains a non valid occurrence of the datatypes being declared

Is there a trick here? The inlined version is perfectly accepted, but I'd like to extract out the wrapper around recursive occurrences.