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

On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby wrote:

Hi Adam. Thanks very much for the response. I'm sorry if the rest of this reads negatively -- I'm on my phone and hence perhaps curt. I'm excited about any dialog here!

(I'll mention that Dimitrios Vytiniotis and Geoffrey Mainland had expressed low priority interest in these topics about a year ago.)

I agree that this is a difficult problem. I think the eventual solution deserves far more attention than I can currently allocate. Hence, I was hoping for a workaround "trick" in the mean time.

It seems to me that such a trick is currently unlikely. So I proposed a light-weight limited-scope patch. Something along the lines of "don't let perfect be the enemy of good."

My main concern with the interface you sketched is how we would pattern match on the demoted Constraint, since Constraint is an open kind. Also, there's unsafePerformIO et al to somehow preclude. The interface does look nicer that way, but it would be simpler to stick to type-level computation, where no "exotic" new mechanisms would be needed.

Maybe there's a middle ground.

...

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?... Cheers, Pedro

GHC would report the result of this family for any unsatisfied constraint that has a matching instance that returns Just msg.

Perhaps GHC even first replaces skolem type variables with an application of GHC.Exts.Skolem :: Symbol -> k -> k before checking for instances.

Of course, the Symbol operations are rather anemic at the moment, but I think improvements there would be valuable as well. Or perhaps Message could yield a type-level Doc data kind that GHC interprets to build a String.

Lastly, I think custom constraint solving sounds like a very delicate language extension, with wide reaching consequences. Unless there's a strong champion dedicated to extensible custom constraint solving, I hope the much more modestly scoped issue of custom error messages can be considered separately for at least one design iteration. I feel like a near-term implementation is more likely that way.

Thanks again for this conversation! On Feb 7, 2014 2:05 PM, "Adam Gundry" wrote:

...

Hi,

Good error messages are a hard problem. That said, I think little tweaks like this might make sense. Richard Eisenberg and I were discussing this earlier, and we wondered if the following might provide an alternative approach:

Suppose a module provides a function

describeError :: Constraint -> Maybe String

(exact type up for discussion). This could be called by the typechecker when reporting errors in other modules, to provide a domain-specific error message. Do you think this might work for your use case?

We need to think about how to mark this function as special: one option is to provide a built-in typeclass like

class TypeCheckerPlugin a where describeError :: Constraint -> Maybe String

and look for instances of this class. Interestingly, the class type is irrelevant here; we're not interested in solving constraints involving this class, just looking at the imported instances when running the typechecker. Perhaps using a pragma might be more principled.

This came up in the context of a more general discussion of plugins to extend the typechecker. For example, we might consider doing something similar to *solve* constraints in a domain-specific way, as well as reporting errors.

Sound plausible?

Adam

...

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 mailto:nicolas.frisby@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

On 30/01/14 21:09, Nicolas Frisby wrote: 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.

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs