<p dir="ltr">Thanks for suggesting that; I was only seeing Constraint as in ConstraintKinds.</p>
<p dir="ltr">I think the gist of my previous concerns doesn't change, though: open type pattern matching (or some dissatisfying approx of), assuredly pure functions, etc.</p>
<div class="gmail_quote">On Feb 11, 2014 12:15 PM, "Richard Eisenberg" <<a href="mailto:eir@cis.upenn.edu">eir@cis.upenn.edu</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div style="word-wrap:break-word"><div>One potential source of confusion in this thread:</div><div><br></div><div>When Adam initially suggested a function (Constraint -> Maybe String), I believe he was referring to constraints as they slosh around within GHC, *not* the kind-level Constraint available with ConstraintKinds. So, the error-reporting function would be written in a separate module from the code it affects, and it would be imported somewhat like Template Haskell does. Then, GHC could call the function when type inference fails. This would make programming the interface much easier and more expressive.</div>
<div><br></div><div>Please correct me if I'm wrong, but it seemed that different people were talking about different solutions!</div><div><br></div><div>Richard</div><br><div><div>On Feb 11, 2014, at 11:10 AM, Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com" target="_blank">nicolas.frisby@gmail.com</a>> wrote:</div>
<br><blockquote type="cite"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães <span dir="ltr"><<a href="mailto:jpm@cs.uu.nl" target="_blank">jpm@cs.uu.nl</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">
<div>On Tue, Feb 11, 2014 at 3:32 AM, Nicolas <span>Frisby</span> <span dir="ltr"><<a href="mailto:nicolas.frisby@gmail.com" target="_blank"><span>nicolas</span>.<span>frisby</span>@gmail.com</a>></span> wrote:<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<p dir="ltr">> type family GHC.Exts.Message (c :: Constraint) :: Maybe Symbol</p></blockquote><div>While I do find this problem very relevant, and think this solution is going in the right direction,<br></div></div>
<div>I'm afraid it's not that simple. Say I have</div><div><br></div><div> type instance Message (<span>MyClass</span> a) = Just ...</div><div><br></div><div>How will this behave if the unsatisfied constraint is of the form (C b, <span>MyClass</span> a)? How about</div>
<div>f (<span>MyClass</span> a), for some f :: Constraint -> Constraint?</div><div><br></div><div>Also, isn't it a bit unsatisfying that an instance such as</div><div><br></div><div> type instance Message a = Just ...</div>
<div><br></div><div>would pollute error messages everywhere?...</div></div></div></div></blockquote><div><br></div><div>Hi Pedro. Very glad you're joining in.</div><div><br></div><div>Thank you for the helpful observations. I see two options.</div>
<div><br></div><div>1) Keep it simple at first. EG An unsatisfied conjunction is decompose into a list of its unsatisfied conjuncts before ab Message is ever sought. Similarly, only support matching the head of the unsatisfied constraint, so the Message pattern would have to match (F (MyClass a)), for whichever F is your `f'. And so on. Lastly, we might consider allowing type class-like overlap for instances of the Message family, since it's use-case is so specific.</div>
<div><br></div><div>These limits each restrict the expressivity but deserve investigation regarding how much mileage we can get out of them.</div><div><br></div><div>2) Or we could design a type-level DSL for querying the "trace" of the constraint-solver that ended up with this unsatisfied constraint. This sounds much harder to me, since I'm unfamiliar with the solver and its internals. But it seems like the way to maximize expressitivity.</div>
<div><br></div><div>-----</div><div><br></div><div>I should point out that I think the courageous library designer could squeeze some of the functionality of (2) out of (1), at the cost of obfuscation. For example:</div>
<div><br></div><div><font face="courier new, monospace">> class Constraint a b where -- this is the actual class of interest</font></div>
<div><font face="courier new, monospace">> <br></font></div><div><font face="courier new, monospace">> data Trace = forall a b. Start a b | ...</font></div><div><font face="courier new, monospace">> </font></div>
<div><font face="courier new, monospace">> instance InternalConstraint (Start a b) a b => Constraint a b</font></div><div><font face="courier new, monospace">> <br>
</font></div><div><font face="courier new, monospace">> class InternalConstraint trace x y -- all instances are parametric wrt `</font><span style="font-family:'courier new',monospace">trace'</span></div><div>
<font face="courier new, monospace">> <br></font></div>
<div><font face="courier new, monospace">> -- I'm assuming Message has range Maybe Doc, where GHC interprets Doc to build an error message.</font></div><div><font face="courier new, monospace">> type instance Message (InternalConstraint a b x y) =</font></div>
<div><font face="courier new, monospace">> Just ( Text "While solving Constraint for " <> ShowType a <> Text " and " <> ShowType b</font></div>
<div><font face="courier new, monospace">> <> Text " the point of failure was " <> ShowType x <> Text " and " <> ShowType y <> Text "."</font></div><div>
<font face="courier new, monospace">> )</font></div></div></div></div>
_______________________________________________<br>ghc-devs mailing list<br><a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</blockquote></div><br></div></blockquote></div>