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,,,