2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Type subsumption and unification}
8 -- Full-blown subsumption
9 tcSubPat, tcSubExp, tcGen,
10 checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
12 -- Various unifications
13 unifyTauTy, unifyTauTyList,
14 unifyKind, unifyKinds, unifyFunKind,
17 --------------------------------
19 Expected(..), tcInfer, readExpectedType,
20 zapExpectedType, zapExpectedTo, zapExpectedBranches,
21 subFunTys, unifyFunTys,
22 zapToListTy, unifyListTy,
23 zapToTyConApp, unifyTyConApp,
27 #include "HsVersions.h"
30 import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats )
31 import TcHsSyn ( mkHsLet, mkHsDictLam,
32 ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) )
33 import TypeRep ( Type(..), PredType(..), TyNote(..) )
35 import TcRnMonad -- TcType, amongst others
36 import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
37 TcTyVarSet, TcThetaType,
38 SkolemInfo( GenSkol ), MetaDetails(..),
39 pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
40 tcSplitAppTy_maybe, tcSplitTyConApp_maybe,
41 tyVarsOfType, mkPhiTy, mkTyVarTy,
42 typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
43 tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
44 pprType, isSkolemTyVar )
45 import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
46 openTypeKind, liftedTypeKind, mkArrowKind, kindFunResult,
47 isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
48 isSubKind, pprKind, splitKindFunTys )
49 import Inst ( newDicts, instToId, tcInstCall )
50 import TcMType ( condLookupTcTyVar, LookupTyVarResult(..),
51 putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
52 newTyFlexiVarTy, zonkTcKind,
53 zonkType, zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV,
54 readKindVar, writeKindVar )
55 import TcSimplify ( tcSimplifyCheck )
56 import TcEnv ( tcGetGlobalTyVars, findGlobals )
57 import TyCon ( TyCon, tyConArity, tyConTyVars )
58 import TysWiredIn ( listTyCon )
59 import Id ( Id, mkSysLocal )
60 import Var ( Var, varName, tyVarKind )
61 import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet,
62 varSetElems, intersectsVarSet, mkVarSet )
64 import Name ( isSystemName, mkSysTvName )
65 import ErrUtils ( Message )
66 import SrcLoc ( noLoc )
67 import BasicTypes ( Arity )
68 import Util ( notNull )
74 * A hole is always filled in with an ordinary type, not another hole.
76 %************************************************************************
78 \subsection{'hole' type variables}
80 %************************************************************************
83 data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
84 | Check ty -- The type to check during type checking
86 newHole = newMutVar (error "Empty hole in typechecker")
88 tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty)
90 = do { hole <- newHole
91 ; res <- tc_infer (Infer hole)
92 ; res_ty <- readMutVar hole
93 ; return (res, res_ty) }
95 readExpectedType :: Expected ty -> TcM ty
96 readExpectedType (Infer hole) = readMutVar hole
97 readExpectedType (Check ty) = returnM ty
99 zapExpectedType :: Expected TcType -> Kind -> TcM TcTauType
100 -- In the inference case, ensure we have a monotype
101 -- (including an unboxed tuple)
102 zapExpectedType (Infer hole) kind
103 = do { ty <- newTyFlexiVarTy kind ;
104 writeMutVar hole ty ;
107 zapExpectedType (Check ty) kind
108 | typeKind ty `isSubKind` kind = return ty
109 | otherwise = do { ty1 <- newTyFlexiVarTy kind
112 -- The unify is to ensure that 'ty' has the desired kind
113 -- For example, in (case e of r -> b) we push an OpenTypeKind
116 zapExpectedBranches :: MatchGroup id -> Expected TcRhoType -> TcM (Expected TcRhoType)
117 -- If there is more than one branch in a case expression,
118 -- and exp_ty is a 'hole', all branches must be types, not type schemes,
119 -- otherwise the order in which we check them would affect the result.
120 zapExpectedBranches (MatchGroup [match] _) exp_ty
121 = return exp_ty -- One branch
122 zapExpectedBranches matches (Check ty)
124 zapExpectedBranches matches (Infer hole)
125 = do { -- Many branches, and inference mode,
126 -- so switch to checking mode with a monotype
127 ty <- newTyFlexiVarTy openTypeKind
128 ; writeMutVar hole ty
129 ; return (Check ty) }
131 zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
132 zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
133 zapExpectedTo (Infer hole) ty2 = do { ty2' <- zonkTcType ty2; writeMutVar hole ty2' }
134 -- See Note [Zonk return type]
136 instance Outputable ty => Outputable (Expected ty) where
137 ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
138 ppr (Infer hole) = ptext SLIT("Inferring type")
142 %************************************************************************
144 \subsection[Unify-fun]{@unifyFunTy@}
146 %************************************************************************
148 @subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
149 creation of type variables.
151 * subFunTy is used when we might be faced with a "hole" type variable,
152 in which case we should create two new holes.
154 * unifyFunTy is used when we expect to encounter only "ordinary"
155 type variables, so we should create new ordinary type variables
158 subFunTys :: MatchGroup name
159 -> Expected TcRhoType -- Fail if ty isn't a function type
160 -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a)
163 subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside
164 = -- This is the interesting case
165 ASSERT( null null_matches )
166 do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match)
167 ; res_hole <- newHole
170 ; res <- thing_inside (map Infer pat_holes) (Infer res_hole)
172 -- Extract the answers
173 ; arg_tys <- mapM readMutVar pat_holes
174 ; res_ty <- readMutVar res_hole
176 -- Write the answer into the incoming hole
177 ; writeMutVar hole (mkFunTys arg_tys res_ty)
179 -- And return the answer
182 subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside
183 = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches )
184 -- Assertion just checks that all the matches have the same number of pats
185 do { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty
186 ; thing_inside (map Check pat_tys) (Check res_ty) }
188 unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
189 -- Fail if ty isn't a function type, otherwise return arg and result types
190 -- The result types are guaranteed wobbly if the argument is wobbly
192 -- Does not allocate unnecessary meta variables: if the input already is
193 -- a function, we just take it apart. Not only is this efficient, it's important
194 -- for (a) higher rank: the argument might be of form
195 -- (forall a. ty) -> other
196 -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd
197 -- blow up with the meta var meets the forall
199 -- (b) GADTs: if the argument is not wobbly we do not want the result to be
201 unifyFunTys arity ty = unify_fun_ty True arity ty
203 unify_fun_ty use_refinement arity ty
205 = do { res_ty <- wobblify use_refinement ty
208 unify_fun_ty use_refinement arity (NoteTy _ ty)
209 = unify_fun_ty use_refinement arity ty
211 unify_fun_ty use_refinement arity ty@(TyVarTy tv)
212 = do { details <- condLookupTcTyVar use_refinement tv
214 IndirectTv use' ty' -> unify_fun_ty use' arity ty'
215 other -> unify_fun_help arity ty
218 unify_fun_ty use_refinement arity ty
219 = case tcSplitFunTy_maybe ty of
220 Just (arg,res) -> do { arg' <- wobblify use_refinement arg
221 ; (args', res') <- unify_fun_ty use_refinement (arity-1) res
222 ; return (arg':args', res') }
224 Nothing -> unify_fun_help arity ty
225 -- Usually an error, but ty could be (a Int Bool), which can match
227 unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType)
228 unify_fun_help arity ty
229 = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind)
230 ; res <- newTyFlexiVarTy openTypeKind
231 ; unifyTauTy ty (mkFunTys args res)
232 ; return (args, res) }
236 ----------------------
237 zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> *
238 -> Expected TcSigmaType -- Expected type (T a b c)
239 -> TcM [TcType] -- Element types, a b c
240 -- Insists that the Expected type is not a forall-type
242 zapToTyConApp tc (Check ty)
243 = unifyTyConApp tc ty -- NB: fails for a forall-type
244 zapToTyConApp tc (Infer hole)
245 = do { (tc_app, elt_tys) <- newTyConApp tc
246 ; writeMutVar hole tc_app
249 zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists
250 zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty
253 ----------------------
254 unifyTyConApp :: TyCon -> TcType -> TcM [TcType]
255 unifyTyConApp tc ty = unify_tc_app True tc ty
256 -- Add a boolean flag to remember whether to use
257 -- the type refinement or not
259 unifyListTy :: TcType -> TcM TcType -- Special case for lists
260 unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty
264 unify_tc_app use_refinement tc (NoteTy _ ty)
265 = unify_tc_app use_refinement tc ty
267 unify_tc_app use_refinement tc ty@(TyVarTy tyvar)
268 = do { details <- condLookupTcTyVar use_refinement tyvar
270 IndirectTv use' ty' -> unify_tc_app use' tc ty'
271 other -> unify_tc_app_help tc ty
274 unify_tc_app use_refinement tc ty
275 | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty,
277 = ASSERT( tyConArity tycon == length arg_tys ) -- ty::*
278 mapM (wobblify use_refinement) arg_tys
280 unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty
283 unify_tc_app_help tc ty -- Revert to ordinary unification
284 = do { (tc_app, arg_tys) <- newTyConApp tc
285 ; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty)
286 unifyMisMatch ty tc_app
288 { unifyTauTy ty tc_app
289 ; returnM arg_tys } }
292 ----------------------
293 unifyAppTy :: TcType -- Expected type function: m
294 -> TcType -- Type to split: m a
295 -> TcM TcType -- Type arg: a
296 unifyAppTy tc ty = unify_app_ty True tc ty
298 unify_app_ty use tc (NoteTy _ ty) = unify_app_ty use tc ty
300 unify_app_ty use tc ty@(TyVarTy tyvar)
301 = do { details <- condLookupTcTyVar use tyvar
303 IndirectTv use' ty' -> unify_app_ty use' tc ty'
304 other -> unify_app_ty_help tc ty
307 unify_app_ty use tc ty
308 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty
309 = do { unifyTauTy tc fun_ty
310 ; wobblify use arg_ty }
312 | otherwise = unify_app_ty_help tc ty
314 unify_app_ty_help tc ty -- Revert to ordinary unification
315 = do { arg_ty <- newTyFlexiVarTy (kindFunResult (typeKind tc))
316 ; unifyTauTy (mkAppTy tc arg_ty) ty
320 ----------------------
321 wobblify :: Bool -- True <=> don't wobblify
324 -- Return a wobbly type. At the moment we do that by
325 -- allocating a fresh meta type variable.
326 wobblify True ty = return ty
327 wobblify False ty = do { uniq <- newUnique
328 ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w"))
331 ; return (mkTyVarTy tv) }
333 ----------------------
334 newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType])
335 newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc)
336 ; return (mkTyConApp tc args, args) }
340 %************************************************************************
342 \subsection{Subsumption}
344 %************************************************************************
346 All the tcSub calls have the form
348 tcSub expected_ty offered_ty
350 offered_ty <= expected_ty
352 That is, that a value of type offered_ty is acceptable in
353 a place expecting a value of type expected_ty.
355 It returns a coercion function
356 co_fn :: offered_ty -> expected_ty
357 which takes an HsExpr of type offered_ty into one of type
361 -----------------------
362 -- tcSubExp is used for expressions
363 tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
365 tcSubExp (Infer hole) offered_ty
366 = do { offered' <- zonkTcType offered_ty
367 -- Note [Zonk return type]
368 -- zonk to take advantage of the current GADT type refinement.
369 -- If we don't we get spurious "existential type variable escapes":
370 -- case (x::Maybe a) of
371 -- Just b (y::b) -> y
372 -- We need the refinement [b->a] to be applied to the result type
373 ; writeMutVar hole offered'
374 ; return idCoercion }
376 tcSubExp (Check expected_ty) offered_ty
377 = tcSub expected_ty offered_ty
379 -----------------------
380 -- tcSubPat is used for patterns
381 tcSubPat :: TcSigmaType -- Pattern type signature
382 -> Expected TcSigmaType -- Type from context
384 -- In patterns we insist on an exact match; hence no CoFn returned
385 -- See Note [Pattern coercions] in TcPat
386 -- However, we can't call unify directly, because both types might be
387 -- polymorphic; hence the call to tcSub, followed by a check for
388 -- the identity coercion
390 tcSubPat sig_ty (Infer hole)
391 = do { sig_ty' <- zonkTcType sig_ty
392 ; writeMutVar hole sig_ty' -- See notes with tcSubExp above
395 tcSubPat sig_ty (Check exp_ty)
396 = do { co_fn <- tcSub sig_ty exp_ty
398 ; if isIdCoercion co_fn then
401 unifyMisMatch sig_ty exp_ty }
406 %************************************************************************
408 tcSub: main subsumption-check code
410 %************************************************************************
412 No holes expected now. Add some error-check context info.
416 tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
417 -- tcSub exp act checks that
419 tcSub expected_ty actual_ty
420 = traceTc (text "tcSub" <+> details) `thenM_`
421 addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
422 (tc_sub expected_ty expected_ty actual_ty actual_ty)
424 details = vcat [text "Expected:" <+> ppr expected_ty,
425 text "Actual: " <+> ppr actual_ty]
428 tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms
429 -> TcSigmaType -- ..and after
430 -> TcSigmaType -- actual_ty, before
431 -> TcSigmaType -- ..and after
434 -----------------------------------
436 tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty
437 tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty
439 -----------------------------------
440 -- Generalisation case
441 -- actual_ty: d:Eq b => b->b
442 -- expected_ty: forall a. Ord a => a->a
443 -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e
445 -- It is essential to do this *before* the specialisation case
446 -- Example: f :: (Eq a => a->a) -> ...
447 -- g :: Ord b => b->b
450 tc_sub exp_sty expected_ty act_sty actual_ty
451 | isSigmaTy expected_ty
452 = tcGen expected_ty (tyVarsOfType actual_ty) (
453 -- It's really important to check for escape wrt the free vars of
454 -- both expected_ty *and* actual_ty
455 \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty
456 ) `thenM` \ (gen_fn, co_fn) ->
457 returnM (gen_fn <.> co_fn)
459 -----------------------------------
460 -- Specialisation case:
461 -- actual_ty: forall a. Ord a => a->a
462 -- expected_ty: Int -> Int
463 -- co_fn e = e Int dOrdInt
465 tc_sub exp_sty expected_ty act_sty actual_ty
466 | isSigmaTy actual_ty
467 = tcInstCall InstSigOrigin actual_ty `thenM` \ (inst_fn, _, body_ty) ->
468 tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn ->
469 returnM (co_fn <.> inst_fn)
471 -----------------------------------
474 tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res)
475 = tcSub_fun exp_arg exp_res act_arg act_res
477 -----------------------------------
478 -- Type variable meets function: imitate
480 -- NB 1: we can't just unify the type variable with the type
481 -- because the type might not be a tau-type, and we aren't
482 -- allowed to instantiate an ordinary type variable with
485 -- NB 2: can we short-cut to an error case?
486 -- when the arg/res is not a tau-type?
487 -- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int
489 -- is perfectly fine, because we can instantiate f's type to a monotype
491 -- However, we get can get jolly unhelpful error messages.
492 -- e.g. foo = id runST
494 -- Inferred type is less polymorphic than expected
495 -- Quantified type variable `s' escapes
496 -- Expected type: ST s a -> t
497 -- Inferred type: (forall s1. ST s1 a) -> a
498 -- In the first argument of `id', namely `runST'
499 -- In a right-hand side of function `foo': id runST
501 -- I'm not quite sure what to do about this!
503 tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty
504 = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty
505 ; tcSub_fun exp_arg exp_res act_arg act_res }
507 tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res)
508 = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty
509 ; tcSub_fun exp_arg exp_res act_arg act_res }
511 -----------------------------------
513 -- If none of the above match, we revert to the plain unifier
514 tc_sub exp_sty expected_ty act_sty actual_ty
515 = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_`
520 tcSub_fun exp_arg exp_res act_arg act_res
521 = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg ->
522 tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res ->
523 newUnique `thenM` \ uniq ->
525 -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg
526 -- co_fn_res :: HsExpr act_res -> HsExpr exp_res
527 -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res)
528 arg_id = mkSysLocal FSLIT("sub") uniq exp_arg
529 coercion | isIdCoercion co_fn_arg,
530 isIdCoercion co_fn_res = idCoercion
531 | otherwise = mkCoercion co_fn
533 co_fn e = DictLam [arg_id]
534 (noLoc (co_fn_res <$> (HsApp (noLoc e) (noLoc (co_fn_arg <$> HsVar arg_id)))))
535 -- Slight hack; using a "DictLam" to get an ordinary simple lambda
536 -- HsVar arg_id :: HsExpr exp_arg
537 -- co_fn_arg $it :: HsExpr act_arg
538 -- HsApp e $it :: HsExpr act_res
539 -- co_fn_res $it :: HsExpr exp_res
545 %************************************************************************
547 \subsection{Generalisation}
549 %************************************************************************
552 tcGen :: TcSigmaType -- expected_ty
553 -> TcTyVarSet -- Extra tyvars that the universally
554 -- quantified tyvars of expected_ty
555 -- must not be unified
556 -> (TcRhoType -> TcM result) -- spec_ty
557 -> TcM (ExprCoFn, result)
558 -- The expression has type: spec_ty -> expected_ty
560 tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type
561 -- If not, the call is a no-op
562 = do { span <- getSrcSpanM
563 ; let rigid_info = GenSkol expected_ty span
564 ; (forall_tvs, theta, phi_ty) <- tcSkolType rigid_info expected_ty
566 -- Type-check the arg and unify with poly type
567 ; (result, lie) <- getLIE (thing_inside phi_ty)
569 -- Check that the "forall_tvs" havn't been constrained
570 -- The interesting bit here is that we must include the free variables
571 -- of the expected_ty. Here's an example:
572 -- runST (newVar True)
573 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool))
574 -- for (newVar True), with s fresh. Then we unify with the runST's arg type
575 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
576 -- So now s' isn't unconstrained because it's linked to a.
577 -- Conclusion: include the free vars of the expected_ty in the
578 -- list of "free vars" for the signature check.
580 ; dicts <- newDicts (SigOrigin rigid_info) theta
581 ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie
584 ; forall_tys <- zonkTcTyVars forall_tvs
585 ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs,
586 text "expected_ty" <+> ppr expected_ty,
587 text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr phi_ty,
588 text "free_tvs" <+> ppr free_tvs,
589 text "forall_tys" <+> ppr forall_tys])
592 ; checkSigTyVarsWrt free_tvs forall_tvs
593 ; traceTc (text "tcGen:done")
596 -- This HsLet binds any Insts which came out of the simplification.
597 -- It's a bit out of place here, but using AbsBind involves inventing
598 -- a couple of new names which seems worse.
599 dict_ids = map instToId dicts
600 co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e)))
601 ; returnM (mkCoercion co_fn, result) }
603 free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
604 sig_msg = ptext SLIT("expected type of an expression")
609 %************************************************************************
611 \subsection[Unify-exported]{Exported unification functions}
613 %************************************************************************
615 The exported functions are all defined as versions of some
616 non-exported generic functions.
618 Unify two @TauType@s. Dead straightforward.
621 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
622 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
623 = -- The unifier should only ever see tau-types
624 -- (no quantification whatsoever)
625 ASSERT2( isTauTy ty1, ppr ty1 )
626 ASSERT2( isTauTy ty2, ppr ty2 )
627 addErrCtxtM (unifyCtxt "type" ty1 ty2) $
628 uTys True ty1 ty1 True ty2 ty2
631 @unifyTauTyList@ unifies corresponding elements of two lists of
632 @TauType@s. It uses @uTys@ to do the real work. The lists should be
633 of equal length. We charge down the list explicitly so that we can
634 complain if their lengths differ.
637 unifyTauTyLists :: Bool -> -- Allow refinements on tys1
639 Bool -> -- Allow refinements on tys2
640 [TcTauType] -> TcM ()
641 -- Precondition: lists must be same length
642 -- Having the caller check gives better error messages
643 -- Actually the caller neve does need to check; see Note [Tycon app]
644 unifyTauTyLists r1 [] r2 [] = returnM ()
645 unifyTauTyLists r1 (ty1:tys1) r2 (ty2:tys2) = uTys r1 ty1 ty1 r2 ty2 ty2 `thenM_`
646 unifyTauTyLists r1 tys1 r2 tys2
647 unifyTauTyLists r1 ty1s r2 ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
650 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
651 all together. It is used, for example, when typechecking explicit
652 lists, when all the elts should be of the same type.
655 unifyTauTyList :: [TcTauType] -> TcM ()
656 unifyTauTyList [] = returnM ()
657 unifyTauTyList [ty] = returnM ()
658 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_`
662 %************************************************************************
664 \subsection[Unify-uTys]{@uTys@: getting down to business}
666 %************************************************************************
668 @uTys@ is the heart of the unifier. Each arg happens twice, because
669 we want to report errors in terms of synomyms if poss. The first of
670 the pair is used in error messages only; it is always the same as the
671 second, except that if the first is a synonym then the second may be a
672 de-synonym'd version. This way we get better error messages.
674 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
677 uTys :: Bool -- Allow refinements to ty1
678 -> TcTauType -> TcTauType -- Error reporting ty1 and real ty1
679 -- ty1 is the *expected* type
680 -> Bool -- Allow refinements to ty2
681 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
682 -- ty2 is the *actual* type
685 -- Always expand synonyms (see notes at end)
686 -- (this also throws away FTVs)
687 uTys r1 ps_ty1 (NoteTy n1 ty1) r2 ps_ty2 ty2 = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
688 uTys r1 ps_ty1 ty1 r2 ps_ty2 (NoteTy n2 ty2) = uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2
690 -- Variables; go for uVar
691 uTys r1 ps_ty1 (TyVarTy tyvar1) r2 ps_ty2 ty2 = uVar False r1 tyvar1 r2 ps_ty2 ty2
692 uTys r1 ps_ty1 ty1 r2 ps_ty2 (TyVarTy tyvar2) = uVar True r2 tyvar2 r1 ps_ty1 ty1
693 -- "True" means args swapped
696 uTys r1 _ (PredTy (IParam n1 t1)) r2 _ (PredTy (IParam n2 t2))
697 | n1 == n2 = uTys r1 t1 t1 r2 t2 t2
698 uTys r1 _ (PredTy (ClassP c1 tys1)) r2 _ (PredTy (ClassP c2 tys2))
699 | c1 == c2 = unifyTauTyLists r1 tys1 r2 tys2
700 -- Guaranteed equal lengths because the kinds check
702 -- Functions; just check the two parts
703 uTys r1 _ (FunTy fun1 arg1) r2 _ (FunTy fun2 arg2)
704 = uTys r1 fun1 fun1 r2 fun2 fun2 `thenM_` uTys r1 arg1 arg1 r2 arg2 arg2
706 -- Type constructors must match
707 uTys r1 ps_ty1 (TyConApp con1 tys1) r2 ps_ty2 (TyConApp con2 tys2)
708 | con1 == con2 = unifyTauTyLists r1 tys1 r2 tys2
709 -- See Note [TyCon app]
711 -- Applications need a bit of care!
712 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
713 -- NB: we've already dealt with type variables and Notes,
714 -- so if one type is an App the other one jolly well better be too
715 uTys r1 ps_ty1 (AppTy s1 t1) r2 ps_ty2 ty2
716 = case tcSplitAppTy_maybe ty2 of
717 Just (s2,t2) -> uTys r1 s1 s1 r2 s2 s2 `thenM_` uTys r1 t1 t1 r2 t2 t2
718 Nothing -> unifyMisMatch ps_ty1 ps_ty2
720 -- Now the same, but the other way round
721 -- Don't swap the types, because the error messages get worse
722 uTys r1 ps_ty1 ty1 r2 ps_ty2 (AppTy s2 t2)
723 = case tcSplitAppTy_maybe ty1 of
724 Just (s1,t1) -> uTys r1 s1 s1 r2 s2 s2 `thenM_` uTys r1 t1 t1 r2 t2 t2
725 Nothing -> unifyMisMatch ps_ty1 ps_ty2
727 -- Not expecting for-alls in unification
728 -- ... but the error message from the unifyMisMatch more informative
729 -- than a panic message!
731 -- Anything else fails
732 uTys r1 ps_ty1 ty1 r2 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
737 When we find two TyConApps, the argument lists are guaranteed equal
738 length. Reason: intially the kinds of the two types to be unified is
739 the same. The only way it can become not the same is when unifying two
740 AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in
741 the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first,
742 which we do, that ensures that f1,f2 have the same kind; and that
743 means a1,a2 have the same kind. And now the argument repeats.
748 If you are tempted to make a short cut on synonyms, as in this
752 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
753 -- NO = if (con1 == con2) then
754 -- NO -- Good news! Same synonym constructors, so we can shortcut
755 -- NO -- by unifying their arguments and ignoring their expansions.
756 -- NO unifyTauTypeLists args1 args2
758 -- NO -- Never mind. Just expand them and try again
762 then THINK AGAIN. Here is the whole story, as detected and reported
763 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
765 Here's a test program that should detect the problem:
769 x = (1 :: Bogus Char) :: Bogus Bool
772 The problem with [the attempted shortcut code] is that
776 is not a sufficient condition to be able to use the shortcut!
777 You also need to know that the type synonym actually USES all
778 its arguments. For example, consider the following type synonym
779 which does not use all its arguments.
784 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
785 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
786 would fail, even though the expanded forms (both \tr{Int}) should
789 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
790 unnecessarily bind \tr{t} to \tr{Char}.
792 ... You could explicitly test for the problem synonyms and mark them
793 somehow as needing expansion, perhaps also issuing a warning to the
798 %************************************************************************
800 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
802 %************************************************************************
804 @uVar@ is called when at least one of the types being unified is a
805 variable. It does {\em not} assume that the variable is a fixed point
806 of the substitution; rather, notice that @uVar@ (defined below) nips
807 back into @uTys@ if it turns out that the variable is already bound.
810 uVar :: Bool -- False => tyvar is the "expected"
811 -- True => ty is the "expected" thing
812 -> Bool -- True, allow refinements to tv1, False don't
814 -> Bool -- Allow refinements to ty2?
815 -> TcTauType -> TcTauType -- printing and real versions
818 uVar swapped r1 tv1 r2 ps_ty2 ty2
819 = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_`
820 condLookupTcTyVar r1 tv1 `thenM` \ details ->
822 IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back
823 | otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order
824 FlexiTv -> uFlexiVar swapped tv1 r2 ps_ty2 ty2
825 RigidTv -> uRigidVar swapped tv1 r2 ps_ty2 ty2
827 -- Expand synonyms; ignore FTVs
828 uFlexiVar :: Bool -> TcTyVar ->
829 Bool -> -- Allow refinements to ty2
830 TcTauType -> TcTauType -> TcM ()
831 -- Invariant: tv1 is Flexi
832 uFlexiVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
833 = uFlexiVar swapped tv1 r2 ps_ty2 ty2
835 uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
836 -- Same type variable => no-op
840 -- Distinct type variables
842 = condLookupTcTyVar r2 tv2 `thenM` \ details ->
844 IndirectTv b ty2' -> uFlexiVar swapped tv1 b ty2' ty2'
845 FlexiTv | update_tv2 -> putMetaTyVar tv2 (TyVarTy tv1)
846 | otherwise -> updateFlexi swapped tv1 ty2
847 RigidTv -> updateFlexi swapped tv1 ty2
848 -- Note that updateFlexi does a sub-kind check
849 -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
853 update_tv2 = k1 `isSubKind` k2 && (k1 /= k2 || nicer_to_update_tv2)
854 -- Update the variable with least kind info
855 -- See notes on type inference in Kind.lhs
856 -- The "nicer to" part only applies if the two kinds are the same,
857 -- so we can choose which to do.
859 nicer_to_update_tv2 = isSystemName (varName tv2)
860 -- Try to update sys-y type variables in preference to sig-y ones
862 -- First one is flexi, second one isn't a type variable
863 uFlexiVar swapped tv1 r2 ps_ty2 non_var_ty2
864 = -- Do the occurs check, and check that we are not
865 -- unifying a type variable with a polytype
866 -- Returns a zonked type ready for the update
867 do { ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
868 ; updateFlexi swapped tv1 ty2 }
870 -- Ready to update tv1, which is flexi; occurs check is done
871 updateFlexi swapped tv1 ty2
872 = do { checkKinds swapped tv1 ty2
873 ; putMetaTyVar tv1 ty2 }
876 uRigidVar :: Bool -> TcTyVar
877 -> Bool -> -- Allow refinements to ty2
878 TcTauType -> TcTauType -> TcM ()
879 -- Invariant: tv1 is Rigid
880 uRigidVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
881 = uRigidVar swapped tv1 r2 ps_ty2 ty2
883 -- The both-type-variable case
884 uRigidVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
885 -- Same type variable => no-op
889 -- Distinct type variables
891 = condLookupTcTyVar r2 tv2 `thenM` \ details ->
893 IndirectTv b ty2' -> uRigidVar swapped tv1 b ty2' ty2'
894 FlexiTv -> updateFlexi swapped tv2 (TyVarTy tv1)
895 RigidTv -> unifyMisMatch (TyVarTy tv1) (TyVarTy tv2)
897 -- Second one isn't a type variable
898 uRigidVar swapped tv1 r2 ps_ty2 non_var_ty2
899 = unifyMisMatch (TyVarTy tv1) ps_ty2
903 checkKinds swapped tv1 ty2
904 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
905 -- ty2 has been zonked at this stage, which ensures that
906 -- its kind has as much boxity information visible as possible.
907 | tk2 `isSubKind` tk1 = returnM ()
910 -- Either the kinds aren't compatible
911 -- (can happen if we unify (a b) with (c d))
912 -- or we are unifying a lifted type variable with an
913 -- unlifted type: e.g. (id 3#) is illegal
914 = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
915 unifyKindMisMatch k1 k2
918 (k1,k2) | swapped = (tk2,tk1)
919 | otherwise = (tk1,tk2)
925 checkValue tv1 r2 ps_ty2 non_var_ty2
926 -- Do the occurs check, and check that we are not
927 -- unifying a type variable with a polytype
928 -- Return the type to update the type variable with, or fail
930 -- Basically we want to update tv1 := ps_ty2
931 -- because ps_ty2 has type-synonym info, which improves later error messages
936 -- f :: (A a -> a -> ()) -> ()
940 -- x = f (\ x p -> p x)
942 -- In the application (p x), we try to match "t" with "A t". If we go
943 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
944 -- an infinite loop later.
945 -- But we should not reject the program, because A t = ().
946 -- Rather, we should bind t to () (= non_var_ty2).
948 -- That's why we have this two-state occurs-check
949 = zonk_tc_type r2 ps_ty2 `thenM` \ ps_ty2' ->
950 case okToUnifyWith tv1 ps_ty2' of {
951 Nothing -> returnM ps_ty2' ; -- Success
954 zonk_tc_type r2 non_var_ty2 `thenM` \ non_var_ty2' ->
955 case okToUnifyWith tv1 non_var_ty2' of
956 Nothing -> -- This branch rarely succeeds, except in strange cases
957 -- like that in the example above
960 Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2')
963 zonk_tc_type refine ty
964 = zonkType (\tv -> return (TyVarTy tv)) refine ty
965 -- We may already be inside a wobbly type t2, and
966 -- should take that into account here
968 data Problem = OccurCheck | NotMonoType
970 okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem
971 -- (okToUnifyWith tv ty) checks whether it's ok to unify
974 -- Just p => not ok, problem p
979 ok (TyVarTy tv') | tv == tv' = Just OccurCheck
980 | otherwise = Nothing
981 ok (AppTy t1 t2) = ok t1 `and` ok t2
982 ok (FunTy t1 t2) = ok t1 `and` ok t2
983 ok (TyConApp _ ts) = oks ts
984 ok (ForAllTy _ _) = Just NotMonoType
985 ok (PredTy st) = ok_st st
986 ok (NoteTy (FTVNote _) t) = ok t
987 ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2
988 -- Type variables may be free in t1 but not t2
989 -- A forall may be in t2 but not t1
991 oks ts = foldr (and . ok) Nothing ts
993 ok_st (ClassP _ ts) = oks ts
994 ok_st (IParam _ t) = ok t
997 Just p `and` m = Just p
1001 %************************************************************************
1005 %************************************************************************
1007 Unifying kinds is much, much simpler than unifying types.
1010 unifyKind :: TcKind -- Expected
1013 unifyKind LiftedTypeKind LiftedTypeKind = returnM ()
1014 unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
1016 unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
1017 unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM ()
1018 -- Respect sub-kinding
1020 unifyKind (FunKind a1 r1) (FunKind a2 r2)
1021 = do { unifyKind a2 a1; unifyKind r1 r2 }
1022 -- Notice the flip in the argument,
1023 -- so that the sub-kinding works right
1025 unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
1026 unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
1027 unifyKind k1 k2 = unifyKindMisMatch k1 k2
1029 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1030 unifyKinds [] [] = returnM ()
1031 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_`
1033 unifyKinds _ _ = panic "unifyKinds: length mis-match"
1036 uKVar :: Bool -> KindVar -> TcKind -> TcM ()
1037 uKVar swapped kv1 k2
1038 = do { mb_k1 <- readKindVar kv1
1040 Nothing -> uUnboundKVar swapped kv1 k2
1041 Just k1 | swapped -> unifyKind k2 k1
1042 | otherwise -> unifyKind k1 k2 }
1045 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
1046 uUnboundKVar swapped kv1 k2@(KindVar kv2)
1047 | kv1 == kv2 = returnM ()
1048 | otherwise -- Distinct kind variables
1049 = do { mb_k2 <- readKindVar kv2
1051 Just k2 -> uUnboundKVar swapped kv1 k2
1052 Nothing -> writeKindVar kv1 k2 }
1054 uUnboundKVar swapped kv1 non_var_k2
1055 = do { k2' <- zonkTcKind non_var_k2
1056 ; kindOccurCheck kv1 k2'
1057 ; k2'' <- kindSimpleKind swapped k2'
1058 -- KindVars must be bound only to simple kinds
1059 -- Polarities: (kindSimpleKind True ?) succeeds
1060 -- returning *, corresponding to unifying
1063 ; writeKindVar kv1 k2'' }
1066 kindOccurCheck kv1 k2 -- k2 is zonked
1067 = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
1069 not_in (KindVar kv2) = kv1 /= kv2
1070 not_in (FunKind a2 r2) = not_in a2 && not_in r2
1073 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
1074 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
1075 -- If the flag is False, it requires k <: sk
1076 -- E.g. kindSimpleKind False ?? = *
1077 -- What about (kv -> *) :=: ?? -> *
1078 kindSimpleKind orig_swapped orig_kind
1079 = go orig_swapped orig_kind
1081 go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
1083 ; return (FunKind k1' k2') }
1084 go True OpenTypeKind = return liftedTypeKind
1085 go True ArgTypeKind = return liftedTypeKind
1086 go sw LiftedTypeKind = return liftedTypeKind
1087 go sw k@(KindVar _) = return k -- KindVars are always simple
1088 go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
1089 <+> ppr orig_swapped <+> ppr orig_kind)
1090 -- I think this can't actually happen
1092 -- T v = MkT v v must be a type
1093 -- T v w = MkT (v -> w) v must not be an umboxed tuple
1096 kindOccurCheckErr tyvar ty
1097 = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:"))
1098 2 (sep [ppr tyvar, char '=', ppr ty])
1100 unifyKindMisMatch ty1 ty2
1101 = zonkTcKind ty1 `thenM` \ ty1' ->
1102 zonkTcKind ty2 `thenM` \ ty2' ->
1104 msg = hang (ptext SLIT("Couldn't match kind"))
1105 2 (sep [quotes (ppr ty1'),
1106 ptext SLIT("against"),
1113 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
1114 -- Like unifyFunTy, but does not fail; instead just returns Nothing
1116 unifyFunKind (KindVar kvar)
1117 = readKindVar kvar `thenM` \ maybe_kind ->
1119 Just fun_kind -> unifyFunKind fun_kind
1120 Nothing -> do { arg_kind <- newKindVar
1121 ; res_kind <- newKindVar
1122 ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
1123 ; returnM (Just (arg_kind,res_kind)) }
1125 unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
1126 unifyFunKind other = returnM Nothing
1129 %************************************************************************
1131 \subsection[Unify-context]{Errors and contexts}
1133 %************************************************************************
1139 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1140 = zonkTcType ty1 `thenM` \ ty1' ->
1141 zonkTcType ty2 `thenM` \ ty2' ->
1142 returnM (err ty1' ty2')
1144 err ty1 ty2 = (env1,
1147 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1148 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1151 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1153 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1154 -- tv1 and ty2 are zonked already
1157 msg = (env2, ptext SLIT("When matching the kinds of") <+>
1158 sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
1160 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1161 | otherwise = (pp1, pp2)
1162 (env1, tv1') = tidyOpenTyVar tidy_env tv1
1163 (env2, ty2') = tidyOpenType env1 ty2
1164 pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
1165 pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
1167 unifyMisMatch ty1 ty2
1168 = do { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1
1169 ; (env2, pp2, extra2) <- ppr_ty env1 ty2
1170 ; let msg = sep [sep [ptext SLIT("Couldn't match") <+> pp1, nest 7 (ptext SLIT("against") <+> pp2)],
1171 nest 2 extra1, nest 2 extra2]
1173 failWithTcM (env2, msg) }
1175 ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
1177 = do { ty' <- zonkTcType ty
1178 ; let (env1,tidy_ty) = tidyOpenType env ty'
1179 simple_result = (env1, quotes (ppr tidy_ty), empty)
1182 | isSkolemTyVar tv -> return (env1, pp_rigid tv,
1184 | otherwise -> return simple_result
1185 other -> return simple_result }
1187 pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv)
1189 unifyCheck problem tyvar ty
1191 2 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1193 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1194 (env2, tidy_ty) = tidyOpenType env1 ty
1196 msg = case problem of
1197 OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:")
1198 NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:")
1202 %************************************************************************
1206 %************************************************************************
1208 ---------------------------
1209 -- We would like to get a decent error message from
1210 -- (a) Under-applied type constructors
1211 -- f :: (Maybe, Maybe)
1212 -- (b) Over-applied type constructors
1213 -- f :: Int x -> Int x
1217 checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM ()
1218 -- A fancy wrapper for 'unifyKind', which tries
1219 -- to give decent error messages.
1220 checkExpectedKind ty act_kind exp_kind
1221 | act_kind `isSubKind` exp_kind -- Short cut for a very common case
1224 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
1226 Just _ -> returnM () ; -- Unification succeeded
1229 -- So there's definitely an error
1230 -- Now to find out what sort
1231 zonkTcKind exp_kind `thenM` \ exp_kind ->
1232 zonkTcKind act_kind `thenM` \ act_kind ->
1234 let (exp_as, _) = splitKindFunTys exp_kind
1235 (act_as, _) = splitKindFunTys act_kind
1236 n_exp_as = length exp_as
1237 n_act_as = length act_as
1239 err | n_exp_as < n_act_as -- E.g. [Maybe]
1240 = quotes (ppr ty) <+> ptext SLIT("is not applied to enough type arguments")
1242 -- Now n_exp_as >= n_act_as. In the next two cases,
1243 -- n_exp_as == 0, and hence so is n_act_as
1244 | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind
1245 = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty)
1246 <+> ptext SLIT("is unlifted")
1248 | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind
1249 = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty)
1250 <+> ptext SLIT("is lifted")
1252 | otherwise -- E.g. Monad [Int]
1253 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
1254 ptext SLIT("but") <+> quotes (ppr ty) <+>
1255 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
1257 failWithTc (ptext SLIT("Kind error:") <+> err)
1261 %************************************************************************
1263 \subsection{Checking signature type variables}
1265 %************************************************************************
1267 @checkSigTyVars@ is used after the type in a type signature has been unified with
1268 the actual type found. It then checks that the type variables of the type signature
1270 (a) Still all type variables
1271 eg matching signature [a] against inferred type [(p,q)]
1272 [then a will be unified to a non-type variable]
1274 (b) Still all distinct
1275 eg matching signature [(a,b)] against inferred type [(p,p)]
1276 [then a and b will be unified together]
1278 (c) Not mentioned in the environment
1279 eg the signature for f in this:
1285 Here, f is forced to be monorphic by the free occurence of x.
1287 (d) Not (unified with another type variable that is) in scope.
1288 eg f x :: (r->r) = (\y->y) :: forall a. a->r
1289 when checking the expression type signature, we find that
1290 even though there is nothing in scope whose type mentions r,
1291 nevertheless the type signature for the expression isn't right.
1293 Another example is in a class or instance declaration:
1295 op :: forall b. a -> b
1297 Here, b gets unified with a
1299 Before doing this, the substitution is applied to the signature type variable.
1301 We used to have the notion of a "DontBind" type variable, which would
1302 only be bound to itself or nothing. Then points (a) and (b) were
1303 self-checking. But it gave rise to bogus consequential error messages.
1306 f = (*) -- Monomorphic
1308 g :: Num a => a -> a
1311 Here, we get a complaint when checking the type signature for g,
1312 that g isn't polymorphic enough; but then we get another one when
1313 dealing with the (Num x) context arising from f's definition;
1314 we try to unify x with Int (to default it), but find that x has already
1315 been unified with the DontBind variable "a" from g's signature.
1316 This is really a problem with side-effecting unification; we'd like to
1317 undo g's effects when its type signature fails, but unification is done
1318 by side effect, so we can't (easily).
1320 So we revert to ordinary type variables for signatures, and try to
1321 give a helpful message in checkSigTyVars.
1324 checkSigTyVars :: [TcTyVar] -> TcM ()
1325 checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs
1327 checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM ()
1328 checkSigTyVarsWrt extra_tvs sig_tvs
1329 = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' ->
1330 check_sig_tyvars extra_tvs' sig_tvs
1333 :: TcTyVarSet -- Global type variables. The universally quantified
1334 -- tyvars should not mention any of these
1335 -- Guaranteed already zonked.
1336 -> [TcTyVar] -- Universally-quantified type variables in the signature
1337 -- Not guaranteed zonked.
1340 check_sig_tyvars extra_tvs []
1342 check_sig_tyvars extra_tvs sig_tvs
1343 = do { gbl_tvs <- tcGetGlobalTyVars
1344 ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs,
1345 text "gbl_tvs" <+> ppr gbl_tvs,
1346 text "extra_tvs" <+> ppr extra_tvs]))
1348 -- Check that that the signature type vars are not free in the envt
1349 ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs
1350 ; checkM (not (mkVarSet sig_tvs `intersectsVarSet` env_tvs))
1351 (complain sig_tvs env_tvs)
1353 ; ASSERT( all isSkolemTyVar sig_tvs )
1356 complain sig_tvs globals
1357 = -- "check" checks each sig tyvar in turn
1359 (env, emptyVarEnv, [])
1360 tidy_tvs `thenM` \ (env2, _, msgs) ->
1362 failWithTcM (env2, main_msg $$ nest 2 (vcat msgs))
1364 (env, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs
1366 main_msg = ptext SLIT("Inferred type is less polymorphic than expected")
1368 check (tidy_env, acc, msgs) tv
1369 -- sig_tyvar is from the signature;
1370 -- ty is what you get if you zonk sig_tyvar and then tidy it
1372 -- acc maps a zonked type variable back to a signature type variable
1373 = case lookupVarEnv acc tv of {
1374 Just sig_tyvar' -> -- Error (b)!
1375 returnM (tidy_env, acc, unify_msg tv thing : msgs)
1377 thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar')
1381 if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes
1382 -- The least comprehensible, so put it last
1384 -- get the local TcIds and TyVars from the environment,
1385 -- and pass them to find_globals (they might have tv free)
1387 findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) ->
1388 -- This rigid type variable has escaped into the envt
1389 -- We make it flexi so that subequent uses of these
1390 -- variables don't give rise to a cascade of further errors
1391 returnM (tidy_env1, acc, escape_msg tv globs : msgs)
1394 returnM (tidy_env, extendVarEnv acc tv tv, msgs)
1400 -----------------------
1401 escape_msg sig_tv globs
1402 = mk_msg sig_tv <+> ptext SLIT("escapes") $$
1403 if notNull globs then
1404 vcat [ptext SLIT("It is mentioned in the environment:"),
1405 nest 2 (vcat globs)]
1407 empty -- Sigh. It's really hard to give a good error message
1408 -- all the time. One bad case is an existential pattern match.
1409 -- We rely on the "When..." context to help.
1411 unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing
1412 mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv)
1415 These two context are used with checkSigTyVars
1418 sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType
1419 -> TidyEnv -> TcM (TidyEnv, Message)
1420 sigCtxt id sig_tvs sig_theta sig_tau tidy_env
1421 = zonkTcType sig_tau `thenM` \ actual_tau ->
1423 (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs
1424 (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau)
1425 (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau
1426 sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho),
1427 ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau
1429 msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id),