FD leads to non-termination of type checker

Here another program that causes the type checker to diverge:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE PatternSignatures, ScopedTypeVariables, FlexibleContexts #-}

module ShouldCompile where

import Prelude hiding (foldr, foldr1)

import Data.Maybe

class Elem a e | a -> e

class Foldable a where
  foldr :: Elem a e => (e -> b -> b) -> b -> a -> b

--  foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e  -- WORKS!
  foldr1 :: Elem a e => (e -> e -> e) -> a -> e
  foldr1 f xs = fromMaybe (error "foldr1: empty structure")
                  (foldr mf Nothing xs)
     where mf :: Elem a e => (e -> Maybe e -> Maybe e)
           mf x Nothing  = Just x
           mf x (Just y) = Just (f x y)

This is the FD version of #1776 (closed). If we use lexically scoped type variables - i.e., the signature marked with "WORKS!" - everything is fine. However, we shouldn't have to use the scoped type variable as the FD rule should combine the Elem a e constraints in the two signatures to establish that the e in foldr1's signature is the same as the e in mf's signature.

In contrast to #1781 (closed), there doesn't seem to be an equality constraint involved in this example.

Trac metadata

Trac field	Value
Version	6.9
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system	Unknown
Architecture	Unknown