On Mon, Mar 15, 2010 at 5:31 PM, Louis Wasserman
GADT types that cannot be reified by TH. Essentially, I think this is "the set of GADT data types that actually couldn't be implemented without GADTs." Not sure, though. In any event, at the moment, I don't think there's any hope of handling GADTs in TH at this point, so I don't really object to this problem.
Actually, with existential types and type equality constraints, GADTs are redundant. Here's a couple examples: data GEqType a b where GRefl :: EqTypeGADT a a data DEqType a b = (a ~ b) => DRefl data Expr t where Lam :: (Expr a -> Expr b) -> Expr (a -> b) App :: Expr (a->b) -> Expr a -> Expr b Prim :: Show a => a -> Expr a Gt :: Expr Int -> Expr Int -> Expr Bool data DExpr t = forall a b. (t ~ (a -> b)) => DLam (DExpr a -> DExpr b) | forall a. DApp (DExpr (a -> t)) (DExpr a) | Show t => DPrim t | (t ~ Bool) => Gt (DExpr Int) (DExpr Int) The algorithm is pretty simple: - existentially quantify over all type variables mentioned in the GADT constructor - add a type equality constraint to match the result type - (optional) simplify -- ryan