#2219: GADT match fails to refine type variable
---------------------------------+------------------------------------------
Reporter: dolio | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 6.9 | Severity: normal
Keywords: gadt type family | Testcase:
Architecture: x86 | Os: Linux
---------------------------------+------------------------------------------
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}}}.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2219>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
