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