Defining fixpoint types

Stream: new members

[aron]

I'm implementing a type system and I'd like to define 3 different Lean types for different purposes

1. a type that can only contain concrete types
2. a type that can contain concrete types and also unification variables
3. a type that can contain both the above and also type variables

To avoid duplication, I'd like to use this inductive to construct these 3 types:

inductive TypeContainer (a : Type u) where
  | primitive : (p : Primitive) → TypeContainer a
  | option : a → TypeContainer a
  | result : (ok : a) → (err : a) → TypeContainer a
  | list : a → TypeContainer a
  | arrow : (from' : a) → (to' : a) → TypeContainer a

To construct the concretes-only type, I'd pass TypeContainer into itself. To construct the concretes + unification vars I'd pass in another type that contains a unification variable variant. And similarly for the type that can contain type variables.

Here's what I'm trying:

inductive Fix (f : Type u → Type u) where
  | mk : f (Fix f) → Fix f

def ConcreteType := Fix TypeContainer

inductive ExtendedType where
  | concrete : Fix TypeContainer → ExtendedType
  | uniVar : UniVar → ExtendedType

def WithUniVars := Fix (TypeContainer ∘ ExtendedType)

But Lean gives me an error for Fix.mk:
(kernel) arg #2 of 'Fix.mk' contains a non valid occurrence of the datatypes being declared

[Arthur Adjedj]

You can't have an arbitrary fixpoint type in Lean, as it would make the system unsound. You can however define your specific ConcreteType as such:

inductive TypeContainer (a : Type u) where
  | primitive : (p : Primitive) → TypeContainer a
  | option : a → TypeContainer a
  | result : (ok : a) → (err : a) → TypeContainer a
  | list : a → TypeContainer a
  | arrow : (from' : a) → (to' : a) → TypeContainer a

inductive FixContainer where
  | mk : TypeContainer FixContainer → FixContainer

[Edward van de Meent]

see this doc issue for more on what makes Fix unsound

[aron]

Hmm ok. Is there a different way to implement these 3 different types around the core TypeContainer type then?