It's a documented bug in GHC. http://www.haskell.org/ghc/docs/latest/html/users_guide/bugs.html#BUGS-G HC Simon | -----Original Message----- | From: haskell-bounces@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Stefan | Karrmann | Sent: 05 September 2004 13:57 | To: haskell@haskell.org | Subject: [Haskell] Non-terminating compilation of non-positive construction. | | Hi, | | in Coq (cf. <http://pauillac.inria.fr/coq/coq1-eng.html>) inductive and | coinductive (aka lazy) types are restricted by the positivity condition | (cf. <http://pauillac.inria.fr/coq/doc8/Reference-Manual006.html#htoc91>). | | My first try to violate this condition in Haskell is: | --------------------------------------------------- | module Limits (module Limits) where | | import qualified Prelude$ | $ | data False = False !False | deriving (Prelude.Show) | -- Approximation of: data False = {- no Value -} | -- The lazy variant has the same result. | -- Of course there is: f = False f | | data Non_positive = Non_pos (Non_positive -> False) | | app :: Non_positive -> Non_positive -> False | app f x = case f of | Non_pos h -> h x | | delta :: Non_positive | delta = Non_pos (\ x -> app x x) | | -- Up to this definition ghc terminates. | | -- (\x -> x x) (\x -> x x) | loop :: False | loop = app delta delta | ---------------------------------------------------- | | The compilation by the Glorious Glasgow Haskell Compilation System, | version 6.2, loops on this small module. IMHO only the execution should | loop or non positive constructions should be excluded. | | Is it a bug or is non positivity too dangerous? | | Sincerly, | -- | Stefan Karrmann | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell