Tom Schrijvers wrote:

Have you first, before you turn to GHC< considered whether this code should be well-typed in any type system?

...

Review3.lhs:67:29: Could not deduce (Expandable (Tuple (Map ((,) t2) ys))) from the context (xs ~ t2 ::: ts2, Expandable t2) arising from a use of `:::' at Review3.lhs:67:29-59

At first sight, it looks like this constraint

Expandable (Tuple (Map ((,) t2) ys)) is indeed one that's required to hold in order to make the code well-typed. Do you agree?

Yet I see no instance of Expandable for Tuple. So why do you think this constraint should hold anyway?

I agree with you. I think the code is not supposed to type check, and that's what I experience from GHC so far. One problem that bothers us is that, as I mentioned in my original message, there were at least two reports that they were possible to type check in GHC, which we cannot reproduce. So, I'm just wondering what version and settings that makes it type check (if such version or setting exists, its good for GHC type system developers to be aware of it), and just double check if there is any other typing rules/theories that I am not aware of makes the code type check (if such version of GHC exists and it is not a bug). Another problem, which I haven't mentioned, I have when I tried to make additional type family instance declarations that latest (stable) distributions of GHC 6.10.x does not let me declare instances of (Expandable (Tuple (Map ((,) t2) ys))). When you try declaring such an instance something like this:

instance Expandable (Tuple (Map ((,) t2) ys)) where ...

GHC will give me an error message that type synonyms are not allowed in instance declarations: kyagrd@kyavaio:~/tmp$ ghci -fglasgow-exts -XUndecidableInstances Review3.lhs GHCi, version 6.10.3: http://www.haskell.org/ghc/ :? for help Loading package ghc-prim ... linking ... done. Loading package integer ... linking ... done. Loading package base ... linking ... done. [1 of 1] Compiling Main ( Review3.lhs, interpreted ) Review3.lhs:62:2: Illegal type synonym family application in instance: Tuple (Map ((,) t2) ys) In the instance declaration for `Expandable (Tuple (Map ((,) t2) ys))' Failed, modules loaded: none. So, my impression is that there is little hope even I try fixing this by adding more instance declarations, even if this was an incomplete code because of space restrictions of the review. But I still wanted to double check and discuss this matter with mailing list readers since there were few reports (which we fail to reproduce) that this type checks in their installation of GHC.