Be careful to instantiate kind variables when dealing with functional dependencies

There were really two bugs
  a) When the fundep fires we must apply the matching
     substitution to the kinds of the remaining type vars
     (This happens in FunDeps.checkClsFD, when we create meta_tvs)

  b) When instantiating the un-matched type variables we must
     instantiate their kinds properly
     (This happens in TcSMonad.instFlexiTcS)

This fixes #6068 and #6015 (second reported bug).

3 files changed, 60 insertions, 41 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index 44d6a8d01f..e3b6a33298 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -1320,11 +1320,9 @@ rewriteWithFunDeps eqn_pred_locs xis wloc
 
 instFunDepEqn :: WantedLoc -> Equation -> TcS [(Int,CtEvidence)]
 -- Post: Returns the position index as well as the corresponding FunDep equality
-instFunDepEqn wl (FDEqn { fd_qtvs = qtvs, fd_eqs = eqs
+instFunDepEqn wl (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
                         , fd_pred1 = d1, fd_pred2 = d2 })
-  = do { let tvs = varSetElems qtvs
-       ; tys' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution
-       ; let subst = zipTopTvSubst tvs tys'
+  = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
        ; foldM (do_one subst) [] eqs }
   where 
     do_one subst ievs (FDEq { fd_pos = i, fd_ty_left = ty1, fd_ty_right = ty2 })
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 287783cb88..5a40df94ae 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1337,11 +1337,15 @@ instDFunType dfun_id mb_inst_tys
            ; return (ty : tys, phi) }
     go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr mb_inst_tys)
 
-instFlexiTcS :: TyVar -> TcS TcType 
+instFlexiTcS :: [TKVar] -> TcS (TvSubst, [TcType])
 -- Like TcM.instMetaTyVar but the variable that is created is 
 -- always touchable; we are supposed to guess its instantiation.
 -- See Note [Touchable meta type variables] 
-instFlexiTcS tv = wrapTcS (instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) )
+instFlexiTcS tvs = wrapTcS (mapAccumLM inst_one emptyTvSubst tvs)
+  where
+     inst_one subst tv = do { ty' <- instFlexiTcSHelper (tyVarName tv) 
+                                                        (substTy subst (tyVarKind tv))
+                            ; return (extendTvSubst subst tv ty', ty') }
 
 newFlexiTcSTy :: Kind -> TcS TcType  
 newFlexiTcSTy knd 
diff --git a/compiler/types/FunDeps.lhs b/compiler/types/FunDeps.lhs
index 31ef9cc7ab..ab1007f29d 100644
--- a/compiler/types/FunDeps.lhs
+++ b/compiler/types/FunDeps.lhs
@@ -28,7 +28,9 @@ module FunDeps (
 import Name
 import Var
 import Class
+import Id( idType )
 import Type
+import TcType( tcSplitDFunTy )
 import Unify
 import InstEnv
 import VarSet
@@ -208,7 +210,7 @@ Finally, the position parameters will help us rewrite the wanted constraint ``on
 type Pred_Loc = (PredType, SDoc)	-- SDoc says where the Pred comes from
 
 data Equation 
-   = FDEqn { fd_qtvs :: TyVarSet		-- Instantiate these to fresh unification vars
+   = FDEqn { fd_qtvs :: [TyVar]   		-- Instantiate these type and kind vars to fresh unification vars
            , fd_eqs  :: [FDEq]			--   and then make these equal
            , fd_pred1, fd_pred2 :: Pred_Loc }	-- The Equation arose from
 	     	       		   	    	-- combining these two constraints
@@ -286,7 +288,7 @@ improveFromAnother pred1@(ty1, _) pred2@(ty2, _)
   | Just (cls1, tys1) <- getClassPredTys_maybe ty1
   , Just (cls2, tys2) <- getClassPredTys_maybe ty2
   , tys1 `lengthAtLeast` 2 && cls1 == cls2
-  = [ FDEqn { fd_qtvs = emptyVarSet, fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
+  = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2 }
     | let (cls_tvs, cls_fds) = classTvsFds cls1
     , fd <- cls_fds
     , let (ltys1, rs1)  = instFD         fd cls_tvs tys1
@@ -303,7 +305,7 @@ improveFromAnother _ _ = []
 
 pprEquation :: Equation -> SDoc
 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs }) 
-  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr (varSetElems qtvs)),
+  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
 	  nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 | (FDEq _ t1 t2) <- pairs])]
 
 improveFromInstEnv :: (InstEnv,InstEnv)
