#1783: FD leads to non-termination of type checker
--------------------------------------+-------------------------------------
Reporter: chak | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.9
Severity: normal | Keywords:
Difficulty: Unknown | Os: Unknown
Testcase: | Architecture: Unknown
--------------------------------------+-------------------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1783>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
