Add kind equalities to GHC.

This implements the ideas originally put forward in
"System FC with Explicit Kind Equality" (ICFP'13).

There are several noteworthy changes with this patch:
 * We now have casts in types. These change the kind
   of a type. See new constructor `CastTy`.

 * All types and all constructors can be promoted.
   This includes GADT constructors. GADT pattern matches
   take place in type family equations. In Core,
   types can now be applied to coercions via the
   `CoercionTy` constructor.

 * Coercions can now be heterogeneous, relating types
   of different kinds. A coercion proving `t1 :: k1 ~ t2 :: k2`
   proves both that `t1` and `t2` are the same and also that
   `k1` and `k2` are the same.

 * The `Coercion` type has been significantly enhanced.
   The documentation in `docs/core-spec/core-spec.pdf` reflects
   the new reality.

 * The type of `*` is now `*`. No more `BOX`.

 * Users can write explicit kind variables in their code,
   anywhere they can write type variables. For backward compatibility,
   automatic inference of kind-variable binding is still permitted.

 * The new extension `TypeInType` turns on the new user-facing
   features.

 * Type families and synonyms are now promoted to kinds. This causes
   trouble with parsing `*`, leading to the somewhat awkward new
   `HsAppsTy` constructor for `HsType`. This is dispatched with in
   the renamer, where the kind `*` can be told apart from a
   type-level multiplication operator. Without `-XTypeInType` the
   old behavior persists. With `-XTypeInType`, you need to import
   `Data.Kind` to get `*`, also known as `Type`.

 * The kind-checking algorithms in TcHsType have been significantly
   rewritten to allow for enhanced kinds.

 * The new features are still quite experimental and may be in flux.

 * TODO: Several open tickets: #11195, #11196, #11197, #11198, #11203.

 * TODO: Update user manual.

Tickets addressed: #9017, #9173, #7961, #10524, #8566, #11142.
Updates Haddock submodule.

10 files changed, 110 insertions, 34 deletions

diff --git a/compiler/utils/Bag.hs b/compiler/utils/Bag.hs
index 4a826fbf4a..d85465081b 100644
--- a/compiler/utils/Bag.hs
+++ b/compiler/utils/Bag.hs
@@ -6,7 +6,7 @@
 Bag: an unordered collection with duplicates
 -}
 
