Lazy evaluation of type families causes quantified type variables to escape
This may be related to tickets #3005 (closed) and #3297 (closed).
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.
Trac metadata
Trac field | Value |
---|---|
Version | 6.12.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |