Code using type synonym families requires workarounds to compile

I am trying to use type synonym families to create GADTs that can be used interchangably as both typed and untyped ASTs for a small programming language. Here are the (cut down & simplified) definitions:

data Typed
data Untyped

type family TU a b :: *
type instance TU Typed b = b
type instance TU Untyped b = ()

-- A type witness type, use eg. for pattern-matching on types
data Type a where
    TypeInt     :: Type Int
    TypeBool    :: Type Bool
    TypeString  :: Type String
    TypeList    :: Type t -> Type [t]

data Expr :: * -> * -> * {- tu a -} where
    Const :: Type a -> a -> Expr tu (TU tu a)
    Var2  :: String -> TU tu (Type a) -> Expr tu (TU tu a)

It mostly works, which still amazes me, but there are some small glitches. For example in some cases I have to use (TU Typed Bool) instead of Bool, even if they should be equal (type instance TU Typed b = b). In other cases I have to artificially restrict or generalize functions' type signatures. Or I have to put type signatures in patterns. The biggest problem is that it isn't obvious which workaround is needed in a given case. For some cases I don't have a satisfactory workaround yet.

Perhaps these problems simply reflect immaturity of type synonym family support in GHC, but, on the other hand, it may be some simple bug which could be fixed for GHC 6.8.

I've created a set of test files which I will attach to this ticket. Run check.sh to see how GHC handles the original (inteded) code and the workarounds. But first set the path to ghc in the script.

Trac metadata

Trac field	Value
Version	6.8
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Unknown
Architecture	Unknown