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