Bug in undecidable instances?

[Simon Peyton-Jones]

You are misunderstanding what 'undecidable instances' does.

GHC wants to solve the constraint (D Foo beta) where beta is as-yet-unconstrained type variable.  It finds that one instance *matches* (by instantiating only the instance declaration, not the constraint we are solving):
	D a b
but another instance *unifies*:
	D Foo Foo
(That is, if 'beta' was later discovered to be 'Foo' then this latter instance would match.)  

Without undecidable instances, GHC will refrain from choosing either.  With undecidable instances, GHC chooses the one that matches (ie D a b) ignoring the possiblity that beta might later instantiate to Foo.

You want to unify beta with Foo, but that wouldn't work if there was another instances
	D Foo Bar

That's the design at the moment.  If you are in undecidable-instance territory the ice is pretty thin.

Simon

| -----Original Message-----
| From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
| users-bounces at haskell.org] On Behalf Of Roman Cheplyaka
| Sent: 31 January 2011 22:01
| To: glasgow-haskell-users at haskell.org
| Subject: Bug in undecidable instances?
| 
| The following looks like a bug in (undecidable) instances resolution.
| 
|     {-# LANGUAGE
| MultiParamTypeClasses,FlexibleInstances,UndecidableInstances,
|                  OverlappingInstances,IncoherentInstances #-}
|     class C a b
| 
|     instance C a (a,b)
| 
|     class D a b
| 
|     instance (D a b, C b c) => D a c
| 
|     data Foo = Foo deriving Show
|     data Bar = Bar deriving Show
| 
|     instance D Foo Foo
| 
|     c :: C x y => x -> y -> ()
|     c _ _ = ()
| 
|     d :: D x y => x -> y -> ()
|     d _ _ = ()
| 
| 
| *Main> d Foo Foo
| () -- as expected
| *Main> c Foo (Foo,Bar)
| () -- as expected
| *Main> d Foo (Foo,Bar)
| 
| <interactive>:1:1:
|     Context reduction stack overflow; size = 21
|     Use -fcontext-stack=N to increase stack size to N
|       [skip]
|       $dD :: D Foo b1
|       $dD :: D Foo b
|       $dD :: D Foo (Foo, Bar)
|     In the expression: d Foo (Foo, Bar)
|     In an equation for `it': it = d Foo (Foo, Bar)
| 
| I.e. for some reason on the second step resolver fails to pick up the
| most specific (and the most obvious) instance D Foo Foo and continues to
| apply the instance (D a b, C b c) => D a c.
| 
| Reproduced with GHC 6.12.1 and 7.0.1.
| 
| --
| Roman I. Cheplyaka :: http://ro-che.info/
| Don't worry what people think, they don't do it very often.
| 
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users