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

[Nicolas Frisby]

Also, on the topic of patching GHC for domain-specific error messages, why
not add a simple means to emit a custom error message? It would beat
piggy-backing on the "no instance" messages as I currently plan to.

This seems safe and straight-forward:

> -- wired-in, cannot be instantiated
> class GHC.Exts.PrintError (msg :: Symbol) (args :: [k])

Consider the class C fromy previous email. It's possible these two
instances are now sufficient.

> instance C a b
> instance PrintError ("You used %1 on the left and %2 on the right!" ::
Symbol) [a,b] => C a b

And let's not forget warnings!

> -- wired-in, cannot be instantiated
> class GHC.Exts.PrintWarn (msg :: Symbol) (args :: '[k])

Thanks again.


On Thu, Jan 30, 2014 at 3:07 PM, Nicolas Frisby <nicolas.frisby at gmail.com>wrote:

> Hi all. I have a question for those savvy to the type-checker's internal
> workings.
>
> For uses of the following function, can anyone suggest a means of forcing
> GHC to attempt to solve C a b even if a~b fails?
>
> > dslAsTypeOf :: (C a b,a~b) => a -> b -> a
> > dslAsTypeOf x _ = x
> >
> > class C a b -- no methods
>
> Just for concreteness, the following are indicative of the variety of
> instances that I expect C to have. (I don't think this actually affects the
> question above.)
>
> > instance C DSLType1 DSLType1
> > instance C DSLType2 DSLType2
> > instance C x y => C (DSLType3 x) (DSLType3 y)
> >
> > instance IndicativeErrorMessage1 => C DSLType1 DSLType2
> > instance IndicativeErrorMessage2 => C DSLType2 (DSLType3 y)
> >
> > class IndicativeErrorMessage1 -- will never have instances
> > class IndicativeErrorMessage2 -- will never have instances
>
> Thank you for your time.
>
> ===================================
>
> Keep reading for the "short story", the "long story", and two ideas for a
> small GHC patch that would enable my technique outlined above.
>
> ===== short story =====
>
> The motivation of dslAsTypeOf is to provide improved error messages when a
> and b are not equal.
>
> Unfortunately, the user will never see IndicativeErrorMessage. It appears
> that GHC does not attempt to solve C a b if a~b fails. That's
> understandable, since the solution of C a b almost certainly depends on the
> "value" of its arguments...
>
> Hence, the question at the top of this email.
>
> ===== long story =====
>
> A lot of the modern type-level programming capabilities can be put to
> great use in creating type systems for embedded domain specific languages.
> These type systems can enforce some impressive properties.
>
> However, the error messages you get when one of those property is not
> satisfied can be pretty abysmal.
>
> In my particular case, I have a phantom type where the tag carries all the
> domain-specific information.
>
> > newtype U (tag :: [Info]) a = U a
>
> and I have an binary operation that requires the tag to be equivalent for
> all three types.
>
> > plus :: Num a => U tag a -> U tag a -> U tag a
> > plus (U x) (U y) = U $ x + y
>
> This effectively enforces the property I want for U values. Unfortunately,
> the error messages can seem dimwitted.
>
> > ill_typed = plus (U 1 :: U [Foo,Bar,Baz] Int)  (U 2 :: U [Foo,Baz] Int)
>
> The `ill_typed` value gives an error message (in GHC 7.8) saying
>
>   Bar : Baz : []      is not equal to       Baz : []
>
> (It's worse in GHC 7.4. I don't have access to a 7.6 at the moment.)
>
> I'd much rather have it say that "Bar is missing from the first summand's
> list." And I can define a class that effectively conveys that information
> in a "domain-specific error message" which is actually a "no instance of
> <IndicativeClassName> tag1 tag2" message.
>
> > friendlier_plus :: (FriendlyEqCheck tag1 tag2 tag3,Num a) => U tag1 a ->
> U tag2 a -> U tag3 a
>
> The `friendlier_plus' function gives useful error messages if tag1, tag2,
> and tag3 are all fully monomorphic.
>
> However, it does not support inference:
>
> > zero :: Num a => U tag a
> > zero = U 0
> >
> > x = U 4 :: U [Foo,Baz] Int
> >
> > -- both of these are ill-typed :(
> > should_work1 = (friendlier_plus zero x) `asTypeOf` x    -- tag1 is
> unconstrained
> > should_work2 = friendlier_plus x x     -- tag3 is unconstrained
>
> Neither of those terms type-check, since FriendlyEqCheck can't determine
> if the unconstrained `tag' variable is equal to the other tags.
>
> So, can we get the best of both worlds?
>
> > best_plus ::
> >   ( FriendlyEqCheck tag1 tag2 tag3
>      , tag1 ~ tag2, tag2 ~ tag3, Num a) => U tag1 a -> U tag2 a -> U tag3 a
>
> No, unfortunately not. Now the `should_work*' functions type-check, but an
> ill-typed use of `best_plus' gives the same poor error message that `plus'
> would give.
>
> Hence, the question at the top of this email.
>
> ===== two ideas =====
>
> If my question at the top of this email cannot be answered in the
> affirmative, perhaps a small patch to GHC would make this sort of approach
> a viable lightweight workaround for improving domain-specific error
> messages.
>
> (I cannot estimate how difficult this would be to implement in the
> type-checker.)
>
> Two alternative ideas.
>
> 1) An "ALWAYS_ATTEMPT" PRAGMA that you can place on the class C so that it
> is attempted even if a related ~ constraint fails.
>
> 2) An OrElse constraint former, offering *very* constrained back-tracking.
>
> > possibleAsTypeOf :: ((a ~ b) `OrElse` C a b) => a -> b -> a
> > possibleAsTypeOf x _ = x
>
> Requirements: C must have no superclasses, no methods, and no fundeps.
>
> Specification: If (a~b) fails and (C a b) is satisfiable, then the
> original inequality error message would be shown to the user. Else, C's
> error message is used.
>
> ===================================
>
> You made it to the bottom of the email! Thanks again.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140130/b2d31614/attachment-0001.html>