-{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables #-}
+{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, CPP #-}
 
 module Bag (
         Bag, -- abstract type
diff --git a/compiler/utils/ListSetOps.hs b/compiler/utils/ListSetOps.hs
index 54faa4f600..207a00cfc1 100644
--- a/compiler/utils/ListSetOps.hs
+++ b/compiler/utils/ListSetOps.hs
@@ -30,22 +30,9 @@ import Util
 
 import Data.List
 
-{-
----------
-#ifndef DEBUG
-getNth :: [a] -> Int -> a
-getNth xs n = xs !! n
-#else
-getNth :: Outputable a => [a] -> Int -> a
-getNth xs n = ASSERT2( xs `lengthAtLeast` n, ppr n $$ ppr xs )
-              xs !! n
-#endif
-----------
--}
-
 getNth :: Outputable a => [a] -> Int -> a
 getNth xs n = ASSERT2( xs `lengthExceeds` n, ppr n $$ ppr xs )
-              xs !! n
+             xs !! n
 
 {-
 ************************************************************************
diff --git a/compiler/utils/MonadUtils.hs b/compiler/utils/MonadUtils.hs
index 255a0f50f6..36eb574e78 100644
--- a/compiler/utils/MonadUtils.hs
+++ b/compiler/utils/MonadUtils.hs
@@ -11,8 +11,8 @@ module MonadUtils
 
         , liftIO1, liftIO2, liftIO3, liftIO4
 
-        , zipWith3M, zipWith3M_, zipWithAndUnzipM
-        , mapAndUnzipM, mapAndUnzip3M, mapAndUnzip4M
+        , zipWith3M, zipWith3M_, zipWith4M, zipWithAndUnzipM
+        , mapAndUnzipM, mapAndUnzip3M, mapAndUnzip4M, mapAndUnzip5M
         , mapAccumLM
         , mapSndM
         , concatMapM
@@ -76,6 +76,19 @@ zipWith3M_ :: Monad m => (a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m ()
 zipWith3M_ f as bs cs = do { _ <- zipWith3M f as bs cs
                            ; return () }
 
+zipWith4M :: Monad m => (a -> b -> c -> d -> m e)
+          -> [a] -> [b] -> [c] -> [d] -> m [e]
+zipWith4M _ []     _      _      _      = return []
+zipWith4M _ _      []     _      _      = return []
+zipWith4M _ _      _      []     _      = return []
+zipWith4M _ _      _      _      []     = return []
+zipWith4M f (x:xs) (y:ys) (z:zs) (a:as)
+  = do { r  <- f x y z a
+       ; rs <- zipWith4M f xs ys zs as
+       ; return $ r:rs
+       }
+
+
 zipWithAndUnzipM :: Monad m
                  => (a -> b -> m (c, d)) -> [a] -> [b] -> m ([c], [d])
 {-# INLINE zipWithAndUnzipM #-}
@@ -102,6 +115,13 @@ mapAndUnzip4M f (x:xs) = do
     (rs1, rs2, rs3, rs4) <- mapAndUnzip4M f xs
     return (r1:rs1, r2:rs2, r3:rs3, r4:rs4)
 
+mapAndUnzip5M :: Monad m => (a -> m (b,c,d,e,f)) -> [a] -> m ([b],[c],[d],[e],[f])
+mapAndUnzip5M _ [] = return ([],[],[],[],[])
+mapAndUnzip5M f (x:xs) = do
+    (r1, r2, r3, r4, r5)      <- f x
+    (rs1, rs2, rs3, rs4, rs5) <- mapAndUnzip5M f xs
+    return (r1:rs1, r2:rs2, r3:rs3, r4:rs4, r5:rs5)
+
 -- | Monadic version of mapAccumL
 mapAccumLM :: Monad m
             => (acc -> x -> m (acc, y)) -- ^ combining funcction
diff --git a/compiler/utils/Outputable.hs b/compiler/utils/Outputable.hs
index 40acbf1d70..8f30f0076e 100644
--- a/compiler/utils/Outputable.hs
+++ b/compiler/utils/Outputable.hs
@@ -75,7 +75,7 @@ module Outputable (
 
         -- * Error handling and debugging utilities
         pprPanic, pprSorry, assertPprPanic, pprPgmError,
-        pprTrace, warnPprTrace, pprSTrace,
+        pprTrace, pprTraceIt, warnPprTrace, pprSTrace,
         trace, pgmError, panic, sorry, assertPanic,
         pprDebugAndThen,
     ) where
@@ -256,6 +256,12 @@ mkUserStyle unqual depth
    | opt_PprStyle_Debug = PprDebug
    | otherwise          = PprUser unqual depth
 
+instance Outputable PprStyle where
+  ppr (PprUser {})  = text "user-style"
+  ppr (PprCode {})  = text "code-style"
+  ppr (PprDump {})  = text "dump-style"
+  ppr (PprDebug {}) = text "debug-style"
+
 {-
 Orthogonal to the above printing styles are (possibly) some
 command-line flags that affect printing (often carried with the
@@ -698,6 +704,11 @@ instance Outputable Bool where
     ppr True  = ptext (sLit "True")
     ppr False = ptext (sLit "False")
 
+instance Outputable Ordering where
+    ppr LT = text "LT"
+    ppr EQ = text "EQ"
+    ppr GT = text "GT"
+
 instance Outputable Int32 where
    ppr n = integer $ fromIntegral n
 
@@ -1052,6 +1063,10 @@ pprTrace str doc x
    | opt_NoDebugOutput = x
    | otherwise         = pprDebugAndThen unsafeGlobalDynFlags trace (text str) doc x
 
+-- | @pprTraceIt desc x@ is equivalent to @pprTrace desc (ppr x) x@
+pprTraceIt :: Outputable a => String -> a -> a
+pprTraceIt desc x = pprTrace desc (ppr x) x
+
 
 -- | If debug output is on, show some 'SDoc' on the screen along
 -- with a call stack when available.
diff --git a/compiler/utils/Pair.hs b/compiler/utils/Pair.hs
index b33ccbac06..8747e619ca 100644
--- a/compiler/utils/Pair.hs
+++ b/compiler/utils/Pair.hs
@@ -5,7 +5,7 @@ Traversable instances.
 
 {-# LANGUAGE CPP #-}
 
-module Pair ( Pair(..), unPair, toPair, swap ) where
+module Pair ( Pair(..), unPair, toPair, swap, pLiftFst, pLiftSnd ) where
 
 #include "HsVersions.h"
 
@@ -37,6 +37,10 @@ instance Foldable Pair where
 instance Traversable Pair where
   traverse f (Pair x y) = Pair <$> f x <*> f y
 
+instance Monoid a => Monoid (Pair a) where
+  mempty = Pair mempty mempty
+  Pair a1 b1 `mappend` Pair a2 b2 = Pair (a1 `mappend` a2) (b1 `mappend` b2)
+
 instance Outputable a => Outputable (Pair a) where
   ppr (Pair a b) = ppr a <+> char '~' <+> ppr b
 
@@ -48,3 +52,9 @@ toPair (x,y) = Pair x y
 
 swap :: Pair a -> Pair a
 swap (Pair x y) = Pair y x
+
+pLiftFst :: (a -> a) -> Pair a -> Pair a
+pLiftFst f (Pair a b) = Pair (f a) b
+
+pLiftSnd :: (a -> a) -> Pair a -> Pair a
+pLiftSnd f (Pair a b) = Pair a (f b)
diff --git a/compiler/utils/Serialized.hs b/compiler/utils/Serialized.hs
index 01fa071cab..41c1cea03f 100644
--- a/compiler/utils/Serialized.hs
+++ b/compiler/utils/Serialized.hs
@@ -9,10 +9,10 @@ module Serialized (
     -- * Main Serialized data type
     Serialized,
     seqSerialized,
-    
+
     -- * Going into and out of 'Serialized'
     toSerialized, fromSerialized,
-    
+
     -- * Handy serialization functions
     serializeWithData, deserializeWithData,
   ) where
diff --git a/compiler/utils/UniqDFM.hs b/compiler/utils/UniqDFM.hs
index aeb5b34116..e5424f2c5d 100644
--- a/compiler/utils/UniqDFM.hs
+++ b/compiler/utils/UniqDFM.hs
@@ -41,6 +41,7 @@ module UniqDFM (
         isNullUDFM,
         sizeUDFM,
         intersectUDFM,
+        intersectsUDFM,
         disjointUDFM,
         minusUDFM,
         partitionUDFM,
@@ -228,6 +229,9 @@ intersectUDFM (UDFM x i) (UDFM y _j) = UDFM (M.intersection x y) i
   -- M.intersection is left biased, that means the result will only have
   -- a subset of elements from the left set, so `i` is a good upper bound.
 
+intersectsUDFM :: UniqDFM elt -> UniqDFM elt -> Bool
+intersectsUDFM x y = isNullUDFM (x `intersectUDFM` y)
+
 disjointUDFM :: UniqDFM elt -> UniqDFM elt -> Bool
 disjointUDFM (UDFM x _i) (UDFM y _j) = M.null (M.intersection x y)
 
diff --git a/compiler/utils/UniqDSet.hs b/compiler/utils/UniqDSet.hs
index 85c5126e57..45ed241df1 100644
--- a/compiler/utils/UniqDSet.hs
+++ b/compiler/utils/UniqDSet.hs
@@ -13,7 +13,7 @@ module UniqDSet (
         UniqDSet,    -- type synonym for UniqFM a
 
         -- ** Manipulating these sets
-        delOneFromUniqDSet,
+        delOneFromUniqDSet, delListFromUniqDSet,
         emptyUniqDSet,
         unitUniqDSet,
         mkUniqDSet,
@@ -21,6 +21,7 @@ module UniqDSet (
         unionUniqDSets, unionManyUniqDSets,
         minusUniqDSet,
         intersectUniqDSets,
+        intersectsUniqDSets,
         foldUniqDSet,
         elementOfUniqDSet,
         filterUniqDSet,
@@ -28,8 +29,7 @@ module UniqDSet (
         isEmptyUniqDSet,
         lookupUniqDSet,
         uniqDSetToList,
-        partitionUniqDSet,
-        delListFromUniqDSet,
+        partitionUniqDSet
     ) where
 
 import UniqDFM
@@ -55,6 +55,9 @@ addListToUniqDSet = foldl addOneToUniqDSet
 delOneFromUniqDSet :: Uniquable a => UniqDSet a -> a -> UniqDSet a
 delOneFromUniqDSet = delFromUDFM
 
+delListFromUniqDSet :: Uniquable a => UniqDSet a -> [a] -> UniqDSet a
+delListFromUniqDSet = delListFromUDFM
+
 unionUniqDSets :: UniqDSet a -> UniqDSet a -> UniqDSet a
 unionUniqDSets = plusUDFM
 
@@ -68,6 +71,9 @@ minusUniqDSet = minusUDFM
 intersectUniqDSets :: UniqDSet a -> UniqDSet a -> UniqDSet a
 intersectUniqDSets = intersectUDFM
 
+intersectsUniqDSets :: UniqDSet a -> UniqDSet a -> Bool
+intersectsUniqDSets = intersectsUDFM
+
 foldUniqDSet :: (a -> b -> b) -> b -> UniqDSet a -> b
 foldUniqDSet = foldUDFM
 
@@ -91,6 +97,3 @@ uniqDSetToList = eltsUDFM
 
 partitionUniqDSet :: (a -> Bool) -> UniqDSet a -> (UniqDSet a, UniqDSet a)
 partitionUniqDSet = partitionUDFM
-
-delListFromUniqDSet :: Uniquable a => UniqDSet a -> [a] -> UniqDSet a
-delListFromUniqDSet = delListFromUDFM
diff --git a/compiler/utils/UniqSet.hs b/compiler/utils/UniqSet.hs
index 4ceeec0000..a3d503f6eb 100644
--- a/compiler/utils/UniqSet.hs
+++ b/compiler/utils/UniqSet.hs
@@ -71,7 +71,7 @@ partitionUniqSet :: (a -> Bool) -> UniqSet a -> (UniqSet a, UniqSet a)
 
 sizeUniqSet :: UniqSet a -> Int
 isEmptyUniqSet :: UniqSet a -> Bool
-lookupUniqSet :: Uniquable a => UniqSet a -> a -> Maybe a
+lookupUniqSet :: Uniquable a => UniqSet b -> a -> Maybe b
 uniqSetToList :: UniqSet a -> [a]
 
 {-
diff --git a/compiler/utils/Util.hs b/compiler/utils/Util.hs
index d3830c3949..75c0c79ea2 100644
--- a/compiler/utils/Util.hs
+++ b/compiler/utils/Util.hs
@@ -14,7 +14,7 @@ module Util (
         zipEqual, zipWithEqual, zipWith3Equal, zipWith4Equal,
         zipLazy, stretchZipWith, zipWithAndUnzip,
 
-        filterByList,
+        filterByList, partitionByList,
 
         unzipWith,
 
@@ -22,7 +22,7 @@ module Util (
         mapAndUnzip, mapAndUnzip3, mapAccumL2,
         nOfThem, filterOut, partitionWith, splitEithers,
 
-        dropWhileEndLE,
+        dropWhileEndLE, spanEnd,
 
         foldl1', foldl2, count, all2,
 
@@ -36,10 +36,11 @@ module Util (
         isIn, isn'tIn,
 
         -- * Tuples
-        fstOf3, sndOf3, thirdOf3,
+        fstOf3, sndOf3, thdOf3,
         firstM, first3M,
-        third3,
+        fst3, snd3, third3,
         uncurry3,
+        liftFst, liftSnd,
 
         -- * List operations controlled by another list
         takeList, dropList, splitAtList, split,
@@ -215,10 +216,16 @@ nTimes n f = f . nTimes (n-1) f
 
 fstOf3   :: (a,b,c) -> a
 sndOf3   :: (a,b,c) -> b
-thirdOf3 :: (a,b,c) -> c
+thdOf3   :: (a,b,c) -> c
 fstOf3      (a,_,_) =  a
 sndOf3      (_,b,_) =  b
-thirdOf3    (_,_,c) =  c
+thdOf3      (_,_,c) =  c
+
+fst3 :: (a -> d) -> (a, b, c) -> (d, b, c)
+fst3 f (a, b, c) = (f a, b, c)
+
+snd3 :: (b -> d) -> (a, b, c) -> (a, d, c)
+snd3 f (a, b, c) = (a, f b, c)
 
 third3 :: (c -> d) -> (a, b, c) -> (a, b, d)
 third3 f (a, b, c) = (a, b, f c)
@@ -226,6 +233,12 @@ third3 f (a, b, c) = (a, b, f c)
 uncurry3 :: (a -> b -> c -> d) -> (a, b, c) -> d
 uncurry3 f (a, b, c) = f a b c
 
+liftFst :: (a -> b) -> (a, c) -> (b, c)
+liftFst f (a,c) = (f a, c)
+
+liftSnd :: (a -> b) -> (c, a) -> (c, b)
+liftSnd f (c,a) = (c, f a)
+
 firstM :: Monad m => (a -> m c) -> (a, b) -> m (c, b)
 firstM f (x, y) = liftM (\x' -> (x', y)) (f x)
 
@@ -319,6 +332,19 @@ filterByList (True:bs)  (x:xs) = x : filterByList bs xs
 filterByList (False:bs) (_:xs) =     filterByList bs xs
 filterByList _          _      = []
 
+-- | 'partitionByList' takes a list of Bools and a list of some elements and
+-- partitions the list according to the list of Bools. Elements corresponding
+-- to 'True' go to the left; elements corresponding to 'False' go to the right.
+-- For example, @partitionByList [True, False, True] [1,2,3] == ([1,3], [2])@
+-- This function does not check whether the lists have equal
+-- length.
+partitionByList :: [Bool] -> [a] -> ([a], [a])
+partitionByList = go [] []
+  where
+    go trues falses (True  : bs) (x : xs) = go (x:trues) falses bs xs
+    go trues falses (False : bs) (x : xs) = go trues (x:falses) bs xs
+    go trues falses _ _ = (reverse trues, reverse falses)
+
 stretchZipWith :: (a -> Bool) -> b -> (a->b->c) -> [a] -> [b] -> [c]
 -- ^ @stretchZipWith p z f xs ys@ stretches @ys@ by inserting @z@ in
 -- the places where @p@ returns @True@
@@ -601,6 +627,17 @@ dropTail n xs
 dropWhileEndLE :: (a -> Bool) -> [a] -> [a]
 dropWhileEndLE p = foldr (\x r -> if null r && p x then [] else x:r) []
 
+-- | @spanEnd p l == reverse (span p (reverse l))@. The first list
+-- returns actually comes after the second list (when you look at the
+-- input list).
+spanEnd :: (a -> Bool) -> [a] -> ([a], [a])
+spanEnd p l = go l [] [] l
+  where go yes _rev_yes rev_no [] = (yes, reverse rev_no)
+        go yes rev_yes  rev_no (x:xs)
+          | p x       = go yes (x : rev_yes) rev_no                  xs
+          | otherwise = go xs  []            (x : rev_yes ++ rev_no) xs
+
+
 snocView :: [a] -> Maybe ([a],a)
         -- Split off the last element
 snocView [] = Nothing