[Haskell] Non-terminating compilation of non-positive construction.

[Stefan Karrmann]

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