workaround to get both domain-specific errors and also multi-modal type inference?
Nicolas Frisby
nicolas.frisby at gmail.com
Tue Feb 11 16:11:13 UTC 2014
Are we reaching the point where a wiki page and perhaps (soon) a Trac
ticket would be appropriate?
On Tue, Feb 11, 2014 at 10:10 AM, Nicolas Frisby
<nicolas.frisby at gmail.com>wrote:
> On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães <jpm at cs.uu.nl>wrote:
>
>> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <nicolas.frisby at gmail.com
>> > wrote:
>>
>>> > type family GHC.Exts.Message (c :: Constraint) :: Maybe Symbol
>>>
>> While I do find this problem very relevant, and think this solution is
>> going in the right direction,
>> I'm afraid it's not that simple. Say I have
>>
>> type instance Message (MyClass a) = Just ...
>>
>> How will this behave if the unsatisfied constraint is of the form (C b,
>> MyClass a)? How about
>> f (MyClass a), for some f :: Constraint -> Constraint?
>>
>> Also, isn't it a bit unsatisfying that an instance such as
>>
>> type instance Message a = Just ...
>>
>> would pollute error messages everywhere?...
>>
>
> Hi Pedro. Very glad you're joining in.
>
> Thank you for the helpful observations. I see two options.
>
> 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.
>
> These limits each restrict the expressivity but deserve investigation
> regarding how much mileage we can get out of them.
>
> 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.
>
> -----
>
> 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:
>
> > class Constraint a b where -- this is the actual class of interest
> >
> > data Trace = forall a b. Start a b | ...
> >
> > instance InternalConstraint (Start a b) a b => Constraint a b
> >
> > class InternalConstraint trace x y -- all instances are parametric wrt `
> trace'
> >
> > -- I'm assuming Message has range Maybe Doc, where GHC interprets Doc to
> build an error message.
> > type instance Message (InternalConstraint a b x y) =
> > Just ( Text "While solving Constraint for " <> ShowType a <> Text "
> and " <> ShowType b
> > <> Text " the point of failure was " <> ShowType x <> Text " and
> " <> ShowType y <> Text "."
> > )
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140211/0d73f780/attachment.html>
More information about the ghc-devs
mailing list