id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential
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,,T2219,,,,