GADT match fails to refine type variable
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
.
Trac metadata
Trac field | Value |
---|---|
Version | 6.9 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |