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

Nicolas Frisby nicolas.frisby at gmail.com
Tue Feb 11 03:32:15 UTC 2014


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

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" <adam at well-typed.com> 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
>
>
> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140210/89128fbc/attachment-0001.html>


More information about the ghc-devs mailing list