Testsuite: delete Windows line endings [skip ci] (#11631)

14 files changed, 650 insertions, 650 deletions

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
+                )