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.