GADT match fails to refine type variable

[dolio]

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.

[chak]

Works with the new solver.