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

Tue Feb 11 18:43:54 UTC 2014

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/