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

[Nicolas Frisby]

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/fb52363e/attachment.html>