Commit c4b2ac37 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by ian@well-typed.com

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.
parent 57c8d1c2
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment