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.