Promote datatypes with arrows, among others

[goldfirere]

In thinking about #78, I realized that fixing that bug opens up a whole new possibility for promotion.

Say a user wants to promote

data NatPred = MkNP (Nat -> Bool)

Currently, that just won't promote, because functions are different in types than they are in terms. But, what if we refactor to

data NatPred2' nat_arrow_bool = MkNP nat_arrow_bool
type NatPred2 = NatPred2' (Nat -> Bool)

The two NatPreds should behave identically in all settings, except that NatPred2 will not promote, because type synonyms do not promote. But, if we expand type synonyms before promotion, then NatPred2 becomes NatPred2' (Nat -> Bool), which is perfectly promotable. And, tantalizingly, it promotes correctly, to NatPred2' (TyFun Nat Bool -> *). Huzzah!

So, the implementation plan here is:

1. Detect datatypes that have members that do not promote but are fixable. This includes arrow members, and members whose types are type synonyms. (But see below for ways of expanding this set.)
2. Refactor the datatype to make the unpromotable bit a parameter to the datatype.
3. Make a type synonym to make this refactoring transparent to term-level users.
4. Promote as usual, making sure always to expand type synonyms.

What's unusual about this approach is that it means that the code the users write is not exactly what they get, at the term level. Currently, in a promote or singletons call, the user's code informs the promoted and singletonized versions but is otherwise passed through unchanged. This new idea would change that, but in (what should be) a harmless way.

Future expansion ideas: we could do something similar with String, promoting to Symbol. Functions that treat String like a list won't work, but just storing Strings would work fine. And, we could also think about doing this trick to get, say, Integer to promote to some custom type-level Integer kind.

[jstolarek]

The two NatPreds should behave identically in all settings, except that NatPred2 will not promote, because type synonyms do not promote. But, if we expand type synonyms before promotion, then NatPred2 becomes NatPred2' (Nat -> Bool), which is perfectly promotable.

So it is enough to expand the type synonym and when we pass the type to promotion all will work fine? I think the details escape me. If I promote:

data NatPred2' nat_arrow_bool = MkNP nat_arrow_bool
type NatPred2 = NatPred2' (Nat -> Bool)

what will I get? A NatPred2Sym0 = NatPred2' (TyFun Nat Bool -> *) type synonym and a datakind NatPred2' nat_arrow_bool = MkNP nat_arrow_bool? Is that correct?

[goldfirere]

Type synonyms don't promote at all -- GHC doesn't support it. But NatPred2 promotes fine. And, if we're expanding synonyms, then any use of NatPred2 gets expanded into NatPred2' (Nat -> Bool), a type which promotes to NatPred2' (TyFun Nat Bool -> *).

Does that help?

[jstolarek]

Yes, I think I'm closer to understanding this now. I think I just need to see this in practice :-)

[RyanGlScott]

#450 allows "semi-automatic" promotion of Natural to Nat etc. by allowing you to specify special name mappings during promotion. It doesn't implement the idea of sharing the same underlying data type (as in NatPred2' above), but the overall idea is very similar.