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

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 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/

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

Are we reaching the point where a wiki page and perhaps (soon) a Trac ticket would be appropriate? On Tue, Feb 11, 2014 at 10:10 AM, Nicolas Frisby wrote:

On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães wrote:

...

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

...

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 "." )

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. On Feb 11, 2014 12:15 PM, "Richard Eisenberg" 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 wrote:

On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães wrote:

...

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

...

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@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

If, when defining the `describeError' method, I wanted to refer to one of my library's classes from inside a pattern (or guard in the rhs, I suppose), how would I do that? Via a Template Haskell literal name? Or would I call the TcM interface for looking up a name? In my opinion [1], the TcM interface is too user-antagonistic, even for GHC power-users [2], and moreover would leak implementation details. I would prefer a more light-weight interface, dedicated to just domain-specific errors. That said, it seems that a general interface comparable to the one I have been hocking could be built atop what you two are proposing and subsequently marked {-# LANGUAGE Trustworthy #-}. Thumbs up. [1] - Disclaimer: I've already noted that I'm not familiar with the type-checker implementation. [2] - I consider myself a GHC power-user. On Tue, Feb 11, 2014 at 12:43 PM, Adam Gundry wrote:

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" mailto:eir@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 mailto:nicolas.frisby@gmail.com> wrote:

...

On Tue, Feb 11, 2014 at 3:55 AM, José Pedro Magalhães mailto:jpm@cs.uu.nl> wrote:

On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby mailto:nicolas.frisby@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@haskell.org mailto:ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs

_______________________________________________ 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

Though I favor the approach Adam wrote about (he and I discussed it before his post), I think these are very valid concerns, and would have to be taken into account in the design of any further work in this area. One observation I would make now is that none of this proposal, as far as I can tell, would change run-time behavior of any program. This proposal concerns only generation of error messages -- correct programs would not notice the feature. Now, you're right to be concerned about the possibility of DSL-specific error messages outside of the DSL! But, my hunch is that it would fairly well-managed, because the DSL-specific messages would be tied to the use of DSL constructs, which would not appear outside of DSL code. That defense is very hand-wavy, and we would want to be more sure that we don't "leak", but I'm not terribly worried about it right now. I will say that, for better or worse, GHC already has constructs that can affect runtime behavior unexpectedly, particularly {#- RULES #-}. Richard On Feb 19, 2014, at 8:25 AM, Jonathan Paugh wrote:

On 02/07/2014 03: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

Strictly from an API-design point of view, I think having __special__ functions that influence the compiler[0] is a __really__ __bad__ idea. (Think of __Python__, where even basic language constructs can be ruthlessly mangled.) How would these special functions behave? Using type classes *might* make that okay, but what to __avoid__ (IMO) is having the compiler treat objects/modules/etc differently based on whether certain values are defined. It leads to in-cohesiveness, and mal-comprehension.

Would you really want a module/function, etc to behave differently based on whether some value were in scope when it was defined? Even for something as benign as error messages? How would you limit the scope of your changes? Would a type class really cut it, especially with the way instances are propagated?

This kind of thinking might make more sense if modules were somehow first-class objects, with a reasonable interface for toying with them generally. (No comment on whether *that's* a good idea.)

...

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.

I'm not a type-foo master, but wouldn't it be hard to restrict the effects of a type class-based solution to strictly your own code? Wouldn't it be easy to have multiple, overlapping instances in various places? How would we keep from seeing DSL-specific error messages out of context?

Like I said, I can't talk about this from the perspective of an implementor, or even a library-designer who might use this feature; I'm merely a library-user who'd have to deal with it.

[0] I exclude TH, which has a well-defined separation from normal code. Perhaps one could cook up a good, well-defined API for this, too, but I have doubts...

Regards, Jonathan Paugh

...

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

On 30/01/14 21:09, Nicolas Frisby wrote:

...

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 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

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