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

Wed Feb 19 13:25:10 UTC 2014

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
>> <nicolas.frisby at gmail.com <mailto: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.
>>
>>
>>
>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://www.haskell.org/mailman/listinfo/ghc-devs
>>
> 
> 