id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc	os	architecture	failure	difficulty	testcase	blockedby	blocking	related
2219	GADT match fails to refine type variable	dolio	chak	"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}}}."	bug	closed	normal	6.10 branch	Compiler (Type checker)	6.9	fixed	gadt type family		Linux	x86		Unknown	T2219