#4178: Lazy evaluation of type families causes quantified type variables to
escape
---------------------------------+------------------------------------------
Reporter: intoverflow | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
Version: 6.12.1 | Keywords:
Os: Unknown/Multiple | Testcase:
Architecture: Unknown/Multiple | Failure: GHC rejects valid program
---------------------------------+------------------------------------------
This may be related to tickets #3005 and #3297.
Consider the following function, which is idiomatic for using rank-2 types
to prevent data from escaping a context:
{{{
useRank2 :: (forall a . a -> b) -> b
useRank2 f = f "foo"
}}}
If {{{b}}} is unified to a type function that makes mention of {{{a}}},
the compiler will reject the program for allowing a quantified type
variable to escape, even in circumstances where evaluating the type
function would yield a type that does not mention {{{a}}}.
Here is complete source for demonstrating the issue:
{{{
{-# LANGUAGE
FlexibleContexts,
Rank2Types,
TypeFamilies,
MultiParamTypeClasses,
FlexibleInstances #-}
data True = T
data False = F
class Decide tf a b where
type If tf a b
nonFunctionalIf :: tf -> a -> b -> If tf a b
instance Decide True a b where
type If True a b = a
nonFunctionalIf T a b = a
instance Decide False a b where
type If False a b = b
nonFunctionalIf F a b = b
useRank2 :: (forall a . a -> b) -> b
useRank2 f = f "foo"
hasTrouble a = nonFunctionalIf F a (2 :: Int)
-- try useRank2 hasTrouble
hasNoTrouble :: a -> Int
hasNoTrouble = hasTrouble
-- try useRank2 hasNoTrouble
}}}
Certainly the program should be rejected when there is inadequate
information to evaluate the type function, but it seems odd to reject
{{{hasTrouble}}} and not {{{hasNoTrouble}}} given that they are equal.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/4178>
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
