<div dir="auto">While you're at it, you should probably add the rest of the implications:<div dir="auto"><div dir="auto"><br></div><div dir="auto">If (r && Not t) (t' ~ 'True) (() :: Constraint),</div><div dir="auto">If (r && Not t') (t ~ 'True) (() :: Constraint)</div></div><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On Dec 7, 2016 9:18 PM, "David Feuer" <<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>> wrote:<br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto"><div>Er... There's a missing close paren at the end of the context; sorry. That should be</div><div dir="auto"><br></div><div dir="auto"><span style="font-family:sans-serif">Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint)) => Expr t -> Expr t' -> Expr r</span><div class="elided-text"><br><div class="gmail_extra" dir="auto"><br><div class="gmail_quote">On Dec 7, 2016 9:16 PM, "David Feuer" <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br type="attribution"><blockquote class="m_-2594511278806432836quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">Yes, you can do this. Enable ConstraintKinds, import Data.Type.Bool and something exporting Constraint, and change your Add constructor to<div dir="auto"><br></div><div dir="auto">Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint) => Expr t -> Expr t' -> Expr r</div><div dir="auto"><br></div><div dir="auto">Then both eval and eval' are accepted. There may be some cleaner way; I'm no expert.<br><div dir="auto"><div dir="auto"><br><div class="gmail_extra"><br><div class="gmail_quote"><div class="m_-2594511278806432836elided-text">On Dec 7, 2016 2:43 AM, "Guillaume Bouchard" <<a href="mailto:guillaum.bouchard%2Bhaskell@gmail.com" target="_blank">guillaum.bouchard+haskell@gma<wbr>il.com</a>> wrote:<br type="attribution"></div><blockquote class="m_-2594511278806432836m_6787817306857906682quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="m_-2594511278806432836elided-text"><div dir="ltr">Hi.<div><br></div><div>I have the following GADT :</div><div><br></div><div>-----------------------------</div><div><div>type family Or a b where</div><div>  Or 'False 'False = 'False</div><div>  Or _ _ = 'True</div><div><br></div><div>data Expr t where</div><div>  Add :: Expr t -> Expr t' -> Expr (Or t t')</div><div>  Lit :: Int -> Expr 'False</div><div>  Var :: Expr 'True</div></div><div>----------------------</div><div><br></div><div>The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.</div><div><br></div><div>I now want to evaluate my expression, something like that :</div><div><br></div><div>--------------</div><div><div>eval :: Expr t -> Int</div><div>eval (Lit i) = i</div><div>eval (Add a b) = eval a + eval b</div><div>eval Var = error "Cannot evaluate expression with variable"</div></div><div>----------------</div><div><br></div><div>Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :</div><div><br></div><div>---------------</div><div><div>eval' :: Expr 'False -> Int</div><div>eval' (Lit i) = i</div><div>eval' (Add a b) = eval' a + eval' b</div></div><div>----------------</div><div><br></div><div>However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.</div><div><br></div><div>The wiki <a href="https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies" target="_blank">https://ghc.haskell.org/t<wbr>rac/ghc/wiki/InjectiveTypeFami<wbr>lies</a> classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.</div><div><br></div><div>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".</div><div><br></div><div>The type checker does not know that, hence my code does not compile.</div><div><br></div><div>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:</div><div><br></div><div>type family InverseOr a where</div><div>     InverseOr 'False = ('False, 'False)</div><div><br></div><div>Thank you.</div><font color="#888888"><div><br></div><div>-- </div><div>G.</div></font></div>
<br></div>______________________________<wbr>_________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bi<wbr>n/mailman/listinfo/haskell-caf<wbr>e</a><br>
Only members subscribed via the mailman list are allowed to post.<br></blockquote></div><br></div></div></div></div></div>
</blockquote></div><br></div></div></div></div>
</blockquote></div><br></div></div>