Support partial type synonyms

[jgbm]

While we're thinking about #3, we should be sure that type synonyms don't give another route to an ill-kinded type. Something like:

data Ord a => BST a = ...
type Pairs a = BST (a, a)
f :: a -> Pairs a
f = undefined
g = f id

There's also a historical detail here: the first version of the Haskell report allowed you to write

type Num a => Point a = (a, a)

but this was dropped from later versions of the report, as nobody knew how to implement it.

There's a similar approach to that for type families:

• [x] Type synonym declarations type T a = U should also generate declarations type X_T a = wft(U)
• [x] Type synonym applications T a should be constrained by X_T a.
• [x] Inlining terms that have type as type synonyms sometimes fails. (ref. in Cabal, #~ unfolding in function liftOptionL)
  • [ ] Support for constraints on type synonym declarations The GHC parser doesn't seem to include support for constraints on type synonym declarations, so I don't think actually supporting them is a top priority.

[fxdpntthm]

The GHC parser doesn't seem to include support for constraints on type synonym declarations, so I don't think actually supporting them is a top priority.

Maybe I misunderstood this comment. did you mean to say type Num a => Point a = (a, a)

Actually they are okay with elaboration: atleast in GHC-9.

~~We now elaborate the type synonyms as follows: type T a = U get elaborated to type T a = wft(U) => U~~

We also perform some optimization where if wft(U) is () then we get a identity elaboration.

[fxdpntthm]

consider the following declarations

data Ord a => T a = ...
type T a = DT a

f :: ... -> T a -> ...

we elaborate the type signature of f to be

f :: DT @ a => ... -> T a -> ...

I don't think we need to generate a special type family X_T a :: Constraint for each type synonym that we encounter. We can get away with expanding the RHS of the type and then generating the constraints to be added to the original type and thus constraining the use of of T.

[fxdpntthm]

Inlining terms with type synonyms are no longer are an issue. I suspect this was an issue when we had disabled type reduction.

[fxdpntthm]

The GHC parser doesn't seem to include support for constraints on type synonym declarations, so I don't think actually supporting them is a top priority.

Marking this as low priority as not having constraint type synonyms is not going to break our work.