workaround to get both domain-specific errors and also multi-modal type inference?
nicolas.frisby at gmail.com
Tue Feb 11 18:24:21 UTC 2014
Thanks for suggesting that; I was only seeing Constraint as in
I think the gist of my previous concerns doesn't change, though: open type
pattern matching (or some dissatisfying approx of), assuredly pure
On Feb 11, 2014 12:15 PM, "Richard Eisenberg" <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!
> On Feb 11, 2014, at 11:10 AM, Nicolas Frisby <nicolas.frisby at gmail.com>
> 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
> 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 `
> > -- 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the ghc-devs