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.

1 files changed, 31 insertions, 34 deletions

diff --git a/compiler/nativeGen/SPARC/CodeGen/Gen64.hs b/compiler/nativeGen/SPARC/CodeGen/Gen64.hs
index 1942891c77..f186d437d0 100644
--- a/compiler/nativeGen/SPARC/CodeGen/Gen64.hs
+++ b/compiler/nativeGen/SPARC/CodeGen/Gen64.hs
@@ -27,30 +27,30 @@ import OrdList
 import Outputable
 
 -- | Code to assign a 64 bit value to memory.
-assignMem_I64Code 
+assignMem_I64Code
         :: CmmExpr              -- ^ expr producing the destination address
         -> CmmExpr              -- ^ expr producing the source value.
         -> NatM InstrBlock
 
-assignMem_I64Code addrTree valueTree 
+assignMem_I64Code addrTree valueTree
  = do
-     ChildCode64 vcode rlo      <- iselExpr64 valueTree  
+     ChildCode64 vcode rlo      <- iselExpr64 valueTree
 
      (src, acode) <- getSomeReg addrTree
-     let 
+     let
          rhi = getHiVRegFromLo rlo
- 
+
          -- Big-endian store
          mov_hi = ST II32 rhi (AddrRegImm src (ImmInt 0))
          mov_lo = ST II32 rlo (AddrRegImm src (ImmInt 4))
-         
+
          code   = vcode `appOL` acode `snocOL` mov_hi `snocOL` mov_lo
 
