id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential,wikipage
1815,Occurs check error from equality constraint,guest,chak,"I was writing that manipulates witnesses for equality constraints,
and saw some occurs check errors for equations matching my constraints.
(This is with ghc-6.9.20071025).
{{{
Bug.hs:19:31:
Occurs check: cannot construct the infinite type: n = Sum Z n
In the pattern: Refl
In a case alternative: Refl -> Refl
In the expression: case zerol n of Refl -> Refl
}}}
Here is the program producing that error:
{{{
{-# OPTIONS -fglasgow-exts #-}
module Bug where
data Z
data S a
type family Sum n m
type instance Sum n Z = n
type instance Sum n (S m) = S (Sum n m)
data Nat n where
NZ :: Nat Z
NS :: (S n ~ sn) => Nat n -> Nat sn
data EQ a b = forall q . (a ~ b) => Refl
zerol :: Nat n -> EQ n (Sum Z n)
zerol NZ = Refl
zerol (NS n) = case zerol n of Refl -> Refl
}}}",bug,closed,normal,6.10 branch,Compiler (Type checker),6.9,fixed,,,Linux,x86,None/Unknown,indexed-types/should_compile/GADT11,,,,,