[commit: ghc] master: Fix TcUnify.matchExpectedTyConApp so that it returns types of compatible kinds (be5cc2e)

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

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/be5cc2e33aa8e54299527af9b91e659d54c4cde5

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

commit be5cc2e33aa8e54299527af9b91e659d54c4cde5
Author: Simon Peyton Jones <[email protected]>
Date:   Wed Dec 19 23:49:47 2012 +0000

    Fix TcUnify.matchExpectedTyConApp so that it returns types of compatible kinds
    
    This fixes Trac #7368. The problem was that we were matching
       Bad w ~ f (Bad f)
    where (f :: * -> *).  Thta leads to (w ~ Bad f), which is
    ill-kinded, but matchExpectedTyConApp was returning the (Bad f)
    as the argument type, and that was being used to instanatiate
    w in the data constructor type, which is very bad.
    
    The code also becomes simpler and easier to understand, which is
    an excellent thing.

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

 compiler/typecheck/TcUnify.lhs |   79 ++++++++++++++++++++--------------------
 1 files changed, 39 insertions(+), 40 deletions(-)

diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 04f1acc..05d7918 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -44,7 +44,6 @@ module TcUnify (
 import HsSyn
 import TypeRep
 import TcMType
-import TcIface
 import TcRnMonad
 import TcType
 import Type
@@ -207,53 +206,53 @@ matchExpectedPArrTy exp_ty
 ----------------------
 matchExpectedTyConApp :: TyCon                -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> *
                       -> TcRhoType 	      -- orig_ty
-                      -> TcM (TcCoercion,      -- T k1 k2 k3 a b c ~ orig_ty
+                      -> TcM (TcCoercion,     -- T k1 k2 k3 a b c ~ orig_ty
                               [TcSigmaType])  -- Element types, k1 k2 k3 a b c
                               
 -- It's used for wired-in tycons, so we call checkWiredInTyCon
 -- Precondition: never called with FunTyCon
 -- Precondition: input type :: *
+-- Postcondition: (T k1 k2 k3 a b c) is well-kinded
 
 matchExpectedTyConApp tc orig_ty
-  = do  { checkWiredInTyCon tc
-        ; go (tyConArity tc) orig_ty [] }
+  = go orig_ty
   where
-    go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (TcCoercion, [TcSigmaType])
-    -- If     go n ty tys = (co, [t1..tn] ++ tys)
-    -- then   co : T t1..tn ~ ty
+    go ty 
+       | Just ty' <- tcView ty 
+       = go ty'
 
-    go n_req ty tys
-      | Just ty' <- tcView ty = go n_req ty' tys
+    go ty@(TyConApp tycon args) 
+       | tc == tycon  -- Common case
+       = return (mkTcReflCo ty, args)
 
-    go n_req ty@(TyVarTy tv) tys
-      | ASSERT( isTcTyVar tv) isMetaTyVar tv
-      = do { cts <- readMetaTyVar tv
-           ; case cts of
-               Indirect ty -> go n_req ty tys
-               Flexi       -> defer n_req ty tys }
-
-    go n_req ty@(TyConApp tycon args) tys
-      | tc == tycon
-      = ASSERT( n_req == length args)   -- ty::*
-        return (mkTcReflCo ty, args ++ tys)
-
-    go n_req (AppTy fun arg) tys
-      | n_req > 0
-      = do { (co, args) <- go (n_req - 1) fun (arg : tys) 
-           ; return (mkTcAppCo co (mkTcReflCo arg), args) }
-
-    go n_req ty tys = defer n_req ty tys
-
-    ----------
-    defer n_req ty tys
-      = do { kappa_tys <- mapM (const newMetaKindVar) kvs
-           ; let arg_kinds' = map (substKiWith kvs kappa_tys) arg_kinds
-           ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
-           ; co <- unifyType (mkTyConApp tc (kappa_tys ++ tau_tys)) ty
-           ; return (co, kappa_tys ++ tau_tys ++ tys) }
-      where
-        (kvs, body) = splitForAllTys (tyConKind tc)
-        (arg_kinds, _) = splitKindFunTysN (n_req - length kvs) body
+    go (TyVarTy tv)
+       | ASSERT( isTcTyVar tv) isMetaTyVar tv
+       = do { cts <- readMetaTyVar tv
+            ; case cts of
+                Indirect ty -> go ty
+                Flexi       -> defer }
+   
+    go _ = defer
+
+    -- If the common case does not occur, instantiate a template
+    -- T k1 .. kn t1 .. tm, and unify with the original type
+    -- Doing it this way ensures that the types we return are
+    -- kind-compatible with T.  For example, suppose we have
+    --       matchExpectedTyConApp T (f Maybe)
+    -- where data T a = MkT a  
+    -- Then we don't want to instantate T's data constructors with  
+    --    (a::*) ~ Maybe
+    -- because that'll make types that are utterly ill-kinded.
+    -- This happened in Trac #7368
+    defer = ASSERT2( isLiftedTypeKind res_kind, ppr tc )
+            do { kappa_tys <- mapM (const newMetaKindVar) kvs
+               ; let arg_kinds' = map (substKiWith kvs kappa_tys) arg_kinds
+               ; tau_tys <- mapM newFlexiTyVarTy arg_kinds'
+               ; co <- unifyType (mkTyConApp tc (kappa_tys ++ tau_tys)) orig_ty
+               ; return (co, kappa_tys ++ tau_tys) }
+
+    (kvs, body)           = splitForAllTys (tyConKind tc)
+    (arg_kinds, res_kind) = splitKindFunTys body
 
 ----------------------
 matchExpectedAppTy :: TcRhoType                         -- orig_ty