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