Partial application of type synonyms

Question

I'm having trouble with unsaturated type synonyms in the following example:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LiberalTypeSynonyms #-}

module TypeFamilyHackery where

data T k v a = T

type family CollectArgTypes arr where
  CollectArgTypes (a -> b) = (a, CollectArgTypes b)
  CollectArgTypes _ = ()

type family MapReturnType f t where
  MapReturnType f (a -> b) = a -> MapReturnType f b
  MapReturnType f r = f r

type MkT k v = T k v v

-- | Goal:
-- @
--   BuryT Int = T () Int Int
--   BuryT (Bool -> Int) = Bool -> T (Bool, ()) Int Int
--   BuryT (a -> b -> c) = a -> b -> T (a,(b,())) c c
-- @
type BuryT t = MapReturnType (MkT (CollectArgTypes t)) t

But this complains with The type synonym 'MkT' should have 2 arguments, but has been given 1. I could specialize MapReturnType for MkT (CollectArgTypes t), but I rather like it how it is.

Since -XLiberalTypeSynonyms doesn't seem to deliver (why?), what are my options to get BuryT working?

Answer 1

LiberalTypeSynonyms works by inlining all “obvious” type definitions. To make your example work, it would have to

1. Treat MapReturnType (MkT (CollectArgTypes t)) t first as some MapReturnType ㄊ t
2. Inline this to ㄊ t, using the definition MapReturnType f r = f r
3. At this point, invoking ㄊ again would give MkT (CollectArgTypes t) t which is a perfectly fine fully-applied synonym and hence no problem.

But step 2 isn't possible, because MapReturnType is not just a synonym. To use MapReturnType f r = f r, the compiler would first have to be sure that r isn't a function type, but it really can't know this – it's after all a completely free parameter.

So what the compiler would actually need to do there is, defer the resolution of MapReturnType and thus also of BuryT to concrete use sites. Now, that might be quite useful, but it would open up quite a can of worms. Namely, it would then be very easy to intertwine Turing-complete programs anywhere in the types of your program. I don't think this is worth it.