2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubOff, tcSubExp, tcGen,
10 checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList, unifyTauTyLists,
14 unifyKind, unifyKinds, unifyFunKind,
16 --------------------------------
18 Expected(..), newHole, readExpectedType,
19 zapExpectedType, zapExpectedTo, zapExpectedBranches,
20 subFunTys, unifyFunTy,
21 zapToListTy, unifyListTy,
22 zapToPArrTy, unifyPArrTy,
23 zapToTupleTy, unifyTupleTy
27 #include "HsVersions.h"
30 import HsSyn ( HsExpr(..) )
31 import TcHsSyn ( mkHsLet,
32 ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
33 import TypeRep ( Type(..), PredType(..), TyNote(..), openKindCon, isSuperKind )
35 import TcRnMonad -- TcType, amongst others
36 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
37 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
38 isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
39 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
40 tcGetTyVar_maybe, tcGetTyVar,
41 mkFunTy, tyVarsOfType, mkPhiTy,
42 typeKind, tcSplitFunTy_maybe, mkForAllTys,
43 isSkolemTyVar, isUserTyVar,
44 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
45 eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind,
46 hasMoreBoxityInfo, allDistinctTyVars, pprType, pprKind )
47 import Inst ( newDicts, instToId, tcInstCall )
48 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar,
49 newTyVarTy, newTyVarTys, newOpenTypeKind,
50 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV )
51 import TcSimplify ( tcSimplifyCheck )
52 import TysWiredIn ( listTyCon, parrTyCon, tupleTyCon )
53 import TcEnv ( tcGetGlobalTyVars, findGlobals )
54 import TyCon ( TyCon, tyConArity, isTupleTyCon, tupleTyConBoxity )
55 import Id ( Id, mkSysLocal )
56 import Var ( Var, varName, tyVarKind )
57 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
59 import Name ( isSystemName )
60 import ErrUtils ( Message )
61 import BasicTypes ( Boxity, Arity, isBoxed )
62 import Util ( equalLength, lengthExceeds, notNull )
68 * A hole is always filled in with an ordinary type, not another hole.
70 %************************************************************************
72 \subsection{'hole' type variables}
74 %************************************************************************
77 data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
78 | Check ty -- The type to check during type checking
80 newHole :: TcM (TcRef ty)
81 newHole = newMutVar (error "Empty hole in typechecker")
83 readExpectedType :: Expected ty -> TcM ty
84 readExpectedType (Infer hole) = readMutVar hole
85 readExpectedType (Check ty) = returnM ty
87 zapExpectedType :: Expected TcType -> TcM TcTauType
88 -- In the inference case, ensure we have a monotype
89 zapExpectedType (Infer hole)
90 = do { ty <- newTyVarTy openTypeKind ;
94 zapExpectedType (Check ty) = return ty
96 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
97 zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2
98 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
100 zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType)
101 -- Zap the expected type to a monotype if there is more than one branch
102 zapExpectedBranches branches exp_ty
103 | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' ->
104 return (Check exp_ty')
105 | otherwise = returnM exp_ty
107 instance Outputable ty => Outputable (Expected ty) where
108 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
109 ppr (Infer hole) = ptext SLIT("Inferring type")
113 %************************************************************************
115 \subsection[Unify-fun]{@unifyFunTy@}
117 %************************************************************************
119 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
120 creation of type variables.
122 * subFunTy is used when we might be faced with a "hole" type variable,
123 in which case we should create two new holes.
125 * unifyFunTy is used when we expect to encounter only "ordinary"
126 type variables, so we should create new ordinary type variables
130 -> Expected TcRhoType -- Fail if ty isn't a function type
131 -> ([(pat, Expected TcRhoType)] -> Expected TcRhoType -> TcM a)
134 subFunTys pats (Infer hole) thing_inside
135 = -- This is the interesting case
136 mapM new_pat_hole pats `thenM` \ pats_w_holes ->
137 newHole `thenM` \ res_hole ->
140 thing_inside pats_w_holes (Infer res_hole) `thenM` \ answer ->
142 -- Extract the answers
143 mapM read_pat_hole pats_w_holes `thenM` \ arg_tys ->
144 readMutVar res_hole `thenM` \ res_ty ->
146 -- Write the answer into the incoming hole
147 writeMutVar hole (mkFunTys arg_tys res_ty) `thenM_`
149 -- And return the answer
152 new_pat_hole pat = newHole `thenM` \ hole -> return (pat, Infer hole)
153 read_pat_hole (pat, Infer hole) = readMutVar hole
155 subFunTys pats (Check ty) thing_inside
156 = go pats ty `thenM` \ (pats_w_tys, res_ty) ->
157 thing_inside pats_w_tys res_ty
159 go [] ty = return ([], Check ty)
160 go (pat:pats) ty = unifyFunTy ty `thenM` \ (arg,res) ->
161 go pats res `thenM` \ (pats_w_tys, final_res) ->
162 return ((pat, Check arg) : pats_w_tys, final_res)
164 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
165 -> TcM (TcType, TcType) -- otherwise return arg and result types
167 unifyFunTy ty@(TyVarTy tyvar)
168 = getTcTyVar tyvar `thenM` \ maybe_ty ->
170 Just ty' -> unifyFunTy ty'
171 Nothing -> unify_fun_ty_help ty
174 = case tcSplitFunTy_maybe ty of
175 Just arg_and_res -> returnM arg_and_res
176 Nothing -> unify_fun_ty_help ty
178 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
179 = newTyVarTy openTypeKind `thenM` \ arg ->
180 newTyVarTy openTypeKind `thenM` \ res ->
181 unifyTauTy ty (mkFunTy arg res) `thenM_`
186 ----------------------
187 zapToListTy, zapToPArrTy :: Expected TcType -- expected list type
188 -> TcM TcType -- list element type
189 unifyListTy, unifyPArrTy :: TcType -> TcM TcType
190 zapToListTy = zapToXTy listTyCon
191 unifyListTy = unifyXTy listTyCon
192 zapToPArrTy = zapToXTy parrTyCon
193 unifyPArrTy = unifyXTy parrTyCon
195 ----------------------
196 zapToXTy :: TyCon -- T :: *->*
197 -> Expected TcType -- Expected type (T a)
198 -> TcM TcType -- Element type, a
200 zapToXTy tc (Check ty) = unifyXTy tc ty
201 zapToXTy tc (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
202 writeMutVar hole (mkTyConApp tc [elt_ty]) ;
205 ----------------------
206 unifyXTy :: TyCon -> TcType -> TcM TcType
207 unifyXTy tc ty@(TyVarTy tyvar)
208 = getTcTyVar tyvar `thenM` \ maybe_ty ->
210 Just ty' -> unifyXTy tc ty'
211 other -> unify_x_ty_help tc ty
214 = case tcSplitTyConApp_maybe ty of
215 Just (tycon, [arg_ty]) | tycon == tc -> returnM arg_ty
216 other -> unify_x_ty_help tc ty
218 unify_x_ty_help tc ty -- Revert to ordinary unification
219 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
220 unifyTauTy ty (mkTyConApp tc [elt_ty]) `thenM_`
225 ----------------------
226 zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
227 zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
228 zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
229 writeMutVar hole tup_ty ;
232 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
233 = getTcTyVar tyvar `thenM` \ maybe_ty ->
235 Just ty' -> unifyTupleTy boxity arity ty'
236 other -> unify_tuple_ty_help boxity arity ty
238 unifyTupleTy boxity arity ty
239 = case tcSplitTyConApp_maybe ty of
240 Just (tycon, arg_tys)
242 && tyConArity tycon == arity
243 && tupleTyConBoxity tycon == boxity
245 other -> unify_tuple_ty_help boxity arity ty
247 unify_tuple_ty_help boxity arity ty
248 = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
249 unifyTauTy ty tup_ty `thenM_`
252 new_tuple_ty boxity arity
253 = newTyVarTys arity kind `thenM` \ arg_tys ->
254 return (mkTyConApp tup_tc arg_tys, arg_tys)
256 tup_tc = tupleTyCon boxity arity
257 kind | isBoxed boxity = liftedTypeKind
258 | otherwise = openTypeKind
262 %************************************************************************
264 \subsection{Subsumption}
266 %************************************************************************
268 All the tcSub calls have the form
270 tcSub expected_ty offered_ty
272 offered_ty <= expected_ty
274 That is, that a value of type offered_ty is acceptable in
275 a place expecting a value of type expected_ty.
277 It returns a coercion function
278 co_fn :: offered_ty -> expected_ty
279 which takes an HsExpr of type offered_ty into one of type
283 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
284 tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn
287 These two check for holes
290 tcSubExp expected_ty offered_ty
291 = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_`
292 checkHole expected_ty offered_ty tcSub
294 tcSubOff expected_ty offered_ty
295 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
297 -- checkHole looks for a hole in its first arg;
298 -- If so, and it is uninstantiated, it fills in the hole
299 -- with its second arg
300 -- Otherwise it calls thing_inside, passing the two args, looking
301 -- through any instantiated hole
303 checkHole (Infer hole) other_ty thing_inside
304 = do { writeMutVar hole other_ty; return idCoercion }
306 checkHole (Check ty) other_ty thing_inside
307 = thing_inside ty other_ty
310 No holes expected now. Add some error-check context info.
313 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
314 tcSub expected_ty actual_ty
315 = traceTc (text "tcSub" <+> details) `thenM_`
316 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
317 (tc_sub expected_ty expected_ty actual_ty actual_ty)
319 details = vcat [text "Expected:" <+> ppr expected_ty,
320 text "Actual: " <+> ppr actual_ty]
323 tc_sub carries the types before and after expanding type synonyms
326 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
327 -> TcSigmaType -- ..and after
328 -> TcSigmaType -- actual_ty, before
329 -> TcSigmaType -- ..and after
332 -----------------------------------
334 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
335 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
337 -----------------------------------
338 -- Generalisation case
339 -- actual_ty: d:Eq b => b->b
340 -- expected_ty: forall a. Ord a => a->a
341 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
343 -- It is essential to do this *before* the specialisation case
344 -- Example: f :: (Eq a => a->a) -> ...
345 -- g :: Ord b => b->b
348 tc_sub exp_sty expected_ty act_sty actual_ty
349 | isSigmaTy expected_ty
350 = tcGen expected_ty (tyVarsOfType actual_ty) (
351 -- It's really important to check for escape wrt the free vars of
352 -- both expected_ty *and* actual_ty
353 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
354 ) `thenM` \ (gen_fn, co_fn) ->
355 returnM (gen_fn <.> co_fn)
357 -----------------------------------
358 -- Specialisation case:
359 -- actual_ty: forall a. Ord a => a->a
360 -- expected_ty: Int -> Int
361 -- co_fn e = e Int dOrdInt
363 tc_sub exp_sty expected_ty act_sty actual_ty
364 | isSigmaTy actual_ty
365 = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
366 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
367 returnM (co_fn <.> inst_fn)
369 -----------------------------------
372 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
373 = tcSub_fun exp_arg exp_res act_arg act_res
375 -----------------------------------
376 -- Type variable meets function: imitate
378 -- NB 1: we can't just unify the type variable with the type
379 -- because the type might not be a tau-type, and we aren't
380 -- allowed to instantiate an ordinary type variable with
383 -- NB 2: can we short-cut to an error case?
384 -- when the arg/res is not a tau-type?
385 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
387 -- is perfectly fine, because we can instantiat f's type to a monotype
389 -- However, we get can get jolly unhelpful error messages.
390 -- e.g. foo = id runST
392 -- Inferred type is less polymorphic than expected
393 -- Quantified type variable `s' escapes
394 -- Expected type: ST s a -> t
395 -- Inferred type: (forall s1. ST s1 a) -> a
396 -- In the first argument of `id', namely `runST'
397 -- In a right-hand side of function `foo': id runST
399 -- I'm not quite sure what to do about this!
401 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
402 = getTcTyVar tv `thenM` \ maybe_ty ->
404 Just ty -> tc_sub exp_sty exp_ty ty ty
405 Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) ->
406 tcSub_fun exp_arg exp_res act_arg act_res
408 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
409 = getTcTyVar tv `thenM` \ maybe_ty ->
411 Just ty -> tc_sub ty ty act_sty act_ty
412 Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
413 tcSub_fun exp_arg exp_res act_arg act_res
415 -----------------------------------
417 -- If none of the above match, we revert to the plain unifier
418 tc_sub exp_sty expected_ty act_sty actual_ty
419 = uTys exp_sty expected_ty act_sty actual_ty `thenM_`
423 %************************************************************************
425 \subsection{Functions}
427 %************************************************************************
430 tcSub_fun exp_arg exp_res act_arg act_res
431 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
432 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
433 newUnique `thenM` \ uniq ->
435 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
436 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
437 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
438 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
439 coercion | isIdCoercion co_fn_arg,
440 isIdCoercion co_fn_res = idCoercion
441 | otherwise = mkCoercion co_fn
443 co_fn e = DictLam [arg_id]
444 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
445 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
446 -- HsVar arg_id :: HsExpr exp_arg
447 -- co_fn_arg $it :: HsExpr act_arg
448 -- HsApp e $it :: HsExpr act_res
449 -- co_fn_res $it :: HsExpr exp_res
453 imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
455 = -- NB: tv is an *ordinary* tyvar and so are the new ones
457 -- Check that tv isn't a type-signature type variable
458 -- (This would be found later in checkSigTyVars, but
459 -- we get a better error message if we do it here.)
460 checkM (not (isSkolemTyVar tv))
461 (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
463 newTyVarTy openTypeKind `thenM` \ arg ->
464 newTyVarTy openTypeKind `thenM` \ res ->
465 putTcTyVar tv (mkFunTy arg res) `thenM_`
470 %************************************************************************
472 \subsection{Generalisation}
474 %************************************************************************
477 tcGen :: TcSigmaType -- expected_ty
478 -> TcTyVarSet -- Extra tyvars that the universally
479 -- quantified tyvars of expected_ty
480 -- must not be unified
481 -> (TcRhoType -> TcM result) -- spec_ty
482 -> TcM (ExprCoFn, result)
483 -- The expression has type: spec_ty -> expected_ty
485 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
486 -- If not, the call is a no-op
487 = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
489 -- Type-check the arg and unify with poly type
490 getLIE (thing_inside phi_ty) `thenM` \ (result, lie) ->
492 -- Check that the "forall_tvs" havn't been constrained
493 -- The interesting bit here is that we must include the free variables
494 -- of the expected_ty. Here's an example:
495 -- runST (newVar True)
496 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
497 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
498 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
499 -- So now s' isn't unconstrained because it's linked to a.
500 -- Conclusion: include the free vars of the expected_ty in the
501 -- list of "free vars" for the signature check.
503 newDicts SignatureOrigin theta `thenM` \ dicts ->
504 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
507 zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
508 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
509 text "expected_ty" <+> ppr expected_ty,
510 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
511 text "free_tvs" <+> ppr free_tvs,
512 text "forall_tys" <+> ppr forall_tys]) `thenM_`
515 checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
517 traceTc (text "tcGen:done") `thenM_`
520 -- This HsLet binds any Insts which came out of the simplification.
521 -- It's a bit out of place here, but using AbsBind involves inventing
522 -- a couple of new names which seems worse.
523 dict_ids = map instToId dicts
524 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
526 returnM (mkCoercion co_fn, result)
528 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
529 sig_msg = ptext SLIT("expected type of an expression")
534 %************************************************************************
536 \subsection[Unify-exported]{Exported unification functions}
538 %************************************************************************
540 The exported functions are all defined as versions of some
541 non-exported generic functions.
543 Unify two @TauType@s. Dead straightforward.
546 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
547 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
548 = -- The unifier should only ever see tau-types
549 -- (no quantification whatsoever)
550 ASSERT2( isTauTy ty1, ppr ty1 )
551 ASSERT2( isTauTy ty2, ppr ty2 )
552 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
556 @unifyTauTyList@ unifies corresponding elements of two lists of
557 @TauType@s. It uses @uTys@ to do the real work. The lists should be
558 of equal length. We charge down the list explicitly so that we can
559 complain if their lengths differ.
562 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
563 unifyTauTyLists [] [] = returnM ()
564 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
565 unifyTauTyLists tys1 tys2
566 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
569 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
570 all together. It is used, for example, when typechecking explicit
571 lists, when all the elts should be of the same type.
574 unifyTauTyList :: [TcTauType] -> TcM ()
575 unifyTauTyList [] = returnM ()
576 unifyTauTyList [ty] = returnM ()
577 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
581 %************************************************************************
583 \subsection[Unify-uTys]{@uTys@: getting down to business}
585 %************************************************************************
587 @uTys@ is the heart of the unifier. Each arg happens twice, because
588 we want to report errors in terms of synomyms if poss. The first of
589 the pair is used in error messages only; it is always the same as the
590 second, except that if the first is a synonym then the second may be a
591 de-synonym'd version. This way we get better error messages.
593 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
596 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
597 -- ty1 is the *expected* type
599 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
600 -- ty2 is the *actual* type
603 -- Always expand synonyms (see notes at end)
604 -- (this also throws away FTVs)
605 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
606 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
608 -- Variables; go for uVar
609 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
610 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
611 -- "True" means args swapped
614 uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2))
615 | n1 == n2 = uTys t1 t1 t2 t2
616 uTys _ (PredTy (ClassP c1 tys1)) _ (PredTy (ClassP c2 tys2))
617 | c1 == c2 = unifyTauTyLists tys1 tys2
619 -- Functions; just check the two parts
620 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
621 = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2
623 -- NewType constructors must match
624 uTys _ (NewTcApp tc1 tys1) _ (NewTcApp tc2 tys2)
625 | tc1 == tc2 = unifyTauTyLists tys1 tys2
627 -- Ordinary type constructors must match
628 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
629 | con1 == con2 && equalLength tys1 tys2
630 = unifyTauTyLists tys1 tys2
632 | con1 == openKindCon
633 -- When we are doing kind checking, we might match a kind '?'
634 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
635 -- (CCallable Int) and (CCallable Int#) are both OK
636 = unifyTypeKind ps_ty2
638 -- Applications need a bit of care!
639 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
640 -- NB: we've already dealt with type variables and Notes,
641 -- so if one type is an App the other one jolly well better be too
642 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
643 = case tcSplitAppTy_maybe ty2 of
644 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
645 Nothing -> unifyMisMatch ps_ty1 ps_ty2
647 -- Now the same, but the other way round
648 -- Don't swap the types, because the error messages get worse
649 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
650 = case tcSplitAppTy_maybe ty1 of
651 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
652 Nothing -> unifyMisMatch ps_ty1 ps_ty2
654 -- Not expecting for-alls in unification
655 -- ... but the error message from the unifyMisMatch more informative
656 -- than a panic message!
658 -- Anything else fails
659 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
665 If you are tempted to make a short cut on synonyms, as in this
669 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
670 -- NO = if (con1 == con2) then
671 -- NO -- Good news! Same synonym constructors, so we can shortcut
672 -- NO -- by unifying their arguments and ignoring their expansions.
673 -- NO unifyTauTypeLists args1 args2
675 -- NO -- Never mind. Just expand them and try again
679 then THINK AGAIN. Here is the whole story, as detected and reported
680 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
682 Here's a test program that should detect the problem:
686 x = (1 :: Bogus Char) :: Bogus Bool
689 The problem with [the attempted shortcut code] is that
693 is not a sufficient condition to be able to use the shortcut!
694 You also need to know that the type synonym actually USES all
695 its arguments. For example, consider the following type synonym
696 which does not use all its arguments.
701 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
702 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
703 would fail, even though the expanded forms (both \tr{Int}) should
706 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
707 unnecessarily bind \tr{t} to \tr{Char}.
709 ... You could explicitly test for the problem synonyms and mark them
710 somehow as needing expansion, perhaps also issuing a warning to the
715 %************************************************************************
717 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
719 %************************************************************************
721 @uVar@ is called when at least one of the types being unified is a
722 variable. It does {\em not} assume that the variable is a fixed point
723 of the substitution; rather, notice that @uVar@ (defined below) nips
724 back into @uTys@ if it turns out that the variable is already bound.
727 uVar :: Bool -- False => tyvar is the "expected"
728 -- True => ty is the "expected" thing
730 -> TcTauType -> TcTauType -- printing and real versions
733 uVar swapped tv1 ps_ty2 ty2
734 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
735 getTcTyVar tv1 `thenM` \ maybe_ty1 ->
737 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
738 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
739 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
741 -- Expand synonyms; ignore FTVs
742 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
743 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
746 -- The both-type-variable case
747 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
749 -- Same type variable => no-op
753 -- Distinct type variables
754 -- ASSERT maybe_ty1 /= Just
756 = getTcTyVar tv2 `thenM` \ maybe_ty2 ->
758 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
762 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
763 putTcTyVar tv2 (TyVarTy tv1) `thenM_`
767 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
768 putTcTyVar tv1 ps_ty2 `thenM_`
773 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
774 -- Try to get rid of open type variables as soon as poss
776 nicer_to_update_tv2 = isUserTyVar tv1
777 -- Don't unify a signature type variable if poss
778 || isSystemName (varName tv2)
779 -- Try to update sys-y type variables in preference to sig-y ones
781 -- Second one isn't a type variable
782 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
783 = -- Check that tv1 isn't a type-signature type variable
784 checkM (not (isSkolemTyVar tv1))
785 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
787 -- Do the occurs check, and check that we are not
788 -- unifying a type variable with a polytype
789 -- Returns a zonked type ready for the update
790 checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
792 -- Check that the kinds match
793 checkKinds swapped tv1 ty2 `thenM_`
795 -- Perform the update
796 putTcTyVar tv1 ty2 `thenM_`
801 checkKinds swapped tv1 ty2
802 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
803 -- ty2 has been zonked at this stage, which ensures that
804 -- its kind has as much boxity information visible as possible.
805 | tk2 `hasMoreBoxityInfo` tk1 = returnM ()
808 -- Either the kinds aren't compatible
809 -- (can happen if we unify (a b) with (c d))
810 -- or we are unifying a lifted type variable with an
811 -- unlifted type: e.g. (id 3#) is illegal
812 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
816 (k1,k2) | swapped = (tk2,tk1)
817 | otherwise = (tk1,tk2)
823 checkValue tv1 ps_ty2 non_var_ty2
824 -- Do the occurs check, and check that we are not
825 -- unifying a type variable with a polytype
826 -- Return the type to update the type variable with, or fail
828 -- Basically we want to update tv1 := ps_ty2
829 -- because ps_ty2 has type-synonym info, which improves later error messages
834 -- f :: (A a -> a -> ()) -> ()
838 -- x = f (\ x p -> p x)
840 -- In the application (p x), we try to match "t" with "A t". If we go
841 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
842 -- an infinite loop later.
843 -- But we should not reject the program, because A t = ().
844 -- Rather, we should bind t to () (= non_var_ty2).
846 -- That's why we have this two-state occurs-check
847 = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
848 case okToUnifyWith tv1 ps_ty2' of {
849 Nothing -> returnM ps_ty2' ; -- Success
852 zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
853 case okToUnifyWith tv1 non_var_ty2' of
854 Nothing -> -- This branch rarely succeeds, except in strange cases
855 -- like that in the example above
858 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
861 data Problem = OccurCheck | NotMonoType
863 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
864 -- (okToUnifyWith tv ty) checks whether it's ok to unify
867 -- Just p => not ok, problem p
872 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
873 | otherwise = Nothing
874 ok (AppTy t1 t2) = ok t1 `and` ok t2
875 ok (FunTy t1 t2) = ok t1 `and` ok t2
876 ok (TyConApp _ ts) = oks ts
877 ok (NewTcApp _ ts) = oks ts
878 ok (ForAllTy _ _) = Just NotMonoType
879 ok (PredTy st) = ok_st st
880 ok (NoteTy (FTVNote _) t) = ok t
881 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
882 -- Type variables may be free in t1 but not t2
883 -- A forall may be in t2 but not t1
885 oks ts = foldr (and . ok) Nothing ts
887 ok_st (ClassP _ ts) = oks ts
888 ok_st (IParam _ t) = ok t
891 Just p `and` m = Just p
894 %************************************************************************
896 \subsection{Kind unification}
898 %************************************************************************
901 unifyKind :: TcKind -- Expected
904 unifyKind k1 k2 = uTys k1 k1 k2 k2
906 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
907 unifyKinds [] [] = returnM ()
908 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
910 unifyKinds _ _ = panic "unifyKinds: length mis-match"
914 unifyTypeKind :: TcKind -> TcM ()
915 -- Ensures that the argument kind is a liftedTypeKind or unliftedTypeKind
916 -- If it's a kind variable, make it (Type bx), for a fresh boxity variable bx
918 unifyTypeKind ty@(TyVarTy tyvar)
919 = getTcTyVar tyvar `thenM` \ maybe_ty ->
921 Just ty' -> unifyTypeKind ty'
922 Nothing -> newOpenTypeKind `thenM` \ kind ->
923 putTcTyVar tyvar kind `thenM_`
927 | isTypeKind ty = returnM ()
928 | otherwise -- Failure
929 = zonkTcType ty `thenM` \ ty1 ->
930 failWithTc (ptext SLIT("Type expected but") <+> quotes (ppr ty1) <+> ptext SLIT("found"))
934 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
935 -- Like unifyFunTy, but does not fail; instead just returns Nothing
937 unifyFunKind (TyVarTy tyvar)
938 = getTcTyVar tyvar `thenM` \ maybe_ty ->
940 Just fun_kind -> unifyFunKind fun_kind
941 Nothing -> newKindVar `thenM` \ arg_kind ->
942 newKindVar `thenM` \ res_kind ->
943 putTcTyVar tyvar (mkArrowKind arg_kind res_kind) `thenM_`
944 returnM (Just (arg_kind,res_kind))
946 unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
947 unifyFunKind (NoteTy _ ty) = unifyFunKind ty
948 unifyFunKind other = returnM Nothing
951 %************************************************************************
953 \subsection[Unify-context]{Errors and contexts}
955 %************************************************************************
961 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
962 = zonkTcType ty1 `thenM` \ ty1' ->
963 zonkTcType ty2 `thenM` \ ty2' ->
964 returnM (err ty1' ty2')
969 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
970 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
973 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
975 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
976 -- tv1 is zonked already
977 = zonkTcType ty2 `thenM` \ ty2' ->
980 err ty2 = (env2, ptext SLIT("When matching types") <+>
981 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
983 (pp_expected, pp_actual) | swapped = (pp2, pp1)
984 | otherwise = (pp1, pp2)
985 (env1, tv1') = tidyOpenTyVar tidy_env tv1
986 (env2, ty2') = tidyOpenType env1 ty2
990 unifyMisMatch ty1 ty2
991 = zonkTcType ty1 `thenM` \ ty1' ->
992 zonkTcType ty2 `thenM` \ ty2' ->
994 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
995 ppr | isSuperKind (typeKind ty1) = pprKind
996 | otherwise = pprType
997 msg = hang (ptext SLIT("Couldn't match"))
998 4 (sep [quotes (ppr tidy_ty1),
999 ptext SLIT("against"),
1000 quotes (ppr tidy_ty2)])
1002 failWithTcM (env, msg)
1004 unifyWithSigErr tyvar ty
1005 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1006 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1008 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1009 (env2, tidy_ty) = tidyOpenType env1 ty
1011 unifyCheck problem tyvar ty
1013 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1015 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1016 (env2, tidy_ty) = tidyOpenType env1 ty
1018 msg = case problem of
1019 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1020 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1025 %************************************************************************
1027 \subsection{Checking signature type variables}
1029 %************************************************************************
1031 @checkSigTyVars@ is used after the type in a type signature has been unified with
1032 the actual type found. It then checks that the type variables of the type signature
1034 (a) Still all type variables
1035 eg matching signature [a] against inferred type [(p,q)]
1036 [then a will be unified to a non-type variable]
1038 (b) Still all distinct
1039 eg matching signature [(a,b)] against inferred type [(p,p)]
1040 [then a and b will be unified together]
1042 (c) Not mentioned in the environment
1043 eg the signature for f in this:
1049 Here, f is forced to be monorphic by the free occurence of x.
1051 (d) Not (unified with another type variable that is) in scope.
1052 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1053 when checking the expression type signature, we find that
1054 even though there is nothing in scope whose type mentions r,
1055 nevertheless the type signature for the expression isn't right.
1057 Another example is in a class or instance declaration:
1059 op :: forall b. a -> b
1061 Here, b gets unified with a
1063 Before doing this, the substitution is applied to the signature type variable.
1065 We used to have the notion of a "DontBind" type variable, which would
1066 only be bound to itself or nothing. Then points (a) and (b) were
1067 self-checking. But it gave rise to bogus consequential error messages.
1070 f = (*) -- Monomorphic
1072 g :: Num a => a -> a
1075 Here, we get a complaint when checking the type signature for g,
1076 that g isn't polymorphic enough; but then we get another one when
1077 dealing with the (Num x) context arising from f's definition;
1078 we try to unify x with Int (to default it), but find that x has already
1079 been unified with the DontBind variable "a" from g's signature.
1080 This is really a problem with side-effecting unification; we'd like to
1081 undo g's effects when its type signature fails, but unification is done
1082 by side effect, so we can't (easily).
1084 So we revert to ordinary type variables for signatures, and try to
1085 give a helpful message in checkSigTyVars.
1088 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1089 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1091 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1092 checkSigTyVarsWrt extra_tvs sig_tvs
1093 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1094 check_sig_tyvars extra_tvs' sig_tvs
1097 :: TcTyVarSet -- Global type variables. The universally quantified
1098 -- tyvars should not mention any of these
1099 -- Guaranteed already zonked.
1100 -> [TcTyVar] -- Universally-quantified type variables in the signature
1101 -- Not guaranteed zonked.
1102 -> TcM [TcTyVar] -- Zonked signature type variables
1104 check_sig_tyvars extra_tvs []
1106 check_sig_tyvars extra_tvs sig_tvs
1107 = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
1108 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
1110 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1112 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1113 text "gbl_tvs" <+> ppr gbl_tvs,
1114 text "extra_tvs" <+> ppr extra_tvs])) `thenM_`
1116 checkM (allDistinctTyVars sig_tys env_tvs)
1117 (complain sig_tys env_tvs) `thenM_`
1119 returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
1122 complain sig_tys globals
1123 = -- "check" checks each sig tyvar in turn
1125 (env2, emptyVarEnv, [])
1126 (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
1128 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1130 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1131 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1133 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1135 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1136 -- sig_tyvar is from the signature;
1137 -- ty is what you get if you zonk sig_tyvar and then tidy it
1139 -- acc maps a zonked type variable back to a signature type variable
1140 = case tcGetTyVar_maybe ty of {
1141 Nothing -> -- Error (a)!
1142 returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1146 case lookupVarEnv acc tv of {
1147 Just sig_tyvar' -> -- Error (b)!
1148 returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1150 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1154 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1155 -- The least comprehensible, so put it last
1157 -- get the local TcIds and TyVars from the environment,
1158 -- and pass them to find_globals (they might have tv free)
1159 then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
1160 returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1163 returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1169 -----------------------
1170 escape_msg sig_tv tv globs
1171 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1172 if notNull globs then
1173 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1174 nest 2 (vcat globs)]
1176 empty -- Sigh. It's really hard to give a good error message
1177 -- all the time. One bad case is an existential pattern match.
1178 -- We rely on the "When..." context to help.
1180 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1181 | otherwise = ptext SLIT("It")
1184 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1185 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1188 These two context are used with checkSigTyVars
1191 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1192 -> TidyEnv -> TcM (TidyEnv, Message)
1193 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1194 = zonkTcType sig_tau `thenM` \ actual_tau ->
1196 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1197 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1198 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1199 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1200 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1202 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),