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. On Feb 11, 2014 12:15 PM, "Richard Eisenberg" <[email protected]> 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 <[email protected]> > wrote: > > On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães <[email protected]>wrote: > >> On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <[email protected] >> > 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 > [email protected] > http://www.haskell.org/mailman/listinfo/ghc-devs > > >
_______________________________________________ ghc-devs mailing list [email protected] http://www.haskell.org/mailman/listinfo/ghc-devs
