diff options
author | Thomas Miedema <thomasmiedema@gmail.com> | 2016-02-22 21:32:51 +0100 |
---|---|---|
committer | Thomas Miedema <thomasmiedema@gmail.com> | 2016-02-23 12:27:57 +0100 |
commit | 6074c108b66ec9cd2230852addb60782a8b17e0a (patch) | |
tree | f63eca7bf384b63a70fa19888c4288ab1243ce12 /testsuite | |
parent | 754a2f2bb7416bd7fe453ba7bcb7c089f5ef3b8f (diff) | |
download | haskell-6074c108b66ec9cd2230852addb60782a8b17e0a.tar.gz |
Testsuite: delete Windows line endings [skip ci] (#11631)
Diffstat (limited to 'testsuite')
34 files changed, 924 insertions, 924 deletions
diff --git a/testsuite/tests/deriving/should_compile/T3012.hs b/testsuite/tests/deriving/should_compile/T3012.hs index 44b1d64a9c..e897bfb726 100644 --- a/testsuite/tests/deriving/should_compile/T3012.hs +++ b/testsuite/tests/deriving/should_compile/T3012.hs @@ -1,10 +1,10 @@ -{-# LANGUAGE GADTs, StandaloneDeriving #-}
-
-module T3012 where
-
-data T a where
- Foo :: T Int
- Bar :: T Bool
-
-deriving instance Show (T a)
-
+{-# LANGUAGE GADTs, StandaloneDeriving #-} + +module T3012 where + +data T a where + Foo :: T Int + Bar :: T Bool + +deriving instance Show (T a) + diff --git a/testsuite/tests/deriving/should_compile/T6031.hs b/testsuite/tests/deriving/should_compile/T6031.hs index b1ca4e11de..eb0e712ae0 100644 --- a/testsuite/tests/deriving/should_compile/T6031.hs +++ b/testsuite/tests/deriving/should_compile/T6031.hs @@ -1,7 +1,7 @@ -{-# LANGUAGE StandaloneDeriving #-}
-
-module T6031 where
-
-import T6031a
-
-deriving instance Show Empty
+{-# LANGUAGE StandaloneDeriving #-} + +module T6031 where + +import T6031a + +deriving instance Show Empty diff --git a/testsuite/tests/deriving/should_compile/T6031a.hs b/testsuite/tests/deriving/should_compile/T6031a.hs index 8871b3ac1b..4cb8aad01e 100644 --- a/testsuite/tests/deriving/should_compile/T6031a.hs +++ b/testsuite/tests/deriving/should_compile/T6031a.hs @@ -1,3 +1,3 @@ -module T6031a where
-
-data Empty
+module T6031a where + +data Empty diff --git a/testsuite/tests/deriving/should_compile/T8893.hs b/testsuite/tests/deriving/should_compile/T8893.hs index 2ebcc94624..8c69c45977 100644 --- a/testsuite/tests/deriving/should_compile/T8893.hs +++ b/testsuite/tests/deriving/should_compile/T8893.hs @@ -1,11 +1,11 @@ -{-# OPTIONS_GHC -Wall #-}
-{-# Language DeriveFunctor #-}
-{-# Language PolyKinds #-}
-
-module T8893 where
-
-data V a = V [a] deriving Functor
-
-data C x a = C (V (P x a)) deriving Functor
-
-data P x a = P (x a) deriving Functor
+{-# OPTIONS_GHC -Wall #-} +{-# Language DeriveFunctor #-} +{-# Language PolyKinds #-} + +module T8893 where + +data V a = V [a] deriving Functor + +data C x a = C (V (P x a)) deriving Functor + +data P x a = P (x a) deriving Functor diff --git a/testsuite/tests/deriving/should_fail/T2701.hs b/testsuite/tests/deriving/should_fail/T2701.hs index 37bffc827d..0d6dab3fbb 100644 --- a/testsuite/tests/deriving/should_fail/T2701.hs +++ b/testsuite/tests/deriving/should_fail/T2701.hs @@ -1,10 +1,10 @@ -{-# LANGUAGE MagicHash, DeriveDataTypeable #-}
-module T2700 where
-
-import GHC.Prim
-
-import Data.Data
-import Data.Typeable
-
-data Foo = MkFoo Int#
- deriving (Typeable, Data)
+{-# LANGUAGE MagicHash, DeriveDataTypeable #-} +module T2700 where + +import GHC.Prim + +import Data.Data +import Data.Typeable + +data Foo = MkFoo Int# + deriving (Typeable, Data) diff --git a/testsuite/tests/deriving/should_fail/T4846.hs b/testsuite/tests/deriving/should_fail/T4846.hs index 66621c04ee..e9cd180d4c 100755 --- a/testsuite/tests/deriving/should_fail/T4846.hs +++ b/testsuite/tests/deriving/should_fail/T4846.hs @@ -1,37 +1,37 @@ -{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving, GADTs, GeneralizedNewtypeDeriving, DeriveDataTypeable #-}
-
-module Main where
-
-import Data.Typeable
-
-data Expr a where
- Lit :: Typeable a => a -> Expr a
-
-class A a where
- mk :: a
-
-class (Typeable a, A a) => B a where
- mkExpr :: Expr a
- mkExpr = Lit mk
-
--- dfunAE
-instance B a => A (Expr a) where
- mk = mkExpr
-
--- dfunAB
-instance A Bool where
- mk = True
-
-newtype BOOL = BOOL Bool
- deriving (Typeable, A)
-
-instance B Bool
-deriving instance B BOOL --dfunBB
-
-showType :: forall a . Expr a -> String
-showType (Lit _) = show (typeOf (undefined :: a))
-
-test1 = showType (mk :: Expr BOOL) -- Prints "Bool" (wrong?)
-test2 = showType (Lit mk :: Expr BOOL) -- Prints "Main.BOOL" (correct)
-
-main = do { print test1; print test2 }
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving, GADTs, GeneralizedNewtypeDeriving, DeriveDataTypeable #-} + +module Main where + +import Data.Typeable + +data Expr a where + Lit :: Typeable a => a -> Expr a + +class A a where + mk :: a + +class (Typeable a, A a) => B a where + mkExpr :: Expr a + mkExpr = Lit mk + +-- dfunAE +instance B a => A (Expr a) where + mk = mkExpr + +-- dfunAB +instance A Bool where + mk = True + +newtype BOOL = BOOL Bool + deriving (Typeable, A) + +instance B Bool +deriving instance B BOOL --dfunBB + +showType :: forall a . Expr a -> String +showType (Lit _) = show (typeOf (undefined :: a)) + +test1 = showType (mk :: Expr BOOL) -- Prints "Bool" (wrong?) +test2 = showType (Lit mk :: Expr BOOL) -- Prints "Main.BOOL" (correct) + +main = do { print test1; print test2 } diff --git a/testsuite/tests/deriving/should_run/T4136.hs b/testsuite/tests/deriving/should_run/T4136.hs index d47014bdb0..c8363dcc68 100644 --- a/testsuite/tests/deriving/should_run/T4136.hs +++ b/testsuite/tests/deriving/should_run/T4136.hs @@ -1,9 +1,9 @@ -module Main where
-
-data T = (:=:) {- | (:!=:) -} deriving (Show,Read)
-
-main
- = do putStrLn ("show (:=:) = " ++ show (:=:))
- putStrLn ("read (show (:=:)) :: T = " ++
- show (read (show (:=:)) :: T))
-
+module Main where + +data T = (:=:) {- | (:!=:) -} deriving (Show,Read) + +main + = do putStrLn ("show (:=:) = " ++ show (:=:)) + putStrLn ("read (show (:=:)) :: T = " ++ + show (read (show (:=:)) :: T)) + diff --git a/testsuite/tests/deriving/should_run/drvrun019.hs b/testsuite/tests/deriving/should_run/drvrun019.hs index 663fb38cd4..c79d401796 100644 --- a/testsuite/tests/deriving/should_run/drvrun019.hs +++ b/testsuite/tests/deriving/should_run/drvrun019.hs @@ -1,15 +1,15 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} -
--- Tests newtype deriving with
--- a non-type constructor in the representation
-
-module Main where
-
-newtype Wrap m a = Wrap { unWrap :: m a }
- deriving (Functor, Applicative, Monad, Eq)
-
-foo :: Int -> Wrap IO a -> Wrap IO ()
-foo 0 a = return ()
-foo n a = do { a; foo (n-1) a }
-
-main = do { unWrap (foo 3 (Wrap (putChar 'x'))); putChar '\n' }
+ +-- Tests newtype deriving with +-- a non-type constructor in the representation + +module Main where + +newtype Wrap m a = Wrap { unWrap :: m a } + deriving (Functor, Applicative, Monad, Eq) + +foo :: Int -> Wrap IO a -> Wrap IO () +foo 0 a = return () +foo n a = do { a; foo (n-1) a } + +main = do { unWrap (foo 3 (Wrap (putChar 'x'))); putChar '\n' } diff --git a/testsuite/tests/driver/Shared001.hs b/testsuite/tests/driver/Shared001.hs index 4f6a3d9c3d..4d827b85ba 100644 --- a/testsuite/tests/driver/Shared001.hs +++ b/testsuite/tests/driver/Shared001.hs @@ -1,9 +1,9 @@ -{-# LANGUAGE ForeignFunctionInterface #-}
-module Shared001 where
-
--- Test for building DLLs with ghc -shared, see #2745
-
-f :: Int -> Int
-f x = x+1
-
-foreign export ccall f :: Int -> Int
+{-# LANGUAGE ForeignFunctionInterface #-} +module Shared001 where + +-- Test for building DLLs with ghc -shared, see #2745 + +f :: Int -> Int +f x = x+1 + +foreign export ccall f :: Int -> Int diff --git a/testsuite/tests/driver/recomp010/X1.hs b/testsuite/tests/driver/recomp010/X1.hs index 7906d4beef..84768c9349 100644 --- a/testsuite/tests/driver/recomp010/X1.hs +++ b/testsuite/tests/driver/recomp010/X1.hs @@ -1,10 +1,10 @@ -module X (x, D1(..), D2(..))
-where
-
-data D1 = D { f :: D2 } -- deriving Show
-data D2 = A | B -- deriving Show
-
-x :: D1
-x = D { f = A }
-
-
+module X (x, D1(..), D2(..)) +where + +data D1 = D { f :: D2 } -- deriving Show +data D2 = A | B -- deriving Show + +x :: D1 +x = D { f = A } + + diff --git a/testsuite/tests/driver/recomp010/X2.hs b/testsuite/tests/driver/recomp010/X2.hs index e120124551..d57bda6a74 100644 --- a/testsuite/tests/driver/recomp010/X2.hs +++ b/testsuite/tests/driver/recomp010/X2.hs @@ -1,10 +1,10 @@ -module X (x, D1(..), D2(..))
-where
-
-data D1 = D { f :: D2 } -- deriving Show
-data D2 = A | B -- deriving Show
-
-x :: D1
-x = D { f = B }
-
-
+module X (x, D1(..), D2(..)) +where + +data D1 = D { f :: D2 } -- deriving Show +data D2 = A | B -- deriving Show + +x :: D1 +x = D { f = B } + + diff --git a/testsuite/tests/dynlibs/T4464H.hs b/testsuite/tests/dynlibs/T4464H.hs index f620866c86..e3b511a63e 100644 --- a/testsuite/tests/dynlibs/T4464H.hs +++ b/testsuite/tests/dynlibs/T4464H.hs @@ -1,7 +1,7 @@ -{-# LANGUAGE ForeignFunctionInterface #-}
-module T4464H where
-
-f :: Int -> Int
-f x = x + 1
-
-foreign export ccall f :: Int -> Int
+{-# LANGUAGE ForeignFunctionInterface #-} +module T4464H where + +f :: Int -> Int +f x = x + 1 + +foreign export ccall f :: Int -> Int diff --git a/testsuite/tests/eyeball/inline4.hs b/testsuite/tests/eyeball/inline4.hs index 2648c9e039..a673de9b2a 100644 --- a/testsuite/tests/eyeball/inline4.hs +++ b/testsuite/tests/eyeball/inline4.hs @@ -1,40 +1,40 @@ -module CmmTx where
-
-data TxRes a = TxRes Bool a
-
-instance Monad TxRes where
- return = TxRes False
-
-{- Here you can get a simplifier loop thus:
-NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52
-NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52
-NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52
-NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52
-
-Reason: 'a' is inline (not pre/post unconditionally; just ordinary inlining)
-Then, since ($dm>>) has arity 3, the rhs of (>>) is a PAP, so the arg is
-floated out, past the big lambdas.
-
-See Note [Unsaturated functions] in SimplUtils
-
-------------------------------------------------------------
-a_s9f{v} [lid] =
- base:GHC.Base.:DMonad{v r5} [gid]
- @ main:CmmTx.TxRes{tc rd}
- >>={v a6E} [lid]
- >>{v a6H} [lid]
- return{v a6J} [lid]
- fail{v a6M} [lid]
->>{v a6H} [lid] [ALWAYS LoopBreaker Nothing] :: forall a{tv a6F} [tv]
- b{tv a6G} [tv].
- main:CmmTx.TxRes{tc rd} a{tv a6F} [tv]
- -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv]
- -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv]
-[Arity 2
- Str: DmdType LL]
->>{v a6H} [lid] =
- \ (@ a{tv a78} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d})
- (@ b{tv a79} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d}) ->
- base:GHC.Base.$dm>>{v r5f} [gid]
- @ main:CmmTx.TxRes{tc rd} a_s9f{v} [lid] @ a{tv a78} [sk] @ b{tv a79} [sk]
- -}
+module CmmTx where + +data TxRes a = TxRes Bool a + +instance Monad TxRes where + return = TxRes False + +{- Here you can get a simplifier loop thus: +NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52 +NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52 +NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52 +NOTE: Simplifier still going after 4 iterations; bailing out. Size = 52 + +Reason: 'a' is inline (not pre/post unconditionally; just ordinary inlining) +Then, since ($dm>>) has arity 3, the rhs of (>>) is a PAP, so the arg is +floated out, past the big lambdas. + +See Note [Unsaturated functions] in SimplUtils + +------------------------------------------------------------ +a_s9f{v} [lid] = + base:GHC.Base.:DMonad{v r5} [gid] + @ main:CmmTx.TxRes{tc rd} + >>={v a6E} [lid] + >>{v a6H} [lid] + return{v a6J} [lid] + fail{v a6M} [lid] +>>{v a6H} [lid] [ALWAYS LoopBreaker Nothing] :: forall a{tv a6F} [tv] + b{tv a6G} [tv]. + main:CmmTx.TxRes{tc rd} a{tv a6F} [tv] + -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv] + -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv] +[Arity 2 + Str: DmdType LL] +>>{v a6H} [lid] = + \ (@ a{tv a78} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d}) + (@ b{tv a79} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d}) -> + base:GHC.Base.$dm>>{v r5f} [gid] + @ main:CmmTx.TxRes{tc rd} a_s9f{v} [lid] @ a{tv a78} [sk] @ b{tv a79} [sk] + -} diff --git a/testsuite/tests/eyeball/record1.hs b/testsuite/tests/eyeball/record1.hs index 1f9084b7a6..dde6f5ee25 100644 --- a/testsuite/tests/eyeball/record1.hs +++ b/testsuite/tests/eyeball/record1.hs @@ -1,17 +1,17 @@ --- Check that the record selector for maskMB unfolds in the body of f
--- At one stage it didn't because the implicit unfolding looked too big
-
--- Trac #2581
-
-module ShouldCompile where
-import Data.Array.Base
-
-data MBloom s a = MB {
- shiftMB :: {-# UNPACK #-} !Int
- , maskMB :: {-# UNPACK #-} !Int
- , bitArrayMB :: {-# UNPACK #-} !(STUArray s Int Int)
- }
-
-f a b c = case maskMB (MB a b c) of
- 3 -> True
- _ -> False
+-- Check that the record selector for maskMB unfolds in the body of f +-- At one stage it didn't because the implicit unfolding looked too big + +-- Trac #2581 + +module ShouldCompile where +import Data.Array.Base + +data MBloom s a = MB { + shiftMB :: {-# UNPACK #-} !Int + , maskMB :: {-# UNPACK #-} !Int + , bitArrayMB :: {-# UNPACK #-} !(STUArray s Int Int) + } + +f a b c = case maskMB (MB a b c) of + 3 -> True + _ -> False diff --git a/testsuite/tests/ffi/should_compile/ffi-deriv1.hs b/testsuite/tests/ffi/should_compile/ffi-deriv1.hs index 1e5d27a0b6..dba0eaa460 100644 --- a/testsuite/tests/ffi/should_compile/ffi-deriv1.hs +++ b/testsuite/tests/ffi/should_compile/ffi-deriv1.hs @@ -1,25 +1,25 @@ -{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
--- Tests newtype unwrapping for the IO monad itself
--- Notice the RenderM monad, which is used in the
--- type of the callback function
-
-module ShouldCompile where
-
-import Control.Applicative (Applicative)
-
-import Foreign.Ptr
-newtype RenderM a = RenderM (IO a) deriving (Functor, Applicative, Monad)
-
-type RenderCallback = Int -> Int -> RenderM ()
-
-foreign import ccall duma_onRender :: FunPtr RenderCallback -> RenderM ()
-
-foreign import ccall "wrapper" mkRenderCallback
- :: RenderCallback -> RenderM (FunPtr RenderCallback)
-
-onRender :: RenderCallback -> RenderM ()
-onRender f = mkRenderCallback f >>= duma_onRender
-
-
-
+{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- Tests newtype unwrapping for the IO monad itself +-- Notice the RenderM monad, which is used in the +-- type of the callback function + +module ShouldCompile where + +import Control.Applicative (Applicative) + +import Foreign.Ptr +newtype RenderM a = RenderM (IO a) deriving (Functor, Applicative, Monad) + +type RenderCallback = Int -> Int -> RenderM () + +foreign import ccall duma_onRender :: FunPtr RenderCallback -> RenderM () + +foreign import ccall "wrapper" mkRenderCallback + :: RenderCallback -> RenderM (FunPtr RenderCallback) + +onRender :: RenderCallback -> RenderM () +onRender f = mkRenderCallback f >>= duma_onRender + + + diff --git a/testsuite/tests/ffi/should_run/T1288.hs b/testsuite/tests/ffi/should_run/T1288.hs index 8b3a8f8417..c57b7c449d 100644 --- a/testsuite/tests/ffi/should_run/T1288.hs +++ b/testsuite/tests/ffi/should_run/T1288.hs @@ -1,6 +1,6 @@ -import Foreign
-import Foreign.C
-
-foreign import stdcall "test" ctest :: CInt -> IO ()
-
-main = ctest 3
+import Foreign +import Foreign.C + +foreign import stdcall "test" ctest :: CInt -> IO () + +main = ctest 3 diff --git a/testsuite/tests/ffi/should_run/T1288_ghci.hs b/testsuite/tests/ffi/should_run/T1288_ghci.hs index 8b3a8f8417..c57b7c449d 100644 --- a/testsuite/tests/ffi/should_run/T1288_ghci.hs +++ b/testsuite/tests/ffi/should_run/T1288_ghci.hs @@ -1,6 +1,6 @@ -import Foreign
-import Foreign.C
-
-foreign import stdcall "test" ctest :: CInt -> IO ()
-
-main = ctest 3
+import Foreign +import Foreign.C + +foreign import stdcall "test" ctest :: CInt -> IO () + +main = ctest 3 diff --git a/testsuite/tests/ffi/should_run/T2276.hs b/testsuite/tests/ffi/should_run/T2276.hs index 0ee1ee91ff..c7b14bd60d 100644 --- a/testsuite/tests/ffi/should_run/T2276.hs +++ b/testsuite/tests/ffi/should_run/T2276.hs @@ -1,7 +1,7 @@ -import Foreign
-import Foreign.C
-
-foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ())
-foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO ()
-
-main = ctest ptest 3
+import Foreign +import Foreign.C + +foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ()) +foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO () + +main = ctest ptest 3 diff --git a/testsuite/tests/ffi/should_run/T2276_ghci.hs b/testsuite/tests/ffi/should_run/T2276_ghci.hs index 0ee1ee91ff..c7b14bd60d 100644 --- a/testsuite/tests/ffi/should_run/T2276_ghci.hs +++ b/testsuite/tests/ffi/should_run/T2276_ghci.hs @@ -1,7 +1,7 @@ -import Foreign
-import Foreign.C
-
-foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ())
-foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO ()
-
-main = ctest ptest 3
+import Foreign +import Foreign.C + +foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ()) +foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO () + +main = ctest ptest 3 diff --git a/testsuite/tests/ffi/should_run/ffi014.hs b/testsuite/tests/ffi/should_run/ffi014.hs index 4434bef21a..8a1a2864c3 100644 --- a/testsuite/tests/ffi/should_run/ffi014.hs +++ b/testsuite/tests/ffi/should_run/ffi014.hs @@ -1,29 +1,29 @@ --- exposed a bug in GHC 6.4 threaded RTS, fixed in Schedule.c rev. 1.232
-
-module Main where
-
-import Control.Concurrent
-import Control.Monad
-import Foreign.Ptr
-import Data.IORef
-
-main = do
- ms <- replicateM 100 $ do putStrLn "."
- m <- newEmptyMVar
- forkOS (thread >> putMVar m ())
- thread
- return m
- mapM takeMVar ms
-
-thread = do var <- newIORef 0
- let f = modifyIORef var (1+)
- callC =<< mkFunc f
-
-type FUNC = IO ()
-
-foreign import ccall unsafe "wrapper"
- mkFunc :: FUNC -> IO (FunPtr FUNC)
-
-foreign import ccall safe "ffi014_cbits.h callC"
- callC:: FunPtr FUNC -> IO ()
-
+-- exposed a bug in GHC 6.4 threaded RTS, fixed in Schedule.c rev. 1.232 + +module Main where + +import Control.Concurrent +import Control.Monad +import Foreign.Ptr +import Data.IORef + +main = do + ms <- replicateM 100 $ do putStrLn "." + m <- newEmptyMVar + forkOS (thread >> putMVar m ()) + thread + return m + mapM takeMVar ms + +thread = do var <- newIORef 0 + let f = modifyIORef var (1+) + callC =<< mkFunc f + +type FUNC = IO () + +foreign import ccall unsafe "wrapper" + mkFunc :: FUNC -> IO (FunPtr FUNC) + +foreign import ccall safe "ffi014_cbits.h callC" + callC:: FunPtr FUNC -> IO () + diff --git a/testsuite/tests/gadt/Arith.hs b/testsuite/tests/gadt/Arith.hs index a98ee729a9..97d757337b 100644 --- a/testsuite/tests/gadt/Arith.hs +++ b/testsuite/tests/gadt/Arith.hs @@ -1,146 +1,146 @@ -{-# LANGUAGE GADTs #-}
-
-module Arith where
-
-data E a b = E (a -> b) (b -> a)
-
-eqRefl :: E a a
-eqRefl = E id id
-
--- just to construct unique strings
-data W
-data M a
-
--- terms
-data Var a where
- VarW :: Var W
- VarM :: Var (M a)
-
--- expose s in the type level making sure it is a string
-data Abs s e1 where
- Abs :: (Var s) -> e1 -> Abs (Var s) e1
-
-data App e1 e2 = App e1 e2
-data Lit = Lit
-
-data TyBase = TyBase
-data TyArr t1 t2 = TyArr t1 t2
-
--- (x:ty) in G
-data IN g p where
- INOne :: IN (g,(x,ty)) (x,ty)
- INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty)
-
-data INEX g x where
- INEX :: IN g (x,v) -> INEX g x
-
-
--- G1 subseteq G2
-type SUP g1 g2 = forall a. IN g1 a -> IN g2 a
-
--- typing derivations
-data DER g a ty where
- DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty
- DApp :: DER g a1 (TyArr ty1 ty2) ->
- DER g a2 ty1 -> DER g (App a1 a2) ty2
- DAbs :: DER (g,(Var a,ty1)) e ty2 ->
- DER g (Abs (Var a) e) (TyArr ty1 ty2)
- DLit :: DER g Lit TyBase
-
--- G |- \x.x : a -> a
-test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty)
-test1 = DAbs (DVar INOne)
-
--- G |- (\x.x) Lit : Lit
-test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase
-test2 = DApp (DAbs (DVar INOne)) DLit
-
--- G |- \x.\y. x y : (C -> C) -> C -> C
-test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty))
-test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne)))
-
-data ISVAL e where
- ISVALAbs :: ISVAL (Abs (Var v) e)
- ISVALLit :: ISVAL Lit
-
-data React e1 e2 where
- SUBSTReact :: React (Abs (Var y) e) v
-
--- evaluation
-data EDER e1 e2 where
- -- EVar :: IN (a,val) -> ISVAL val -> EDER c a val
- EApp1 :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2)
- EApp2 :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2')
- EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1
-
--- (\x.x) 3 -> 3
--- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit
--- test4 = EAppAbs ISVALLit SUBSTEqVar
-
-
--- existential
-data REDUCES e1 where
- REDUCES :: EDER e1 e2 -> REDUCES e1
-
--- data WFEnv x c g where
--- WFOne :: ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty))
--- WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1))
-
--- data WFENVWRAP c g where
--- WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g
-
-
--- data INEXVAL c x where
--- INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x
-
--- -- the first cool theorem!
--- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g -> INEXVAL c x
--- fromTEnvToEnv INOne (WFOne isv _) = INEXVAL INOne isv
--- fromTEnvToEnv (INShift ind1) (WFShift ind2) =
--- case (fromTEnvToEnv ind1 ind2) of
--- INEXVAL i isv -> INEXVAL (INShift i) isv
-
-
-data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e)
-data ISLIT v where ISLIT :: ISLIT Lit
-
-data EXISTAbs where
- EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs
-
-bot = bot
-
-canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v
-canFormsLam ISVALAbs _ = ISLAMBDA
--- canFormsLam ISVALLit _ = bot <== unfortunately I cannot catch this ... requires some exhaustiveness check :-(
-
-canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v
-canFormsLit ISVALLit _ = ISLIT
-
-data NULL
-
-progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e)
-
-progress (DAbs prem) = Left ISVALAbs
-progress (DLit) = Left ISVALLit
--- progress (DVar iw) = bot <== here is the cool trick! I cannot even wite this down!
-progress (DApp e1 e2) =
- case (progress e1) of
- Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
- Left isv1 -> case (progress e2) of
- Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
- Left isv2 -> case (canFormsLam isv1 e1) of
- ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact))
-
-
--- case fromTEnvToEnv iw (f iw) of
--- INEXVAL i isv -> Right (REDUCES (EVar i isv))
--- progress (WFENVWRAP f) (DApp e1 e2) =
--- case (progress (WFENVWRAP f) e1) of
--- Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
--- Left isv1 -> case (progress (WFENVWRAP f) e2) of
--- Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
--- Left isv2 -> case (canFormsLam isv1 e1) of
--- ISLAMBDA -> EAppAbs isv2 e1
-
-
-
+{-# LANGUAGE GADTs #-} + +module Arith where + +data E a b = E (a -> b) (b -> a) + +eqRefl :: E a a +eqRefl = E id id + +-- just to construct unique strings +data W +data M a + +-- terms +data Var a where + VarW :: Var W + VarM :: Var (M a) + +-- expose s in the type level making sure it is a string +data Abs s e1 where + Abs :: (Var s) -> e1 -> Abs (Var s) e1 + +data App e1 e2 = App e1 e2 +data Lit = Lit + +data TyBase = TyBase +data TyArr t1 t2 = TyArr t1 t2 + +-- (x:ty) in G +data IN g p where + INOne :: IN (g,(x,ty)) (x,ty) + INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty) + +data INEX g x where + INEX :: IN g (x,v) -> INEX g x + + +-- G1 subseteq G2 +type SUP g1 g2 = forall a. IN g1 a -> IN g2 a + +-- typing derivations +data DER g a ty where + DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty + DApp :: DER g a1 (TyArr ty1 ty2) -> + DER g a2 ty1 -> DER g (App a1 a2) ty2 + DAbs :: DER (g,(Var a,ty1)) e ty2 -> + DER g (Abs (Var a) e) (TyArr ty1 ty2) + DLit :: DER g Lit TyBase + +-- G |- \x.x : a -> a +test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty) +test1 = DAbs (DVar INOne) + +-- G |- (\x.x) Lit : Lit +test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase +test2 = DApp (DAbs (DVar INOne)) DLit + +-- G |- \x.\y. x y : (C -> C) -> C -> C +test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty)) +test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne))) + +data ISVAL e where + ISVALAbs :: ISVAL (Abs (Var v) e) + ISVALLit :: ISVAL Lit + +data React e1 e2 where + SUBSTReact :: React (Abs (Var y) e) v + +-- evaluation +data EDER e1 e2 where + -- EVar :: IN (a,val) -> ISVAL val -> EDER c a val + EApp1 :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2) + EApp2 :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2') + EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1 + +-- (\x.x) 3 -> 3 +-- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit +-- test4 = EAppAbs ISVALLit SUBSTEqVar + + +-- existential +data REDUCES e1 where + REDUCES :: EDER e1 e2 -> REDUCES e1 + +-- data WFEnv x c g where +-- WFOne :: ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty)) +-- WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1)) + +-- data WFENVWRAP c g where +-- WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g + + +-- data INEXVAL c x where +-- INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x + +-- -- the first cool theorem! +-- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g -> INEXVAL c x +-- fromTEnvToEnv INOne (WFOne isv _) = INEXVAL INOne isv +-- fromTEnvToEnv (INShift ind1) (WFShift ind2) = +-- case (fromTEnvToEnv ind1 ind2) of +-- INEXVAL i isv -> INEXVAL (INShift i) isv + + +data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e) +data ISLIT v where ISLIT :: ISLIT Lit + +data EXISTAbs where + EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs + +bot = bot + +canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v +canFormsLam ISVALAbs _ = ISLAMBDA +-- canFormsLam ISVALLit _ = bot <== unfortunately I cannot catch this ... requires some exhaustiveness check :-( + +canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v +canFormsLit ISVALLit _ = ISLIT + +data NULL + +progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e) + +progress (DAbs prem) = Left ISVALAbs +progress (DLit) = Left ISVALLit +-- progress (DVar iw) = bot <== here is the cool trick! I cannot even wite this down! +progress (DApp e1 e2) = + case (progress e1) of + Right (REDUCES r1) -> Right (REDUCES (EApp1 r1)) + Left isv1 -> case (progress e2) of + Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2)) + Left isv2 -> case (canFormsLam isv1 e1) of + ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact)) + + +-- case fromTEnvToEnv iw (f iw) of +-- INEXVAL i isv -> Right (REDUCES (EVar i isv)) +-- progress (WFENVWRAP f) (DApp e1 e2) = +-- case (progress (WFENVWRAP f) e1) of +-- Right (REDUCES r1) -> Right (REDUCES (EApp1 r1)) +-- Left isv1 -> case (progress (WFENVWRAP f) e2) of +-- Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2)) +-- Left isv2 -> case (canFormsLam isv1 e1) of +-- ISLAMBDA -> EAppAbs isv2 e1 + + + diff --git a/testsuite/tests/gadt/T2587.hs b/testsuite/tests/gadt/T2587.hs index bcd0a443ac..cea1c092d3 100644 --- a/testsuite/tests/gadt/T2587.hs +++ b/testsuite/tests/gadt/T2587.hs @@ -1,18 +1,18 @@ -{-# LANGUAGE GADTs, ExistentialQuantification #-}
-{-# OPTIONS_GHC -O -fno-warn-overlapping-patterns #-}
-
--- Trac #2587
--- Actually this bug related to free variables and
--- type lets, but ostensibly it has a GADT flavour
--- Hence being in the GADT directory.
-
-module GadtBug(bug) where
-
-data Existential = forall a . Existential (Gadt a)
-
-data Gadt a where Value :: Gadt Double
-
-bug = [ match undefined | ps <- undefined, _ <- ps ]
- where
- match (Existential _) = undefined
- match (Existential _) = undefined
+{-# LANGUAGE GADTs, ExistentialQuantification #-} +{-# OPTIONS_GHC -O -fno-warn-overlapping-patterns #-} + +-- Trac #2587 +-- Actually this bug related to free variables and +-- type lets, but ostensibly it has a GADT flavour +-- Hence being in the GADT directory. + +module GadtBug(bug) where + +data Existential = forall a . Existential (Gadt a) + +data Gadt a where Value :: Gadt Double + +bug = [ match undefined | ps <- undefined, _ <- ps ] + where + match (Existential _) = undefined + match (Existential _) = undefined diff --git a/testsuite/tests/gadt/data1.hs b/testsuite/tests/gadt/data1.hs index 9dac84000e..b9c6ffe19c 100644 --- a/testsuite/tests/gadt/data1.hs +++ b/testsuite/tests/gadt/data1.hs @@ -1,17 +1,17 @@ -{-# LANGUAGE GADTs #-}
-
--- Trac #289
-
-module ShouldCompile where
-
-class C a where
- f :: a -> Bool
-
-data T a where
- MkT :: (C a) => a -> T a
-
-tf1 :: T Int -> Bool
-tf1 (MkT aa) = f aa
-
-tf2 :: T a -> Bool
-tf2 (MkT aa) = f aa
+{-# LANGUAGE GADTs #-} + +-- Trac #289 + +module ShouldCompile where + +class C a where + f :: a -> Bool + +data T a where + MkT :: (C a) => a -> T a + +tf1 :: T Int -> Bool +tf1 (MkT aa) = f aa + +tf2 :: T a -> Bool +tf2 (MkT aa) = f aa diff --git a/testsuite/tests/gadt/data2.hs b/testsuite/tests/gadt/data2.hs index 5b8a009d05..fcac05880b 100644 --- a/testsuite/tests/gadt/data2.hs +++ b/testsuite/tests/gadt/data2.hs @@ -1,19 +1,19 @@ -{-# LANGUAGE GADTs, ExistentialQuantification #-}
-
--- Trac #289
-
-module ShouldCompile where
-
-class Foo a where
- foo :: a -> Int
-
-data T = forall a. T (G a)
-data G a where
- A :: G a
- B :: Foo a => a -> G a
-
-doFoo :: T -> Int
-doFoo (T A) = 2
-doFoo (T (B x)) = foo x
-
-
+{-# LANGUAGE GADTs, ExistentialQuantification #-} + +-- Trac #289 + +module ShouldCompile where + +class Foo a where + foo :: a -> Int + +data T = forall a. T (G a) +data G a where + A :: G a + B :: Foo a => a -> G a + +doFoo :: T -> Int +doFoo (T A) = 2 +doFoo (T (B x)) = foo x + + diff --git a/testsuite/tests/gadt/gadt-fd.hs b/testsuite/tests/gadt/gadt-fd.hs index 4db7b62889..7efac2288f 100644 --- a/testsuite/tests/gadt/gadt-fd.hs +++ b/testsuite/tests/gadt/gadt-fd.hs @@ -1,23 +1,23 @@ -{-# LANGUAGE GADTs #-}
-
--- Trac #345
-
-module ShouldCompile where
-
-data Succ n
-data Zero
-
-class Plus x y z | x y -> z
-instance Plus Zero x x
-instance Plus x y z => Plus (Succ x) y (Succ z)
-
-infixr 5 :::
-
-data List :: * -> * -> * where
- Nil :: List a Zero
- (:::) :: a -> List a n -> List a (Succ n)
-
-append :: Plus x y z => List a x -> List a y -> List a z
-append Nil ys = ys
-append (x ::: xs) ys = x ::: append xs ys
-
+{-# LANGUAGE GADTs #-} + +-- Trac #345 + +module ShouldCompile where + +data Succ n +data Zero + +class Plus x y z | x y -> z +instance Plus Zero x x +instance Plus x y z => Plus (Succ x) y (Succ z) + +infixr 5 ::: + +data List :: * -> * -> * where + Nil :: List a Zero + (:::) :: a -> List a n -> List a (Succ n) + +append :: Plus x y z => List a x -> List a y -> List a z +append Nil ys = ys +append (x ::: xs) ys = x ::: append xs ys + diff --git a/testsuite/tests/gadt/gadt14.hs b/testsuite/tests/gadt/gadt14.hs index c5bdbcb5de..5f6e9fa690 100644 --- a/testsuite/tests/gadt/gadt14.hs +++ b/testsuite/tests/gadt/gadt14.hs @@ -1,8 +1,8 @@ -{-# LANGUAGE GADTs #-}
-
--- Check that trailing parens are ok in data con signatures
-
-module ShouldCompile where
-
-data T where
- MkT :: Int -> (Int -> T)
+{-# LANGUAGE GADTs #-} + +-- Check that trailing parens are ok in data con signatures + +module ShouldCompile where + +data T where + MkT :: Int -> (Int -> T) diff --git a/testsuite/tests/gadt/gadt18.hs b/testsuite/tests/gadt/gadt18.hs index 4ac12efa84..a7ae5a20c5 100644 --- a/testsuite/tests/gadt/gadt18.hs +++ b/testsuite/tests/gadt/gadt18.hs @@ -1,18 +1,18 @@ -{-# LANGUAGE GADTs #-}
--- A simple GADT test from Roman
--- which nevertheless showed up a bug at one stage
-
-module ShouldCompile where
-
-data T a where
- T1 :: () -> T ()
- T2 :: T a -> T b -> T (a,b)
-
-class C a where
- f :: T a -> a
-
-instance C () where
- f (T1 x) = x
-
-instance (C a, C b) => C (a,b) where
- f (T2 x y) = (f x, f y)
+{-# LANGUAGE GADTs #-} +-- A simple GADT test from Roman +-- which nevertheless showed up a bug at one stage + +module ShouldCompile where + +data T a where + T1 :: () -> T () + T2 :: T a -> T b -> T (a,b) + +class C a where + f :: T a -> a + +instance C () where + f (T1 x) = x + +instance (C a, C b) => C (a,b) where + f (T2 x y) = (f x, f y) diff --git a/testsuite/tests/gadt/gadt9.hs b/testsuite/tests/gadt/gadt9.hs index df9e0bceb2..ab8d70d07a 100644 --- a/testsuite/tests/gadt/gadt9.hs +++ b/testsuite/tests/gadt/gadt9.hs @@ -1,15 +1,15 @@ -{-# LANGUAGE GADTs #-}
-
--- This one requires careful handling in
--- TcUnify.unifyTyConApp, to preserve rigidity.
-
-module ShouldCompile where
-
-data X a b where
- X :: X a a
-
-data Y x a b where
- Y :: x a b -> x b c -> Y x a c
-
-doy :: Y X a b -> Y X a b
-doy (Y X X) = Y X X
+{-# LANGUAGE GADTs #-} + +-- This one requires careful handling in +-- TcUnify.unifyTyConApp, to preserve rigidity. + +module ShouldCompile where + +data X a b where + X :: X a a + +data Y x a b where + Y :: x a b -> x b c -> Y x a c + +doy :: Y X a b -> Y X a b +doy (Y X X) = Y X X diff --git a/testsuite/tests/gadt/karl1.hs b/testsuite/tests/gadt/karl1.hs index e3af7adb1d..b671db7cd3 100644 --- a/testsuite/tests/gadt/karl1.hs +++ b/testsuite/tests/gadt/karl1.hs @@ -1,79 +1,79 @@ -{-# LANGUAGE GADTs, KindSignatures #-}
-
--- See Trac #301
--- This particular one doesn't use GADTs per se,
--- but it does use dictionaries in constructors
-
-module Expr1 where
-
-data Expr :: * -> * where -- Not a GADT at all
- Const :: Show a => a -> Expr a
- -- Note the Show constraint here
- Var :: Var a -> Expr a
-
-newtype Var a = V String
-
-instance Show (Var a) where show (V s) = s
-
---------------------------
-e1 :: Expr Int
-e1 = Const 42
-
-e2 :: Expr Bool
-e2 = Const True
-
-e3 :: Expr Integer
-e3 = Var (V "mersenne100")
-
---------------------------
-eval :: Expr a -> a
-eval (Const c) = c
-eval (Var v) = error ("free variable `" ++ shows v "'")
-
-{-
- Up to here, everything works nicely:
-
- \begin{verbatim}
- *Expr0> eval e1
- 42
- *Expr0> eval e2
- True
- *Expr1> eval e3
- *** Exception: free variable `mersenne100'
- \end{verbatim}
-
- But let us now try to define a |shows| function.
-
- In the following, without the type signature we get:
- \begin{verbatim}
- *Expr1> :t showsExpr
- showsExpr :: forall a. (Show a) => Expr a -> String -> String
- *Expr1> showsExpr e1 ""
- "42"
- *Expr1> showsExpr e2 ""
- "True"
- *Expr1> showsExpr e3 ""
- "mersenne100"
- \end{verbatim}
-
- However, in the last case, the instance |Show Integer| was not used,
- so should not have been required.
- Therefore I would expect it to work as it is now, i.e.,
- with the type signature:
--}
-
-showsExpr :: Expr a -> ShowS
-showsExpr (Const c) = shows c
-showsExpr (Var v) = shows v
-
-{-
-
-We used to get a complaint about the |Const| alternative (then line
-63) that documents that the constraint in the type of |Const| must
-have been ignored:
-
- No instance for (Show a)
- arising from use of `shows' at Expr1.lhs:63:22-26
- Probable fix: add (Show a) to the type signature(s) for `showsExpr'
- In the definition of `showsExpr': showsExpr (Const c) = shows c
--}
+{-# LANGUAGE GADTs, KindSignatures #-} + +-- See Trac #301 +-- This particular one doesn't use GADTs per se, +-- but it does use dictionaries in constructors + +module Expr1 where + +data Expr :: * -> * where -- Not a GADT at all + Const :: Show a => a -> Expr a + -- Note the Show constraint here + Var :: Var a -> Expr a + +newtype Var a = V String + +instance Show (Var a) where show (V s) = s + +-------------------------- +e1 :: Expr Int +e1 = Const 42 + +e2 :: Expr Bool +e2 = Const True + +e3 :: Expr Integer +e3 = Var (V "mersenne100") + +-------------------------- +eval :: Expr a -> a +eval (Const c) = c +eval (Var v) = error ("free variable `" ++ shows v "'") + +{- + Up to here, everything works nicely: + + \begin{verbatim} + *Expr0> eval e1 + 42 + *Expr0> eval e2 + True + *Expr1> eval e3 + *** Exception: free variable `mersenne100' + \end{verbatim} + + But let us now try to define a |shows| function. + + In the following, without the type signature we get: + \begin{verbatim} + *Expr1> :t showsExpr + showsExpr :: forall a. (Show a) => Expr a -> String -> String + *Expr1> showsExpr e1 "" + "42" + *Expr1> showsExpr e2 "" + "True" + *Expr1> showsExpr e3 "" + "mersenne100" + \end{verbatim} + + However, in the last case, the instance |Show Integer| was not used, + so should not have been required. + Therefore I would expect it to work as it is now, i.e., + with the type signature: +-} + +showsExpr :: Expr a -> ShowS +showsExpr (Const c) = shows c +showsExpr (Var v) = shows v + +{- + +We used to get a complaint about the |Const| alternative (then line +63) that documents that the constraint in the type of |Const| must +have been ignored: + + No instance for (Show a) + arising from use of `shows' at Expr1.lhs:63:22-26 + Probable fix: add (Show a) to the type signature(s) for `showsExpr' + In the definition of `showsExpr': showsExpr (Const c) = shows c +-} diff --git a/testsuite/tests/gadt/karl2.hs b/testsuite/tests/gadt/karl2.hs index a701400689..aa96d689d7 100644 --- a/testsuite/tests/gadt/karl2.hs +++ b/testsuite/tests/gadt/karl2.hs @@ -1,136 +1,136 @@ -{-# LANGUAGE GADTs, KindSignatures #-}
-
-module Expr0 where
-
--- See Trac #301
--- This one *does* use GADTs (Fct)
-
-data Expr :: * -> * where
- Const :: Show a => a -> Expr a
- Apply :: Fct a b -> Expr a -> Expr b
-
-data Fct :: * -> * -> * where
- Succ :: Fct Int Int
- EqZero :: Fct Int Bool
- Add :: Fct Int (Int -> Int)
-
-------------------------------
-e1 :: Expr Int
-e1 = Apply Succ (Const 41)
-
-e2 :: Expr Bool
-e2 = Apply EqZero e1
-
-e3 :: Expr (Int -> Int)
-e3 = Apply Add e1
-
-------------------------------
-eval :: Expr a -> a
-eval (Const c) = c
-eval (Apply f a) = evalFct f $ eval a
-
-evalFct :: Fct a b -> a -> b
-evalFct Succ = succ
-evalFct EqZero = (0 ==)
-evalFct Add = (+)
-
-
-{- Up to here, everything works nicely:
-
- \begin{verbatim}
- *Expr0> eval e1
- 42
- *Expr0> eval e2
- False
- *Expr0> eval e3 5
- 47
- \end{verbatim}
-
- But let us now try to define a |Show| instance.
- For |Fct|, this is not a problem:
--}
-
-instance Show (Fct a b) where
- show Succ = "S"
- show EqZero = "isZero"
- show Add = "add"
-
-showsExpr :: Expr a -> ShowS
-showsExpr (Const c) = shows c
-showsExpr (Apply f a) =
- ('(' :) . shows f . (' ' :) . showsExpr a . (')' :)
-
-instance Show (Expr a) where
- showsPrec _ (Const c) = shows c
- showsPrec _ (Apply f a) =
- ('(' :) . shows f . (' ' :) . shows a . (')' :)
-
-{- But we used to get a complaint about the |Const| alternative (then
- line 56) that documents that the constraint in the type of |Const|
- must have been ignored:
-
- \begin{verbatim}
- No instance for (Show a)
- arising from use of `shows' at Expr0.lhs:56:22-26
- Probable fix: add (Show a) to the type signature(s) for `showsExpr'
- In the definition of `showsExpr': showsExpr (Const c) = shows c
- \end{verbatim}
-
- But if we do that, the recursive call is of course still unsatisfied:
- \begin{verbatim}
- No instance for (Show a)
- arising from use of `showsExpr' at Expr0.lhs:65:34-42
- Probable fix: add (Show a) to the existential context for `Apply'
- In the first argument of `(.)', namely `showsExpr a'
- In the second argument of `(.)', namely `(showsExpr a) . ((')' :))'
- In the second argument of `(.)', namely
- `((' ' :)) . ((showsExpr a) . ((')' :)))'
- \end{verbatim}
-
- Following also the advice given in this last error message
- actually makes GHC accept this, and then we can say:
-
- \begin{verbatim}
- *Expr0> showsExpr e1 ""
- "(S 41)"
- *Expr0> showsExpr e2 ""
- "(isZero (S 41))"
- \end{verbatim}
-
- However, following this advice is counterintuitive
- and should be unnecessary
- since the |Show| instance for argument types
- is only ever used in the const case.
- We get:
-
- \begin{verbatim}
- *Expr0> showsExpr e3 ""
-
- <interactive>:1:0:
- No instance for (Show (Int -> Int))
- arising from use of `showsExpr' at <interactive>:1:0-8
- Probable fix: add an instance declaration for (Show (Int -> Int))
- In the definition of `it': it = showsExpr e3 ""
- \end{verbatim}
-
- But of course we would expect the following:
-
- \begin{verbatim}
- *Expr0> showsExpr e3 ""
- "(add (S 41))"
- \end{verbatim}
-
-
- \bigskip
- The error messages are almost the same
- if we define a |Show| instance directly
- (line 90 was the |Const| alternative):
-
- \begin{verbatim}
- Could not deduce (Show a) from the context (Show (Expr a))
- arising from use of `shows' at Expr0.lhs:90:26-30
- Probable fix: add (Show a) to the class or instance method `showsPrec'
- \end{verbatim}
--}
-
-
+{-# LANGUAGE GADTs, KindSignatures #-} + +module Expr0 where + +-- See Trac #301 +-- This one *does* use GADTs (Fct) + +data Expr :: * -> * where + Const :: Show a => a -> Expr a + Apply :: Fct a b -> Expr a -> Expr b + +data Fct :: * -> * -> * where + Succ :: Fct Int Int + EqZero :: Fct Int Bool + Add :: Fct Int (Int -> Int) + +------------------------------ +e1 :: Expr Int +e1 = Apply Succ (Const 41) + +e2 :: Expr Bool +e2 = Apply EqZero e1 + +e3 :: Expr (Int -> Int) +e3 = Apply Add e1 + +------------------------------ +eval :: Expr a -> a +eval (Const c) = c +eval (Apply f a) = evalFct f $ eval a + +evalFct :: Fct a b -> a -> b +evalFct Succ = succ +evalFct EqZero = (0 ==) +evalFct Add = (+) + + +{- Up to here, everything works nicely: + + \begin{verbatim} + *Expr0> eval e1 + 42 + *Expr0> eval e2 + False + *Expr0> eval e3 5 + 47 + \end{verbatim} + + But let us now try to define a |Show| instance. + For |Fct|, this is not a problem: +-} + +instance Show (Fct a b) where + show Succ = "S" + show EqZero = "isZero" + show Add = "add" + +showsExpr :: Expr a -> ShowS +showsExpr (Const c) = shows c +showsExpr (Apply f a) = + ('(' :) . shows f . (' ' :) . showsExpr a . (')' :) + +instance Show (Expr a) where + showsPrec _ (Const c) = shows c + showsPrec _ (Apply f a) = + ('(' :) . shows f . (' ' :) . shows a . (')' :) + +{- But we used to get a complaint about the |Const| alternative (then + line 56) that documents that the constraint in the type of |Const| + must have been ignored: + + \begin{verbatim} + No instance for (Show a) + arising from use of `shows' at Expr0.lhs:56:22-26 + Probable fix: add (Show a) to the type signature(s) for `showsExpr' + In the definition of `showsExpr': showsExpr (Const c) = shows c + \end{verbatim} + + But if we do that, the recursive call is of course still unsatisfied: + \begin{verbatim} + No instance for (Show a) + arising from use of `showsExpr' at Expr0.lhs:65:34-42 + Probable fix: add (Show a) to the existential context for `Apply' + In the first argument of `(.)', namely `showsExpr a' + In the second argument of `(.)', namely `(showsExpr a) . ((')' :))' + In the second argument of `(.)', namely + `((' ' :)) . ((showsExpr a) . ((')' :)))' + \end{verbatim} + + Following also the advice given in this last error message + actually makes GHC accept this, and then we can say: + + \begin{verbatim} + *Expr0> showsExpr e1 "" + "(S 41)" + *Expr0> showsExpr e2 "" + "(isZero (S 41))" + \end{verbatim} + + However, following this advice is counterintuitive + and should be unnecessary + since the |Show| instance for argument types + is only ever used in the const case. + We get: + + \begin{verbatim} + *Expr0> showsExpr e3 "" + + <interactive>:1:0: + No instance for (Show (Int -> Int)) + arising from use of `showsExpr' at <interactive>:1:0-8 + Probable fix: add an instance declaration for (Show (Int -> Int)) + In the definition of `it': it = showsExpr e3 "" + \end{verbatim} + + But of course we would expect the following: + + \begin{verbatim} + *Expr0> showsExpr e3 "" + "(add (S 41))" + \end{verbatim} + + + \bigskip + The error messages are almost the same + if we define a |Show| instance directly + (line 90 was the |Const| alternative): + + \begin{verbatim} + Could not deduce (Show a) from the context (Show (Expr a)) + arising from use of `shows' at Expr0.lhs:90:26-30 + Probable fix: add (Show a) to the class or instance method `showsPrec' + \end{verbatim} +-} + + diff --git a/testsuite/tests/gadt/lazypat.hs b/testsuite/tests/gadt/lazypat.hs index f16da207aa..e05e3cb80c 100644 --- a/testsuite/tests/gadt/lazypat.hs +++ b/testsuite/tests/gadt/lazypat.hs @@ -1,7 +1,7 @@ -{-# LANGUAGE GADTs, ExistentialQuantification #-}
-
-module ShouldFail where
-
-data T = forall a. T a (a->Int)
-
-f ~(T x f) = f x
\ No newline at end of file +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +module ShouldFail where + +data T = forall a. T a (a->Int) + +f ~(T x f) = f x diff --git a/testsuite/tests/gadt/lazypatok.hs b/testsuite/tests/gadt/lazypatok.hs index 544705f92d..9903a6653e 100644 --- a/testsuite/tests/gadt/lazypatok.hs +++ b/testsuite/tests/gadt/lazypatok.hs @@ -1,14 +1,14 @@ -{-# LANGUAGE GADTs #-}
-
--- It's not clear whether this one should succed or fail,
--- Arguably it should succeed because the type refinement on
+{-# LANGUAGE GADTs #-} + +-- It's not clear whether this one should succed or fail, +-- Arguably it should succeed because the type refinement on -- T1 should make (y::Int). Currently, though, it fails. -
-module ShouldFail where
-
-data T a where
- T1 :: Int -> T Int
-
-f :: (T a, a) -> Int
-f ~(T1 x, y) = x+y
-
+ +module ShouldFail where + +data T a where + T1 :: Int -> T Int + +f :: (T a, a) -> Int +f ~(T1 x, y) = x+y + diff --git a/testsuite/tests/gadt/rw.hs b/testsuite/tests/gadt/rw.hs index 0d0018ac30..081dc3643b 100644 --- a/testsuite/tests/gadt/rw.hs +++ b/testsuite/tests/gadt/rw.hs @@ -1,29 +1,29 @@ -{-# LANGUAGE GADTs #-}
-
-module Main where
-
-import Data.IORef
-
-data T a where
- Li:: Int -> T Int
- Lb:: Bool -> T Bool
- La:: a -> T a
-
-writeInt:: T a -> IORef a -> IO ()
-writeInt v ref = case v of
- ~(Li x) -> writeIORef ref (1::Int)
-
-readBool:: T a -> IORef a -> IO ()
-readBool v ref = case v of
- ~(Lb x) ->
- readIORef ref >>= (print . not)
-
-tt::T a -> IO ()
-tt v = case v of
- ~(Li x) -> print "OK"
-
-main = do
- tt (La undefined)
- ref <- newIORef undefined
- writeInt (La undefined) ref
- readBool (La undefined) ref
+{-# LANGUAGE GADTs #-} + +module Main where + +import Data.IORef + +data T a where + Li:: Int -> T Int + Lb:: Bool -> T Bool + La:: a -> T a + +writeInt:: T a -> IORef a -> IO () +writeInt v ref = case v of + ~(Li x) -> writeIORef ref (1::Int) + +readBool:: T a -> IORef a -> IO () +readBool v ref = case v of + ~(Lb x) -> + readIORef ref >>= (print . not) + +tt::T a -> IO () +tt v = case v of + ~(Li x) -> print "OK" + +main = do + tt (La undefined) + ref <- newIORef undefined + writeInt (La undefined) ref + readBool (La undefined) ref diff --git a/testsuite/tests/gadt/tc.hs b/testsuite/tests/gadt/tc.hs index 247b9eb615..a476343b3a 100644 --- a/testsuite/tests/gadt/tc.hs +++ b/testsuite/tests/gadt/tc.hs @@ -1,122 +1,122 @@ -{-# LANGUAGE GADTs, ExistentialQuantification #-}
-
--- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
--- demonstrates that it's possible to write functions of type
--- tc :: String -> Term a
--- where Term a is our strongly-typed GADT.
--- That is, generate a typed term from an untyped source; Lennart
--- Augustsson set this as a challenge.
---
--- In fact the main function goes
--- tc :: UTerm -> exists ty. (Ty ty, Term ty)
--- so the type checker returns a pair of an expression and its type,
--- wrapped, of course, in an existential.
-
-module Main where
-
--- Untyped world --------------------------------------------
-data UTerm = UVar String
- | ULam String UType UTerm
- | UApp UTerm UTerm
- | UConBool Bool
- | UIf UTerm UTerm UTerm
-
-data UType = UBool | UArr UType UType
-
--- Typed world -----------------------------------------------
-data Ty t where
- Bool :: Ty Bool
- Arr :: Ty a -> Ty b -> Ty (a -> b)
-
-data Term g t where
- Var :: Var g t -> Term g t
- Lam :: Ty a -> Term (g,a) b -> Term g (a->b)
- App :: Term g (s -> t) -> Term g s -> Term g t
- ConBool :: Bool -> Term g Bool
- If :: Term g Bool -> Term g a -> Term g a -> Term g a
-
-data Var g t where
- ZVar :: Var (h,t) t
- SVar :: Var h t -> Var (h,s) t
-
-data Typed thing = forall ty. Typed (Ty ty) (thing ty)
-
--- Typechecking types
-data ExType = forall t. ExType (Ty t)
-
-tcType :: UType -> ExType
-tcType UBool = ExType Bool
-tcType (UArr t1 t2) = case tcType t1 of { ExType t1' ->
- case tcType t2 of { ExType t2' ->
- ExType (Arr t1' t2') }}
-
--- The type environment and lookup
-data TyEnv g where
- Nil :: TyEnv g
- Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)
-
-lookupVar :: String -> TyEnv g -> Typed (Var g)
-lookupVar _ Nil = error "Variable not found"
-lookupVar v (Cons s ty e)
- | v==s = Typed ty ZVar
- | otherwise = case lookupVar v e of
- Typed ty v -> Typed ty (SVar v)
-
--- Comparing types
-newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) }
-newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) }
-
-cast2 :: Ty a -> Ty b -> (c a -> c b)
-cast2 Bool Bool x = x
-cast2 (Arr a1 a2) (Arr b1 b2) f
- = let C1 x = cast2 a1 b1 (C1 f)
- C2 y = cast2 a2 b2 (C2 x)
- in y
-
-data Equal a b where
- Equal :: Equal c c
-
-cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)
-cmpTy Bool Bool = Just Equal
-cmpTy (Arr a1 a2) (Arr b1 b2)
- = do { Equal <- cmpTy a1 b1
- ; Equal <- cmpTy a2 b2
- ; return Equal }
-
--- Typechecking terms
-tc :: UTerm -> TyEnv g -> Typed (Term g)
-tc (UVar v) env = case lookupVar v env of
- Typed ty v -> Typed ty (Var v)
-tc (UConBool b) env
- = Typed Bool (ConBool b)
-tc (ULam s ty body) env
- = case tcType ty of { ExType bndr_ty' ->
- case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->
- Typed (Arr bndr_ty' body_ty')
- (Lam bndr_ty' body') }}
-tc (UApp e1 e2) env
- = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->
- case tc e2 env of { Typed arg_ty e2' ->
- case cmpTy arg_ty bndr_ty of
- Nothing -> error "Type error"
- Just Equal -> Typed body_ty (App e1' e2') }}
-tc (UIf e1 e2 e3) env
- = case tc e1 env of { Typed Bool e1' ->
- case tc e2 env of { Typed t2 e2' ->
- case tc e3 env of { Typed t3 e3' ->
- case cmpTy t2 t3 of
- Nothing -> error "Type error"
- Just Equal -> Typed t2 (If e1' e2' e3') }}}
-
-showType :: Ty a -> String
-showType Bool = "Bool"
-showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"
-
-uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))
-
-test :: UTerm
-test = UApp uNot (UConBool True)
-
-main = putStrLn (case tc test Nil of
- Typed ty _ -> showType ty
- )
\ No newline at end of file +{-# LANGUAGE GADTs, ExistentialQuantification #-} + +-- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04) +-- demonstrates that it's possible to write functions of type +-- tc :: String -> Term a +-- where Term a is our strongly-typed GADT. +-- That is, generate a typed term from an untyped source; Lennart +-- Augustsson set this as a challenge. +-- +-- In fact the main function goes +-- tc :: UTerm -> exists ty. (Ty ty, Term ty) +-- so the type checker returns a pair of an expression and its type, +-- wrapped, of course, in an existential. + +module Main where + +-- Untyped world -------------------------------------------- +data UTerm = UVar String + | ULam String UType UTerm + | UApp UTerm UTerm + | UConBool Bool + | UIf UTerm UTerm UTerm + +data UType = UBool | UArr UType UType + +-- Typed world ----------------------------------------------- +data Ty t where + Bool :: Ty Bool + Arr :: Ty a -> Ty b -> Ty (a -> b) + +data Term g t where + Var :: Var g t -> Term g t + Lam :: Ty a -> Term (g,a) b -> Term g (a->b) + App :: Term g (s -> t) -> Term g s -> Term g t + ConBool :: Bool -> Term g Bool + If :: Term g Bool -> Term g a -> Term g a -> Term g a + +data Var g t where + ZVar :: Var (h,t) t + SVar :: Var h t -> Var (h,s) t + +data Typed thing = forall ty. Typed (Ty ty) (thing ty) + +-- Typechecking types +data ExType = forall t. ExType (Ty t) + +tcType :: UType -> ExType +tcType UBool = ExType Bool +tcType (UArr t1 t2) = case tcType t1 of { ExType t1' -> + case tcType t2 of { ExType t2' -> + ExType (Arr t1' t2') }} + +-- The type environment and lookup +data TyEnv g where + Nil :: TyEnv g + Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t) + +lookupVar :: String -> TyEnv g -> Typed (Var g) +lookupVar _ Nil = error "Variable not found" +lookupVar v (Cons s ty e) + | v==s = Typed ty ZVar + | otherwise = case lookupVar v e of + Typed ty v -> Typed ty (SVar v) + +-- Comparing types +newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) } +newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) } + +cast2 :: Ty a -> Ty b -> (c a -> c b) +cast2 Bool Bool x = x +cast2 (Arr a1 a2) (Arr b1 b2) f + = let C1 x = cast2 a1 b1 (C1 f) + C2 y = cast2 a2 b2 (C2 x) + in y + +data Equal a b where + Equal :: Equal c c + +cmpTy :: Ty a -> Ty b -> Maybe (Equal a b) +cmpTy Bool Bool = Just Equal +cmpTy (Arr a1 a2) (Arr b1 b2) + = do { Equal <- cmpTy a1 b1 + ; Equal <- cmpTy a2 b2 + ; return Equal } + +-- Typechecking terms +tc :: UTerm -> TyEnv g -> Typed (Term g) +tc (UVar v) env = case lookupVar v env of + Typed ty v -> Typed ty (Var v) +tc (UConBool b) env + = Typed Bool (ConBool b) +tc (ULam s ty body) env + = case tcType ty of { ExType bndr_ty' -> + case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' -> + Typed (Arr bndr_ty' body_ty') + (Lam bndr_ty' body') }} +tc (UApp e1 e2) env + = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' -> + case tc e2 env of { Typed arg_ty e2' -> + case cmpTy arg_ty bndr_ty of + Nothing -> error "Type error" + Just Equal -> Typed body_ty (App e1' e2') }} +tc (UIf e1 e2 e3) env + = case tc e1 env of { Typed Bool e1' -> + case tc e2 env of { Typed t2 e2' -> + case tc e3 env of { Typed t3 e3' -> + case cmpTy t2 t3 of + Nothing -> error "Type error" + Just Equal -> Typed t2 (If e1' e2' e3') }}} + +showType :: Ty a -> String +showType Bool = "Bool" +showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")" + +uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True)) + +test :: UTerm +test = UApp uNot (UConBool True) + +main = putStrLn (case tc test Nil of + Typed ty _ -> showType ty + ) |