#1118: Type check loop on impredicativaty + GADT mix
-------------------------+--------------------------------------------------
Reporter: japple | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 6.6
Severity: normal | Keywords: impredicativity, GADTs
Difficulty: Unknown | Testcase:
Architecture: x86 | Os: Linux
-------------------------+--------------------------------------------------
The type checker runs out of stack space on checking {{{compose}}}, but
not {{{compose'}}} or {{{composeS}}}
{{{
{-# OPTIONS_GHC -fglasgow-exts #-}
module Compose where
data Z
data S n
data List n a where
Nil :: List Z a
(:-) :: a -> List n a -> List (S n) a
data Hold a = Hold (forall m . a m -> a (S m))
compose' :: List n (Hold a) -> a (S Z) -> a (S n)
compose' Nil x = x
compose' ((Hold f) :- fs) x = f (compose' fs x)
compose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)
compose Nil x = x
compose (f :- fs) x = f (compose fs x)
composeS :: [forall m . a m -> a m] -> a n -> a n
composeS [] x = x
composeS (f:fs) x = f (composeS fs x)
}}}
--
Ticket URL: <http://cvs.haskell.org/trac/ghc/ticket/1118>
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
