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, unifyOpenTypeKind, unifyFunKind,
16 --------------------------------
18 Expected(..), newHole, readExpectedType,
19 zapExpectedType, zapExpectedTo, zapExpectedBranches,
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(..), SourceType(..), TyNote(..), openKindCon )
35 import TcRnMonad -- TcType, amongst others
36 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
37 TcTyVarSet, TcThetaType, TyVarDetails(SigTv),
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
48 import Inst ( newDicts, instToId, tcInstCall )
49 import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar,
50 newTyVarTy, newTyVarTys, newOpenTypeKind,
51 zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV )
52 import TcSimplify ( tcSimplifyCheck )
53 import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
54 import TcEnv ( tcGetGlobalTyVars, findGlobals )
55 import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity )
56 import PprType ( pprType )
57 import Id ( Id, mkSysLocal )
58 import Var ( Var, varName, tyVarKind )
59 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems )
61 import Name ( isSystemName )
62 import ErrUtils ( Message )
63 import BasicTypes ( Boxity, Arity, isBoxed )
64 import Util ( equalLength, lengthExceeds, notNull )
70 * A hole is always filled in with an ordinary type, not another hole.
72 %************************************************************************
74 \subsection{'hole' type variables}
76 %************************************************************************
79 data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
80 | Check ty -- The type to check during type checking
82 newHole :: TcM (TcRef ty)
83 newHole = newMutVar (error "Empty hole in typechecker")
85 readExpectedType :: Expected ty -> TcM ty
86 readExpectedType (Infer hole) = readMutVar hole
87 readExpectedType (Check ty) = returnM ty
89 zapExpectedType :: Expected TcType -> TcM TcTauType
90 -- In the inference case, ensure we have a monotype
91 zapExpectedType (Infer hole)
92 = do { ty <- newTyVarTy openTypeKind ;
96 zapExpectedType (Check ty) = return ty
98 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
99 zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2
100 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
102 zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType)
103 -- Zap the expected type to a monotype if there is more than one branch
104 zapExpectedBranches branches exp_ty
105 | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' ->
106 return (Check exp_ty')
107 | otherwise = returnM exp_ty
109 instance Outputable ty => Outputable (Expected ty) where
110 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
111 ppr (Infer hole) = ptext SLIT("Inferring type")
115 %************************************************************************
117 \subsection[Unify-fun]{@unifyFunTy@}
119 %************************************************************************
121 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
122 creation of type variables.
124 * subFunTy is used when we might be faced with a "hole" type variable,
125 in which case we should create two new holes.
127 * unifyFunTy is used when we expect to encounter only "ordinary"
128 type variables, so we should create new ordinary type variables
131 subFunTy :: Expected TcRhoType -- Fail if ty isn't a function type
132 -- If it's a hole, make two holes, feed them to...
133 -> (Expected TcRhoType -> Expected TcRhoType -> TcM a) -- the thing inside
134 -> TcM a -- and bind the function type to the hole
136 subFunTy (Infer hole) thing_inside
137 = -- This is the interesting case
138 newHole `thenM` \ arg_hole ->
139 newHole `thenM` \ res_hole ->
142 thing_inside (Infer arg_hole) (Infer res_hole) `thenM` \ answer ->
144 -- Extract the answers
145 readMutVar arg_hole `thenM` \ arg_ty ->
146 readMutVar res_hole `thenM` \ res_ty ->
148 -- Write the answer into the incoming hole
149 writeMutVar hole (mkFunTy arg_ty res_ty) `thenM_`
151 -- And return the answer
154 subFunTy (Check ty) thing_inside
155 = unifyFunTy ty `thenM` \ (arg,res) ->
156 thing_inside (Check arg) (Check res)
159 unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
160 -> TcM (TcType, TcType) -- otherwise return arg and result types
162 unifyFunTy ty@(TyVarTy tyvar)
163 = getTcTyVar tyvar `thenM` \ maybe_ty ->
165 Just ty' -> unifyFunTy ty'
166 Nothing -> unify_fun_ty_help ty
169 = case tcSplitFunTy_maybe ty of
170 Just arg_and_res -> returnM arg_and_res
171 Nothing -> unify_fun_ty_help ty
173 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
174 = newTyVarTy openTypeKind `thenM` \ arg ->
175 newTyVarTy openTypeKind `thenM` \ res ->
176 unifyTauTy ty (mkFunTy arg res) `thenM_`
181 zapToListTy :: Expected TcType -- expected list type
182 -> TcM TcType -- list element type
184 zapToListTy (Check ty) = unifyListTy ty
185 zapToListTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
186 writeMutVar hole (mkListTy elt_ty) ;
189 unifyListTy :: TcType -> TcM TcType
190 unifyListTy ty@(TyVarTy tyvar)
191 = getTcTyVar tyvar `thenM` \ maybe_ty ->
193 Just ty' -> unifyListTy ty'
194 other -> unify_list_ty_help ty
197 = case tcSplitTyConApp_maybe ty of
198 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty
199 other -> unify_list_ty_help ty
201 unify_list_ty_help ty -- Revert to ordinary unification
202 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
203 unifyTauTy ty (mkListTy elt_ty) `thenM_`
206 -- variant for parallel arrays
208 zapToPArrTy :: Expected TcType -- Expected list type
209 -> TcM TcType -- List element type
211 zapToPArrTy (Check ty) = unifyPArrTy ty
212 zapToPArrTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
213 writeMutVar hole (mkPArrTy elt_ty) ;
216 unifyPArrTy :: TcType -> TcM TcType
218 unifyPArrTy ty@(TyVarTy tyvar)
219 = getTcTyVar tyvar `thenM` \ maybe_ty ->
221 Just ty' -> unifyPArrTy ty'
222 _ -> unify_parr_ty_help ty
224 = case tcSplitTyConApp_maybe ty of
225 Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty
226 _ -> unify_parr_ty_help ty
228 unify_parr_ty_help ty -- Revert to ordinary unification
229 = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
230 unifyTauTy ty (mkPArrTy elt_ty) `thenM_`
235 zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
236 zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
237 zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
238 writeMutVar hole tup_ty ;
241 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
242 = getTcTyVar tyvar `thenM` \ maybe_ty ->
244 Just ty' -> unifyTupleTy boxity arity ty'
245 other -> unify_tuple_ty_help boxity arity ty
247 unifyTupleTy boxity arity ty
248 = case tcSplitTyConApp_maybe ty of
249 Just (tycon, arg_tys)
251 && tyConArity tycon == arity
252 && tupleTyConBoxity tycon == boxity
254 other -> unify_tuple_ty_help boxity arity ty
256 unify_tuple_ty_help boxity arity ty
257 = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
258 unifyTauTy ty tup_ty `thenM_`
261 new_tuple_ty boxity arity
262 = newTyVarTys arity kind `thenM` \ arg_tys ->
263 return (mkTupleTy boxity arity arg_tys, arg_tys)
265 kind | isBoxed boxity = liftedTypeKind
266 | otherwise = openTypeKind
270 %************************************************************************
272 \subsection{Subsumption}
274 %************************************************************************
276 All the tcSub calls have the form
278 tcSub expected_ty offered_ty
280 offered_ty <= expected_ty
282 That is, that a value of type offered_ty is acceptable in
283 a place expecting a value of type expected_ty.
285 It returns a coercion function
286 co_fn :: offered_ty -> expected_ty
287 which takes an HsExpr of type offered_ty into one of type
291 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
292 tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn
295 These two check for holes
298 tcSubExp expected_ty offered_ty
299 = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_`
300 checkHole expected_ty offered_ty tcSub
302 tcSubOff expected_ty offered_ty
303 = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off)
305 -- checkHole looks for a hole in its first arg;
306 -- If so, and it is uninstantiated, it fills in the hole
307 -- with its second arg
308 -- Otherwise it calls thing_inside, passing the two args, looking
309 -- through any instantiated hole
311 checkHole (Infer hole) other_ty thing_inside
312 = do { writeMutVar hole other_ty; return idCoercion }
314 checkHole (Check ty) other_ty thing_inside
315 = thing_inside ty other_ty
318 No holes expected now. Add some error-check context info.
321 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
322 tcSub expected_ty actual_ty
323 = traceTc (text "tcSub" <+> details) `thenM_`
324 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
325 (tc_sub expected_ty expected_ty actual_ty actual_ty)
327 details = vcat [text "Expected:" <+> ppr expected_ty,
328 text "Actual: " <+> ppr actual_ty]
331 tc_sub carries the types before and after expanding type synonyms
334 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
335 -> TcSigmaType -- ..and after
336 -> TcSigmaType -- actual_ty, before
337 -> TcSigmaType -- ..and after
340 -----------------------------------
342 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
343 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
345 -----------------------------------
346 -- Generalisation case
347 -- actual_ty: d:Eq b => b->b
348 -- expected_ty: forall a. Ord a => a->a
349 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
351 -- It is essential to do this *before* the specialisation case
352 -- Example: f :: (Eq a => a->a) -> ...
353 -- g :: Ord b => b->b
356 tc_sub exp_sty expected_ty act_sty actual_ty
357 | isSigmaTy expected_ty
358 = tcGen expected_ty (tyVarsOfType actual_ty) (
359 -- It's really important to check for escape wrt the free vars of
360 -- both expected_ty *and* actual_ty
361 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
362 ) `thenM` \ (gen_fn, co_fn) ->
363 returnM (gen_fn <.> co_fn)
365 -----------------------------------
366 -- Specialisation case:
367 -- actual_ty: forall a. Ord a => a->a
368 -- expected_ty: Int -> Int
369 -- co_fn e = e Int dOrdInt
371 tc_sub exp_sty expected_ty act_sty actual_ty
372 | isSigmaTy actual_ty
373 = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) ->
374 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
375 returnM (co_fn <.> inst_fn)
377 -----------------------------------
380 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
381 = tcSub_fun exp_arg exp_res act_arg act_res
383 -----------------------------------
384 -- Type variable meets function: imitate
386 -- NB 1: we can't just unify the type variable with the type
387 -- because the type might not be a tau-type, and we aren't
388 -- allowed to instantiate an ordinary type variable with
391 -- NB 2: can we short-cut to an error case?
392 -- when the arg/res is not a tau-type?
393 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
395 -- is perfectly fine, because we can instantiat f's type to a monotype
397 -- However, we get can get jolly unhelpful error messages.
398 -- e.g. foo = id runST
400 -- Inferred type is less polymorphic than expected
401 -- Quantified type variable `s' escapes
402 -- Expected type: ST s a -> t
403 -- Inferred type: (forall s1. ST s1 a) -> a
404 -- In the first argument of `id', namely `runST'
405 -- In a right-hand side of function `foo': id runST
407 -- I'm not quite sure what to do about this!
409 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
410 = getTcTyVar tv `thenM` \ maybe_ty ->
412 Just ty -> tc_sub exp_sty exp_ty ty ty
413 Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) ->
414 tcSub_fun exp_arg exp_res act_arg act_res
416 tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res)
417 = getTcTyVar tv `thenM` \ maybe_ty ->
419 Just ty -> tc_sub ty ty act_sty act_ty
420 Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
421 tcSub_fun exp_arg exp_res act_arg act_res
423 -----------------------------------
425 -- If none of the above match, we revert to the plain unifier
426 tc_sub exp_sty expected_ty act_sty actual_ty
427 = uTys exp_sty expected_ty act_sty actual_ty `thenM_`
431 %************************************************************************
433 \subsection{Functions}
435 %************************************************************************
438 tcSub_fun exp_arg exp_res act_arg act_res
439 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
440 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
441 newUnique `thenM` \ uniq ->
443 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
444 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
445 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
446 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
447 coercion | isIdCoercion co_fn_arg,
448 isIdCoercion co_fn_res = idCoercion
449 | otherwise = mkCoercion co_fn
451 co_fn e = DictLam [arg_id]
452 (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id))))
453 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
454 -- HsVar arg_id :: HsExpr exp_arg
455 -- co_fn_arg $it :: HsExpr act_arg
456 -- HsApp e $it :: HsExpr act_res
457 -- co_fn_res $it :: HsExpr exp_res
461 imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
463 = -- NB: tv is an *ordinary* tyvar and so are the new ones
465 -- Check that tv isn't a type-signature type variable
466 -- (This would be found later in checkSigTyVars, but
467 -- we get a better error message if we do it here.)
468 checkM (not (isSkolemTyVar tv))
469 (failWithTcM (unifyWithSigErr tv ty)) `thenM_`
471 newTyVarTy openTypeKind `thenM` \ arg ->
472 newTyVarTy openTypeKind `thenM` \ res ->
473 putTcTyVar tv (mkFunTy arg res) `thenM_`
478 %************************************************************************
480 \subsection{Generalisation}
482 %************************************************************************
485 tcGen :: TcSigmaType -- expected_ty
486 -> TcTyVarSet -- Extra tyvars that the universally
487 -- quantified tyvars of expected_ty
488 -- must not be unified
489 -> (TcRhoType -> TcM result) -- spec_ty
490 -> TcM (ExprCoFn, result)
491 -- The expression has type: spec_ty -> expected_ty
493 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
494 -- If not, the call is a no-op
495 = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) ->
497 -- Type-check the arg and unify with poly type
498 getLIE (thing_inside phi_ty) `thenM` \ (result, lie) ->
500 -- Check that the "forall_tvs" havn't been constrained
501 -- The interesting bit here is that we must include the free variables
502 -- of the expected_ty. Here's an example:
503 -- runST (newVar True)
504 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
505 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
506 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
507 -- So now s' isn't unconstrained because it's linked to a.
508 -- Conclusion: include the free vars of the expected_ty in the
509 -- list of "free vars" for the signature check.
511 newDicts SignatureOrigin theta `thenM` \ dicts ->
512 tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds ->
515 zonkTcTyVars forall_tvs `thenM` \ forall_tys ->
516 traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
517 text "expected_ty" <+> ppr expected_ty,
518 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
519 text "free_tvs" <+> ppr free_tvs,
520 text "forall_tys" <+> ppr forall_tys]) `thenM_`
523 checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs ->
525 traceTc (text "tcGen:done") `thenM_`
528 -- This HsLet binds any Insts which came out of the simplification.
529 -- It's a bit out of place here, but using AbsBind involves inventing
530 -- a couple of new names which seems worse.
531 dict_ids = map instToId dicts
532 co_fn e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e))
534 returnM (mkCoercion co_fn, result)
536 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
537 sig_msg = ptext SLIT("expected type of an expression")
542 %************************************************************************
544 \subsection[Unify-exported]{Exported unification functions}
546 %************************************************************************
548 The exported functions are all defined as versions of some
549 non-exported generic functions.
551 Unify two @TauType@s. Dead straightforward.
554 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
555 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
556 = -- The unifier should only ever see tau-types
557 -- (no quantification whatsoever)
558 ASSERT2( isTauTy ty1, ppr ty1 )
559 ASSERT2( isTauTy ty2, ppr ty2 )
560 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
564 @unifyTauTyList@ unifies corresponding elements of two lists of
565 @TauType@s. It uses @uTys@ to do the real work. The lists should be
566 of equal length. We charge down the list explicitly so that we can
567 complain if their lengths differ.
570 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
571 unifyTauTyLists [] [] = returnM ()
572 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_`
573 unifyTauTyLists tys1 tys2
574 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
577 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
578 all together. It is used, for example, when typechecking explicit
579 lists, when all the elts should be of the same type.
582 unifyTauTyList :: [TcTauType] -> TcM ()
583 unifyTauTyList [] = returnM ()
584 unifyTauTyList [ty] = returnM ()
585 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
589 %************************************************************************
591 \subsection[Unify-uTys]{@uTys@: getting down to business}
593 %************************************************************************
595 @uTys@ is the heart of the unifier. Each arg happens twice, because
596 we want to report errors in terms of synomyms if poss. The first of
597 the pair is used in error messages only; it is always the same as the
598 second, except that if the first is a synonym then the second may be a
599 de-synonym'd version. This way we get better error messages.
601 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
604 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
605 -- ty1 is the *expected* type
607 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
608 -- ty2 is the *actual* type
611 -- Always expand synonyms (see notes at end)
612 -- (this also throws away FTVs)
613 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
614 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
616 -- Variables; go for uVar
617 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
618 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
619 -- "True" means args swapped
622 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
623 | n1 == n2 = uTys t1 t1 t2 t2
624 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
625 | c1 == c2 = unifyTauTyLists tys1 tys2
626 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
627 | tc1 == tc2 = unifyTauTyLists tys1 tys2
629 -- Functions; just check the two parts
630 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
631 = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2
633 -- Type constructors must match
634 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
635 | con1 == con2 && equalLength tys1 tys2
636 = unifyTauTyLists tys1 tys2
638 | con1 == openKindCon
639 -- When we are doing kind checking, we might match a kind '?'
640 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
641 -- (CCallable Int) and (CCallable Int#) are both OK
642 = unifyOpenTypeKind ps_ty2
644 -- Applications need a bit of care!
645 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
646 -- NB: we've already dealt with type variables and Notes,
647 -- so if one type is an App the other one jolly well better be too
648 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
649 = case tcSplitAppTy_maybe ty2 of
650 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
651 Nothing -> unifyMisMatch ps_ty1 ps_ty2
653 -- Now the same, but the other way round
654 -- Don't swap the types, because the error messages get worse
655 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
656 = case tcSplitAppTy_maybe ty1 of
657 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2
658 Nothing -> unifyMisMatch ps_ty1 ps_ty2
660 -- Not expecting for-alls in unification
661 -- ... but the error message from the unifyMisMatch more informative
662 -- than a panic message!
664 -- Anything else fails
665 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
671 If you are tempted to make a short cut on synonyms, as in this
675 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
676 -- NO = if (con1 == con2) then
677 -- NO -- Good news! Same synonym constructors, so we can shortcut
678 -- NO -- by unifying their arguments and ignoring their expansions.
679 -- NO unifyTauTypeLists args1 args2
681 -- NO -- Never mind. Just expand them and try again
685 then THINK AGAIN. Here is the whole story, as detected and reported
686 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
688 Here's a test program that should detect the problem:
692 x = (1 :: Bogus Char) :: Bogus Bool
695 The problem with [the attempted shortcut code] is that
699 is not a sufficient condition to be able to use the shortcut!
700 You also need to know that the type synonym actually USES all
701 its arguments. For example, consider the following type synonym
702 which does not use all its arguments.
707 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
708 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
709 would fail, even though the expanded forms (both \tr{Int}) should
712 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
713 unnecessarily bind \tr{t} to \tr{Char}.
715 ... You could explicitly test for the problem synonyms and mark them
716 somehow as needing expansion, perhaps also issuing a warning to the
721 %************************************************************************
723 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
725 %************************************************************************
727 @uVar@ is called when at least one of the types being unified is a
728 variable. It does {\em not} assume that the variable is a fixed point
729 of the substitution; rather, notice that @uVar@ (defined below) nips
730 back into @uTys@ if it turns out that the variable is already bound.
733 uVar :: Bool -- False => tyvar is the "expected"
734 -- True => ty is the "expected" thing
736 -> TcTauType -> TcTauType -- printing and real versions
739 uVar swapped tv1 ps_ty2 ty2
740 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
741 getTcTyVar tv1 `thenM` \ maybe_ty1 ->
743 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
744 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
745 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
747 -- Expand synonyms; ignore FTVs
748 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
749 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
752 -- The both-type-variable case
753 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
755 -- Same type variable => no-op
759 -- Distinct type variables
760 -- ASSERT maybe_ty1 /= Just
762 = getTcTyVar tv2 `thenM` \ maybe_ty2 ->
764 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
768 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
769 putTcTyVar tv2 (TyVarTy tv1) `thenM_`
773 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
774 putTcTyVar tv1 ps_ty2 `thenM_`
779 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
780 -- Try to get rid of open type variables as soon as poss
782 nicer_to_update_tv2 = isUserTyVar tv1
783 -- Don't unify a signature type variable if poss
784 || isSystemName (varName tv2)
785 -- Try to update sys-y type variables in preference to sig-y ones
787 -- Second one isn't a type variable
788 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
789 = -- Check that tv1 isn't a type-signature type variable
790 checkM (not (isSkolemTyVar tv1))
791 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_`
793 -- Do the occurs check, and check that we are not
794 -- unifying a type variable with a polytype
795 -- Returns a zonked type ready for the update
796 checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 ->
798 -- Check that the kinds match
799 checkKinds swapped tv1 ty2 `thenM_`
801 -- Perform the update
802 putTcTyVar tv1 ty2 `thenM_`
807 checkKinds swapped tv1 ty2
808 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
809 -- ty2 has been zonked at this stage, which ensures that
810 -- its kind has as much boxity information visible as possible.
811 | tk2 `hasMoreBoxityInfo` tk1 = returnM ()
814 -- Either the kinds aren't compatible
815 -- (can happen if we unify (a b) with (c d))
816 -- or we are unifying a lifted type variable with an
817 -- unlifted type: e.g. (id 3#) is illegal
818 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
822 (k1,k2) | swapped = (tk2,tk1)
823 | otherwise = (tk1,tk2)
829 checkValue tv1 ps_ty2 non_var_ty2
830 -- Do the occurs check, and check that we are not
831 -- unifying a type variable with a polytype
832 -- Return the type to update the type variable with, or fail
834 -- Basically we want to update tv1 := ps_ty2
835 -- because ps_ty2 has type-synonym info, which improves later error messages
840 -- f :: (A a -> a -> ()) -> ()
844 -- x = f (\ x p -> p x)
846 -- In the application (p x), we try to match "t" with "A t". If we go
847 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
848 -- an infinite loop later.
849 -- But we should not reject the program, because A t = ().
850 -- Rather, we should bind t to () (= non_var_ty2).
852 -- That's why we have this two-state occurs-check
853 = zonkTcType ps_ty2 `thenM` \ ps_ty2' ->
854 case okToUnifyWith tv1 ps_ty2' of {
855 Nothing -> returnM ps_ty2' ; -- Success
858 zonkTcType non_var_ty2 `thenM` \ non_var_ty2' ->
859 case okToUnifyWith tv1 non_var_ty2' of
860 Nothing -> -- This branch rarely succeeds, except in strange cases
861 -- like that in the example above
864 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
867 data Problem = OccurCheck | NotMonoType
869 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
870 -- (okToUnifyWith tv ty) checks whether it's ok to unify
873 -- Just p => not ok, problem p
878 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
879 | otherwise = Nothing
880 ok (AppTy t1 t2) = ok t1 `and` ok t2
881 ok (FunTy t1 t2) = ok t1 `and` ok t2
882 ok (TyConApp _ ts) = oks ts
883 ok (ForAllTy _ _) = Just NotMonoType
884 ok (SourceTy st) = ok_st st
885 ok (NoteTy (FTVNote _) t) = ok t
886 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
887 -- Type variables may be free in t1 but not t2
888 -- A forall may be in t2 but not t1
890 oks ts = foldr (and . ok) Nothing ts
892 ok_st (ClassP _ ts) = oks ts
893 ok_st (IParam _ t) = ok t
894 ok_st (NType _ ts) = oks ts
897 Just p `and` m = Just p
900 %************************************************************************
902 \subsection{Kind unification}
904 %************************************************************************
907 unifyKind :: TcKind -- Expected
910 unifyKind k1 k2 = uTys k1 k1 k2 k2
912 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
913 unifyKinds [] [] = returnM ()
914 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
916 unifyKinds _ _ = panic "unifyKinds: length mis-match"
920 unifyOpenTypeKind :: TcKind -> TcM ()
921 -- Ensures that the argument kind is of the form (Type bx)
922 -- for some boxity bx
924 unifyOpenTypeKind ty@(TyVarTy tyvar)
925 = getTcTyVar tyvar `thenM` \ maybe_ty ->
927 Just ty' -> unifyOpenTypeKind ty'
928 other -> unify_open_kind_help ty
931 | isTypeKind ty = returnM ()
932 | otherwise = unify_open_kind_help ty
934 unify_open_kind_help ty -- Revert to ordinary unification
935 = newOpenTypeKind `thenM` \ open_kind ->
936 unifyKind ty open_kind
940 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
941 -- Like unifyFunTy, but does not fail; instead just returns Nothing
943 unifyFunKind (TyVarTy tyvar)
944 = getTcTyVar tyvar `thenM` \ maybe_ty ->
946 Just fun_kind -> unifyFunKind fun_kind
947 Nothing -> newKindVar `thenM` \ arg_kind ->
948 newKindVar `thenM` \ res_kind ->
949 putTcTyVar tyvar (mkArrowKind arg_kind res_kind) `thenM_`
950 returnM (Just (arg_kind,res_kind))
952 unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
953 unifyFunKind (NoteTy _ ty) = unifyFunKind ty
954 unifyFunKind other = returnM Nothing
957 %************************************************************************
959 \subsection[Unify-context]{Errors and contexts}
961 %************************************************************************
967 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
968 = zonkTcType ty1 `thenM` \ ty1' ->
969 zonkTcType ty2 `thenM` \ ty2' ->
970 returnM (err ty1' ty2')
975 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
976 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
979 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
981 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
982 -- tv1 is zonked already
983 = zonkTcType ty2 `thenM` \ ty2' ->
986 err ty2 = (env2, ptext SLIT("When matching types") <+>
987 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
989 (pp_expected, pp_actual) | swapped = (pp2, pp1)
990 | otherwise = (pp1, pp2)
991 (env1, tv1') = tidyOpenTyVar tidy_env tv1
992 (env2, ty2') = tidyOpenType env1 ty2
996 unifyMisMatch ty1 ty2
997 = zonkTcType ty1 `thenM` \ ty1' ->
998 zonkTcType ty2 `thenM` \ ty2' ->
1000 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1001 msg = hang (ptext SLIT("Couldn't match"))
1002 4 (sep [quotes (ppr tidy_ty1),
1003 ptext SLIT("against"),
1004 quotes (ppr tidy_ty2)])
1006 failWithTcM (env, msg)
1008 unifyWithSigErr tyvar ty
1009 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1010 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1012 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1013 (env2, tidy_ty) = tidyOpenType env1 ty
1015 unifyCheck problem tyvar ty
1017 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1019 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1020 (env2, tidy_ty) = tidyOpenType env1 ty
1022 msg = case problem of
1023 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1024 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1029 %************************************************************************
1031 \subsection{Checking signature type variables}
1033 %************************************************************************
1035 @checkSigTyVars@ is used after the type in a type signature has been unified with
1036 the actual type found. It then checks that the type variables of the type signature
1038 (a) Still all type variables
1039 eg matching signature [a] against inferred type [(p,q)]
1040 [then a will be unified to a non-type variable]
1042 (b) Still all distinct
1043 eg matching signature [(a,b)] against inferred type [(p,p)]
1044 [then a and b will be unified together]
1046 (c) Not mentioned in the environment
1047 eg the signature for f in this:
1053 Here, f is forced to be monorphic by the free occurence of x.
1055 (d) Not (unified with another type variable that is) in scope.
1056 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1057 when checking the expression type signature, we find that
1058 even though there is nothing in scope whose type mentions r,
1059 nevertheless the type signature for the expression isn't right.
1061 Another example is in a class or instance declaration:
1063 op :: forall b. a -> b
1065 Here, b gets unified with a
1067 Before doing this, the substitution is applied to the signature type variable.
1069 We used to have the notion of a "DontBind" type variable, which would
1070 only be bound to itself or nothing. Then points (a) and (b) were
1071 self-checking. But it gave rise to bogus consequential error messages.
1074 f = (*) -- Monomorphic
1076 g :: Num a => a -> a
1079 Here, we get a complaint when checking the type signature for g,
1080 that g isn't polymorphic enough; but then we get another one when
1081 dealing with the (Num x) context arising from f's definition;
1082 we try to unify x with Int (to default it), but find that x has already
1083 been unified with the DontBind variable "a" from g's signature.
1084 This is really a problem with side-effecting unification; we'd like to
1085 undo g's effects when its type signature fails, but unification is done
1086 by side effect, so we can't (easily).
1088 So we revert to ordinary type variables for signatures, and try to
1089 give a helpful message in checkSigTyVars.
1092 checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar]
1093 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1095 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar]
1096 checkSigTyVarsWrt extra_tvs sig_tvs
1097 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1098 check_sig_tyvars extra_tvs' sig_tvs
1101 :: TcTyVarSet -- Global type variables. The universally quantified
1102 -- tyvars should not mention any of these
1103 -- Guaranteed already zonked.
1104 -> [TcTyVar] -- Universally-quantified type variables in the signature
1105 -- Not guaranteed zonked.
1106 -> TcM [TcTyVar] -- Zonked signature type variables
1108 check_sig_tyvars extra_tvs []
1110 check_sig_tyvars extra_tvs sig_tvs
1111 = zonkTcTyVars sig_tvs `thenM` \ sig_tys ->
1112 tcGetGlobalTyVars `thenM` \ gbl_tvs ->
1114 env_tvs = gbl_tvs `unionVarSet` extra_tvs
1116 traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys,
1117 text "gbl_tvs" <+> ppr gbl_tvs,
1118 text "extra_tvs" <+> ppr extra_tvs])) `thenM_`
1120 checkM (allDistinctTyVars sig_tys env_tvs)
1121 (complain sig_tys env_tvs) `thenM_`
1123 returnM (map (tcGetTyVar "checkSigTyVars") sig_tys)
1126 complain sig_tys globals
1127 = -- "check" checks each sig tyvar in turn
1129 (env2, emptyVarEnv, [])
1130 (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) ->
1132 failWithTcM (env3, main_msg $$ nest 4 (vcat msgs))
1134 (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1135 (env2, tidy_tys) = tidyOpenTypes env1 sig_tys
1137 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1139 check (tidy_env, acc, msgs) (sig_tyvar,ty)
1140 -- sig_tyvar is from the signature;
1141 -- ty is what you get if you zonk sig_tyvar and then tidy it
1143 -- acc maps a zonked type variable back to a signature type variable
1144 = case tcGetTyVar_maybe ty of {
1145 Nothing -> -- Error (a)!
1146 returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ;
1150 case lookupVarEnv acc tv of {
1151 Just sig_tyvar' -> -- Error (b)!
1152 returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs)
1154 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1158 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1159 -- The least comprehensible, so put it last
1161 -- get the local TcIds and TyVars from the environment,
1162 -- and pass them to find_globals (they might have tv free)
1163 then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
1164 returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs)
1167 returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs)
1173 -----------------------
1174 escape_msg sig_tv tv globs
1175 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1176 if notNull globs then
1177 vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"),
1178 nest 2 (vcat globs)]
1180 empty -- Sigh. It's really hard to give a good error message
1181 -- all the time. One bad case is an existential pattern match.
1182 -- We rely on the "When..." context to help.
1184 pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
1185 | otherwise = ptext SLIT("It")
1188 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1189 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1192 These two context are used with checkSigTyVars
1195 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1196 -> TidyEnv -> TcM (TidyEnv, Message)
1197 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1198 = zonkTcType sig_tau `thenM` \ actual_tau ->
1200 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1201 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1202 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1203 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1204 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1206 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),