Recursive type synonym with promoted constructors

Question

I have a nice way to wrap multiple type parameters into one.

data WorldModel = WorldModel Type Type Type
-- plus type families to extract them

I had a type synonym type PlainWorldModel = 'WorldModel Some Instantiation Here which works fine.

Now I want the parameterisation to be recursive type PlainWorldModel = 'WorldModel Some Instantiation (Here PlainWorldModel) which I cannot obviously do with type synonyms, because of substitution.

How can I do it with newtype? I can't make the newtyped field be of type WorldModel, only of Type.

Do I need to bring in singletons?

Concisely,

type PlainWorldModel = 'WorldModel Some Instantiation Here -- this was fine
type PlainWorldModel = 'WorldModel Some Instantiation (HereParameterised PlainWorldModel) -- I want to do this and it is not fine

newtype PlainWorldModel = PWM ( 'WorldModel Some Instantiation (HereParameterised PlainWorldModel)) -- this does not work

Answer 1

I don't have a definite answer, but I am leaning towards this being impossible to achieve in Haskell.

A key feature of types in Haskell is that whenever we have t :: k where k is any kind, then the (type-level) expression t should be (strongly) normalizing. In other words we should be able to expand all type synonyms, all type families, etc. in t and reach its normal form in a finite number of steps.

There are a few culprits here that partially break this property. UndecidableInstances for instance allows for infinitely recursing type families. Having Type :: Type is also problematic. However, if we disregard those, normalization should hold.

Now, what you want to achieve is general type-level recursion type T = F T for some F. This is called "equi-recursion" and would break normalization and arguably should be prevented at all kinds.

You might then wonder why in the kind Type we do allow recursion, then. Well, there we only allow "iso-recursion". We never have the strict equality T ~ F T but we only allow the two distinct types T and F T which "just happen" to be isomorphic, and provide the constructors/eliminators to express such isomorphism. This also makes our type system nominal (and not structural).

Such recursion only happens at the kind Type though.

My hunch is that, if we wanted to allow recursion in other kinds, we would need to have some form of "iso-recursion", so to ensure normalization. I am not completely sure about how that would work.