workaround to get both domain-specific errors and also multi-modal type inference?

[Nicolas Frisby]

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/94de443b/attachment.html>