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 |