Typechecking regression

[igloo]

7.0.1 accepts this module (cut down from hashed-storage-0.5.4):

{-# LANGUAGE UndecidableInstances,
             MultiParamTypeClasses,
             KindSignatures,
             FlexibleInstances,
             FunctionalDependencies #-}

module Storage.Hashed.Monad () where

class Monad m => TreeRO m where
    withDirectory :: (MonadError e m) => Int -> m a -> m a
    expandTo :: (MonadError e m) => Int -> m Int

instance (Monad m, MonadError e m) => TreeRO (M m) where
    expandTo = undefined
    withDirectory dir _ = do
      _ <- expandTo dir
      undefined

data M (m :: * -> *) a

instance Monad m => Monad (M m) where
    (>>=) = undefined
    return = undefined

instance MonadError e m => MonadError e (M m)

class Monad m => MonadError e m | m -> e

but 7.0 branch says:

[1 of 1] Compiling Storage.Hashed.Monad ( Storage/Hashed/Monad.hs, interpreted )

Storage/Hashed/Monad.hs:17:12:
    Could not deduce (MonadError e1 m) arising from a use of `expandTo'
    from the context (Monad m, MonadError e m)
      bound by the instance declaration
      at Storage/Hashed/Monad.hs:14:10-50
    or from (MonadError e1 (M m))
      bound by the type signature for
                 withDirectory :: MonadError e1 (M m) => Int -> M m a -> M m a
      at Storage/Hashed/Monad.hs:(16,5)-(18,15)
    Possible fix:
      add (MonadError e1 m) to the context of
        the type signature for
          withDirectory :: MonadError e1 (M m) => Int -> M m a -> M m a
        or the instance declaration
    In a stmt of a 'do' expression: _ <- expandTo dir
    In the expression:
      do { _ <- expandTo dir;
           undefined }
    In an equation for `withDirectory':
        withDirectory dir _
          = do { _ <- expandTo dir;
                 undefined }
Failed, modules loaded: none.

[igloo]

queuelike 1.0.9 fails in a similar looking way.

[dimitris]

OK I think I see what's going on. We get a given from the instance

     [Given] MonadError e1 m       (e1 is a skolem)

And an implication from the definition of withDirectory:

     MonadError e2 (M m) =>  [Wanted] MonadError $e (M m)  
             ($e is a unification var)

Now, if we first improve $e ~ e2 then we will unify $e := e2, and then we will apply the top-level instance declaration which will then leave us with an unsolvable goal:

     [Wanted] MonadError e2 m 

If instead we first apply the top-level instance, we are left with a simpler

     [Wanted] MonadError $e m 

which will improve with the outer given and become solvable!

But it is not at all clear to me that one strategy is better than the other in general ... It just seems wrong that the two *given* skolems e1 and e2 are not equal, but fundeps have no way to express that. If the fundeps were encoded with equality superclasses we'd be just fine because we would get that e1 ~ e2 I believe.

Anyway, a quick (perhaps non-functional) solution is to remove the class context from the definition of withDirectory ...

[simonpj]

working on this... but not till Monday or Tuesday.

Simon

[simonpj]

Fixed by

Thu Feb 17 14:09:21 GMT 2011  simonpj@microsoft.com
  * Use "on the spot" solving for fundeps
  
  When we spot an equality arising from a functional dependency,
  we now use that equality (a "wanted") to rewrite the work-item
  constraint right away.  This avoids two dangers
  
   Danger 1: If we send the original constraint on down the pipeline
             it may react with an instance declaration, and in delicate
  	   situations (when a Given overlaps with an instance) that
  	   may produce new insoluble goals: see Trac #4952
  
   Danger 2: If we don't rewrite the constraint, it may re-react
             with the same thing later, and produce the same equality
             again --> termination worries.
  
  To achieve this required some refactoring of FunDeps.lhs (nicer
  now!).  
  
  This patch also contains a couple of unrelated improvements
  
  * A bad bug in TcSMonad.nestImplicTcS whereby the Tcs tyvars
    of an outer implication were not untouchable inside
  
  * Improved logging machinery for the type constraint solver;
    use -ddump-cs-trace (probably with a wider default line width
    -dppr-cols=200 or something)

    M ./compiler/main/DynFlags.hs +2
    M ./compiler/typecheck/TcCanonical.lhs -2 +76
    M ./compiler/typecheck/TcInteract.lhs -134 +199
    M ./compiler/typecheck/TcRnTypes.lhs -4 +3
    M ./compiler/typecheck/TcSMonad.lhs -70 +44
    M ./compiler/types/FunDeps.lhs -116 +173

Simon

[igloo]

Merged.