[commit: ghc] ghc-kinds: fix kind substitution in templates in tcResultType (923e459)

[Julien Cretin]

Repository : ssh://darcs.haskell.org//srv/darcs/ghc

On branch  : ghc-kinds

http://hackage.haskell.org/trac/ghc/changeset/923e459416821c23ad72934f5e55546ad2d2a1c1

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

commit 923e459416821c23ad72934f5e55546ad2d2a1c1
Author: Julien Cretin <ghc at ia0.eu>
Date:   Tue Sep 13 17:08:18 2011 +0200

    fix kind substitution in templates in tcResultType

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

 compiler/coreSyn/CoreLint.lhs       |    3 ++
 compiler/typecheck/TcTyClsDecls.lhs |   43 ++++++++++++++++++++++++++++++++++-
 compiler/types/Type.lhs             |    2 +-
 3 files changed, 46 insertions(+), 2 deletions(-)

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index fc7121b..fa167bb 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -418,10 +418,13 @@ lintValApp arg fun_ty arg_ty
 checkTyKind :: OutTyVar -> OutType -> LintM ()
 -- Both args have had substitution applied
 checkTyKind tyvar arg_ty
+  | isSuperKind tyvar_kind  -- kind forall
+  = lintKind arg_ty
 	-- Arg type might be boxed for a function with an uncommitted
 	-- tyvar; notably this is used so that we can give
 	-- 	error :: forall a:*. String -> a
 	-- and then apply it to both boxed and unboxed types.
+  | otherwise  -- type forall
   = do { arg_kind <- lintType arg_ty
        ; unless (arg_kind `isSubKind` tyvar_kind)
                 (addErrL (mkKindErrMsg tyvar arg_ty)) }
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 3e28c81..3790d43 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -871,7 +871,10 @@ tcResultType (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
 		= case tcGetTyVar_maybe ty of
 		    Just tv | not (tv `elem` univs)
 			    -> (tv:univs,   eqs)
-		    _other  -> (tmpl:univs, (tmpl,ty):eqs)
+		    _other  -> (new_tmpl:univs, (new_tmpl,ty):eqs)
+                               where  -- see Note [Substitution in template variables kinds]
+                                 new_kind = substTy subst (tyVarKind tmpl)
+                                 new_tmpl = setTyVarKind tmpl new_kind
 		| otherwise = pprPanic "tcResultType" (ppr res_ty)
 	      ex_tvs = dc_tvs `minusList` univ_tvs
 
@@ -889,6 +892,44 @@ tcResultType (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
 		 name = tyVarName tv
 		 (env', occ') = tidyOccName env (getOccName name) 
 
+{-
+Note [Substitution in template variables kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+data List a = Nil | Cons a (List a)
+data SList s as where
+  SNil :: SList s Nil
+
+We call tcResultType with
+  tmpl_tvs = [(k :: BOX), (s :: k -> *), (as :: List k)]
+  res_tmpl = SList k s as)
+  res_ty = ResTyGADT (SList k1 (s1 :: k1 -> *) (Nil k1))
+
+We get subst:
+  k -> k1
+  s -> s1
+  as -> Nil k1
+
+Now we want to find out the universal variables and the equivalences
+between some of them and types (GADT).
+
+In this example, k and s are mapped to exactly variables which are not
+already present in the universal set, so we just add them without any
+coercion.
+
+But 'as' is mapped to 'Nil k1', so we add 'as' to the universal set,
+and add the equivalence with 'Nil k1' in 'eqs'.
+
+The problem is that with kind polymorphism, as's kind may now contain
+kind variables, and we have to apply the template substitution to it,
+which is why we create new_tmpl.
+
+The template substitution only maps kind variables to kind variables,
+since GADTs are not kind indexed.
+
+-}
+
+
 consUseH98Syntax :: [LConDecl a] -> Bool
 consUseH98Syntax (L _ (ConDecl { con_res = ResTyGADT _ }) : _) = False
 consUseH98Syntax _                                             = True
diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs
index 228e104..6cadc82 100644
--- a/compiler/types/Type.lhs
+++ b/compiler/types/Type.lhs
@@ -1404,7 +1404,7 @@ substTyVarBndr subst@(TvSubst in_scope tenv) old_var
 
     old_ki = tyVarKind old_var
     no_kind_change = isEmptyVarSet (tyVarsOfType old_ki) -- verify that kind is closed
-    no_change = new_var == old_var
+    no_change = no_kind_change && (new_var == old_var)
 	-- no_change means that the new_var is identical in
 	-- all respects to the old_var (same unique, same kind)
 	-- See Note [Extending the TvSubst]