Attached file causes stack overflow

[jgbailey@…]

The code below is from the paper "Functional Pearl: Implicit Configurations" found at  http://www.cs.rutgers.edu/~ccshan/prepose/prepose.lhs. When compiled with GHC 6.7.20070816 on Windows XP using:

  ghc --make implicit_config.hs

A stack overflow results.

---

{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Prepose where

import System.IO.Unsafe       (unsafePerformIO)
import Control.Exception      (handle, handleJust, errorCalls)
import Foreign.Marshal.Utils  (with, new)
import Foreign.Marshal.Array  (peekArray, pokeArray)
import Foreign.Marshal.Alloc  (alloca)
import Foreign.Ptr            (Ptr, castPtr)
import Foreign.Storable       (Storable(sizeOf, peek))
import Foreign.C.Types        (CChar)
import Foreign.StablePtr      (StablePtr, newStablePtr,
                               deRefStablePtr, freeStablePtr)
import Data.Bits              (Bits(..))
import Prelude hiding         (getLine)
newtype Modulus s a  =  Modulus a  deriving (Eq, Show)
newtype M s a        =  M a        deriving (Eq, Show)

add  ::  Integral a => Modulus s a -> M s a -> M s a -> M s a
add (Modulus m) (M a) (M b)  =  M (mod (a + b) m)

mul  ::  Integral a => Modulus s a -> M s a -> M s a -> M s a
mul (Modulus m) (M a) (M b)  =  M (mod (a * b) m)
unM :: M s a -> a
unM (M a) = a
data AnyModulus a = forall s. AnyModulus (Modulus s a)

makeModulus :: a -> AnyModulus a
makeModulus a = AnyModulus (Modulus a)
withModulus'' :: a -> (forall s. Modulus s a -> w) -> w
withModulus'' m k = k (Modulus m)
__ = __

class Modular s a | s -> a where modulus :: s -> a

normalize :: forall s a. (Modular s a, Integral a) => a -> M s a
normalize a = M (mod a (modulus (__ :: s))) :: M s a

instance (Modular s a, Integral a) => Num (M s a) where
  M a + M b      =  normalize (a + b)
  M a - M b      =  normalize (a - b)
  M a * M b      =  normalize (a * b)
  negate (M a)   =  normalize (negate a)
  fromInteger i  =  normalize (fromInteger i)
  signum         =  error "Modular numbers are not signed"
  abs            =  error "Modular numbers are not signed"

withModulus :: a -> (forall s. Modular s a => s -> w) -> w
data Zero; data Twice s; data Succ s; data Pred s
class NumNat a
instance NumNat (Succ Zero)
instance NumNat  a => NumNat (Succ (Twice a))
instance NumNat  a => NumNat (Twice a)
class NumGood a
instance NumGood Zero
instance NumGood (Succ Zero)
instance NumNat a => NumGood (Succ (Twice a))
instance NumNat a => NumGood (Twice a)
instance NumNat a => NumGood (Pred a)
test_num:: NumGood a => a -> (); test_num _ = ()

data Positive s; data Negative s; data TwiceSucc s

class ReflectUnsigned s where reflectUnsigned :: Num a => s -> a
instance                        ReflectUnsigned Zero where
  reflectUnsigned _  =  0
instance ReflectUnsigned s  =>  ReflectUnsigned (Twice s) where
  reflectUnsigned _  =  reflectUnsigned (__ :: s) * 2
instance ReflectUnsigned s  =>  ReflectUnsigned (TwiceSucc s) where
  reflectUnsigned _  =  reflectUnsigned (__ :: s) * 2 + 1

instance ReflectUnsigned s  =>  ReflectNum (Positive s) where
  reflectNum _       =  reflectUnsigned (__ :: s)
instance ReflectUnsigned s  =>  ReflectNum (Negative s) where
  reflectNum _       =  -1 - reflectUnsigned (__ :: s)
class ReflectNum s where reflectNum :: Num a => s -> a
instance                   ReflectNum Zero where
  reflectNum _  =  0
instance ReflectNum s  =>  ReflectNum (Twice s) where
  reflectNum _  =  reflectNum (__ :: s) * 2
instance ReflectNum s  =>  ReflectNum (Succ s) where
  reflectNum _  =  reflectNum (__ :: s) + 1
instance ReflectNum s  =>  ReflectNum (Pred s) where
  reflectNum _  =  reflectNum (__ :: s) - 1
reifyIntegral  ::  Integral a =>
                     a -> (forall s. ReflectNum s => s -> w) -> w
reifyIntegral i k = case quotRem i 2 of
  (0,   0) -> k (__ :: Zero)
  (j,   0) -> reifyIntegral j (\(_ :: s) -> k (__ :: Twice s))
  (j,   1) -> reifyIntegral j (\(_ :: s) -> k (__ :: Succ (Twice s)))
  (j,-  1) -> reifyIntegral j (\(_ :: s) -> k (__ :: Pred (Twice s)))
data ModulusNum s a

instance  (ReflectNum s, Num a) =>
            Modular (ModulusNum s a) a where
  modulus _ = reflectNum (__ :: s)
withIntegralModulus  ::  Integral a =>
                         a -> (forall s. Modular s a => s -> w) -> w
withIntegralModulus i k =
  reifyIntegral i (\(_ :: s) -> k (__ :: ModulusNum s a))
data Nil; data Cons s ss

class ReflectNums ss where reflectNums :: Num a => ss -> [a]
instance  ReflectNums Nil where
  reflectNums _ = []
instance  (ReflectNum s, ReflectNums ss) =>
            ReflectNums (Cons s ss) where
  reflectNums _ = reflectNum (__ :: s) : reflectNums (__ :: ss)

reifyIntegrals  ::  Integral a =>
                      [a] -> (forall ss. ReflectNums ss => ss -> w) -> w
reifyIntegrals []      k  =  k (__ :: Nil)
reifyIntegrals (i:ii)  k  =  reifyIntegral i (\(_ :: s) ->
                               reifyIntegrals ii (\(_ :: ss) ->
                                 k (__ :: Cons s ss)))
type Byte   = CChar

data Store s a

class ReflectStorable s where
  reflectStorable :: Storable a => s a -> a
instance ReflectNums s => ReflectStorable (Store s) where
  reflectStorable _  =  unsafePerformIO
                     $  alloca
                     $  \p -> do  pokeArray (castPtr p) bytes
                                  peek p
    where bytes  =  reflectNums (__ :: s) :: [Byte]

reifyStorable  ::  Storable a =>
                      a -> (forall s. ReflectStorable s => s a -> w) -> w
reifyStorable a k =
  reifyIntegrals (bytes :: [Byte]) (\(_ :: s) -> k (__ :: Store s a))
    where bytes  =  unsafePerformIO
                 $  with a (peekArray (sizeOf a) . castPtr)
class Reflect s a | s -> a where reflect :: s -> a

data Stable (s :: * -> *) a

instance ReflectStorable s => Reflect (Stable s a) a where
  reflect  =   unsafePerformIO
           $   do  a <- deRefStablePtr p
                   return (const a)
    where p = reflectStorable (__ :: s p)

reify :: forall a w. a -> (forall s. Reflect s a => s -> w) -> w
reify a k  =  unsafePerformIO
                  $  do  p <- newStablePtr a
                         reifyStorable p foo
    where k' s = return (k s)
          -- foo :: ReflectStorable s => s a -> (s a -> w) -> w
          foo :: (forall s1. ReflectStorable s1 => s1 (StablePtr a) -> IO w)
          foo _ = k' (__ :: Stable s1 a)
          
data ModulusAny s

instance Reflect s a => Modular (ModulusAny s) a where
  modulus _ = reflect (__ :: s)

withModulus a k = reify a (\(_ :: s) -> k (__ :: ModulusAny s))
withIntegralModulus'  ::  forall a w. Integral a =>
                          a -> (forall s. Modular s a => M s w) -> w
withIntegralModulus' (i::a) k {- :: w -} =
  reifyIntegral i (  \(_ :: t) ->
                       unM (k :: M (ModulusNum t a) w))

test4'  ::  (Modular s a, Integral a) => M s a
test4'  =   3*3 + 5*5
		       
test4   =   withIntegralModulus' 4 test4'
data Even p q u v a = E a a deriving (Eq, Show)
normalizeEven :: forall p q a u v. (ReflectNum p, ReflectNum q, Integral a,
                      Bits a) => a -> a -> Even p q u v a
normalizeEven a b {- :: Even p q u v a -} =
  E  (a .&. (shiftL 1 (reflectNum (__ :: p)) - 1))   -- $a \bmod 2^p$
     (mod b (reflectNum (__ :: q)))                  -- $b \bmod q$

instance (  ReflectNum p, ReflectNum q,
            ReflectNum u, ReflectNum v,
            Integral a, Bits a) => Num (Even p q u v a) where
    E a1 b1  +   E a2 b2  =  normalizeEven  (a1  +  a2)  (b1  +  b2)
                          {-"\raisebox{0pt}[2.5ex][0pt]{$\vdots$}"-}
    E a1 b1  -   E a2 b2  =  normalizeEven  (a1  -  a2)  (b1  -  b2)
    E a1 b1  *   E a2 b2  =  normalizeEven  (a1  *  a2)  (b1  *  b2)
    negate (E a b)        =  normalizeEven  (-a)         (-b)
    fromInteger i         =  normalizeEven  (fromInteger i)
                                            (fromInteger i)
    signum                =  error "Modular numbers are not signed"
    abs                   =  error "Modular numbers are not signed"
dotsb = dotsb
withIntegralModulus'' ::  (Integral a, Bits a) =>
                            a -> (forall s. Num (s a) => s a) -> a
withIntegralModulus'' (i::a) k = case factor 0 i of
    (0,  i)  ->  withIntegralModulus' i k             -- odd case
    (p,  q)  ->  let (u, v) = dotsb in                -- even case: $i = 2^p q$
                   reifyIntegral p  (\(_::p  ) ->
                   reifyIntegral q  (\(_::q  ) ->
                   reifyIntegral u  (\(_::u  ) ->
                   reifyIntegral v  (\(_::v  ) ->
                   unEven (k :: Even p q u v a)))))

factor :: (Num p, Integral q) => p -> q -> (p, q)
factor p i = case quotRem i 2 of
    (0,  0)  ->  (0, 0)          -- just zero
    (j,  0)  ->  factor (p+1) j  -- accumulate powers of two
    _        ->  (p, i)          -- not even

unEven ::(  ReflectNum p, ReflectNum q, ReflectNum u,
  ReflectNum v, Integral a, Bits a) => Even p q u v a -> a
unEven (E a b :: Even p q u v a) =
  mod  (a * (reflectNum (__ :: u)) + b * (reflectNum (__ :: v)))
       (shiftL (reflectNum (__ :: q)) (reflectNum (__ :: p)))
test5  ::  Num (s a) => s a
test5  =   1000*1000 + 513*513

test5'   =  withIntegralModulus'' 1279 test5 :: Integer
test5''  =  withIntegralModulus'' 1280 test5 :: Integer

[jgbailey@…]

The original code at the link above did not compile with GHC 6.6.1. I was able to update it so it would compile. It seemed to work. To test a small portion of it, load the file in ghci and type:

withIntegralModulus (-42) modulus

The answer, -42, should come back.

[simonpj]

Good bug. Here is a much smaller module showing the same problem

newtype M s a = M a       

class Modular s a | s -> a

wim ::  forall a w. Integral a 
                      => a -> (forall s. Modular s a => M s w) -> w
wim i k = error "urk"

test4'  ::  (Modular s a, Integral a) => M s a
test4'  =   error "urk"
		       
test4   =   wim 4 test4'

Also, removing the first parameter of wim gives an ASSERT failure.