[commit: ghc] master: Apply the kind subst to the (kinds of the) quanitifed tyvars in deriveTyData (ffed708)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/ffed708c30f2d1d4b4c5cd08d9c19aeb0bb623ec/ghc

>---------------------------------------------------------------

commit ffed708c30f2d1d4b4c5cd08d9c19aeb0bb623ec
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Sat Mar 22 23:11:10 2014 +0000

    Apply the kind subst to the (kinds of the) quanitifed tyvars in deriveTyData
    
    I've elaboated Note [Unify kinds in deriving] to explain
    what is going on here.
    
    The change fixes Trac #8893.


>---------------------------------------------------------------

ffed708c30f2d1d4b4c5cd08d9c19aeb0bb623ec
 compiler/typecheck/TcDeriv.lhs |   56 ++++++++++++++++++++++++++++++----------
 1 file changed, 43 insertions(+), 13 deletions(-)

diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs
index a89adda..4cec134 100644
--- a/compiler/typecheck/TcDeriv.lhs
+++ b/compiler/typecheck/TcDeriv.lhs
@@ -685,13 +685,19 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
               tc_args_to_keep = take n_args_to_keep tc_args
               inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
               dropped_tvs     = tyVarsOfTypes args_to_drop
-              mb_match        = tcUnifyTy inst_ty_kind cls_arg_kind
-              Just subst      = mb_match   -- See Note [Unify kinds in deriving]
-              -- We are assuming the tycon tyvars and the class tyvars are distinct
 
-              final_tc_args   = substTys subst tc_args_to_keep
-              final_cls_tys   = substTys subst cls_tys
-              univ_tvs        = mkVarSet deriv_tvs `unionVarSet` tyVarsOfTypes final_tc_args
+              -- Match up the kinds, and apply the resulting kind substitution
+              -- to the types.  See Note [Unify kinds in deriving]
+              -- We are assuming the tycon tyvars and the class tyvars are distinct
+              mb_match        = tcUnifyTy inst_ty_kind cls_arg_kind
+              Just kind_subst = mb_match 
+              (univ_kvs, univ_tvs) = partition isKindVar $ varSetElems $
+                                     mkVarSet deriv_tvs `unionVarSet` 
+                                     tyVarsOfTypes tc_args_to_keep
+              univ_kvs'           = filter (`notElemTvSubst` kind_subst) univ_kvs
+              (subst', univ_tvs') = mapAccumL substTyVarBndr kind_subst univ_tvs
+              final_tc_args       = substTys subst' tc_args_to_keep
+              final_cls_tys       = substTys subst' cls_tys
 
         ; traceTc "derivTyData1" (vcat [ pprTvBndrs tvs, ppr tc, ppr tc_args, ppr deriv_pred
                                        , pprTvBndrs (varSetElems $ tyVarsOfTypes tc_args)
@@ -705,9 +711,9 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
 
         ; traceTc "derivTyData2" (vcat [ ppr univ_tvs ])
 
-        ; checkTc (allDistinctTyVars args_to_drop &&            -- (a) and (b)
-                   univ_tvs `disjointVarSet` dropped_tvs)       -- (c)
-                  (derivingEtaErr cls cls_tys (mkTyConApp tc final_tc_args))
+        ; checkTc (allDistinctTyVars args_to_drop &&              -- (a) and (b)
+                   not (any (`elemVarSet` dropped_tvs) univ_tvs)) -- (c)
+                  (derivingEtaErr cls final_cls_tys (mkTyConApp tc final_tc_args))
                 -- Check that
                 --  (a) The args to drop are all type variables; eg reject:
                 --              data instance T a Int = .... deriving( Monad )
@@ -719,7 +725,7 @@ deriveTyData tvs tc tc_args (L loc deriv_pred)
                 --              newtype T a s = ... deriving( ST s )
                 --              newtype K a a = ... deriving( Monad )
 
-        ; mkEqnHelp (varSetElemsKvsFirst univ_tvs)
+        ; mkEqnHelp (univ_kvs' ++ univ_tvs')
                     cls final_cls_tys tc final_tc_args Nothing } }
 
 derivePolyKindedTypeable :: Class -> [Type]
@@ -775,10 +781,34 @@ So we need to
    kind arguments.
 
 In the two examples,
- * we unify ( T k (a:k) ) ~ (* -> *) to find k:=*.
- * we unify ( Either ~ (k -> k -> k) ) to find k:=*.
+ * we unify   kind-of( T k (a:k) ) ~ kind-of( Functor )
+         i.e.      (k -> *) ~ (* -> *)   to find k:=*.
+         yielding  k:=*
+
+ * we unify   kind-of( Either ) ~ kind-of( Category )
+         i.e.      (* -> * -> *)  ~ (k -> k -> k)
+         yielding  k:=*
+
+Now we get a kind substition.  We then need to:
+
+  1. Remove the substituted-out kind variables from the quantifed kind vars
+
+  2. Apply the substitution to the kinds of quantified *type* vars
+     (and extend the substitution to reflect this change)
+
+  3. Apply that extended substitution to the non-dropped args (types and
+     kinds) of the type and class
+
+Forgetting step (2) caused Trac #8893:
+  data V a = V [a] deriving Functor
+  data P (x::k->*) (a:k) = P (x a) deriving Functor
+  data C (x::k->*) (a:k) = C (V (P x a)) deriving Functor
+
+When deriving Functor for P, we unify k to *, but we then want
+an instance   $df :: forall (x:*->*). Functor x => Functor (P * (x:*->*))
+and similarly for C.  Notice the modifed kind of x, both at binding
+and occurrence sites.
 
-Tricky stuff.
 
 \begin{code}
 mkEqnHelp :: [TyVar]