#1815: Occurs check error from equality constraint
--------------------------------------+-------------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler (Type checker) | Version: 6.9
Severity: normal | Keywords:
Difficulty: Unknown | Os: Linux
Testcase: | Architecture: x86
--------------------------------------+-------------------------------------
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
}}}
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1815>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