-{-     pprTrace "assignMem_I64Code" 
+{-     pprTrace "assignMem_I64Code"
         (vcat   [ text "addrTree:  " <+> ppr addrTree
                 , text "valueTree: " <+> ppr valueTree
                 , text "vcode:"
-                , vcat $ map ppr $ fromOL vcode 
+                , vcat $ map ppr $ fromOL vcode
                 , text ""
                 , text "acode:"
                 , vcat $ map ppr $ fromOL acode ])
@@ -59,15 +59,15 @@ assignMem_I64Code addrTree valueTree
 
 
 -- | Code to assign a 64 bit value to a register.
-assignReg_I64Code 
+assignReg_I64Code
         :: CmmReg               -- ^ the destination register
         -> CmmExpr              -- ^ expr producing the source value
         -> NatM InstrBlock
 
-assignReg_I64Code (CmmLocal (LocalReg u_dst pk)) valueTree 
+assignReg_I64Code (CmmLocal (LocalReg u_dst pk)) valueTree
  = do
-     ChildCode64 vcode r_src_lo <- iselExpr64 valueTree    
-     let 
+     ChildCode64 vcode r_src_lo <- iselExpr64 valueTree
+     let
          r_dst_lo = RegVirtual $ mkVirtualReg u_dst (cmmTypeFormat pk)
          r_dst_hi = getHiVRegFromLo r_dst_lo
          r_src_hi = getHiVRegFromLo r_src_lo
@@ -88,7 +88,7 @@ assignReg_I64Code _ _
 iselExpr64 :: CmmExpr -> NatM ChildCode64
 
 -- Load a 64 bit word
-iselExpr64 (CmmLoad addrTree ty) 
+iselExpr64 (CmmLoad addrTree ty)
  | isWord64 ty
  = do   Amode amode addr_code   <- getAmode addrTree
         let result
@@ -98,8 +98,8 @@ iselExpr64 (CmmLoad addrTree ty)
                         tmp     <- getNewRegNat II32
                         let rhi = getHiVRegFromLo rlo
 
-                        return  $ ChildCode64 
-                                (        addr_code 
+                        return  $ ChildCode64
+                                (        addr_code
                                 `appOL`  toOL
                                          [ ADD False False r1 (RIReg r2) tmp
                                          , LD II32 (AddrRegImm tmp (ImmInt 0)) rhi
@@ -109,9 +109,9 @@ iselExpr64 (CmmLoad addrTree ty)
                 | AddrRegImm r1 (ImmInt i) <- amode
                 = do    rlo     <- getNewRegNat II32
                         let rhi = getHiVRegFromLo rlo
-                        
-                        return  $ ChildCode64 
-                                (        addr_code 
+
+                        return  $ ChildCode64
+                                (        addr_code
                                 `appOL`  toOL
                                          [ LD II32 (AddrRegImm r1 (ImmInt $ 0 + i)) rhi
                                          , LD II32 (AddrRegImm r1 (ImmInt $ 4 + i)) rlo ])
@@ -119,23 +119,23 @@ iselExpr64 (CmmLoad addrTree ty)
 
                 | otherwise
                 = panic "SPARC.CodeGen.Gen64: no match"
-                
+
         result
 
 
 -- Add a literal to a 64 bit integer
-iselExpr64 (CmmMachOp (MO_Add _) [e1, CmmLit (CmmInt i _)]) 
+iselExpr64 (CmmMachOp (MO_Add _) [e1, CmmLit (CmmInt i _)])
  = do   ChildCode64 code1 r1_lo <- iselExpr64 e1
         let r1_hi       = getHiVRegFromLo r1_lo
-        
+
         r_dst_lo        <- getNewRegNat II32
-        let r_dst_hi    =  getHiVRegFromLo r_dst_lo 
-        
+        let r_dst_hi    =  getHiVRegFromLo r_dst_lo
+
         let code =      code1
                 `appOL` toOL
                         [ ADD False True  r1_lo (RIImm (ImmInteger i)) r_dst_lo
                         , ADD True  False r1_hi (RIReg g0)         r_dst_hi ]
-                        
+
         return  $ ChildCode64 code r_dst_lo
 
 
@@ -146,21 +146,21 @@ iselExpr64 (CmmMachOp (MO_Add _) [e1, e2])
 
         ChildCode64 code2 r2_lo <- iselExpr64 e2
         let r2_hi       = getHiVRegFromLo r2_lo
-        
+
         r_dst_lo        <- getNewRegNat II32
         let r_dst_hi    = getHiVRegFromLo r_dst_lo
-        
+
         let code =      code1
                 `appOL` code2
                 `appOL` toOL
                         [ ADD False True  r1_lo (RIReg r2_lo) r_dst_lo
                         , ADD True  False r1_hi (RIReg r2_hi) r_dst_hi ]
-        
+
         return  $ ChildCode64 code r_dst_lo
 
 
-iselExpr64 (CmmReg (CmmLocal (LocalReg uq ty))) 
- | isWord64 ty 
+iselExpr64 (CmmReg (CmmLocal (LocalReg uq ty)))
+ | isWord64 ty
  = do
      r_dst_lo <-  getNewRegNat II32
      let r_dst_hi = getHiVRegFromLo r_dst_lo
@@ -174,7 +174,7 @@ iselExpr64 (CmmReg (CmmLocal (LocalReg uq ty)))
          )
 
 -- Convert something into II64
-iselExpr64 (CmmMachOp (MO_UU_Conv _ W64) [expr]) 
+iselExpr64 (CmmMachOp (MO_UU_Conv _ W64) [expr])
  = do
         r_dst_lo        <- getNewRegNat II32
         let r_dst_hi    = getHiVRegFromLo r_dst_lo
@@ -188,12 +188,9 @@ iselExpr64 (CmmMachOp (MO_UU_Conv _ W64) [expr])
                 `appOL` toOL
                         [ mkRegRegMoveInstr platform g0    r_dst_hi     -- clear high 32 bits
                         , mkRegRegMoveInstr platform a_reg r_dst_lo ]
-                        
+
         return  $ ChildCode64 code r_dst_lo
 
 
 iselExpr64 expr
    = pprPanic "iselExpr64(sparc)" (ppr expr)
-
-
-