From c4b2ac3775323948b7a6abdb241a4ad02afa7141 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Wed, 19 Dec 2012 23:49:47 +0000
Subject: [PATCH] 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 | 77 +++++++++++++++++-----------------
1 file changed, 38 insertions(+), 39 deletions(-)
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index b0ccbbc1e06f..cdeeea0eb113 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -43,7 +43,6 @@ module TcUnify (
import HsSyn
import TypeRep
import TcMType
-import TcIface
import TcRnMonad
import TcType
import Type
@@ -198,53 +197,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
--
GitLab