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