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

Tue Feb 11 18:55:51 UTC 2014

If, when defining the `describeError' method, I wanted to refer to one of
my library's classes from inside a pattern (or guard in the rhs, I
suppose), how would I do that? Via a Template Haskell literal name? Or
would I call the TcM interface for looking up a name?

In my opinion [1], the TcM interface is too user-antagonistic, even for GHC
power-users [2], and moreover would leak implementation details. I would
prefer a more light-weight interface, dedicated to just domain-specific
errors.

That said, it seems that a general interface comparable to the one I have
been hocking could be built atop what you two are proposing and
subsequently marked {-# LANGUAGE Trustworthy #-}. Thumbs up.

[1] - Disclaimer: I've already noted that I'm not familiar with the
type-checker implementation.
[2] - I consider myself a GHC power-user.

On Tue, Feb 11, 2014 at 12:43 PM, Adam Gundry <adam at well-typed.com> wrote:

> Thanks for clarifying, Richard, I should have been clearer. "Constraint"
> was a poor choice of type without further explanation.
>
> Nicolas, Pedro, thanks for your feedback!
>
> On 11/02/14 18:24, Nicolas Frisby wrote:
> > Thanks for suggesting that; I was only seeing Constraint as in
> > ConstraintKinds.
> >
> > 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.
>
> The point of doing it this way - effectively hooking code into GHC - is
> that the error-reporting code would work with the GHC internal
> representation of constraints, thereby avoiding trouble with open types.
> The GHC API can be used to decompose the constraint type. This would
> make it much easier to do complex processing than trying to write tricky
> functional programs with type families. We might also want the
> error-reporting function to live in GHC's TcM monad so it has access to
> whatever state it wanted.
>
> Cheers,
>
> Adam
>
> [Resent to ghc-devs from the correct email address.]
>
>
> > On Feb 11, 2014 12:15 PM, "Richard Eisenberg" <eir at cis.upenn.edu
> > <mailto:eir at cis.upenn.edu>> wrote:
> >
> >     One potential source of confusion in this thread:
> >
> >     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.
> >
> >     Please correct me if I'm wrong, but it seemed that different people
> >     were talking about different solutions!
> >
> >     Richard
> >
> >     On Feb 11, 2014, at 11:10 AM, Nicolas Frisby
> >     <nicolas.frisby at gmail.com <mailto:nicolas.frisby at gmail.com>> wrote:
> >
> >>     On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães
> >>     <jpm at cs.uu.nl <mailto:jpm at cs.uu.nl>> wrote:
> >>
> >>         On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby
> >>         <nicolas.frisby at gmail.com <mailto: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 "."
> >>     >        )
> >>     _______________________________________________
> >>     ghc-devs mailing list
> >>     ghc-devs at haskell.org <mailto:ghc-devs at haskell.org>
> >>     http://www.haskell.org/mailman/listinfo/ghc-devs
> >
> >
> >
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://www.haskell.org/mailman/listinfo/ghc-devs
> >
>
>
> --
> Adam Gundry, Haskell Consultant
> Well-Typed LLP, http://www.well-typed.com/
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140211/1754d1cd/attachment-0001.html>