id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,difficulty,testcase,blockedby,blocking,related
1783,FD leads to non-termination of type checker,chak,,"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.  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, there doesn't seem to be an equality constraint involved in this example.",bug,closed,normal,,Compiler (Type checker),6.9,fixed,,,Unknown/Multiple,Unknown/Multiple,,Unknown,FD2,,,