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

[Adam Gundry]

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


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