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 |