A different way to achieve the guarantee you want is to let unification do the "oring" for you: {-# LANGUAGE GADTs #-} {-# LANGUAGE Rank2Types #-} {-# OPTIONS_GHC -fwarn-incomplete-patterns #-} data HasVar data Expr t where Add :: Expr x -> Expr x -> Expr x Lit :: Int -> Expr x Var :: Expr HasVar eval :: (forall x . Expr x) -> Int eval = go where go :: Expr () -> Int go (Add a b) = go a + go b go (Lit a) = a / Emil Den 2016-12-07 kl. 08:43, skrev Guillaume Bouchard:
Hi.
I have the following GADT :
----------------------------- type family Or a b where Or 'False 'False = 'False Or _ _ = 'True
data Expr t where Add :: Expr t -> Expr t' -> Expr (Or t t') Lit :: Int -> Expr 'False Var :: Expr 'True ----------------------
The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.
I now want to evaluate my expression, something like that :
-------------- eval :: Expr t -> Int eval (Lit i) = i eval (Add a b) = eval a + eval b eval Var = error "Cannot evaluate expression with variable" ----------------
Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :
--------------- eval' :: Expr 'False -> Int eval' (Lit i) = i eval' (Add a b) = eval' a + eval' b ----------------
However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.
The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.
Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".
The type checker does not know that, hence my code does not compile.
Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:
type family InverseOr a where InverseOr 'False = ('False, 'False)
Thank you.
-- G.
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.