There are some questions / notes:
1. Could ghc use reduced "vanila types" for calculation with definition stored somewhere specially for error messages?
2. I didn't expect that type families can be without any parameters. But they really can. So instead of
> type T2 = T1 Int Int
I can write
> type family T2 where T2 = T1 Int Int
which is rather strange though.
Moreover in this case ghc asks me for TypeFamilies and UndecidableInstances.
In my scenario such code should write library-user. So including these (especially UndecidableInstances) extensions in his/her code is Undesirable.
3. For type families more natural to have parameters but in this case we often can't reduce it deeply I suppose.
Short simple example:
type family L a b where
L a () = (a,())
L a (b,c) = (a,(b,c))
type T1 = L Int ()
type T2 = L Int T1
type T3 = L Int T2
type T3_Char = L Char T2
and so on...
Well, about my "complicated type-level program" now. I start to play/work with well-known "named-fields" problem. My code is here. I hoped to find decision with properties:
- O(log n) time to get field from record by name
- record construction independent from order of fields definitions
- no TH preferrable, some TH possible
- projections and joins are desirable
I tried to implement it using "very-well balanced tree" (I don't know the right name) on type level.
This is a binary search (by name) tree with count of left items is the same or one more than on the right side (for each subtree).
The problem is construction. I realized it with FunDeps and with TF. User should write > type Rec = () <+ "a":>Int <+ "b":>Char <+ "c":>String
> rec = () <+ (V "c" :: "c":>String) <+ (V 1 :: "a":>Int) <+ (V 'b' :: "b":>Char)
or
> rec = () <+ (V "c" :: "c":>String) <+ (V 1 :: "a":>Int) <+ (V 'b' :: "b":>Char) :: Rec
and got
rec = (((),V 1,()),V'b',((),V "c")) :: (((),"a":>Int,()),"b":>Char,((),"c":>String,())
(Constructions like (V 1 :: "a" :> Int) rather ugly. Any ideas are welcomed... Perhaps some TH?)
I tried also to make a type-level sorted list but it is also too complicated for ghc.
I didn't check time with no-parameters-TF as you suggested. I will.
Best regards,
Dmitry