GADT match fails to refine type variable

The following code is accepted by the type checker in 6.8.2, but is rejected by a HEAD build, 6.9.20080411:

{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators #-}

data Zero
data Succ a

data FZ
data FS fn

data Fin n fn where
  FZ :: Fin (Succ n) FZ
  FS :: Fin n fn -> Fin (Succ n) (FS fn)

data Nil
data a ::: b

type family Lookup ts fn :: *
type instance Lookup (t ::: ts) FZ = t
type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn

data Tuple n ts where
  Nil   :: Tuple Zero Nil
  (:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)

proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
proj FZ      (v ::: _)  = v
proj (FS fn) (_ ::: vs) = proj fn vs

The error in question is:

Bug.hs:25:16:
    Occurs check: cannot construct the infinite type:
      t = Lookup (t ::: ts) fn
    In the pattern: v ::: _
    In the definition of `proj': proj FZ (v ::: _) = v

Which seems to indicate that the pattern match against FZ in the first case is failing to refine the type variable fn to FZ. Reversing the order of the cases yields the same error, so either the match against FS is working correctly, or the type checker thinks that it can solve Lookup (t ::: ts) fn ~ Lookup ts fn.

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
Architecture