On Tue, Feb 11, 2014 at 3:32 AM, Nicolas Frisby <nicolas.fri...@gmail.com>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" <a...@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.fri...@gmail.com <mailto:nicolas.fri...@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/ >> > > _______________________________________________ > 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