Resolving overloading loops for circular constraint graph
Manuel, Simon, I've spotted a hopefully small but for us quite annoying bug in GHC's type checker: it loops when overloading resolving involves a circular constraint graph containing type-family applications. The following program (also attached) demonstrates the problem: {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-} type family F a :: * type instance F Int = (Int, ()) class C a instance C () instance (C (F a), C b) => C (a, b) f :: C (F a) => a -> Int f _ = 2 main :: IO () main = print (f (3 :: Int)) My guess is that the loop is caused by the constraint C (F Int) that arises from the use of f in main: C (F Int) = C (Int, ()) <= C (F Int) Indeed, overloading can be resolved successfully by "black-holing" the initial constraint, but it seems like the type checker refuses to do so. Can you confirm my findings? I'm not sure whether this is a known defect. If it isn't, I'd be more than happy to issue a report. Since this problem arises in a piece of very mission-critical code, I would be pleased to learn about any workarounds. Thanks in advance, Stefan
Your example must loop because as you show below
the instance declaration leads to a cycle.
By "black-holing" you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.
In any case, this is not a bug, you simply play with fire
once type functions show up in the instance context.
There are sufficient conditions to guarantee termination,
but they are fairly restrictive.
-Martin
2009/9/9 Stefan Holdermans
Manuel, Simon,
I've spotted a hopefully small but for us quite annoying bug in GHC's type checker: it loops when overloading resolving involves a circular constraint graph containing type-family applications.
The following program (also attached) demonstrates the problem:
{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-}
type family F a :: * type instance F Int = (Int, ())
class C a instance C () instance (C (F a), C b) => C (a, b)
f :: C (F a) => a -> Int f _ = 2
main :: IO () main = print (f (3 :: Int))
My guess is that the loop is caused by the constraint C (F Int) that arises from the use of f in main:
C (F Int) = C (Int, ()) <= C (F Int)
Indeed, overloading can be resolved successfully by "black-holing" the initial constraint, but it seems like the type checker refuses to do so.
Can you confirm my findings?
I'm not sure whether this is a known defect. If it isn't, I'd be more than happy to issue a report.
Since this problem arises in a piece of very mission-critical code, I would be pleased to learn about any workarounds.
Thanks in advance,
Stefan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Dear Martin,
Your example must loop because as you show below the instance declaration leads to a cycle.
By "black-holing" you probably mean co-induction. That is, if the statement to proven appears again, we assume it must hold. However, type classes are by default inductive, so there's no easy fix to offer to your problem.
Yes, I meant coinductive resolving of overloading. By that line of reasoning, the following should loop as well, but doesn't: {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE UndecidableInstances #-} class C a instance C () instance (C (a, ()), C b) => C (a, b) f :: C (a, ()) => a -> Int f _ = 2 main :: IO () main = print (f (3 :: Int)) Note: here I would accept looping behaviour as this program requires undecidable instances.
In any case, this is not a bug, you simply play with fire once type functions show up in the instance context. There are sufficient conditions to guarantee termination, but they are fairly restrictive.
I disagree: it is a bug. I think the original program should require undecidable instances as well: indeed, the presence of the type family makes that the constraint is possibly no smaller than the instance head. However, without the undecidable-instance requirement (i.e., as it is now), I expect type checking to terminate. Cheers, Stefan
Dear Martin,
By "black-holing" you probably mean co-induction. That is, if the statement to proven appears again, we assume it must hold. However, type classes are by default inductive, so there's no easy fix to offer to your problem.
A propos: are there fundamental objections to coinductive resolving, i.e., constructing recursive dictionaries. I suppose termination is hard to guarantee then: is it enough to require constraints to be productive w.r.t. instance heads? Cheers, Stefan
2009/9/9 Stefan Holdermans
Dear Martin,
By "black-holing" you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold. However, type classes are by default inductive, so there's no easy fix to offer to your problem.
A propos: are there fundamental objections to coinductive resolving, i.e., constructing recursive dictionaries. I suppose termination is hard to guarantee then: is it enough to require constraints to be productive w.r.t. instance heads?
Yes, you need instances to be productive, otherwise, you get bogus cyclic proofs like instance Foo a => Foo a dictFooa = dictFooa You could call this a bug, or simply blame the programmer for writing down a 'bogus' instance. Under co-inductive type class solving more (type class) programs will terminate (my guess). Here are some references: Satish R. Thatte: Semantics of Type Classes Revisited. LISP and Functional Programming 1994http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94: 208-219 As far as I know, the first paper which talks about co-induction and type classes. I myself and some co-workers explored this idea further in some unpublished draft: AUTHOR = {M. Sulzmann and J. Wazny and P. J. Stuckey}, TITLE = {Co-induction and Type Improvement in Type Class Proofs}, NOTE = {Manuscript}, YEAR = {2005}, MONTH = {July}, PS = {http://www.cs.mu.oz.au/~sulzmann/manuscript/coind-type-class-proofs.ps http://www.cs.mu.oz.au/%7Esulzmann/manuscript/coind-type-class-proofs.ps} I'm quite fond of co-induction because it's such an elegant and powerful proof technique. However, GHC's co-induction mechanism is fairly limited, see Simon's reply, so I'm also curious to see what's happening in the future. -Martin
Stefan You are trying to do something quite delicate here. The whole idea of solving constraints in a co-inductive way (building a recursive group of dictionary definitions) relies on spotting something we've seen before to "tie the knot". To date, the main application I knew for this fairly exotic idea was described in the SYB3 paper [1]. So I'm curious about your application (and that of anyone else) that relies on this recursive-dictionary-solving mechanism. Returning to your problem, this "loop spotting" mechanism is rather syntactic at the moment, whereas your application needs something more refined, involving equality modulo type function reductions. Alas, the constraint solving machinery for type classes and for type functions is not properly integrated. I'm amazed it works as well as it does, actually. We [Manuel, Dimitrios, and I] are (slowly, slowly) working on a complete rewrite of GHC's constraint-solving mechanism. I'm pretty sure that it'll solve this problem among many others. But don't hold your breath. It'll be months not weeks. But not years! sorry not to be able to solve your problem sooner. I'll open a ticket. Simon [1] http://research.microsoft.com/~simonpj/papers/hmap | -----Original Message----- | From: Stefan Holdermans [mailto:stefan@cs.uu.nl] | Sent: 09 September 2009 14:38 | To: Manuel M T Chakravarty; Simon Peyton-Jones | Cc: glasgow-haskell-users; haskell-cafe; José Pedro Magalhães; Thomas van Noort; | Johan Jeuring | Subject: Resolving overloading loops for circular constraint graph | | Manuel, Simon, | | I've spotted a hopefully small but for us quite annoying bug in GHC's | type checker: it loops when overloading resolving involves a circular | constraint graph containing type-family applications. | | The following program (also attached) demonstrates the problem: | | {-# LANGUAGE FlexibleContexts #-} | {-# LANGUAGE TypeFamilies #-} | | type family F a :: * | type instance F Int = (Int, ()) | | class C a | instance C () | instance (C (F a), C b) => C (a, b) | | f :: C (F a) => a -> Int | f _ = 2 | | main :: IO () | main = print (f (3 :: Int)) | | My guess is that the loop is caused by the constraint C (F Int) that | arises from the use of f in main: | | C (F Int) = C (Int, ()) <= C (F Int) | | Indeed, overloading can be resolved successfully by "black-holing" the | initial constraint, but it seems like the type checker refuses to do so. | | Can you confirm my findings? | | I'm not sure whether this is a known defect. If it isn't, I'd be more | than happy to issue a report. | | Since this problem arises in a piece of very mission-critical code, I | would be pleased to learn about any workarounds. | | Thanks in advance, | | Stefan
participants (3)
-
Martin Sulzmann -
Simon Peyton-Jones -
Stefan Holdermans