Fix bug in type-checking case expressions

Ignore-this: aefce547baa908229cf7112641d53501

darcs-hash:20111024123413-e29d1-2ae697e151eaf78920ae7994c430f7bb047757fb.gz

examples/InchPrelude.hs

@@ -3,14 +3,15 @@
 
 module InchPrelude where
 
-import Prelude hiding (subtract, const, flip, maybe, either,
-                         curry, uncurry, until, asTypeOf, map,
-                         filter, concat, concatMap, head, tail,
-                         last, init, null, length, foldl, foldl1,
+import Prelude hiding (subtract, const, flip, maybe, either, curry,
+                         uncurry, until, asTypeOf, map, filter,
+                         concat, concatMap, head, tail, last, init,
+                         null, length, foldl, foldl1, scanl, scanl1,
                          foldr, foldr1, iterate, repeat, replicate,
-                         take, drop, splitAt, takeWhile, reverse,
-                         and, or, any, all, sum, product, maximum,
-                         minimum, zip, zipWith, zipWith3)
+                         take, drop, splitAt, takeWhile, unlines,
+                         unwords, reverse, and, or, any, all, sum,
+                         product, maximum, minimum, zip, zipWith,
+                         zipWith3)
 
 -- Numeric functions
 
@@ -262,22 +263,15 @@ foldl1           :: (a -> a -> a) -> [a] -> a
 foldl1 f (x:xs)  =  foldl f x xs
 foldl1 _ []      =  error "Prelude.foldl1: empty list"
 
-
-{-
--- Why doesn't this type check?
 scanl            :: (a -> b -> a) -> a -> [b] -> [a]
 scanl f q xs     =  q : (case xs of
                             []   -> []
                             x:xs -> scanl f (f q x) xs
                         )
 
-
 scanl1           :: (a -> a -> a) -> [a] -> [a]
 scanl1 f (x:xs)  =  scanl f x xs
 scanl1 _ []      =  []
--}
-
-
 
 foldr            :: (a -> b -> b) -> b -> [a] -> b
 foldr f z []     =  z
@@ -317,11 +311,9 @@ repeat x         =  xs where xs = x:xs
 replicate        :: Integer -> a -> [a]
 replicate n x    =  take n (repeat x)
 
-{-
 cycle            :: [a] -> [a]
 cycle []         =  error "Prelude.cycle: empty list"
-cycle xs         =  xs' where xs' = xs ++ xs'
--}
+cycle xs         =  xs' where xs' = append xs xs'
 
 take                   :: Integer -> [a] -> [a]
 -- take n _      | n <= 0 =  []
@@ -385,24 +377,20 @@ words s          =  case dropWhile Char.isSpace s of
                       "" -> []
                       s' -> w : words s''
                             where (w, s'') = break Char.isSpace s'
+-}
 
+unlines          :: [[Char]] -> [Char]
+unlines          =  concatMap (\ x -> append x "\n")
 
-unlines          :: [String] -> String
-unlines          =  concatMap (++ "\n")
 
 
-unwords          :: [String] -> String
+unwords          :: [[Char]] -> [Char]
 unwords []       =  ""
-unwords ws       =  foldr1 (\w s -> w ++ ' ':s) ws
--}
-
-
+unwords ws       =  foldr1 (\w s -> append w (' ':s)) ws
 
 reverse          :: [a] -> [a]
 reverse          =  foldl (flip (:)) []
 
-
-
 and              :: [Bool] -> Bool
 and              =  foldr amp True
 or               =  foldr bar False

src/Language/Inch/TypeCheck.lhs

@@ -365,7 +365,7 @@ status.
 >   inLocation (text "in case alternative" <++> prettyHigh c) $
 >   withLayer CaseTop $ do
 >     ca <- checkPat True (sty --> resty) (p :! P0) $ \ (p :! P0, ex, vs, rty) -> do
->       gt <- checkGuardTerms sty (rawCoerce gt)
+>       gt <- checkGuardTerms rty (rawCoerce gt)
 >       return $ CaseAlt p (renameTypes (renameVS vs) gt)
 >     unifySolveConstraints
 >     solveConstraints
@@ -377,7 +377,7 @@ status.
 >   inLocation (text "in case alternative" <++> prettyHigh c) $
 >    withLayer CaseTop $ do
 >     ca <- checkPat True (sty --> resty) (p :! P0) $ \ (p :! P0, ex, vs, rty) -> do
->       gt <- checkGuardTerms resty (rawCoerce gt)
+>       gt <- checkGuardTerms rty (rawCoerce gt)
 >       return $ CaseAlt p (renameTypes (renameVS vs) gt)
 >     return $ ca ::: resty
 

tests/Main.lhs

@@ -483,9 +483,11 @@
 >   ("f () = ()\ng (x, y) = (y, x)", True) : 
 >   ("f () = ()\nf (x, y) = (y, x)", False) : 
 >   ("f xs = case xs of\n      [] -> []\n      y:ys -> y : f ys", True) :
->   ("scanl            :: (a -> b -> a) -> a -> [b] -> [a]\nscanl f q xs     =  q : (case xs of\n                            []   -> []\n                            x:xs -> scanl f (f q x) xs\n                        )", True) :
+>   ("scanl            :: (a -> b -> a) -> a -> [b] -> [a]\nscanl f q xs     =  q : (case xs of\n                            []   -> []\n                            x:ys -> scanl f (f q x) ys\n                        )", True) :
 >   ("a = \"hello\"", True) :
 >   ("b w = w : 'o' : 'r' : ['l', 'd']", True) :
 >   ("x = y\n  where y = 3", True) :
 >   ("f x | z = 3\n   | otherwise = 2\n  where z = x", True) :
+>   ("f = case True of True -> 3", True) :
+>   ("f :: Integer\nf = case True of True -> 3", True) :
 >   []