@@ -320,7 +322,7 @@ improveFromInstEnv inst_env pred@(ty, _)
   , let (cls_tvs, cls_fds) = classTvsFds cls
         instances          = classInstances inst_env cls
         rough_tcs          = roughMatchTcs tys
-  = [ FDEqn { fd_qtvs = qtvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
+  = [ FDEqn { fd_qtvs = meta_tvs, fd_eqs = eqs, fd_pred1 = p_inst, fd_pred2=pred }
     | fd <- cls_fds		-- Iterate through the fundeps first,
 				-- because there often are none!
     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
@@ -328,25 +330,27 @@ improveFromInstEnv inst_env pred@(ty, _)
 		-- Remember that instanceCantMatch treats both argumnents
 		-- symmetrically, so it's ok to trim the rough_tcs,
 		-- rather than trimming each inst_tcs in turn
-    , ispec@(ClsInst { is_tvs = qtvs, is_tys = tys_inst,
-		 	is_tcs = inst_tcs }) <- instances
-    , not (instanceCantMatch inst_tcs trimmed_tcs)
-    , let p_inst = (mkClassPred cls tys_inst,
+    , ispec <- instances
+    , (meta_tvs, eqs) <- checkClsFD fd cls_tvs ispec 
+                                    emptyVarSet tys trimmed_tcs -- NB: orientation
+    , let p_inst = (mkClassPred cls (is_tys ispec),
 		    sep [ ptext (sLit "arising from the dependency") <+> quotes (pprFunDep fd)	
 		        , ptext (sLit "in the instance declaration")
 			  <+> pprNameDefnLoc (getName ispec)])
-    , (qtvs, eqs) <- checkClsFD qtvs fd cls_tvs tys_inst tys -- NB: orientation
-    , not (null eqs)
     ]
 improveFromInstEnv _ _ = []
 
 
-checkClsFD :: TyVarSet 			-- Quantified type variables; see note below
-	   -> FunDep TyVar -> [TyVar] 	-- One functional dependency from the class
-	   -> [Type] -> [Type]
-	   -> [(TyVarSet, [FDEq])]
+checkClsFD :: FunDep TyVar -> [TyVar] 	          -- One functional dependency from the class
+           -> ClsInst                             -- An instance template
+           -> TyVarSet -> [Type] -> [Maybe Name]  -- Arguments of this (C tys) predicate
+                                                  -- TyVarSet are extra tyvars that can be instantiated
+	   -> [([TyVar], [FDEq])]
+
+checkClsFD fd clas_tvs 
+           (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst, is_dfun = dfun })
+           extra_qtvs tys_actual rough_tcs_actual
 
-checkClsFD qtvs fd clas_tvs tys1 tys2
 -- 'qtvs' are the quantified type variables, the ones which an be instantiated 
 -- to make the types match.  For example, given
 --	class C a b | a->b where ...
@@ -355,8 +359,8 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
 -- and an Inst of form (C (Maybe t1) t2), 
 -- then we will call checkClsFD with
 --
---	qtvs = {x}, tys1 = [Maybe x,  Tree x]
---		    tys2 = [Maybe t1, t2]
+--	is_qtvs = {x}, is_tys = [Maybe x,  Tree x]
+--		       tys_actual = [Maybe t1, t2]
 --
 -- We can instantiate x to t1, and then we want to force
 -- 	(Tree x) [t1/x]  ~   t2
@@ -368,10 +372,14 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
 -- This function is also used by InstEnv.badFunDeps, which needs to *unify*
 -- For the one-sided matching case, the qtvs are just from the template,
 -- so we get matching
---
-  = ASSERT2( length tys1 == length tys2     && 
-	     length tys1 == length clas_tvs 
-	    , ppr tys1 <+> ppr tys2 )
+
+  | instanceCantMatch rough_tcs_inst rough_tcs_actual
+  = []		-- Filter out ones that can't possibly match, 
+
+  | otherwise
+  = ASSERT2( length tys_inst == length tys_actual     && 
+	     length tys_inst == length clas_tvs 
+	    , ppr tys_inst <+> ppr tys_actual )
 
     case tcUnifyTys bind_fn ltys1 ltys2 of
 	Nothing  -> []
@@ -391,8 +399,11 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
                         -- so we would produce no FDs, which is clearly wrong. 
                   -> [] 
 
+                  | null fdeqs
+                  -> []
+
                   | otherwise
-                  -> [(qtvs', fdeqs)]
+                  -> [(meta_tvs, fdeqs)]
 		  	-- We could avoid this substTy stuff by producing the eqn
 		  	-- (qtvs, ls1++rs1, ls2++rs2)
 		  	-- which will re-do the ls1/ls2 unification when the equation is
@@ -409,8 +420,10 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
                         -- eqType again, since we know for sure that /at least one/ 
                         -- equation in there is useful)
 
-		    qtvs' = filterVarSet (`notElemTvSubst` subst) qtvs
-		        -- qtvs' are the quantified type variables
+                    (dfun_tvs, _, _, _) = tcSplitDFunTy (idType dfun)
+		    meta_tvs = [ setVarType tv (substTy subst (varType tv))
+                               | tv <- dfun_tvs, tv `notElemTvSubst` subst ]
+		        -- meta_tvs are the quantified type variables
 		        -- that have not been substituted out
 		        --	
 		        -- Eg. 	class C a b | a -> b
@@ -418,12 +431,21 @@ checkClsFD qtvs fd clas_tvs tys1 tys2
 		        -- Given constraint C Int z
 		        -- we generate the equation
 		        --	({y}, [y], z)
+                        --
+                        -- But note (a) we get them from the dfun_id, so they are *in order*
+                        --              because the kind variables may be mentioned in the
+                        --              type variabes' kinds
+                        --          (b) we must apply 'subst' to the kinds, in case we have
+                        --              matched out a kind variable, but not a type variable
+                        --              whose kind mentions that kind variable!
+                        --          Trac #6015, #6068
   where
-    bind_fn tv | tv `elemVarSet` qtvs = BindMe
-	       | otherwise	      = Skolem
+    bind_fn tv | tv `elemVarSet` qtvs       = BindMe
+               | tv `elemVarSet` extra_qtvs = BindMe
+	       | otherwise	            = Skolem
 
-    (ltys1, rtys1) = instFD         fd clas_tvs tys1
-    (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys2
+    (ltys1, rtys1) = instFD         fd clas_tvs tys_inst
+    (ltys2, irs2)  = instFD_WithPos fd clas_tvs tys_actual
 \end{code}
 
 
@@ -529,13 +551,8 @@ badFunDeps cls_insts clas ins_tv_set ins_tys
   = nubBy eq_inst $
     [ ispec | fd <- fds,	-- fds is often empty, so do this first!
 	      let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
-	      ispec@(ClsInst { is_tcs = inst_tcs, is_tvs = tvs, 
-				is_tys = tys }) <- cls_insts,
-		-- Filter out ones that can't possibly match, 
-		-- based on the head of the fundep
-	      not (instanceCantMatch inst_tcs trimmed_tcs),	
-	      notNull (checkClsFD (tvs `unionVarSet` ins_tv_set) 
-				   fd clas_tvs tys ins_tys)
+	      ispec <- cls_insts,
+	      notNull (checkClsFD fd clas_tvs ispec ins_tv_set ins_tys trimmed_tcs)
     ]
   where
     (clas_tvs, fds) = classTvsFds clas