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?
LiberalTypeSynonyms
works by inlining all “obvious” type definitions. To make your example work, it would have toMapReturnType (MkT (CollectArgTypes t)) t
first as someMapReturnType ㄊ t
ㄊ t
, using the definitionMapReturnType f r = f r
ㄊ
again would giveMkT (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 useMapReturnType f r = f r
, the compiler would first have to be sure thatr
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 ofBuryT
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.