[GHC] #3018: Constraints of function in record appears to nullifiy instance constraints.

[GHC]

#3018: Constraints of function in record appears to nullifiy instance constraints.
---------------------------------+------------------------------------------
    Reporter:  ben.kavanagh      |        Owner:  simonpj         
        Type:  bug               |       Status:  new             
    Priority:  normal            |    Milestone:  _|_             
   Component:  Compiler          |      Version:  6.10.1          
    Severity:  normal            |   Resolution:                  
    Keywords:                    |   Difficulty:  Unknown         
    Testcase:                    |           Os:  Unknown/Multiple
Architecture:  Unknown/Multiple  |  
---------------------------------+------------------------------------------
Changes (by simonpj):

  * owner:  => simonpj
  * difficulty:  => Unknown
  * milestone:  => _|_

Comment:

 Here are the key lines of code:
 {{{
 class Subst a t t' where
     subst :: (Monad m) => a -> t -> t' -> m t'

 data SubstD a t t'
   = SubstD (forall m. Monad m => a -> t -> t' -> m t')

 instance Data (SubstD a t) t' => Subst a t t'          -- (1)

 instance Subst a t t' => Sat (SubstD a t t') where     -- (2)
     dict = SubstD subst
 }}}
 The call to 'subst' on the last line gives rise to a constraint
 `(Subst a t t')`.  But that constraint can be satisfied in '''two
 different ways''':
  1. Using the instance declaration for `Subst` (which matches
 ''anything''!)
  2. Using the context of the `Sat (SubstD ..)` instance declaration itself

 If GHC uses (1) it gets into a corner it can't get out of, because now
 it needs `(Data (SubstD a t) t')`, and that it can't get.  The error
 message
 is a bit misleading:
 {{{
 T3018.hs:29:28:
     Could not deduce (Data (SubstD a t) t') from the context (Monad m)
       arising from a use of `subst' at T3018.hs:29:28-32
 }}}
 it should really say
 {{{
  ...from the context (Subst a t t', Monad m)
 }}}
 but that's a bit of a separate matter.

 Now, you are hoping that (2) will happen, but I hope you can see that it's
 delicate.
 Adding the `(Monad m)` context just tips things over the edge so
 that GHC doesn't "see"
 the `(Subst a t t')` in the context until too late.  But the real problem
 is
 that you are asking too much.  Here is a simpler example:
 {{{
 f :: Eq [a] => a -> blah
 f x = let g :: Int -> Int
           g = ....([x]==[x])...
       in ...
 }}}
 The use of `==` requires `Eq [a]`, but GHC will probably use the list
 equality
 instance to simplify this to `Eq a`; and then it can't deduce `Eq a` from
 `Eq [a]`.
 Local constraints that shadow or override global instance declarations are
 extremely delicate.

 All this is perhaps soluble if GHC were to be lazier about solving
 constraints,
 and only makes the attempt when it has all the evidence in hand.  I'm
 thinking
 quite a bit about constraint solving at the moment and will bear that in
 mind.
 But I can't offer you an immediate solution. At least I hope I've
 explained the
 problem.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3018#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler