Hurrah! This major commit adds support for scoped kind variables,

which (finally) fills out the functionality of polymorphic kinds.
It also fixes numerous bugs.

Main changes are:

Renaming stuff
~~~~~~~~~~~~~~
* New type in HsTypes:
     data HsBndrSig sig = HsBSig sig [Name]
  which is used for type signatures in patterns, and kind signatures
  in types.  So when you say
       f (x :: [a]) = x ++ x
  or
       data T (f :: k -> *) (x :: *) = MkT (f x)
  the signatures in both cases are a HsBndrSig.

* The [Name] in HsBndrSig records the variables bound by the
  pattern, that is 'a' in the first example, 'k' in the second,
  and nothing in the third.  The renamer initialises the field.

* As a result I was able to get rid of
     RnHsSyn.extractHsTyNames :: LHsType Name -> NameSet
  and its friends altogether.  Deleted the entire module!
  This led to some knock-on refactoring; in particular the
  type renamer now returns the free variables just like the
  term renamer.

Kind-checking types: mainly TcHsType
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A major change is that instead of kind-checking types in two
passes, we now do one. Under the old scheme, the first pass did
kind-checking and (hackily) annotated the HsType with the
inferred kinds; and the second pass desugared the HsType to a
Type.  But now that we have kind variables inside types, the
first pass (TcHsType.tc_hs_type) can go straight to Type, and
zonking will squeeze out any kind unification variables later.

This is much nicer, but it was much more fiddly than I had expected.

The nastiest corner is this: it's very important that tc_hs_type
uses lazy constructors to build the returned type. See
Note [Zonking inside the knot] in TcHsType.

Type-checking type and class declarations: mainly TcTyClsDecls
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I did tons of refactoring in TcTyClsDecls.  Simpler and nicer now.

Typechecking bindings: mainly TcBinds
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
I rejigged (yet again) the handling of type signatures in TcBinds.
It's a bit simpler now.  The main change is that tcTySigs goes
right through to a TcSigInfo in one step; previously it was split
into two, part here and part later.

Unsafe coercions
~~~~~~~~~~~~~~~~
Usually equality coercions have exactly the same kind on both
sides.  But we do allow an *unsafe* coercion between Int# and Bool,
say, used in
    case error Bool "flah" of { True -> 3#; False -> 0# }
-->
    (error Bool "flah") |> unsafeCoerce Bool Int#

So what is the instantiation of (~#) here?
   unsafeCoerce Bool Int# :: (~#) ??? Bool Int#
I'm using OpenKind here for now, but it's un-satisfying that
the lhs and rhs of the ~ don't have precisely the same kind.

More minor
~~~~~~~~~~
* HsDecl.TySynonym has its free variables attached, which makes
  the cycle computation in TcTyDecls.mkSynEdges easier.

* Fixed a nasty reversed-comparison bug in FamInstEnv:
  @@ -490,7 +490,7 @@ lookup_fam_inst_env' match_fun one_sided ie fam tys
     n_tys = length tys
     extra_tys = drop arity tys
     (match_tys, add_extra_tys)
-       | arity > n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
+       | arity < n_tys = (take arity tys, \res_tys -> res_tys ++ extra_tys)
        | otherwise     = (tys,            \res_tys -> res_tys)

1 files changed, 15 insertions, 15 deletions

diff --git a/compiler/stgSyn/StgLint.lhs b/compiler/stgSyn/StgLint.lhs
index ea1fab7eea..9ccdfc32ed 100644
--- a/compiler/stgSyn/StgLint.lhs
+++ b/compiler/stgSyn/StgLint.lhs
@@ -121,10 +121,10 @@ lint_binds_help (binder, rhs)
                (mkUnLiftedTyMsg binder rhs)
 
         -- Check match to RHS type
-	-- Actually we *can't* check the RHS type, because
-	-- unsafeCoerce means it really might not match at all
-	-- notably;  eg x::Int = (error @Bool "urk") |> unsafeCoerce...
-	-- case maybe_rhs_ty of
+        -- Actually we *can't* check the RHS type, because
+        -- unsafeCoerce means it really might not match at all
+        -- notably;  eg x::Int = (error @Bool "urk") |> unsafeCoerce...
+        -- case maybe_rhs_ty of
         --  Nothing     -> return ()
         --    Just rhs_ty -> checkTys binder_ty
         --                          rhs_ty
@@ -237,8 +237,8 @@ lintStgAlts alts scrut_ty = do
                            return (Just first_ty)
         where
           -- check ty = checkTys first_ty ty (mkCaseAltMsg alts)
-	  -- We can't check that the alternatives have the
-	  -- same type, becuase they don't, with unsafeCoerce#
+          -- We can't check that the alternatives have the
+          -- same type, becuase they don't, with unsafeCoerce#
 
 lintAlt :: Type -> (AltCon, [Id], [Bool], StgExpr) -> LintM (Maybe Type)
 lintAlt _ (DEFAULT, _, _, rhs)
@@ -398,8 +398,8 @@ checkFunApp fun_ty arg_tys msg
  where
   (mb_ty, mb_msg) = cfa True fun_ty arg_tys
 
-  cfa :: Bool -> Type -> [Type] -> (Maybe Type		-- Accurate result?
-                                   , Maybe MsgDoc)	-- Errors?
+  cfa :: Bool -> Type -> [Type] -> (Maybe Type          -- Accurate result?
+                                   , Maybe MsgDoc)      -- Errors?
 
   cfa accurate fun_ty []      -- Args have run out; that's fine
       = (if accurate then Just fun_ty else Nothing, Nothing)
@@ -446,12 +446,12 @@ stgEqType orig_ty1 orig_ty2
       | Just (tc1, tc_args1) <- splitTyConApp_maybe ty1
       , Just (tc2, tc_args2) <- splitTyConApp_maybe ty2
       , let res = if tc1 == tc2 
-        	  then equalLength tc_args1 tc_args2 
-        	    && and (zipWith go tc_args1 tc_args2)
-        	  else  -- TyCons don't match; but don't bleat if either is a 
-    		        -- family TyCon because a coercion might have made it 
-        	        -- equal to something else
-        	    (isFamilyTyCon tc1 || isFamilyTyCon tc2)
+                  then equalLength tc_args1 tc_args2 
+                    && and (zipWith go tc_args1 tc_args2)
+                  else  -- TyCons don't match; but don't bleat if either is a 
+                        -- family TyCon because a coercion might have made it 
+                        -- equal to something else
+                    (isFamilyTyCon tc1 || isFamilyTyCon tc2)
       = if res then True
         else 
         pprTrace "stgEqType: unequal" (vcat [ppr orig_ty1, ppr orig_ty2, ppr rep_ty1
@@ -459,7 +459,7 @@ stgEqType orig_ty1 orig_ty2
         False
 
       | otherwise = True  -- Conservatively say "fine".  
-      		    	  -- Type variables in particular
+                          -- Type variables in particular
 
 checkInScope :: Id -> LintM ()
 checkInScope id = LintM $ \loc scope errs